Topos Institute Colloquium, 3rd of October 2024.
———
Cubical type theory is an extension of dependent type theory designed
to make the univalence principle *provable*, rather than an axiom.
Then, by what is essentially a happy coincidence, it also provides a
design for working with higher inductive types and with coinductive
types.

However, the tradeoff for these features is a hit to usability: In
practice, the user of cubical type theory is directly exposed to the
complicated primitive operations that let us implement these higher
features, even if they're working on set-level mathematics. Worse, any
implementation of HoTT imposes additional proof obligations to stay in
the realm of sets rather than escaping off into coherence purgatory.

This talk discusses the experience of using cubical type theory to
build the 1Lab— in particular, the automation we've been building so
the end-user of the library does not have to memorise the cubical type
theory papers if all they want is to formalise traditional,
low-homotopy level mathematics.