Category Archives: Code

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

Posted in Code, Higher Inductive Types | 14 Comments

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

Posted in Code, Higher Inductive Types, Programming | 48 Comments

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

Posted in Code, Higher Inductive Types | 25 Comments

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

Posted in Code, Programming | 19 Comments

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

Posted in Code, Homotopy Theory | 31 Comments

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

Posted in Code, Homotopy Theory | Leave a comment

Splitting Idempotents

A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.

Posted in Code, Homotopy Theory, Univalence | 13 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

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

Posted in Applications, Code, Higher Inductive Types, Paper, Univalence | 6 Comments

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

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

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

Posted in Code, Higher Inductive Types | 42 Comments

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

Posted in Code, Foundations, Talk, Univalence | Leave a comment

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

Posted in Code, Higher Inductive Types, Homotopy Theory | 5 Comments

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

Posted in Code, Higher Inductive Types | Leave a comment

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

Posted in Code, Foundations | 17 Comments

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

Posted in Applications, Code, Univalence | 13 Comments

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

Posted in Code | 18 Comments

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

Posted in Code, Higher Inductive Types | 15 Comments

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

Posted in Code, Higher Inductive Types | Leave a comment

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

Posted in Code | 10 Comments

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

Posted in Code | 5 Comments

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

Posted in Code, Foundations, Paper | 9 Comments

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

Posted in Code, Higher Inductive Types | Leave a comment

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

Posted in Code, Higher Inductive Types | 2 Comments

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

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

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

Posted in Code, Higher Inductive Types | 7 Comments

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

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

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.

Posted in Code | 4 Comments