A proposition is the (homotopy) type of its proofs

Abstract

An introduction and survey of homotopy type theory in honor of W.W. Tait.

References in corpus (2)

• The identity type weak factorisation system
• Impredicative Encodings of (Higher) Inductive Types