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
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
Last revised on March 13, 2018 at 18:42:30. See the history of this page for a list of all contributions to it.