The axiom of propositional extensionality. It asserts that if propositions
a and b are logically equivalent (i.e. we can prove a from b and vice versa),
then a and b are equal, meaning that we can replace a with b in all
contexts.
For simple expressions like a ∧ c ∨ d → e we can prove that because all the logical
connectives respect logical equivalence, we can replace a with b in this expression
without using propext. However, for higher order expressions like P a where
P : Prop → Prop is unknown, or indeed for a = b itself, we cannot replace a with b
without an axiom which says exactly this.
This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using #reduce to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type Nat normalize to numerals,
fails to hold when this (or any) axiom is used:
set_option pp.proofs true
def foo : Nat := by
have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
have := propext this ▸ (2 : Nat)
exact this
#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
#eval foo -- 2
#eval can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so propext, whose return type is a proposition,
can never block it.