# 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