Monthly Archives: April 2011

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

What’s Special About Identity Types

From a homotopy theorist’s point of view, identity types and their connection to homotopy theory are perfectly natural: they are “path objects” in the category of types. However, from a type theorist’s point of view, they are somewhat more mysterious. … Continue reading

Posted in Uncategorized | 9 Comments

Oberwolfach Report

Richard Garner has now completed and posted the report from the Oberwolfach meeting.

Posted in Foundations, Univalence | 1 Comment

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

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

Posted in Foundations | 35 Comments

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

Posted in Foundations | 53 Comments