structure CategoryTheory.UvPoly' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasFiniteWidePullbacks C] (E : C) (B : C) : Type (max u_1 u_2)

P : UvPoly C is a polynomial functors in a single variable

• p : E ⟶ B
• exp : CartesianExponentiable self.p

def UvPoly.equiv' {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] [CategoryTheory.Limits.HasPullbacks 𝒞] {E : 𝒞} {B : 𝒞} (P : UvPoly E B) (Γ : 𝒞) (X : 𝒞) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (CategoryTheory.Limits.pullback P.p b ⟶ X)

Universal property of the polynomial functor.

Equations

• P.equiv' Γ X = (P.equiv Γ X).trans (Equiv.sigmaCongrRight fun (x : Γ ⟶ B) => ((CategoryTheory.yoneda.obj X).mapIso (CategoryTheory.Limits.pullbackSymmetry P.p x).op).toEquiv)

def UvPoly.comp {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Limits.HasFiniteWidePullbacks 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {E : 𝒞} {B : 𝒞} {D : 𝒞} {C : 𝒞} (P1 : UvPoly E B) (P2 : UvPoly D C) : UvPoly (P2.functor.obj E) (P1.functor.obj C)

Equations

• P1.comp P2 = { p := sorry, exp := sorry }

Natural Models

def CategoryTheory.«termY(_)» : Lean.ParserDescr

Equations

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

class CategoryTheory.NaturalModel.NaturalModelBase (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] : Type (u + 1)

• Tm : CategoryTheory.Psh Ctx
• Ty : CategoryTheory.Psh Ctx
• tp : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Ty
• ext : (Γ : Ctx) → (CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) → Ctx
• disp : (Γ : Ctx) → (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) → CategoryTheory.NaturalModel.ext Γ A ⟶ Γ
• var : (Γ : Ctx) → (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) → CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Tm
• disp_pullback : ∀ {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty), CategoryTheory.IsPullback (CategoryTheory.NaturalModel.var Γ A) (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Γ A)) CategoryTheory.NaturalModel.tp A

theorem CategoryTheory.NaturalModel.NaturalModelBase.disp_pullback {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} [self : CategoryTheory.NaturalModel.NaturalModelBase Ctx] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty), CategoryTheory.IsPullback (CategoryTheory.NaturalModel.var Γ A) (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Γ A)) CategoryTheory.NaturalModel.tp A

instance CategoryTheory.NaturalModel.instHasFiniteWidePullbacksPsh_groupoidModel {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] : CategoryTheory.Limits.HasFiniteWidePullbacks (CategoryTheory.Psh Ctx)

Equations

• ⋯ = ⋯

instance CategoryTheory.NaturalModel.instLCCPsh_groupoidModel {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] : LCC (CategoryTheory.Psh Ctx)

Equations

• CategoryTheory.NaturalModel.instLCCPsh_groupoidModel = LCCC.mkOfOverCC

instance CategoryTheory.NaturalModel.instCartesianExponentiablePsh_groupoidModel {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm : CategoryTheory.Psh Ctx} {Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) : CartesianExponentiable tp

Equations

• CategoryTheory.NaturalModel.instCartesianExponentiablePsh_groupoidModel tp = { functor := LCC.pushforward tp, adj := LCC.adj tp }

def CategoryTheory.NaturalModel.uvPoly {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm : CategoryTheory.Psh Ctx} {Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) : UvPoly Tm Ty

Equations

• CategoryTheory.NaturalModel.uvPoly tp = { p := tp, exp := inferInstance }

def CategoryTheory.NaturalModel.uvPolyT {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm : CategoryTheory.Psh Ctx} {Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) : UvPoly.Total (CategoryTheory.Psh Ctx)

Equations

• CategoryTheory.NaturalModel.uvPolyT tp = { E := Tm, B := Ty, poly := CategoryTheory.NaturalModel.uvPoly tp }

def CategoryTheory.NaturalModel.P {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm : CategoryTheory.Psh Ctx} {Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) : CategoryTheory.Functor (CategoryTheory.Psh Ctx) (CategoryTheory.Psh Ctx)

Equations

• CategoryTheory.NaturalModel.P tp = (CategoryTheory.NaturalModel.uvPoly tp).functor

def CategoryTheory.NaturalModel.P_naturality {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {E : CategoryTheory.Psh Ctx} {B : CategoryTheory.Psh Ctx} {E' : CategoryTheory.Psh Ctx} {B' : CategoryTheory.Psh Ctx} {f : E ⟶ B} {f' : E' ⟶ B'} (α : CategoryTheory.NaturalModel.uvPolyT f ⟶ CategoryTheory.NaturalModel.uvPolyT f') : CategoryTheory.NaturalModel.P f ⟶ CategoryTheory.NaturalModel.P f'

Equations

• CategoryTheory.NaturalModel.P_naturality α = UvPoly.naturality α

def CategoryTheory.NaturalModel.proj {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm : CategoryTheory.Psh Ctx} {Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) : (CategoryTheory.NaturalModel.P tp).obj Ty ⟶ Ty

Equations

• CategoryTheory.NaturalModel.proj tp = (CategoryTheory.NaturalModel.uvPoly tp).proj Ty

class CategoryTheory.NaturalModel.NaturalModelPi (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] : Type u

• Pi : (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Ty ⟶ CategoryTheory.NaturalModel.Ty
• lam : (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm
• Pi_pullback : CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelPi.lam ((CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).map CategoryTheory.NaturalModel.tp) CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelPi.Pi

theorem CategoryTheory.NaturalModel.NaturalModelPi.Pi_pullback {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} {M : CategoryTheory.NaturalModel.NaturalModelBase Ctx} [self : CategoryTheory.NaturalModel.NaturalModelPi Ctx], CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelPi.lam ((CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).map CategoryTheory.NaturalModel.tp) CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelPi.Pi

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

• Sig : (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Ty ⟶ CategoryTheory.NaturalModel.Ty
• pair : (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm
• Sig_pullback : CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelSigma.pair ((CategoryTheory.NaturalModel.uvPoly CategoryTheory.NaturalModel.tp).comp (CategoryTheory.NaturalModel.uvPoly CategoryTheory.NaturalModel.tp)).p CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelSigma.Sig

theorem CategoryTheory.NaturalModel.NaturalModelSigma.Sig_pullback {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} {M : CategoryTheory.NaturalModel.NaturalModelBase Ctx} [self : CategoryTheory.NaturalModel.NaturalModelSigma Ctx], CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelSigma.pair ((CategoryTheory.NaturalModel.uvPoly CategoryTheory.NaturalModel.tp).comp (CategoryTheory.NaturalModel.uvPoly CategoryTheory.NaturalModel.tp)).p CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelSigma.Sig

def CategoryTheory.NaturalModel.δ {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.Limits.pullback CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.tp

Equations

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

class CategoryTheory.NaturalModel.NaturalModelEq (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] : Type u

• Eq : CategoryTheory.Limits.pullback CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.tp ⟶ CategoryTheory.NaturalModel.Ty
• refl : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm
• Eq_pullback : CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelEq.refl CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelEq.Eq

theorem CategoryTheory.NaturalModel.NaturalModelEq.Eq_pullback {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} {M : CategoryTheory.NaturalModel.NaturalModelBase Ctx} [self : CategoryTheory.NaturalModel.NaturalModelEq Ctx], CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelEq.refl CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.NaturalModelEq.Eq

class CategoryTheory.NaturalModel.NaturalModelIdBase (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] : Type u

• Id : CategoryTheory.Limits.pullback CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.tp ⟶ CategoryTheory.NaturalModel.Ty
• i : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm
• Id_commute : CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.NaturalModelIdBase.Id = CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelIdBase.i CategoryTheory.NaturalModel.tp

theorem CategoryTheory.NaturalModel.NaturalModelIdBase.Id_commute {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} {M : CategoryTheory.NaturalModel.NaturalModelBase Ctx} [self : CategoryTheory.NaturalModel.NaturalModelIdBase Ctx], CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.NaturalModelIdBase.Id = CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelIdBase.i CategoryTheory.NaturalModel.tp

def CategoryTheory.NaturalModel.I {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.Psh Ctx

Equations

• CategoryTheory.NaturalModel.I = CategoryTheory.Limits.pullback CategoryTheory.NaturalModel.NaturalModelIdBase.Id CategoryTheory.NaturalModel.tp

def CategoryTheory.NaturalModel.q {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.NaturalModel.I ⟶ CategoryTheory.NaturalModel.Ty

Equations

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

def CategoryTheory.NaturalModel.ρ {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.I

Equations

• CategoryTheory.NaturalModel.ρ = CategoryTheory.Limits.pullback.lift CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.NaturalModelIdBase.i ⋯

def CategoryTheory.NaturalModel.ρs {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.q ⟶ CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp

Equations

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

def CategoryTheory.NaturalModel.pb2 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.Psh Ctx

Equations

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

def CategoryTheory.NaturalModel.ε {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.q).obj CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.pb2

Equations

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

theorem CategoryTheory.NaturalModel.NaturalModelIdData_def (Ctx : Type u_1) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : CategoryTheory.NaturalModel.NaturalModelIdData Ctx = { J : CategoryTheory.NaturalModel.pb2 ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.q).obj CategoryTheory.NaturalModel.Tm // CategoryTheory.CategoryStruct.comp J CategoryTheory.NaturalModel.ε = CategoryTheory.CategoryStruct.id CategoryTheory.NaturalModel.pb2 }

@[irreducible]

def CategoryTheory.NaturalModel.NaturalModelIdData (Ctx : Type u_1) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelIdBase Ctx] : Type u_1

Equations

• CategoryTheory.NaturalModel.NaturalModelIdData = CategoryTheory.NaturalModel.wrapped✝.1

class CategoryTheory.NaturalModel.NaturalModelId (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] extends CategoryTheory.NaturalModel.NaturalModelIdBase : Type u

• Id : CategoryTheory.Limits.pullback CategoryTheory.NaturalModel.tp CategoryTheory.NaturalModel.tp ⟶ CategoryTheory.NaturalModel.Ty
• i : CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm
• Id_commute : CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.δ CategoryTheory.NaturalModel.NaturalModelIdBase.Id = CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelIdBase.i CategoryTheory.NaturalModel.tp
• data : CategoryTheory.NaturalModel.NaturalModelIdData Ctx

def CategoryTheory.NaturalModel.NaturalModelId.J {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelId Ctx] : CategoryTheory.NaturalModel.pb2 ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.q).obj CategoryTheory.NaturalModel.Tm

Equations

• CategoryTheory.NaturalModel.NaturalModelId.J = ↑(⋯.mp CategoryTheory.NaturalModel.NaturalModelId.data)

theorem CategoryTheory.NaturalModel.NaturalModelId.J_section {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelId Ctx] : CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelId.J CategoryTheory.NaturalModel.ε = CategoryTheory.CategoryStruct.id CategoryTheory.NaturalModel.pb2

class CategoryTheory.NaturalModel.NaturalModelU (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] : Type u

• U : CategoryTheory.yoneda.obj (⊤_ Ctx) ⟶ CategoryTheory.NaturalModel.Ty
• El : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) ⟶ CategoryTheory.NaturalModel.Ty

def CategoryTheory.NaturalModel.toPiArgs {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelU Ctx] [CategoryTheory.NaturalModel.NaturalModelPi Ctx] : (CategoryTheory.NaturalModel.P (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) CategoryTheory.NaturalModel.El))).obj (CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U)) ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Ty

Equations

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

class CategoryTheory.NaturalModel.NaturalModelSmallPi (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelU Ctx] [CategoryTheory.NaturalModel.NaturalModelPi Ctx] : Type u

• SmallPi : (CategoryTheory.NaturalModel.P (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) CategoryTheory.NaturalModel.El))).obj (CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U)) ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U)
• SmallPi_eq : CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelSmallPi.SmallPi CategoryTheory.NaturalModel.El = CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.toPiArgs CategoryTheory.NaturalModel.NaturalModelPi.Pi

theorem CategoryTheory.NaturalModel.NaturalModelSmallPi.SmallPi_eq {Ctx : Type u} : ∀ {inst : CategoryTheory.SmallCategory Ctx} {inst_1 : CategoryTheory.Limits.HasTerminal Ctx} {M : CategoryTheory.NaturalModel.NaturalModelBase Ctx} {inst_2 : CategoryTheory.NaturalModel.NaturalModelU Ctx} {inst_3 : CategoryTheory.NaturalModel.NaturalModelPi Ctx} [self : CategoryTheory.NaturalModel.NaturalModelSmallPi Ctx], CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.NaturalModelSmallPi.SmallPi CategoryTheory.NaturalModel.El = CategoryTheory.CategoryStruct.comp CategoryTheory.NaturalModel.toPiArgs CategoryTheory.NaturalModel.NaturalModelPi.Pi

def CategoryTheory.NaturalModel.NaturalModelSmallPi.lambda {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelU Ctx] [CategoryTheory.NaturalModel.NaturalModelPi Ctx] : (CategoryTheory.NaturalModel.P (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) CategoryTheory.NaturalModel.El))).obj CategoryTheory.NaturalModel.Tm ⟶ CategoryTheory.NaturalModel.Tm

Equations

• CategoryTheory.NaturalModel.NaturalModelSmallPi.lambda = sorry

theorem CategoryTheory.NaturalModel.NaturalModelSmallPi.pullback {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel.NaturalModelBase Ctx] [CategoryTheory.NaturalModel.NaturalModelU Ctx] [CategoryTheory.NaturalModel.NaturalModelPi Ctx] : CategoryTheory.IsPullback CategoryTheory.NaturalModel.NaturalModelSmallPi.lambda ((CategoryTheory.NaturalModel.P (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) CategoryTheory.NaturalModel.El))).map CategoryTheory.NaturalModel.tp) CategoryTheory.NaturalModel.tp (CategoryTheory.CategoryStruct.comp ((CategoryTheory.NaturalModel.P_naturality { e := CategoryTheory.NaturalModel.var (CategoryTheory.NaturalModel.ext (⊤_ Ctx) CategoryTheory.NaturalModel.U) CategoryTheory.NaturalModel.El, b := CategoryTheory.NaturalModel.El, is_pullback := ⋯ }).app CategoryTheory.NaturalModel.Ty) CategoryTheory.NaturalModel.NaturalModelPi.Pi)

def CategoryTheory.NaturalModel.NaturalModelSmallSigma : Type

Equations

• CategoryTheory.NaturalModel.NaturalModelSmallSigma = sorry

def CategoryTheory.NaturalModel.NaturalModelSmallId : Type

Equations

• CategoryTheory.NaturalModel.NaturalModelSmallId = sorry

def CategoryTheory.NaturalModel.NaturalModelUnivalentU : Type

Equations

• CategoryTheory.NaturalModel.NaturalModelUnivalentU = sorry

class CategoryTheory.NaturalModel (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] extends CategoryTheory.NaturalModel.NaturalModelBase , CategoryTheory.NaturalModel.NaturalModelPi , CategoryTheory.NaturalModel.NaturalModelSigma , CategoryTheory.NaturalModel.NaturalModelId , CategoryTheory.NaturalModel.NaturalModelU , CategoryTheory.NaturalModel.NaturalModelSmallPi , CategoryTheory.NaturalModel.NaturalModelIdBase : Type (u + 1)