Cartan Geometry in Modal Homotopy Type Theory
Felix Cherubini – 12 May 2021
Homotopy Type Theory together with a monadic modality can be interpreted in an oo-topos equipped with a stable factorization system. In the examples of interest, the factorization system will be generated by a reflection. We show how an approach to Cartan Geometry, developed by Urs Schreiber, can be implemented on the type theory side of this abstract setup.
Back