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) [SmallCategory Ctx] : Type (u + 1)

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

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

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

Equations

• CategoryTheory.NaturalModel.instLCCPsh_groupoidModel = LCCC.mkOfOverCC

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

Equations

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

@[reducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

@[irreducible]

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

Equations

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

Equations

• CategoryTheory.NaturalModel.NaturalModelSmallPi.lambda = sorry

theorem CategoryTheory.NaturalModel.NaturalModelSmallPi.pullback {Ctx : Type u} [SmallCategory Ctx] [Limits.HasTerminal Ctx] [M : NaturalModelBase Ctx] [NaturalModelU Ctx] [NaturalModelPi Ctx] : IsPullback lambda ((P (yoneda.map (disp (ext (⊤_ Ctx) U) El))).map tp) tp (CategoryStruct.comp ((P_naturality { e := var (ext (⊤_ Ctx) U) El, b := El, is_pullback := ⋯ }).app Ty) 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) [SmallCategory Ctx] [Limits.HasTerminal Ctx] extends CategoryTheory.NaturalModel.NaturalModelBase Ctx, CategoryTheory.NaturalModel.NaturalModelPi Ctx, CategoryTheory.NaturalModel.NaturalModelSigma Ctx, CategoryTheory.NaturalModel.NaturalModelId Ctx, CategoryTheory.NaturalModel.NaturalModelU Ctx, CategoryTheory.NaturalModel.NaturalModelSmallPi Ctx : Type (u + 1)

• Tm : Psh Ctx
• Ty : Psh Ctx
• tp : Tm ⟶ Ty
• ext (Γ : Ctx) (A : yoneda.obj Γ ⟶ Ty) : Ctx
• disp (Γ : Ctx) (A : yoneda.obj Γ ⟶ Ty) : ext Γ A ⟶ Γ
• var (Γ : Ctx) (A : yoneda.obj Γ ⟶ Ty) : yoneda.obj (ext Γ A) ⟶ Tm
• disp_pullback {Γ : Ctx} (A : yoneda.obj Γ ⟶ Ty) : IsPullback (var Γ A) (yoneda.map (disp Γ A)) tp A
• Pi : (P tp).obj Ty ⟶ Ty
• lam : (P tp).obj Tm ⟶ Tm
• Pi_pullback : IsPullback lam ((P tp).map tp) tp Pi
• Sig : (P tp).obj Ty ⟶ Ty
• pair : (uvPoly tp).compDom (uvPoly tp) ⟶ Tm
• Sig_pullback : IsPullback pair ((uvPoly tp).comp (uvPoly tp)).p tp Sig
• Id : Limits.pullback tp tp ⟶ Ty
• i : Tm ⟶ Tm
• Id_commute : CategoryStruct.comp δ Id = CategoryStruct.comp i tp
• data : NaturalModelIdData Ctx
• U : yoneda.obj (⊤_ Ctx) ⟶ Ty
• El : yoneda.obj (ext (⊤_ Ctx) U) ⟶ Ty
• SmallPi : (P (yoneda.map (disp (ext (⊤_ Ctx) U) El))).obj (yoneda.obj (ext (⊤_ Ctx) U)) ⟶ yoneda.obj (ext (⊤_ Ctx) U)
• SmallPi_eq : CategoryStruct.comp SmallPi El = CategoryStruct.comp toPiArgs NaturalModelPi.Pi