Zulip Chat Archive
Stream: Is there code for X?
Topic: General lift
Adam Topaz (Feb 19 2021 at 16:03):
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 (Feb 19 2021 at 16:35):
docs#pi_setoid seems relevant
Eric Wieser (Feb 19 2021 at 16:38):
It's λ i, quotient.lift_on (quotient.choice i) f c
Eric Wieser (Feb 19 2021 at 16:38):
Or quotient.lift f c ∘ quotient.choice
for short
Adam Topaz (Feb 19 2021 at 16:51):
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
Last updated: Dec 20 2023 at 11:08 UTC