The Axiom of Univalence

Previously: Modeling Identity Types. On first viewing, the identity type seems odd. Does it make sense to replace the traditional yes/no equality predicate with an elaborate type of equality proofs? In fact the father or modern type theory Martin Löf had his doubts, and initially tried to reflect all identity proofs into more basic judgmental […]