Lifting dependent functions to quotient map

Stream: Is there code for X?

[Kin Yau James Wong]

Hello all, I've been working on trying to lift a function f : (a : α) → (b : α) → P a → P b → β to the quotient map
f' : (a : Quotient s) → (b : Quotient s) → P' a → P' b → β where P is a predicate that also respects the equivalence relation defined by the Setoid, s (and consequently lifts to P'), but I've had little success with using the theorems in the Quotient module. Many thanks for the advice :pray:

(p.s. I'm trying to avoid using Quotient.out)

[Junyan Xu]

Maybe you want to use Equiv.subtypeQuotientEquivQuotientSubtype to reduce your problem to lifting a non-dependent function?

[Aaron Liu]

Try using Quotient.rec?

[Aaron Liu]

import Mathlib

-- there must be a better name
def Quotient.liftProp {α β : Type*} {s : Setoid α} {P : Quotient s → Prop}
    (f : (a : α) → P (Quotient.mk s a) → β)
    (sound : ∀ a b ha hb, a ≈ b → f a ha = f b hb)
    (a : Quotient s) (ha : P a) : β :=
  @Quotient.rec α s (fun u => P u → β) f (fun u v huv =>
    eq_of_heq (eqRec_heq_iff.mpr
      (Function.hfunext (congrArg P (Quotient.sound huv)) fun hu hv _ =>
        heq_of_eq (sound u v hu hv huv)))) a ha

theorem Quotient.liftProp_mk {α β : Type*} {s : Setoid α} {P : Quotient s → Prop}
    (f : (a : α) → P (Quotient.mk s a) → β)
    (sound : ∀ a b ha hb, a ≈ b → f a ha = f b hb)
    (a : α) (ha : P (Quotient.mk s a)) :
    Quotient.liftProp f sound (Quotient.mk s a) ha = f a ha := rfl

def Quotient.liftProp₂ {α β : Type*} {s : Setoid α} {P : Quotient s → Prop}
    (f : (a : α) → (b : α) → P (Quotient.mk s a) → P (Quotient.mk s b) → β)
    (sound : ∀ a b c d ha hb hc hd, a ≈ c → b ≈ d → f a b ha hb = f c d hc hd)
    (a b : Quotient s) (ha : P a) (hb : P b) : β :=
  Quotient.liftProp (fun c hc =>
    Quotient.liftProp (fun d hd => f c d hc hd) (fun u v hu hv huv =>
      sound c u c v hc hu hc hv (Setoid.refl c) huv) b hb) (fun u v hu hv huv =>
        Quotient.ind (motive := fun b => ∀ (hb : P b),
          Quotient.liftProp (fun d hd => f u d hu hd) _ b hb =
          Quotient.liftProp (fun d hd => f v d hv hd) _ b hb)
          (fun b hb => sound u b v b hu hb hv hb huv (Setoid.refl b)) b hb) a ha

def Quotient.liftProp₂_mk {α β : Type*} {s : Setoid α} {P : Quotient s → Prop}
    (f : (a : α) → (b : α) → P (Quotient.mk s a) → P (Quotient.mk s b) → β)
    (sound : ∀ a b c d ha hb hc hd, a ≈ c → b ≈ d → f a b ha hb = f c d hc hd)
    (a b : α) (ha : P (Quotient.mk s a)) (hb : P (Quotient.mk s b)) :
    Quotient.liftProp₂ f sound (Quotient.mk s a) (Quotient.mk s b) ha hb = f a b ha hb := rfl

[Kin Yau James Wong]

Thanks! Is this something you might push to Mathlib?

[Aaron Liu]

Maybe if someone comes up with a better name and a use case

[Robin Arnez]

I encountered the same problem while developing ExtHashMaps, so I added Quotient.pliftOn and Quot.pliftOn:

structure MyType where
  value : Nat

def MyType.P : MyType → Prop := fun n => n.value % 2 = 0

opaque fn : (a : MyType) → (b : MyType) → a.P → b.P → Nat

def MyType.rel : MyType → MyType → Prop := fun a b => a.value % 2 = b.value % 2

theorem MyType.P_congr {x y : MyType} (h : x.rel y) : x.P ↔ y.P := by
  unfold rel at h
  simp [P, h]

def MyType.P' : Quot MyType.rel → Prop := Quot.lift MyType.P (fun _ _ h => propext (MyType.P_congr h))

def f' (a : Quot MyType.rel) (b : Quot MyType.rel) (h : MyType.P' a) (h' : MyType.P' b) : Nat :=
  a.pliftOn (fun a' ha => b.pliftOn (fun b' hb => fn a' b' (ha ▸ h :) (hb ▸ h' :)) sorry) sorry

[Robin Arnez]

Should be available since v4.20.0

[Kin Yau James Wong]

ah this is perfect - thanks!