General lift

Stream: Is there code for X?

[Adam Topaz]

Do we have something like this?

def general_lift {α ι β : Type*} [I : setoid α] (f : (ι → α) → β)
  (c : ∀ i j : ι → α, (∀ x : ι, i x ≈ j x) → f i = f j) :
  (ι → quotient I) → β := sorry

[Eric Wieser]

docs#pi_setoid seems relevant

[Eric Wieser]

It's λ i, quotient.lift_on (quotient.choice i) f c

[Eric Wieser]

Or quotient.lift f c ∘ quotient.choice for short

[Adam Topaz]

Here's the fully dependent version:

noncomputable def quotient.pi_lift {ι : Type*} {α : ι → Type*} {β : Type*}
  [I : Π i, setoid (α i)] (f : (Π i, α i) → β)
  (c : ∀ g h : (Π i, α i), (∀ i, g i ≈ h i) → f g = f h) :
  (Π i, quotient (I i)) → β := quotient.lift f c ∘ quotient.choice