Category Archives: Higher Inductive Types
Reducing all HIT’s to 1-HIT’s
For a while, Mike Shulman and I (and others) have wondered on and off whether it might be possible to represent all higher inductive types (i.e. with constructors of arbitrary dimension) using just 1-HIT’s (0- and 1-cell constructors only), somewhat … 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
