Category Archives: Code
The HoTT Game
What is the HoTT Game? The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying … Continue reading
Colimits in HoTT
In this post, I would want to present you two things: the small library about colimits that I formalized in Coq, a construction of the image of a function as a colimit, which is essentially a sliced version of the … Continue reading
The Lean Theorem Prover
Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code … Continue reading
Constructing the Propositional Truncation using Nonrecursive HITs
In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another … Continue reading
Modules for Modalities
As defined in chapter 7 of the book, a modality is an operation on types that behaves somewhat like the n-truncation. Specifically, it consists of a collection of types, called the modal ones, together with a way to turn any … Continue reading
Double Groupoids and Crossed Modules in HoTT
The past eight months I spent at CMU for my master thesis project. I ended up formalizing some algebraic structures used in Ronald Brown’s book “Non-Abelian Algebraic Topology”: Double groupoids with thin structure and crossed modules over groupoids. As the … Continue reading
Splitting Idempotents, II
I ended my last post about splitting idempotents with several open questions: If we have a map , a witness of idempotency , and a coherence datum , and we use them to split as in the previous post, do … Continue reading
Splitting Idempotents
A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.
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
Eilenberg-MacLane Spaces in HoTT
For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … 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 Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible
Magic tricks are often entertaining, sometimes boring, and in some rarer cases astonishing. For me, the following trick belongs to the third type: the magician asks a volunteer in the audience to think of a natural number. The volunteer secretly … 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
Covering Spaces
Covering spaces are one of the important topics in classical homotopy theory, and this post summarizes what we have done in HoTT. We have formulated the covering spaces and (re)proved the classification theorem based on (right) -sets, i.e., sets equipped with … Continue reading
Running Spheres in Agda, Part II
(Sorry for the long delay after the Part I of this post.) This post will summarize my work on defining spheres in arbitrary finite dimensions (Sⁿ) in Agda. I am going to use the tools for higher-order paths (discussed in … 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
Isomorphism implies equality
Thierry Coquand and I have proved that, for a large class of algebraic structures, isomorphism implies equality (assuming univalence). A class of algebraic structures Structures in this class consist of a type, some operations on this type, and propositional axioms … Continue reading
Positive h-levels are closed under W
I was asked about my proof showing that positive h-levels are closed under W (assuming extensionality), so I decided to write a short note about it. W-types are defined inductively as follows (using Agda notation): data W (A : Set) … Continue reading
Truncations and truncated higher inductive types
Truncation is a homotopy-theoretic construction that given a space and an integer n returns an n-truncated space together with a map in an universal way. More precisely, if i is the inclusion of n-truncated spaces into spaces, then n-truncation is … Continue reading
Running Spheres in Agda, Part I
Running Spheres in Agda, Part I Introduction Where will we end up with if we generalize circles S¹ to spheres Sⁿ? Here is the first part of my journey to a 95% working definition for arbitrary finite dimension. The 5% … Continue reading
Homotopy equivalences are equivalences: take 3
A basic fact in homotopy type theory is that homotopy equivalences are (coherent) equivalences. This is important because on the one hand, homotopy equivalences are the “correct” sort of equivalence, but on the other hand, for a function f the … Continue reading
A direct proof of Hedberg’s theorem
In his article published 1998, Michael Hedberg has shown that a type with decidable equality also features the uniqueness of identity proofs property. Reading through Nils Anders Danielsson’s Agda formalization, I noticed that the statement “A has decidable equality”, i.e. … 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
Localization as an Inductive Definition
I’ve been talking a lot about reflective subcategories (or more precisely, reflective subfibrations) in type theory lately (here and here and here), so I started to wonder about general ways to construct them inside type theory. There are some simple … Continue reading
A formal proof that π₁(S¹)=Z
The idea of higher inductive types, as described here and here, purports (among other things) to give us objects in type theory which represent familiar homotopy types from topology. Perhaps the simplest nontrivial such type is the circle, , which … 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
Higher Inductive Types: a tour of the menagerie
(This was written in inadvertent parallel with Mike’s latest post at the Café, so there’s a little overlap — Mike’s discusses the homotopy-theoretic aspects more, this post the type-theoretic nitty-gritty.) Higher inductive types have been mentioned now in several other … 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
Another Formal Proof that the Higher Homotopy Groups are Abelian
I have adapted Dan Licata’s Agda proof that the higher homotopy groups are abelian to Coq, and I have added a link to the code on the code page of this blog.
Homotopy Type Theory 