## Stream: general

### Topic: propext axiom

#### Heather Macbeth (Jan 05 2023 at 19:29):

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 (Jan 05 2023 at 19:30):

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

#### Floris van Doorn (Jan 05 2023 at 19:30):

Let f x := P = x

#### Heather Macbeth (Jan 05 2023 at 19:33):

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

#### Heather Macbeth (Jan 05 2023 at 19:35):

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 (Jan 05 2023 at 19:38):

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

Last updated: Aug 03 2023 at 10:10 UTC