def CategoryTheory.UvPoly.equiv {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B : C} (P : UvPoly E B) (Γ X : C) : (Γ ⟶ P @ X) ≃ (b : Γ ⟶ B) × (Limits.pullback b P.p ⟶ X)

Universal property of the polynomial functor.

Equations

• P.equiv Γ X = { toFun := P.proj, invFun := fun (u : (b : Γ ⟶ B) × (CategoryTheory.Limits.pullback b P.p ⟶ X)) => P.lift u.fst u.snd, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.UvPoly.equiv_symm_apply {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B : C} (P : UvPoly E B) (Γ X : C) (u : (b : Γ ⟶ B) × (Limits.pullback b P.p ⟶ X)) : (P.equiv Γ X).symm u = P.lift u.fst u.snd

@[simp]

theorem CategoryTheory.UvPoly.equiv_apply {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B : C} (P : UvPoly E B) (Γ X : C) (f : Γ ⟶ P @ X) : (P.equiv Γ X) f = P.proj f