Schreiber Formalizing Cartan Geometry in Modal HoTT

This page collects material related to

---

• Urs Schreiber

  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

$\,$

---

• Felix Wellen,

  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

• Urs Schreiber, Some thoughts on the future of modal homotopy type theory, talk at Homotopy Type Theory and Univalent Foundations - Mini-Symposium, within the German Mathematical Society meeting 2015 21st - 25th Sept, Hamburg (talk notes pdf)

concerning the formalization in HoTT of results that are presented in

• Urs Schreiber, Differential cohomology in a cohesive topos

• Igor Khavkine, Urs Schreiber, Synthetic geometry of differential equations Part I. Jets and comonad structure (arXiv:1701.06238)

$\,$

Related projects

• Synthetic variational calculus