Oberwolfach HoTT-Coq tutorial

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

At an Oberwolfach workshop in 2011 on homotopy type theory, Andrej Bauer and Peter LeFanu Lumsdaine created a tutorial that walks the reader through the proof that the univalence axiom implies functional extensionality, formalized entirely in Coq-proof assistant code.

For a pdf-version of the tutorial see

- Andrej Bauer, Peter LeFanu Lumsdaine,
*A Coq proof that Univalence Axioms implies Functional Extensionality*(2011) (pdf).

In order to follow the proof explicitly in Coq-itself, download the accompanying source files here:

and feed them into your Coq. See the README file there for further hints.

A rephrasing of the Coq-proofs given there in terms of ordinary language is given in

category: reference

Revised on January 14, 2012 07:38:52
by Urs Schreiber
(89.204.130.46)