Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

This is the formalization of my article on cartan geometry in modal hott. The basis was the formalization of my thesis. If you want to look at a state compatible with the latter or see other things that have been here earlier, you can check out the tag 'compatible_with_thesis'. Everything should check with Agda-


Differential cohesion in Homotopy Type Theory by an axiomatized coreduction modality. This doesn't really require a modal type theory in sense that the rules are different from book-hott, since the coreduction is a monadic modality.

The following is proved and could also be interpreted as theorems about general modalities:

  • The formal disk bundle over a group is trivial.
  • The formal disk bundle over a V-manifold is locally trivial.
  • All F - fiber bundles are associated to an Aut(F) principal bundle.

In place of groups, a more general structure called homogeneous type is used in the code. Here is more information on this project. Here (theorem 3.6, 1) and some part of 2) is a short account of the question this code solves. The classical, category theoretic, version of the theory together with a lot of opportunities to extend the formalized version is here.

State of the code

Notation is not as consequent and compatible with the rest of the HoTT-World as it should be. This code grew while I was learning homotopy type theory and agda. This is still witnessed by some stupid definitions for the basic stuff like equivalences and probably some agda-clumsyness. If you want to have a look at what has been formalized, the following files are probably the right places:

  • FormalDiskBundle.agda
  • Manifolds.agda
  • G-structure.agda
  • FiberBundle.agda
  • Im.agda

A Modality 'I' is defined in Im.agda in a way similar to the HoTT-Book, 7.7.5.


Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality






No releases published


No packages published