structure NaturalModelBase.NaturalModelPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) : Type u

• Pi : M.Ptp.obj M.Ty ⟶ M.Ty
• lam : M.Ptp.obj M.Tm ⟶ M.Tm
• Pi_pullback : CategoryTheory.IsPullback self.lam (M.Ptp.map M.tp) M.tp self.Pi

class NaturalModelBase.NaturalModelSigma {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) : Type u

• Sig : M.Ptp.obj M.Ty ⟶ M.Ty
• pair : M.uvPolyTp.compDom M.uvPolyTp ⟶ M.Tm
• Sig_pullback : CategoryTheory.IsPullback pair (M.uvPolyTp.comp M.uvPolyTp).p M.tp Sig

def NaturalModelBase.pullbackIsoExt {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) : CategoryTheory.Limits.pullback A M.uvPolyTp.p ≅ CategoryTheory.yoneda.obj (M.ext A)

Equations

• M.pullbackIsoExt A = ⋯.isoPullback.symm

def NaturalModelBase.uvPolyTpEquiv {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} : (CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.functor.obj X) ≃ (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) × (CategoryTheory.yoneda.obj (M.ext A) ⟶ X)

This is a specialization of UvPoly.equiv the universal property of UvPoly to M.uvPolyTp. We use the chosen pullback M.ext A instead of pullback from the HasPullback instance

Equations

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

@[simp]

theorem NaturalModelBase.uvPolyTpEquiv_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.functor.obj X) : (M.uvPolyTpEquiv AB).fst = CategoryTheory.CategoryStruct.comp AB (M.uvPolyTp.proj X)

@[simp]

theorem NaturalModelBase.uvPolyTpEquiv_symm_snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (M.uvPolyTpEquiv (M.uvPolyTpEquiv.symm ⟨A, B⟩)).snd = B

theorem NaturalModelBase.uvPolyTpEquiv_symm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : M.uvPolyTpEquiv.symm ⟨A, B⟩ = M.uvPolyTp.pairPoly A (CategoryTheory.CategoryStruct.comp (M.pullbackIsoExt A).hom B)

@[simp]

theorem NaturalModelBase.uvPolyTpEquiv_symm_proj {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (M.uvPolyTpEquiv.symm ⟨A, B⟩) (M.uvPolyTp.proj X) = A

def NaturalModelBase.sec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (M.ext (CategoryTheory.CategoryStruct.comp α M.tp))

sec is the universal lift in the following diagram, which is a section of Groupoidal.forget

===== Γ -------α--------------¬ ‖ ↓ sec V ‖ M.ext A ⋯ -------------> M.Tm ‖ | | ‖ | | ‖ forget M.tp ‖ | | ‖ V V ===== Γ ---- α ≫ M.tp -----> M.Ty

Equations

• M.sec α = ⋯.lift α (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.obj Γ)) ⋯

@[simp]

theorem NaturalModelBase.sec_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (M.sec α) (M.var (CategoryTheory.CategoryStruct.comp α M.tp)) = α

@[simp]

theorem NaturalModelBase.sec_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (M.sec α) (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp α M.tp))) = CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.obj Γ)

theorem NaturalModelBase.lift_ev {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.functor.obj M.Ty} {α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm} (hA : CategoryTheory.CategoryStruct.comp AB (M.uvPolyTp.proj M.Ty) = CategoryTheory.CategoryStruct.comp α M.tp) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift AB α hA) (UvPoly.genPb.u₂ M.uvPolyTp M.Ty) = CategoryTheory.CategoryStruct.comp (M.sec α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (M.uvPolyTpEquiv AB).snd)

def NaturalModelBase.uvPolyTpCompDomEquiv {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) (Γ : Ctx) : (CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom M.uvPolyTp) ≃ (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) × (B : CategoryTheory.yoneda.obj (M.ext (CategoryTheory.CategoryStruct.comp α M.tp)) ⟶ M.Ty) × (β : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) ×' CategoryTheory.CategoryStruct.comp β M.tp = CategoryTheory.CategoryStruct.comp (M.sec α) B

A specialization of the universal property of UvPoly.compDom to M.uvPolyTp, using the chosen pullback M.ext instead of pullback.

Equations

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