nLab
Oberwolfach HoTT-Coq tutorial

natural deduction metalanguage, practical foundations

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

logic	category theory	type theory
true	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	initial object	empty type
proposition	(-1)-truncated object	h-level 1-type/h-prop
proof	generalized element	program
conjunction	product	product type
disjunction	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	internal hom	function type
negation	internal hom into initial object	function type into empty type
universal quantification	dependent product	dependent product type
existential quantification	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
equivalence	path space object	identity type
equivalence class	quotient	quotient type
induction	colimit	inductive type, W-type, M-type
higher induction	higher colimit	higher inductive type
completely presented set	discrete object/0-truncated object	h-level 2-type/preset/h-set
set	internal 0-groupoid	Bishop set/setoid
universe	object classifier	type of types
modality	closure operator monad	modal type theory, monad (in computer science)

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)