This page collects material related to
Formalizing Cartan geometry in Modal Homotopy Type Theory
talk at
Homotopy Type Theory in Logic, Metaphysics and Philosophy of Physics
at Bristol, 12-16 September 2016
(talk slides pdf)
$\,$
about the formalization of Cartan geometry (manifolds, G-structures, torsion of G-structures) in modal homotopy type theory. The talk provides motivation and introduction to the thesis
$\,$
Formalizing Cartan Geometry in Modal Homotopy Type Theory
PhD Thesis
(thesis pdf, talk slides: pdf, HoTT-Agda code: DCHoTT-Agda.
$\,$
which solves the first of the list of problems posed in
concerning the formalization in HoTT of results that are presented in
Igor Khavkine, Urs Schreiber, Synthetic geometry of differential equations Part I. Jets and comonad structure (arXiv:1701.06238)
$\,$