Propext necessary in `Quotient.exact` ?

Stream: Type theory

[Rémi Bottinelli]

Hey, looking at the proof that quotients define the transitive+symmetric+reflexive closure of a relation, I see that propext is used to define an induced relation on the quotient. Is propext a necessary axiom in this proof, or just a convenience?

Ah Theorem 3.3 here also uses propext and refers to Hofmann, so I guess it's at least not trivial without propext.

Still, I wonder if not-propext implies not-quotient-is-equivalence-closure. I vaguely tried by taking the quotient of Prop by iffbut that didn't lead me anywhere.
It seems proving that quotienting by Eq doesn't do anything is itself not dependent on propext, which is interesting.

[Junyan Xu]

Ah Theorem 3.3 here also uses propext and refers to Hofmann, so I guess it's at least not trivial without propext.

Nice find! I did some explorations in my early days learning Lean and concluded it's probably impossible to prove quotient exactness without propext (or some other axioms), but I didn't find any reference. The idea of taking the quotient Prop/iff just pushes the problem to exactness of Prop/iff, which is just as hard.

I wonder if not-propext implies not-quotient-is-equivalence-closure.

I think this implication is invalid because I can prove quotient exactness using choice and excluded middle (actually, decidability of the relation is enough) without propext. Notice that propext is necessary to excluded middle from choice; at least we don't know a way to avoid it.

[Rémi Bottinelli]

So, a decidable relation yields an exact quotient, if I'm reading you correctly? That's interesting, I'll have a proper look, thanks!

[Junyan Xu]

Yeah, the idea is that given any a you can then map those b that satisfies r a b to true and those b that doesn't to false, if r is decidable, and this function passes down to the quotient by r, if r is an equivalence relation. (So in the case of an arbitrary relation, we need to assume its trans-symm-refl closure is decidable, which is generally not equivalent to itself being decidable.)

[Junyan Xu]

A direct proof:

lemma quot_exact {α} (r : α → α → Prop) [decidable_rel r] [is_refl α r] [is_symm α r] [is_trans α r]
  {a b : α} (h : quot.mk r a = quot.mk r b) : r a b :=
begin
  let f : quot r → Prop := quot.lift (λ b, if r a b then true else false) (λ c d hcd, _),
  { have := congr_arg f h,
    dsimp only [f] at this,
    rw if_pos (@is_refl.refl α r _ a) at this,
    by_cases r a b, { exact h },
    rw if_neg h at this,
    exact (true_ne_false this).elim },
  dsimp only,
  by_cases r a c,
  { rw [if_pos h, if_pos (trans h hcd)] },
  { rw [if_neg h, if_neg (λ had, h $ trans had $ is_symm.symm c d hcd)] },
end

#print axioms quot_exact -- no axioms

You can see the proof only ever uses decidable_pred (r a).

[Rémi Bottinelli]

Ah, it makes sense: instead of passing the relation r itself to the quotient, you re-encode it by means of true+false, so that you don't get to need propext to prove r a b = r a c, but instead just true = true.
Your proof but with propext:

lemma quot_exact {α} (r : α → α → Prop) [is_refl α r] [is_symm α r] [is_trans α r]
  {a b : α} (h : quot.mk r a = quot.mk r b) : r a b :=
begin
  let f : quot r → Prop := quot.lift (λ b, r a b) (λ c d hcd, _),
  { have := congr_arg f h,
    dsimp only [f] at this,
    rw ←this,
    exact @is_refl.refl α r _ a, },
  dsimp only,
  exact propext ⟨λ hac, trans hac hcd, λ had, trans had (symm hcd)⟩,
end

#print axioms quot_exact -- propext

or in term-mode:

lemma quot_exact {α} (r : α → α → Prop) [is_refl α r] [is_symm α r] [is_trans α r]
  {a b : α} (h : quot.mk r a = quot.mk r b) : r a b :=
let
  f : quot r → Prop :=
    quot.lift (λ b, r a b) (λ c d (hcd : r c d),
      propext ⟨λ (hac : r a c), trans hac hcd, λ (had : r a d), trans had (symm hcd)⟩)
in
  (congr_arg f h).mp (refl a : r a a)