Category Archives: Foundations

Parametricity, automorphisms of the universe, and excluded middle

Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was previously featured on this blog, and the latter is part of a discussion on the HoTT mailing list. In a cooperation … Continue reading

Posted in Foundations | 7 Comments

Parametricity and excluded middle

Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function  such that is a non-identity function  I have proved the converse of this. Like in exercise 6.9, we assume univalence. Parametricity In a … Continue reading

Posted in Foundations | 13 Comments

Real-cohesive homotopy type theory

Two new papers have recently appeared online: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory by me, and Adjoint logic with a 2-category of modes, by Dan Licata with a bit of help from me. Both of them have fairly … Continue reading

Posted in Applications, Foundations, Paper | 12 Comments

Universal Properties of Truncations

Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation , and I want to write this blog post in case … Continue reading

Posted in Foundations, Homotopy Theory, Models, Paper, Talk | 3 Comments

Universal properties without function extensionality

A universal property, in the sense of category theory, generally expresses that a map involving hom-sets, induced by composition with some canonical map(s), is an isomorphism. In type theory we express this using equivalences of hom-types. For instance, the universal … Continue reading

Posted in Code, Foundations, Higher Inductive Types | 16 Comments

A Formalized Interpreter

I’d like to announce a result that might be interesting: an interpreter for a very small dependent type system in Coq, assuming uniqueness of identity proofs (UIP). Because it assumes UIP, it’s not immediately compatible with HoTT, but it seems … Continue reading

Posted in Code, Foundations, Programming | 77 Comments

Higher inductive-recursive univalence and type-directed definitions

In chapter 2 of the HoTT book, we prove theorems (or, in a couple of cases, assert axioms) characterizing the equality types of all the standard type formers. For instance, we have and (that’s function extensionality) and (that’s univalence). However, … Continue reading

Posted in Code, Foundations, Higher Inductive Types, Univalence | 7 Comments