## 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: May 16 2021 at 05:21 UTC