propext axiom

Stream: general

[Heather Macbeth]

If I understand correctly, the fact that P ↔ Q implies P can be substituted for Q is a consequence (in Lean's setup) of the docs#propext axiom:

example {P Q : Prop} {f : Prop → Sort*} (h1 : P ↔ Q) (h2 : f P) : f Q :=
eq.rec h2 (propext h1)

Does the implication go the other way? Can propext be deduced from this?

[Gabriel Ebner]

Hint: use f := fun R => R = P

[Floris van Doorn]

Let f x := P = x

[Heather Macbeth]

Ha! I guess that was a pretty easy question for people who know type theory :). Thanks!

[Heather Macbeth]

So we could set up the foundations as

axiom iff.subst {P Q : Prop} {f : Prop → Sort*} (h1 : P ↔ Q) (h3 : f P) : f Q

lemma propext' {P Q : Prop} (h : P ↔ Q) : P = Q := h.subst rfl

if we wanted to. Are there other systems where this approach is taken?

[Heather Macbeth]

Oh, I see this exact question is treated in TPIL.
https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#propositional-extensionality