theorem UvPoly.pair_proj {𝒞 : Type u_2} [CategoryTheory.Category.{u_1, u_2} 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] [CategoryTheory.Limits.HasPullbacks 𝒞] {E B : 𝒞} (P : UvPoly E B) (A : 𝒞) {Γ : 𝒞} (b : Γ ⟶ B) (e : CategoryTheory.Limits.pullback b P.p ⟶ A) : CategoryTheory.CategoryStruct.comp (P.pairPoly b e) (P.proj A) = b

def UvPoly.genPb.snd {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] [CategoryTheory.Limits.HasPullbacks 𝒞] {E B : 𝒞} (P : UvPoly E B) (A : 𝒞) : P.genPb A ⟶ E

Equations

• UvPoly.genPb.snd P A = CategoryTheory.Limits.pullback.snd (P.proj A) P.p

theorem UvPoly.genPb.condition {𝒞 : Type u_2} [CategoryTheory.Category.{u_1, u_2} 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] [CategoryTheory.Limits.HasPullbacks 𝒞] {E B : 𝒞} (P : UvPoly E B) {A : 𝒞} : CategoryTheory.CategoryStruct.comp (snd P A) P.p = CategoryTheory.CategoryStruct.comp (fst P A) (P.proj A)

def UvPoly.compDomEquiv {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] [CategoryTheory.Limits.HasPullbacks 𝒞] {Γ E B D A : 𝒞} {P : UvPoly E B} {Q : UvPoly D A} : (Γ ⟶ P.compDom Q) ≃ (AB : Γ ⟶ P.functor.obj A) × (α : Γ ⟶ E) × (β : Γ ⟶ D) ×' (h : CategoryTheory.CategoryStruct.comp AB (P.proj A) = CategoryTheory.CategoryStruct.comp α P.p) ×' CategoryTheory.CategoryStruct.comp β Q.p = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift AB α h) (genPb.u₂ P A)

Equations

• One or more equations did not get rendered due to their size.

instance instLCCPsh_groupoidModel {𝒞 : Type u_1} [CategoryTheory.SmallCategory 𝒞] : LCC (CategoryTheory.Psh 𝒞)

Equations

• instLCCPsh_groupoidModel = LCCC.mkOfOverCC

instance instCartesianExponentiablePsh_groupoidModel {𝒞 : Type u_1} [CategoryTheory.SmallCategory 𝒞] {X Y : CategoryTheory.Psh 𝒞} (f : X ⟶ Y) : CartesianExponentiable f

Equations

• instCartesianExponentiablePsh_groupoidModel f = { functor := LCC.pushforward f, adj := LCC.adj f }