Definition
Proposition is homotopy level -1. It refers to the type in which the identity type of any two elements is contractible. In other words, all elements are equal to all other elements, meaning that at most one element may be present. For a type ,
Remarks
It is sometimes taken as an axiom in HoTT that all propositions exist in all universe levels through “propositional resizing”. This effectively gives rise to impredicative . At first it may seem that Girard’s Paradox applies here, however no contradiction has yet been found that shows its inconsistency.
See also
Contractibility Set (HoTT) Homotopy Level Truncation (HoTT)