GroupoidModel.Syntax.NaturalModel

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

Type (max u (u_1 + 1))

A natural model with support for dependent types (and nothing more). The data is a natural transformation with representable fibers, stored as a choice of representative for each fiber.

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

source

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

CategoryTheory.Limits.pullback A M.tp ≅ CategoryTheory.yoneda.obj (M.ext A)

Equations

M.pullbackIsoExt A = ⋯.isoPullback.symm

Instances For

source

@[simp]

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

(M.pullbackIsoExt A).hom = ⋯.isoPullback.inv

source

@[simp]

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

(M.pullbackIsoExt A).inv = ⋯.isoPullback.hom

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_functor_map {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) {D : Type _uniq.18952} [CategoryTheory.Category.{_uniq.18951, _uniq.18952} D] (F : CategoryTheory.Functor Ctx D) :

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

source

@[simp]

theorem NaturalModelBase.substCons_disp_functor_map_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) {D : Type _uniq.18952} [CategoryTheory.Category.{_uniq.18951, _uniq.18952} D] (F : CategoryTheory.Functor Ctx D) {Z : D} (h : F.obj Γ ⟶ Z) :

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

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

@[simp]

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.wk_tp_assoc {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) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : N.Ty ⟶ Z) :

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

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

@[simp]

theorem NaturalModelBase.var_tp_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.Ty ⟶ Z) :

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

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

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

theorem NaturalModelBase.substWk_disp_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) {D : Type _uniq.36540} [CategoryTheory.Category.{_uniq.36539, _uniq.36540} D] (F : CategoryTheory.Functor Ctx D) :

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

source

theorem NaturalModelBase.substWk_disp_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) {D : Type _uniq.36540} [CategoryTheory.Category.{_uniq.36539, _uniq.36540} D] (F : CategoryTheory.Functor Ctx D) {Z : D} (h : F.obj Γ ⟶ Z) :

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

source

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.sec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) :

Γ ⟶ M.ext A

sec is the section of disp A corresponding to a.

Equations

M.sec A a a_tp = M.substCons (CategoryTheory.CategoryStruct.id Γ) A a ⋯

Instances For

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (M.disp A) = CategoryTheory.CategoryStruct.id Γ

source

@[simp]

theorem NaturalModelBase.sec_disp_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {D : Type _uniq.43333} [CategoryTheory.Category.{_uniq.43332, _uniq.43333} D] (F : CategoryTheory.Functor Ctx D) :

CategoryTheory.CategoryStruct.comp (F.map (M.sec A a a_tp)) (F.map (M.disp A)) = CategoryTheory.CategoryStruct.id (F.obj Γ)

source

@[simp]

theorem NaturalModelBase.sec_disp_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {D : Type _uniq.43333} [CategoryTheory.Category.{_uniq.43332, _uniq.43333} D] (F : CategoryTheory.Functor Ctx D) {Z : D} (h : F.obj Γ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (M.sec A a a_tp)) (CategoryTheory.CategoryStruct.comp (F.map (M.disp A)) h) = h

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = h

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A a a_tp)) (M.var A) = a

source

@[simp]

theorem NaturalModelBase.sec_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : M.Tm ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A a a_tp)) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp a h

source

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

CategoryTheory.CategoryStruct.comp σ (M.sec A a a_tp) = CategoryTheory.CategoryStruct.comp (M.sec (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯) (M.substWk σ A)

source

theorem NaturalModelBase.comp_sec_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {D : Type _uniq.49935} [CategoryTheory.Category.{_uniq.49934, _uniq.49935} D] (F : CategoryTheory.Functor Ctx D) :

CategoryTheory.CategoryStruct.comp (F.map σ) (F.map (M.sec A a a_tp)) = CategoryTheory.CategoryStruct.comp (F.map (M.sec (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯)) (F.map (M.substWk σ A))

source

theorem NaturalModelBase.comp_sec_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {Z : Ctx} (h : M.ext A ⟶ Z) :

CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) h) = CategoryTheory.CategoryStruct.comp (M.sec (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯) (CategoryTheory.CategoryStruct.comp (M.substWk σ A) h)

source

theorem NaturalModelBase.comp_sec_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {D : Type _uniq.49935} [CategoryTheory.Category.{_uniq.49934, _uniq.49935} D] (F : CategoryTheory.Functor Ctx D) {Z : D} (h : F.obj (M.ext A) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map σ) (CategoryTheory.CategoryStruct.comp (F.map (M.sec A a a_tp)) h) = CategoryTheory.CategoryStruct.comp (F.map (M.sec (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯)) (CategoryTheory.CategoryStruct.comp (F.map (M.substWk σ A)) h)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A a a_tp)) (M.wk A x) = x

source

@[simp]

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

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A a a_tp)) (CategoryTheory.CategoryStruct.comp (M.wk A x) h) = CategoryTheory.CategoryStruct.comp x h

Polynomial functor on `tp` #

Specializations of results from the Poly package to natural models.

source

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

CategoryTheory.UvPoly M.Tm M.Ty

Equations

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

Instances For

source

@[simp]

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

M.uvPolyTp.p = M.tp

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} :

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

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

Equations

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

Instances For

source

@[simp]

theorem NaturalModelBase.Ptp_equiv_symm_apply_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (a✝ : (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) × (CategoryTheory.yoneda.obj (M.ext A) ⟶ X)) (X✝ : Ctxᵒᵖ) (a✝¹ : (CategoryTheory.Over.mk { pt := CategoryTheory.yoneda.obj Γ, fst := ((Equiv.sigmaCongrRight fun (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) => (M.pullbackIsoExt x).homCongr (CategoryTheory.Iso.refl X)).symm a✝).fst, snd := ((Equiv.sigmaCongrRight fun (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) => (M.pullbackIsoExt x).homCongr (CategoryTheory.Iso.refl X)).symm a✝).snd }.fst).left.obj X✝) :

(M.Ptp_equiv.symm a✝).app X✝ a✝¹ = ((CategoryTheory.Over.pullback M.tp).rightAdjoint.map (CategoryTheory.overPullbackToStar ((Equiv.sigmaCongrRight fun (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) => (M.pullbackIsoExt x).homCongr (CategoryTheory.Iso.refl X)).symm a✝).fst ((Equiv.sigmaCongrRight fun (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) => (M.pullbackIsoExt x).homCongr (CategoryTheory.Iso.refl X)).symm a✝).snd)).left.app X✝ (((CategoryTheory.ExponentiableMorphism.adj M.tp).unit.app (CategoryTheory.Over.mk ((Equiv.sigmaCongrRight fun (x : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) => (M.pullbackIsoExt x).homCongr (CategoryTheory.Iso.refl X)).symm a✝).fst)).left.app X✝ a✝¹)

source

@[simp]

theorem NaturalModelBase.Ptp_equiv_apply_snd_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (a✝ : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp @ X) (X✝ : Ctxᵒᵖ) (a✝¹ : (CategoryTheory.yoneda.obj (M.ext ((M.uvPolyTp.equiv (CategoryTheory.yoneda.obj Γ) X) a✝).fst)).obj X✝) :

(M.Ptp_equiv a✝).snd.app X✝ a✝¹ = ((M.uvPolyTp.equiv (CategoryTheory.yoneda.obj Γ) X) a✝).snd.app X✝ (⋯.isoPullback.hom.app X✝ a✝¹)

source

@[simp]

theorem NaturalModelBase.Ptp_equiv_apply_fst_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (a✝ : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp @ X) (X✝ : Ctxᵒᵖ) (a✝¹ : (CategoryTheory.yoneda.obj Γ).obj X✝) :

(M.Ptp_equiv a✝).fst.app X✝ a✝¹ = (M.uvPolyTp.fstProj X).app X✝ (a✝.app X✝ a✝¹)

source

def NaturalModelBase.PtpEquiv.fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X) :

CategoryTheory.yoneda.obj Γ ⟶ M.Ty

A map (AB : y(Γ) ⟶ M.Ptp.obj X) is equivalent to a pair of maps A : y(Γ) ⟶ M.Ty and B : y(M.ext (fst M AB)) ⟶ X, thought of as a dependent pair A : Type and B : A ⟶ Type. PtpEquiv.fst is the A in this pair.

Equations

NaturalModelBase.PtpEquiv.fst M AB = ((M.uvPolyTp.equiv (CategoryTheory.yoneda.obj Γ) X) AB).fst

Instances For

source

def NaturalModelBase.PtpEquiv.snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X) :

CategoryTheory.yoneda.obj (M.ext (fst M AB)) ⟶ X

A map (AB : y(Γ) ⟶ M.Ptp.obj X) is equivalent to a pair of maps A : y(Γ) ⟶ M.Ty and B : y(M.ext (fst M AB)) ⟶ X, thought of as a dependent pair A : Type and B : A ⟶ Type PtpEquiv.snd is the B in this pair.

Equations

NaturalModelBase.PtpEquiv.snd M AB = CategoryTheory.CategoryStruct.comp (M.pullbackIsoExt (NaturalModelBase.PtpEquiv.fst M AB)).inv ((M.uvPolyTp.equiv (CategoryTheory.yoneda.obj Γ) X) AB).snd

Instances For

source

def NaturalModelBase.PtpEquiv.mk {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.yoneda.obj Γ ⟶ M.Ptp.obj X

A map (AB : y(Γ) ⟶ M.Ptp.obj X) is equivalent to a pair of maps A : y(Γ) ⟶ M.Ty and B : y(M.ext (fst M AB)) ⟶ X, thought of as a dependent pair A : Type and B : A ⟶ Type PtpEquiv.mk constructs such a map AB from such a pair A and B.

Equations

NaturalModelBase.PtpEquiv.mk M A B = M.Ptp_equiv.symm ⟨A, B⟩

Instances For

source

theorem NaturalModelBase.PtpEquiv.fst_naturality_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} :

fst M (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (fst M AB)

source

theorem NaturalModelBase.PtpEquiv.snd_naturality_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} :

snd M (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ (fst M AB))) (snd M AB)

source

theorem NaturalModelBase.Ptp_equiv_naturality_right {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) :

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

source

theorem NaturalModelBase.Ptp_equiv_symm_naturality_right {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.symm ⟨A, x⟩) (M.Ptp.map α) = M.Ptp_equiv.symm ⟨A, CategoryTheory.CategoryStruct.comp x α⟩

source

theorem NaturalModelBase.Ptp_equiv_symm_naturality_right_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.symm ⟨A, x⟩) (CategoryTheory.CategoryStruct.comp (M.Ptp.map α) h) = CategoryTheory.CategoryStruct.comp (M.Ptp_equiv.symm ⟨A, CategoryTheory.CategoryStruct.comp x α⟩) h

Polynomial composition `M.tp ▸ N.tp` #

source

def NaturalModelBase.compDomEquiv.fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

CategoryTheory.yoneda.obj Γ ⟶ M.Tm

Universal property of compDom, decomposition (part 1).

A map ab : y(Γ) ⟶ M.uvPolyTp.compDom N.uvPolyTp is equivalently three maps fst, dependent, snd such that snd_tp. The map fst : y(Γ) ⟶ M.Tm is the (a : A) in (a : A) × (b : B a).

Equations

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

Instances For

source

def NaturalModelBase.compDomEquiv.dependent {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

CategoryTheory.yoneda.obj (M.ext (CategoryTheory.CategoryStruct.comp (fst N ab) M.tp)) ⟶ N.Ty

Universal property of compDom, decomposition (part 2).

A map ab : y(Γ) ⟶ M.uvPolyTp.compDom N.uvPolyTp is equivalently three maps fst, dependent, snd such that snd_tp. The map dependent : y(M.ext (fst N ab ≫ M.tp)) ⟶ M.Ty is the B : A ⟶ Type in (a : A) × (b : B a). Here A is implicit, derived by the typing of fst, or (a : A).

Equations

NaturalModelBase.compDomEquiv.dependent N ab = sorry

Instances For

source

def NaturalModelBase.compDomEquiv.snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

CategoryTheory.yoneda.obj Γ ⟶ N.Tm

Universal property of compDom, decomposition (part 3).

A map ab : y(Γ) ⟶ M.uvPolyTp.compDom N.uvPolyTp is equivalently three maps fst, dependent, snd such that snd_tp. The map snd : y(Γ) ⟶ M.Tm is the (b : B a) in (a : A) × (b : B a).

Equations

NaturalModelBase.compDomEquiv.snd N ab = sorry

Instances For

source

theorem NaturalModelBase.compDomEquiv.snd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

CategoryTheory.CategoryStruct.comp (snd N ab) N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec (CategoryTheory.CategoryStruct.comp (fst N ab) M.tp) (fst N ab) ⋯)) (dependent N ab)

Universal property of compDom, decomposition (part 4).

A map ab : y(Γ) ⟶ M.uvPolyTp.compDom N.uvPolyTp is equivalently three maps fst, dependent, snd such that snd_tp. The equation snd_tp says that the type of b : B a agrees with the expression for B a obtained solely from dependent, or B : A ⟶ Type.

source

def NaturalModelBase.compDomEquiv.mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (B : CategoryTheory.yoneda.obj (M.ext (CategoryTheory.CategoryStruct.comp α M.tp)) ⟶ N.Ty) (β : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (h : CategoryTheory.CategoryStruct.comp β N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec (CategoryTheory.CategoryStruct.comp α M.tp) α ⋯)) B) :

CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp

Universal property of compDom, constructing a map into compDom.

Equations

NaturalModelBase.compDomEquiv.mk N α B β h = sorry

Instances For

source

theorem NaturalModelBase.compDomEquiv.fst_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

CategoryTheory.CategoryStruct.comp (fst N ab) M.tp = PtpEquiv.fst M (CategoryTheory.CategoryStruct.comp ab (M.uvPolyTp.comp N.uvPolyTp).p)

Computation of comp (part 1).

fst_tp is (part 1) of the computation that (α, B, β, h) Γ ⟶ compDom \ | \ | comp (α ≫ tp, B) | \ V > P_tp Ty Namely the first projection α ≫ tp agrees.

source

theorem NaturalModelBase.compDomEquiv.dependent_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : NaturalModelBase Ctx} (N : NaturalModelBase Ctx) {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) :

dependent N ab = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (CategoryTheory.eqToHom ⋯)) (PtpEquiv.snd M (CategoryTheory.CategoryStruct.comp ab (M.uvPolyTp.comp N.uvPolyTp).p))

Computation of comp (part 2).

dependent_eq is (part 2) of the computation that (α, B, β, h) Γ ⟶ compDom \ | \ | comp (α ≫ tp, B) | \ V > P_tp Ty Namely the second projection B agrees.

source