Univalent Foundations
Univalent Foundations refers to a collection of proposed foundations of mathematics which take seriously the structuralist claim that isomorphic objects should be regarded as the same (see Univalence axiom). In order to rigorously and consistently make this true, it must be possible for objects to be equal in more than one way (to reflect different identifications coming from different isomorphisms). This has two important consequences on the kinds of foundational systems suitable for the cause:
- We are doing Proof-relevant mathematics, which is naturally suited to the paradigm of Propositions as types as present in MLTT and its extensions — the isomorphism used to prove that two objects are identified needs to be retained in order to transport along that identification.
- UIP is false, so we must take seriously the Anima-structure of types and the principles of Homotopy type theory.