Category Archives: Foundations
The Cantor-Schröder-Bernstein Theorem for ∞-groupoids
The classical Cantor-Schröder-Bernstein Theorem (CSB) of set theory, formulated by Cantor and first proved by Bernstein, states that for any pair of sets, if there is an injection of each one into the other, then the two sets are in … Continue reading
Impredicative Encodings, Part 3
In this post I will argue that, improving on previous work of Awodey-Frey-Speight, (higher) inductive types can be defined using impredicative encodings with their full dependent induction principles — in particular, eliminating into all type families without any truncation hypotheses … Continue reading
Impredicative Encodings of Inductive Types in HoTT
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading
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
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
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
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
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
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
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
Homotopy Type Theory should eat itself (but so far, it’s too big to swallow)
The title of this post is an homage to a well-known paper by James Chapman called Type theory should eat itself. I also considered titling the post How I spent my Christmas vacation trying to construct semisimplicial types in a … Continue reading
Composition is not what you think it is! Why “nearly invertible” isn’t.
A few months ago, Nicolai Kraus posted an interesting and surprising result: the truncation map 
: ℕ → ‖ℕ‖ is nearly invertible. This post attempts to explain why “nearly invertible” is a misnomer. I, like many others, was very … Continue reading
The HoTT Book
This posting is the official announcement of The HoTT Book, or more formally: Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program, Institute for Advanced Study The book is the result of an amazing collaboration between virtually everyone involved … Continue reading
Universe n is not an n-Type
Joint work with Christian Sattler Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here. One … Continue reading
On h-Propositional Reflection and Hedberg’s Theorem
Thorsten Altenkirch, Thierry Coquand, Martin Escardo, Nicolai Kraus Overview Hedberg’s theorem states that decidable equality of a type implies that the type is an h-set, meaning that it has unique equality proofs. We describe how the assumption can be weakened. … Continue reading
A type theoretical Yoneda lemma
In this blog post I would like to approach dependendent types from a presheaf point of view. This allows us to take the theory of presheaves as an inspiration for results in homotopy type theory. The first result from this … Continue reading
Inductive Types in HoTT
With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report … Continue reading
Modeling Univalence in Subtoposes
In my recent post at the n-Category Café, I described a notion of “higher modality” in type theory, which semantically ought to represent a left-exact-reflective sub–category of an -topos — once we can prove that homotopy type theory has models … Continue reading
Canonicity for 2-Dimensional Type Theory
A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading
Higher Inductive Types via Impredicative Polymorphism
The proof assistant Coq is based on a formal system called the “Predicative Calculus of (Co)Inductive Constructions” (pCiC). But before pCiC, there was the “Calculus of Constructions” (CoC), in which inductive types were not a basic object, but could be … Continue reading
Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute
Higher-dimensional inductive types are an idea that many people have been kicking around lately; for example, in An Interval Type Implies Function Extensionality. The basic idea is that you define a type by specifying both what it’s elements are (as … Continue reading
Oberwolfach Report
Richard Garner has now completed and posted the report from the Oberwolfach meeting.
Just Kidding: Understanding Identity Elimination in Homotopy Type Theory
Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP … Continue reading
An Interval Type Implies Function Extensionality
One of the most important spaces in homotopy theory is the interval (be it the topological interval or the simplicial interval ). Thus, it is natural to ask whether there is, or can be, an “interval type” in homotopy type … Continue reading
Constructive Validity
(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.) The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold … Continue reading
Homotopy Type Theory, II | The n-Category Café
Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this: Homotopy Type Theory, II — Posted by Mike Shulman … Last time we talked about the correspondence between the syntax of intensional … Continue reading
