Anders Mörtberg
@mortberg@mathstodon.xyz
Associate professor (docent) in computational mathematics at Stockholm University. I'm interested in HoTT/UF, cubical stuff, constructive mathematics, logic and type theory, category theoretical foundations, functional programming, computer formalization of mathematics and computer science, and much more. Webpage: https://staff.math.su.se/anders.mortberg/
mathstodon.xyz
Replying to
@amy@types.pl
@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
