Proving funext using quotients

Stream: Type theory

[Riccardo Brasca]

I am trying to prove funext by hand, using quotient types. If I understand correctly, quotient types are built in into Lean (for example I don't find quotient.liftanywhere), so I tried to add them by hand, as follows

namespace foo

universes u v

constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u

constant quot.mk :
  Π {α : Sort u} (r : α → α → Prop), α → quot r

axiom quot.ind :
  ∀ {α : Sort u} {r : α → α → Prop} {β : quot r → Prop},
    (∀ a, β (quot.mk r a)) → ∀ (q : quot r), β q

constant quot.lift :
  Π {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β),
    (∀ a b, r a b → f a = f b) → quot r → β

/-- This is built in into Lean as a definitional equality I think. -/
constant quot.lift_eq {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (a : α)
  (h : ∀ a b, r a b → f a = f b) : quot.lift f h (quot.mk r a) = f a

axiom quot.sound :
  ∀ {α : Type*} (r : α → α → Prop) {a b : α},
    r a b → quot.mk r a = quot.mk r b

section funext

variables {A B : Type*} {f g : A → B}

def R : (A → B) → (A → B) → Prop := λ α β, ∀ a, α a = β a

noncomputable
def foo : (quot R) → (A → B) := λ q a, quot.lift (λ (α : A → B), α a) (λ α β (h : R α β), h a) q

lemma foo_eq (f : A → B) : foo (quot.mk R f) = f :=
by simp [foo, quot.lift_eq]

lemma funext (H : ∀ a, f a = g a) : f = g :=
begin
  rw [← foo_eq f, ← foo_eq g, quot.sound R H],
end

#print axioms talk.funext --there is quot.sound

end funext

end foo

Is it possible to prove my funext without using Lean's quotient.sound? It is introduced by the simp in the proof of foo_eq, and if I try to prove it by hand I have to rewrite quot.lift_eq into a λ, something I don't know how to do without using the "real" funext (and maybe it is equivalent to it). I think that the real proof works because the quot.lift_eqis definitionally true, so there is no need to rewrite it.

[Kevin Buzzard]

What axioms does Lean's actual funext use?

[Mario Carneiro]

quotients and propext IIRC

[Mario Carneiro]

lean says:

'funext' depends on axioms: [Quot.sound]

[Riccardo Brasca]

Yes, Lean's proof is essentially the same as my proof, but the two rw [← foo_eq f, ← foo_eq g] are done using show ... from .... In particular no axiom is used here.

[Riccardo Brasca]

I mean, no axiom that is literally written somewhere in the library.

[Mario Carneiro]

yes, I'm pretty sure this use is essential

[Mario Carneiro]

without it you get "propositional quotients", which are most easily done the way it is done in math class, taking the set of equivalence classes

[Mario Carneiro]

and this construction requires propext and funext

[Mario Carneiro]

BTW not sure if you saw it but lean 4 has a much shorter and documented version of the proof:

/--
**Function extensionality** is the statement that if two functions take equal values
every point, then the functions themselves are equal: `(∀ x, f x = g x) → f = g`.
It is called "extensionality" because it talks about how to prove two objects are equal
based on the properties of the object (compare with set extensionality,
which is `(∀ x, x ∈ s ↔ x ∈ t) → s = t`).

This is often an axiom in dependent type theory systems, because it cannot be proved
from the core logic alone. However in lean's type theory this follows from the existence
of quotient types (note the `Quot.sound` in the proof, as well as the `show` line
which makes use of the definitional equality `Quot.lift f h (Quot.mk x) = f x`).
-/
theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by
  let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
  let extfunApp (f : Quot eqv) (x : α) : β x :=
    Quot.liftOn f
      (fun (f : ∀ (x : α), β x) => f x)
      (fun _ _ h => h x)
  show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
  exact congrArg extfunApp (Quot.sound h)

[Riccardo Brasca]

Oh, nice! Thanks