# Category Archives: Higher Inductive Types

## 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

## 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 surreals contain the plump ordinals

The very last section of the book presents a constructive definition of Conway’s surreal numbers as a higher inductive-inductive type. Conway’s classical surreals include the ordinal numbers; so it’s natural to wonder whether, or in what sense, this may be … Continue reading

Posted in Higher Inductive Types | 3 Comments

## New writeup of πn(Sn)

I’m giving a talk this week at CPP.  While I’m going to talk more broadly about applications of higher inductive types, for the proceedings, Guillaume Brunerie and I put together an “informalization” of πn(Sn), which you can find here. This is … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 1 Comment

## 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

## 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