Post #2049523

@amy @ncf @totbwf Any thoughts about taking this opportunity to change the cubical type theory a bit? I think my dream system in terms of ergonomics would be cartesian Kan ops together with connections and reversals. I don't know how hard it would be to implement, but adapting the existing cubical libraries should be feasible. The main gain that I see is that we get rid of transp and replace it with coe r->s which is much easier to understand