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.