4.2. Propositions🔗

Propositions are meaningful statements that admit proof. Nonsensical statements are not propositions, but false statements are. All propositions are classified by Prop.

Propositions have the following properties:

Definitional proof irrelevance: Any two proofs of the same proposition are completely interchangeable.
Run-time irrelevance: Propositions are erased from compiled code.
Impredicativity: Propositions may quantify over types from any universe whatsoever.
Restricted Elimination: With the exception of subsingletons, propositions cannot be eliminated into non-proposition types.
Extensionality: Any two logically equivalent propositions can be proven to be equal with the propext axiom.

axiom

propext {a b : Prop} : (a ↔ b) → a = b
propext {a b : Prop} : (a ↔ b) → a = b

The axiom of propositional extensionality. It asserts that if propositions a and b are logically equivalent (that is, if a can be proved from b and vice versa), then a and b are equal, meaning a can be replaced with b in all contexts.

The standard logical connectives provably respect propositional extensionality. However, an axiom is needed for higher order expressions like P a where P : Prop → Prop is unknown, as well as for equality. Propositional extensionality is intuitionistically valid.