GroupoidModel.Russell_PER_MS.NaturalModelBase

source

def «termY(_)» :

Lean.ParserDescr

Equations

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

Instances For

source

def «termYm(_)» :

Lean.ParserDescr

Equations

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

Instances For

source

structure NaturalModelBase (Ctx : Type u) [CategoryTheory.Category.{u_1, u} Ctx] :

Type (max u (u_1 + 1))

A representable map with choice of representability witnesses.

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

Instances For

Pullback of representable natural transformation #

source

def NaturalModelBase.pullback {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) :

NaturalModelBase Ctx

Pull a natural model back along a type.

Equations

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

Instances For

source

def NaturalModelBase.ofIsPullback {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {U E : CategoryTheory.Psh Ctx} {π : E ⟶ U} {toTy : U ⟶ M.Ty} {toTm : E ⟶ M.Tm} (pb : CategoryTheory.IsPullback toTm π M.tp toTy) :

NaturalModelBase Ctx

Given the pullback square on the right, with a natural model structure on tp : Tm ⟶ Ty giving the outer pullback square.

construct a natural model structure on π : E ⟶ U, by pullback pasting.

Equations

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

Instances For

Substitutions #

source

def NaturalModelBase.substCons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (t : CategoryTheory.yoneda.obj Δ ⟶ M.Tm) (t_tp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) :

Δ ⟶ M.ext A

Δ ⊢ σ : Γ  Γ ⊢ A type  Δ ⊢ t : A[σ]
-----------------------------------
Δ ⊢ σ.t : Γ.A

Equations

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

Instances For

source

@[simp]

theorem NaturalModelBase.substCons_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (t : CategoryTheory.yoneda.obj Δ ⟶ M.Tm) (tTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) :

CategoryTheory.CategoryStruct.comp (M.substCons σ A t tTp) (M.disp A) = σ

source

@[simp]

theorem NaturalModelBase.substCons_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (t : CategoryTheory.yoneda.obj Δ ⟶ M.Tm) (tTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) {Z : Ctx} (h : Γ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (M.substCons σ A t tTp) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = CategoryTheory.CategoryStruct.comp σ h

source

@[simp]

theorem NaturalModelBase.substCons_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (t : CategoryTheory.yoneda.obj Δ ⟶ M.Tm) (aTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substCons σ A t aTp)) (M.var A) = t

source

@[simp]

theorem NaturalModelBase.substCons_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (t : CategoryTheory.yoneda.obj Δ ⟶ M.Tm) (aTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) {Z : CategoryTheory.Functor Ctx ᵒᵖ (Type u)} (h : M.Tm ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substCons σ A t aTp)) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp t h

source

def NaturalModelBase.substFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) :

Δ ⟶ Γ

Δ ⊢ σ : Γ.A
------------
Δ ⊢ ↑∘σ : Γ

Equations

M.substFst σ = CategoryTheory.CategoryStruct.comp σ (M.disp A)

Instances For

source

def NaturalModelBase.substSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) :

CategoryTheory.yoneda.obj Δ ⟶ M.Tm

Δ ⊢ σ : Γ.A
-------------------
Δ ⊢ v₀[σ] : A[↑∘σ]

Equations

M.substSnd σ = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (M.var A)

Instances For

source

theorem NaturalModelBase.substSnd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) :

CategoryTheory.CategoryStruct.comp (M.substSnd σ) M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substFst σ)) A

source

def NaturalModelBase.wk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {X : CategoryTheory.Psh Ctx} {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ X) :

CategoryTheory.yoneda.obj (M.ext A) ⟶ X

Equations

M.wk A f = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp A)) f

Instances For

source

theorem NaturalModelBase.wk_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {N : NaturalModelBase Ctx} {Γ : Ctx} {B : CategoryTheory.yoneda.obj Γ ⟶ N.Ty} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f N.tp = B) :

CategoryTheory.CategoryStruct.comp (M.wk A f) N.tp = M.wk A B

source

@[simp]

theorem NaturalModelBase.var_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) :

CategoryTheory.CategoryStruct.comp (M.var A) M.tp = M.wk A A

source

def NaturalModelBase.substWk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) :

M.ext (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) ⟶ M.ext A

Weaken a substitution.

Δ ⊢ σ : Γ  Γ ⊢ A type
----------------------------------------
Δ.A[σ] ⊢ ↑≫σ : Γ  Δ.A[σ] ⊢ v₀ : A[↑≫σ]
----------------------------------------
Δ.A[σ] ⊢ (↑≫σ).v₀ : Γ.A

Equations

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

Instances For

source

@[simp]

theorem NaturalModelBase.substWk_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) :

CategoryTheory.CategoryStruct.comp (M.substWk σ A) (M.disp A) = CategoryTheory.CategoryStruct.comp (M.disp (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)) σ

source

@[simp]

theorem NaturalModelBase.substWk_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) {Z : Ctx} (h : Γ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (M.substWk σ A) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = CategoryTheory.CategoryStruct.comp (M.disp (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)) (CategoryTheory.CategoryStruct.comp σ h)

source

@[simp]

theorem NaturalModelBase.substWk_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A)) (M.var A) = M.var (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)

source

@[simp]

theorem NaturalModelBase.substWk_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) {Z : CategoryTheory.Functor Ctx ᵒᵖ (Type u)} (h : M.Tm ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A)) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp (M.var (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)) h

source

def NaturalModelBase.inst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (x : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) :

CategoryTheory.yoneda.obj Γ ⟶ X

Γ ⊢ A type  Γ.A ⊢ x ⟶ X  Γ ⊢ a : A
-----------------------------------
Γ ⊢ x[id.a] ⟶ X

Equations

M.inst A x a a_tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substCons (CategoryTheory.CategoryStruct.id Γ) A a ⋯)) x

Instances For

source

@[simp]

def NaturalModelBase.inst_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {N : NaturalModelBase Ctx} {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Ty) (t : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Tm) (t_tp : CategoryTheory.CategoryStruct.comp t N.tp = B) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) :

CategoryTheory.CategoryStruct.comp (M.inst A t a a_tp) N.tp = M.inst A B a a_tp

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem NaturalModelBase.inst_wk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (x : CategoryTheory.yoneda.obj Γ ⟶ X) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) :

M.inst A (M.wk A x) a a_tp = x

Polynomial functor on `tp` #

source

instance NaturalModelBase.instHasFiniteWidePullbacksPsh {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] :

CategoryTheory.Limits.HasFiniteWidePullbacks (CategoryTheory.Psh Ctx)

source

instance NaturalModelBase.instLCCPsh {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] :

LCC (CategoryTheory.Psh Ctx)

Equations

NaturalModelBase.instLCCPsh = LCCC.mkOfOverCC

source

instance NaturalModelBase.instCartesianExponentiablePsh {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Tm Ty : CategoryTheory.Psh Ctx} (tp : Tm ⟶ Ty) :

CartesianExponentiable tp

Equations

NaturalModelBase.instCartesianExponentiablePsh tp = { functor := LCC.pushforward tp, adj := LCC.adj tp }

source

def NaturalModelBase.uvPolyTp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) :

UvPoly M.Tm M.Ty

Equations

M.uvPolyTp = { p := M.tp, exp := inferInstance }

Instances For

source

@[simp]

theorem NaturalModelBase.uvPolyTp_exp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) :

M.uvPolyTp.exp = inferInstance

source

@[simp]

theorem NaturalModelBase.uvPolyTp_p {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) :

M.uvPolyTp.p = M.tp

source

def NaturalModelBase.uvPolyTpT {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) :

UvPoly.Total (CategoryTheory.Psh Ctx)

Equations

M.uvPolyTpT = { E := M.Tm, B := M.Ty, poly := M.uvPolyTp }

Instances For

source

def NaturalModelBase.Ptp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) :

CategoryTheory.Functor (CategoryTheory.Psh Ctx) (CategoryTheory.Psh Ctx)

Equations

M.Ptp = M.uvPolyTp.functor

Instances For

source

def NaturalModelBase.Ptp_equiv {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} :

(A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) × (CategoryTheory.yoneda.obj (M.ext A) ⟶ X) ≃ (CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X)

Γ ⊢ A type  y(Γ.A) ⟶ X
=======================
yΓ ⟶ P_tp(X)

Equations

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

Instances For

source

theorem NaturalModelBase.Ptp_equiv_naturality {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X Y : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (x : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) (α : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp (M.Ptp_equiv ⟨A, x⟩) (M.Ptp.map α) = M.Ptp_equiv ⟨A, CategoryTheory.CategoryStruct.comp x α⟩

source

theorem NaturalModelBase.Ptp_equiv_naturality_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X Y : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (x : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) (α : X ⟶ Y) {Z : CategoryTheory.Functor Ctx ᵒᵖ (Type u)} (h : M.Ptp.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (M.Ptp_equiv ⟨A, x⟩) (CategoryTheory.CategoryStruct.comp (M.Ptp.map α) h) = CategoryTheory.CategoryStruct.comp (M.Ptp_equiv ⟨A, CategoryTheory.CategoryStruct.comp x α⟩) h

source

theorem NaturalModelBase.Ptp_equiv_symm_naturality {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X Y : CategoryTheory.Psh Ctx} (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X) (α : X ⟶ Y) :

let S := M.Ptp_equiv.symm x; M.Ptp_equiv.symm (CategoryTheory.CategoryStruct.comp x (M.Ptp.map α)) = ⟨S.fst, CategoryTheory.CategoryStruct.comp S.snd α⟩

source

theorem NaturalModelBase.Ptp_ext {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {x y : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} :

x = y ↔ (M.Ptp_equiv.symm x).fst = (M.Ptp_equiv.symm y).fst ∧ HEq (M.Ptp_equiv.symm x).snd (M.Ptp_equiv.symm y).snd

Pullback of representable natural transformation #

Substitutions #

Polynomial functor on tp #

Polynomial functor on `tp` #