Zulip Chat Archive

Stream: Is there code for X?

Topic: General lift


view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 19 2021 at 16:35):

docs#pi_setoid seems relevant

view this post on Zulip Eric Wieser (Feb 19 2021 at 16:38):

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

view this post on Zulip Eric Wieser (Feb 19 2021 at 16:38):

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

view this post on Zulip 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