structure NaturalModel.Universe (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

def NaturalModel.Universe.pullbackIsoExt {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.pullbackIsoExt_hom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) : (M.pullbackIsoExt A).hom = ⋯.isoPullback.inv

@[simp]

theorem NaturalModel.Universe.pullbackIsoExt_inv {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) : (M.pullbackIsoExt A).inv = ⋯.isoPullback.hom

Pullback of representable natural transformation

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

Pull a natural model back along a type.

Equations

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

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

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

Γ.A -.-.- var -.-,-> E ------ toTm ------> Tm | | | | | | M.disp π tp | | | V V V Γ ------- A -------> U ------ toTy ------> Ty

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

Equations

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

Substitutions

def NaturalModel.Universe.substCons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

------ Δ ------ t --------¬ | ↓ substCons ↓ | M.ext A ---var A---> M.Tm | | | σ | | | disp A M.tp | | | | V V ---> Γ ------ A -----> M.Ty

Equations

• M.substCons σ A t t_tp = CategoryTheory.Yoneda.fullyFaithful.preimage (⋯.lift t (CategoryTheory.yoneda.map σ) t_tp)

@[simp]

theorem NaturalModel.Universe.substCons_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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) = σ

@[simp]

theorem NaturalModel.Universe.substCons_disp_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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.16142} [CategoryTheory.Category.{_uniq.16141, _uniq.16142} D] (F : CategoryTheory.Functor Ctx D) : CategoryTheory.CategoryStruct.comp (F.map (M.substCons σ A t tTp)) (F.map (M.disp A)) = F.map σ

@[simp]

theorem NaturalModel.Universe.substCons_disp_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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.16142} [CategoryTheory.Category.{_uniq.16141, _uniq.16142} 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

@[simp]

theorem NaturalModel.Universe.substCons_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.substCons_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.substCons_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.comp_substCons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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 τ (M.substCons σ A t aTp) = M.substCons (CategoryTheory.CategoryStruct.comp τ σ) A (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map τ) t) ⋯

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

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

Equations

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

def NaturalModel.Universe.substSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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)

theorem NaturalModel.Universe.substSnd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.var_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) : CategoryTheory.CategoryStruct.comp (M.var A) M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp A)) A

@[simp]

theorem NaturalModel.Universe.var_tp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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 (CategoryTheory.yoneda.map (M.disp A)) (CategoryTheory.CategoryStruct.comp A h)

def NaturalModel.Universe.substWk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty := CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A' := by rfl) : M.ext A' ⟶ M.ext A

Weaken a substitution.

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

Equations

• M.substWk σ A A' eq = M.substCons (CategoryTheory.CategoryStruct.comp (M.disp A') σ) A (M.var A') ⋯

theorem NaturalModel.Universe.substWk_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (M.disp A) = CategoryTheory.CategoryStruct.comp (M.disp A') σ

theorem NaturalModel.Universe.substWk_disp_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') {D : Type _uniq.31229} [CategoryTheory.Category.{_uniq.31228, _uniq.31229} D] (F : CategoryTheory.Functor Ctx D) : CategoryTheory.CategoryStruct.comp (F.map (M.substWk σ A A' eq)) (F.map (M.disp A)) = CategoryTheory.CategoryStruct.comp (F.map (M.disp A')) (F.map σ)

theorem NaturalModel.Universe.substWk_disp_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') {D : Type _uniq.31229} [CategoryTheory.Category.{_uniq.31228, _uniq.31229} D] (F : CategoryTheory.Functor Ctx D) {Z : D} (h : F.obj Γ ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (M.substWk σ A A' eq)) (CategoryTheory.CategoryStruct.comp (F.map (M.disp A)) h) = CategoryTheory.CategoryStruct.comp (F.map (M.disp A')) (CategoryTheory.CategoryStruct.comp (F.map σ) h)

theorem NaturalModel.Universe.substWk_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') {Z : Ctx} (h : Γ ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = CategoryTheory.CategoryStruct.comp (M.disp A') (CategoryTheory.CategoryStruct.comp σ h)

@[simp]

theorem NaturalModel.Universe.substWk_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A A' eq)) (M.var A) = M.var A'

@[simp]

theorem NaturalModel.Universe.substWk_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (A' : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A') {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A A' eq)) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp (M.var A') h

def NaturalModel.Universe.sec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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.

===== Γ ------ a --------¬ ‖ ↓ sec V ‖ M.ext A -----------> M.Tm ‖ | | ‖ | | ‖ disp A M.tp ‖ | | ‖ V V ===== Γ ------ A -----> M.Ty

Equations

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

@[simp]

theorem NaturalModel.Universe.sec_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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 Γ

@[simp]

theorem NaturalModel.Universe.sec_disp_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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.37191} [CategoryTheory.Category.{_uniq.37190, _uniq.37191} 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 Γ)

@[simp]

theorem NaturalModel.Universe.sec_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.sec_disp_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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.37191} [CategoryTheory.Category.{_uniq.37190, _uniq.37191} 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

@[simp]

theorem NaturalModel.Universe.sec_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

@[simp]

theorem NaturalModel.Universe.sec_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

theorem NaturalModel.Universe.comp_sec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (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 σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯) (M.substWk σ A σA eq)

theorem NaturalModel.Universe.comp_sec_functor_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (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 σ) (F.map (M.sec A a a_tp)) = CategoryTheory.CategoryStruct.comp (F.map (M.sec σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯)) (F.map (M.substWk σ A σA eq))

theorem NaturalModel.Universe.comp_sec_functor_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (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 (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 σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯)) (CategoryTheory.CategoryStruct.comp (F.map (M.substWk σ A σA eq)) h)

theorem NaturalModel.Universe.comp_sec_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (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 σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯) (CategoryTheory.CategoryStruct.comp (M.substWk σ A σA eq) h)

Polynomial functor on tp

Specializations of results from the Poly package to natural models.

def NaturalModel.Universe.uvPolyTp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : CategoryTheory.UvPoly M.Tm M.Ty

Equations

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

@[simp]

theorem NaturalModel.Universe.uvPolyTp_p {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : M.uvPolyTp.p = M.tp

def NaturalModel.Universe.Ptp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : CategoryTheory.Functor (CategoryTheory.Psh Ctx) (CategoryTheory.Psh Ctx)

Equations

• M.Ptp = M.uvPolyTp.functor

def NaturalModel.Universe.PtpEquiv.fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

• NaturalModel.Universe.PtpEquiv.fst M AB = CategoryTheory.UvPoly.Equiv.fst M.uvPolyTp X AB

def NaturalModel.Universe.PtpEquiv.snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty := fst M AB) (eq : fst M AB = A := by rfl) : CategoryTheory.yoneda.obj (M.ext A) ⟶ 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

• NaturalModel.Universe.PtpEquiv.snd M AB A eq = CategoryTheory.UvPoly.Equiv.snd' M.uvPolyTp X AB ⋯

def NaturalModel.Universe.PtpEquiv.mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

• NaturalModel.Universe.PtpEquiv.mk M A B = CategoryTheory.UvPoly.Equiv.mk' M.uvPolyTp X A ⋯ B

@[simp]

theorem NaturalModel.Universe.PtpEquiv.fst_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : fst M (mk M A B) = A

@[simp]

theorem NaturalModel.Universe.PtpEquiv.snd_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : snd M (mk M A B) A ⋯ = B

theorem NaturalModel.Universe.PtpEquiv.fst_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {Δ : Ctx} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) : fst M (CategoryTheory.CategoryStruct.comp σ AB) = CategoryTheory.CategoryStruct.comp σ (fst M AB)

theorem NaturalModel.Universe.PtpEquiv.fst_comp_right {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} {Y : CategoryTheory.Psh Ctx} (σ : X ⟶ Y) : fst M (CategoryTheory.CategoryStruct.comp AB (M.Ptp.map σ)) = fst M AB

theorem NaturalModel.Universe.PtpEquiv.snd_comp_right {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} {Y : CategoryTheory.Psh Ctx} (σ : X ⟶ Y) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : fst M AB = A) : snd M (CategoryTheory.CategoryStruct.comp AB (M.Ptp.map σ)) A ⋯ = CategoryTheory.CategoryStruct.comp (snd M AB A eq) σ

theorem NaturalModel.Universe.PtpEquiv.snd_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eqA : fst M AB = A) {σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty} (eqσ : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) : snd M (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) σA ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A σA eqσ)) (snd M AB A eqA)

theorem NaturalModel.Universe.PtpEquiv.mk_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Δ Γ : Ctx} (M : Universe Ctx) (σ : Δ ⟶ Γ) {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (mk M A B) = mk M σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A σA eq)) B)

theorem NaturalModel.Universe.PtpEquiv.mk_comp_right {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {Γ : Ctx} (M : Universe Ctx) {X Y : CategoryTheory.Psh Ctx} (σ : X ⟶ Y) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (mk M A B) (M.Ptp.map σ) = mk M A (CategoryTheory.CategoryStruct.comp B σ)

theorem NaturalModel.Universe.PtpEquiv.ext {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {AB AB' : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty := fst M AB) (eq : fst M AB = A := by rfl) (h1 : fst M AB = fst M AB') (h2 : snd M AB A eq = snd M AB' A ⋯) : AB = AB'

theorem NaturalModel.Universe.PtpEquiv.eta {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ M.Ptp.obj X) : mk M (fst M AB) (snd M AB (fst M AB) ⋯) = AB

theorem NaturalModel.Universe.PtpEquiv.mk_map {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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 (mk M A x) (M.Ptp.map α) = mk M A (CategoryTheory.CategoryStruct.comp x α)

theorem NaturalModel.Universe.PtpEquiv.mk_map_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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 (mk M A x) (CategoryTheory.CategoryStruct.comp (M.Ptp.map α) h) = CategoryTheory.CategoryStruct.comp (mk M A (CategoryTheory.CategoryStruct.comp x α)) h

Polynomial composition M.tp ▸ N.tp

def NaturalModel.Universe.compDomEquiv.fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe 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 fst_tp and 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.

theorem NaturalModel.Universe.compDomEquiv.fst_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) : CategoryTheory.CategoryStruct.comp (fst ab) M.tp = PtpEquiv.fst M (CategoryTheory.CategoryStruct.comp ab (M.uvPolyTp.compP N.uvPolyTp))

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.

theorem NaturalModel.Universe.compDomEquiv.comp_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ Δ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) : CategoryTheory.CategoryStruct.comp σ (fst ab) = fst (CategoryTheory.CategoryStruct.comp σ ab)

def NaturalModel.Universe.compDomEquiv.dependent {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty := CategoryTheory.CategoryStruct.comp (fst ab) M.tp) (eq : CategoryTheory.CategoryStruct.comp (fst ab) M.tp = A := by rfl) : CategoryTheory.yoneda.obj (M.ext A) ⟶ 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 fst_tp and 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

• NaturalModel.Universe.compDomEquiv.dependent ab A eq = NaturalModel.Universe.PtpEquiv.snd M (CategoryTheory.CategoryStruct.comp ab (M.uvPolyTp.compP N.uvPolyTp)) A ⋯

theorem NaturalModel.Universe.compDomEquiv.comp_dependent {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq1 : CategoryTheory.CategoryStruct.comp (fst ab) M.tp = A) {σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty} (eq2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A σA eq2)) (dependent ab A eq1) = dependent (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ab) σA ⋯

def NaturalModel.Universe.compDomEquiv.snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe 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 fst_tp and snd_tp. The map snd : y(Γ) ⟶ M.Tm is the (b : B a) in (a : A) × (b : B a).

Equations

• NaturalModel.Universe.compDomEquiv.snd ab = CategoryTheory.CategoryStruct.comp ab (CategoryTheory.Limits.pullback.fst N.tp (CategoryTheory.UvPoly.PartialProduct.fan M.uvPolyTp N.Ty).snd)

theorem NaturalModel.Universe.compDomEquiv.comp_snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ Δ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) : CategoryTheory.CategoryStruct.comp σ (snd ab) = snd (CategoryTheory.CategoryStruct.comp σ ab)

theorem NaturalModel.Universe.compDomEquiv.snd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp (fst ab) M.tp = A) : CategoryTheory.CategoryStruct.comp (snd ab) N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A (fst ab) eq)) (dependent ab A eq)

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 fst_tp and 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.

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

Universal property of compDom, constructing a map into compDom.

Equations

• NaturalModel.Universe.compDomEquiv.mk α eq B β h = CategoryTheory.Limits.pullback.lift β (CategoryTheory.Limits.pullback.lift (NaturalModel.Universe.PtpEquiv.mk M A B) α ⋯) ⋯

@[simp]

theorem NaturalModel.Universe.compDomEquiv.fst_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp α M.tp = A) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Ty) (β : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (h : CategoryTheory.CategoryStruct.comp β N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A α eq)) B) : fst (mk α eq B β h) = α

@[simp]

theorem NaturalModel.Universe.compDomEquiv.dependent_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp α M.tp = A) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Ty) (β : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (h : CategoryTheory.CategoryStruct.comp β N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A α eq)) B) : dependent (mk α eq B β h) A ⋯ = B

@[simp]

theorem NaturalModel.Universe.compDomEquiv.snd_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp α M.tp = A) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Ty) (β : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (h : CategoryTheory.CategoryStruct.comp β N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A α eq)) B) : snd (mk α eq B β h) = β

theorem NaturalModel.Universe.compDomEquiv.ext {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} {ab₁ ab₂ : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp} {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp (fst ab₁) M.tp = A) (h1 : fst ab₁ = fst ab₂) (h2 : dependent ab₁ A eq = dependent ab₂ A ⋯) (h3 : snd ab₁ = snd ab₂) : ab₁ = ab₂

theorem NaturalModel.Universe.compDomEquiv.comp_mk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ Δ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (e1 : CategoryTheory.CategoryStruct.comp α M.tp = A) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ N.Ty) (β : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (e2 : CategoryTheory.CategoryStruct.comp β N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.sec A α e1)) B) (σ : Δ ⟶ Γ) {σA : CategoryTheory.yoneda.obj Δ ⟶ M.Ty} (e3 : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (mk α e1 B β e2) = mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) α) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ A σA e3)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) β) ⋯

theorem NaturalModel.Universe.compDomEquiv.eta {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) {A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty} (eq : CategoryTheory.CategoryStruct.comp (fst ab) M.tp = A) : mk (fst ab) eq (dependent ab A eq) (snd ab) ⋯ = ab

Pi and Sigma types

structure NaturalModel.Universe.Pi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe 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

structure NaturalModel.Universe.Sigma {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : Type u

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

structure NaturalModel.Universe.IdIntro {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : Type (u + 1)

Universe.IdIntro consists of the following commutative square refl M.Tm ------> M.Tm | | | | diag M.tp | | | | V V k --------> M.Ty Id

where K (for "Kernel" of tp) is a chosen pullback for the square k1 k ---------> Tm | | | | k2 | tp | | V V Tm ----------> Ty tp and diag denotes the diagonal into the pullback K.

We require a choice of pullback because, although all pullbacks exist in presheaf categories, when constructing a model it is convenient to know that k is some specific construction on-the-nose.

• k : CategoryTheory.Psh Ctx
• k1 : self.k ⟶ M.Tm
• k2 : self.k ⟶ M.Tm
• isKernelPair : CategoryTheory.IsKernelPair M.tp self.k1 self.k2
• Id : self.k ⟶ M.Ty
• refl : M.Tm ⟶ M.Tm
• refl_tp : CategoryTheory.CategoryStruct.comp self.refl M.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.lift ⋯ (CategoryTheory.CategoryStruct.id M.Tm) (CategoryTheory.CategoryStruct.id M.Tm) ⋯) self.Id

def NaturalModel.Universe.IdIntro.mkId {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a0 a1 : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (a0_tp_eq_a1_tp : CategoryTheory.CategoryStruct.comp a0 M.tp = CategoryTheory.CategoryStruct.comp a1 M.tp) : CategoryTheory.yoneda.obj Γ ⟶ M.Ty

The introduction rule for identity types. To minimize the number of arguments, we infer the type from the terms.

Equations

• idIntro.mkId a0 a1 a0_tp_eq_a1_tp = CategoryTheory.CategoryStruct.comp (⋯.lift a1 a0 ⋯) idIntro.Id

theorem NaturalModel.Universe.IdIntro.comp_mkId {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (a0 a1 : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (eq : CategoryTheory.CategoryStruct.comp a0 M.tp = CategoryTheory.CategoryStruct.comp a1 M.tp) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (idIntro.mkId a0 a1 eq) = idIntro.mkId (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a1) ⋯

def NaturalModel.Universe.IdIntro.mkRefl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.yoneda.obj Γ ⟶ M.Tm

Equations

• idIntro.mkRefl a = CategoryTheory.CategoryStruct.comp a idIntro.refl

theorem NaturalModel.Universe.IdIntro.comp_mkRefl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (idIntro.mkRefl a) = idIntro.mkRefl (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a)

@[simp]

theorem NaturalModel.Universe.IdIntro.mkRefl_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (idIntro.mkRefl a) M.tp = idIntro.mkId a a ⋯

def NaturalModel.Universe.IdIntro.motiveCtx {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : Ctx

The context appearing in the motive for identity elimination J Γ ⊢ A Γ ⊢ a : A Γ.(x:A).(h:Id(A,a,x)) ⊢ M ...

Equations

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

def NaturalModel.Universe.IdIntro.motiveSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : idIntro.motiveCtx (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⟶ idIntro.motiveCtx a

Equations

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

def NaturalModel.Universe.IdIntro.reflSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : Γ ⟶ idIntro.motiveCtx a

The substitution (a,refl) appearing in identity elimination J (a,refl) : y(Γ) ⟶ y(Γ.(x:A).(h:Id(A,a,x))) so that we can write Γ ⊢ r : M(a,refl)

Equations

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

theorem NaturalModel.Universe.IdIntro.comp_reflSubst' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (CategoryTheory.yoneda.map (idIntro.reflSubst a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (idIntro.reflSubst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a))) (CategoryTheory.yoneda.map (idIntro.motiveSubst σ a))

theorem NaturalModel.Universe.IdIntro.comp_reflSubst'_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : CategoryTheory.yoneda.obj (idIntro.motiveCtx a) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (idIntro.reflSubst a)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (idIntro.reflSubst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (idIntro.motiveSubst σ a)) h)

@[simp]

theorem NaturalModel.Universe.IdIntro.comp_reflSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {Δ : Ctx} (σ : Δ ⟶ Γ) : CategoryTheory.CategoryStruct.comp (idIntro.reflSubst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a)) (idIntro.motiveSubst σ a) = CategoryTheory.CategoryStruct.comp σ (idIntro.reflSubst a)

theorem NaturalModel.Universe.IdIntro.comp_reflSubst_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (idIntro : M.IdIntro) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {Δ : Ctx} (σ : Δ ⟶ Γ) {Z : Ctx} (h : idIntro.motiveCtx a ⟶ Z) : CategoryTheory.CategoryStruct.comp (idIntro.reflSubst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a)) (CategoryTheory.CategoryStruct.comp (idIntro.motiveSubst σ a) h) = CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (idIntro.reflSubst a) h)

def NaturalModel.Universe.IdIntro.toK {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {Γ : Ctx} (ii : M.IdIntro) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.yoneda.obj (M.ext (CategoryTheory.CategoryStruct.comp a M.tp)) ⟶ ii.k

Equations

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

theorem NaturalModel.Universe.IdIntro.toK_comp_k1 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {Γ : Ctx} (ii : M.IdIntro) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (ii.toK a) ii.k1 = M.var (CategoryTheory.CategoryStruct.comp a M.tp)

theorem NaturalModel.Universe.IdIntro.ext_a_tp_isPullback {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {Γ : Ctx} (ii : M.IdIntro) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.IsPullback (ii.toK a) (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp))) ii.k2 a

structure NaturalModel.Universe.Id' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) (i : M.IdIntro) (N : Universe Ctx) : Type u

The full structure interpreting the natural model semantics for identity types requires an IdIntro and an elimination rule j which satisfies a typing rule j_tp and a β-rule reflSubst_j. There is an equivalent formulation of these extra conditions later in Id1 that uses the language of polynomial endofunctors.

Note that the universe/model N for the motive C is different from the universe M that the identity type lives in.

• j {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (i.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.reflSubst a)) C) : CategoryTheory.yoneda.obj (i.motiveCtx a) ⟶ N.Tm
• j_tp {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (i.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (self.j a C r r_tp) N.tp = C
• comp_j {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (i.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.motiveSubst σ a)) (self.j a C r r_tp) = self.j (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.motiveSubst σ a)) C) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) r) ⋯
• reflSubst_j {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (i.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (i.reflSubst a)) (self.j a C r r_tp) = r

def NaturalModel.Universe.Id'.endPtSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {Γ : Ctx} (a b : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b M.tp = CategoryTheory.CategoryStruct.comp a M.tp) (h : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (h_tp : CategoryTheory.CategoryStruct.comp h M.tp = CategoryTheory.CategoryStruct.comp (⋯.lift b a ⋯) ii.Id) : Γ ⟶ ii.motiveCtx a

Equations

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

def NaturalModel.Universe.Id'.mkJ {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} (i : M.Id' ii N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) (b : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b M.tp = CategoryTheory.CategoryStruct.comp a M.tp) (h : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (h_tp : CategoryTheory.CategoryStruct.comp h M.tp = CategoryTheory.CategoryStruct.comp (⋯.lift b a ⋯) ii.Id) : CategoryTheory.yoneda.obj Γ ⟶ N.Tm

The elimination rule for identity types, now with the parameters as explicit terms. Γ ⊢ A is the type with a term Γ ⊢ a : A. Γ (y : A) (p : Id(A,a,y)) ⊢ C is the motive for the elimination. Γ ⊢ b : A is a second term in A and Γ ⊢ h : Id(A,a,b) is a path from a to b. Then Γ ⊢ mkJ' : C [b/y,h/p] is a term of the motive with b and h substituted

Equations

• i.mkJ a C r r_tp b b_tp h h_tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (NaturalModel.Universe.Id'.endPtSubst a b b_tp h h_tp)) (i.j a C r r_tp)

theorem NaturalModel.Universe.Id'.mkJ_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} (i : M.Id' ii N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) (b : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b M.tp = CategoryTheory.CategoryStruct.comp a M.tp) (h : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (h_tp : CategoryTheory.CategoryStruct.comp h M.tp = CategoryTheory.CategoryStruct.comp (⋯.lift b a ⋯) ii.Id) : CategoryTheory.CategoryStruct.comp (i.mkJ a C r r_tp b b_tp h h_tp) N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (endPtSubst a b b_tp h h_tp)) C

Typing for elimination rule J

theorem NaturalModel.Universe.Id'.mkJ_refl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} (i : M.Id' ii N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : i.mkJ a C r r_tp a ⋯ (ii.mkRefl a) ⋯ = r

β rule for identity types. Substituting J with refl gives the user-supplied value r

structure NaturalModel.Universe.IdElimBase {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} (ii : M.IdIntro) : Type (u + 1)

UniverseBase.IdElimBase extends the structure UniverseBase.IdIntro with a chosen pullback of Id i1 i --------> M.Tm | | | | i2 M.tp | | V V k --------> M.Ty Id

Again, we always have a pullback, but when we construct a natural model, this may not be definitionally equal to the pullbacks we construct, for example using context extension.

• i : CategoryTheory.Psh Ctx
• i1 : self.i ⟶ M.Tm
• i2 : self.i ⟶ ii.k
• i_isPullback : CategoryTheory.IsPullback self.i1 self.i2 M.tp ii.Id

def NaturalModel.Universe.IdElimBase.comparison {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : M.Tm ⟶ ie.i

The comparison map M.tm ⟶ i induced by the pullback universal property of i.

      refl

M.Tm ---------> i1 | i --------> M.Tm | | | diag | | | i2 M.tp | | | | V V V k --------> M.Ty Id

Equations

• ie.comparison = ⋯.lift ii.refl (CategoryTheory.IsPullback.lift ⋯ (CategoryTheory.CategoryStruct.id M.Tm) (CategoryTheory.CategoryStruct.id M.Tm) ⋯) ⋯

@[simp]

theorem NaturalModel.Universe.IdElimBase.comparison_comp_i1 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : CategoryTheory.CategoryStruct.comp ie.comparison ie.i1 = ii.refl

@[simp]

theorem NaturalModel.Universe.IdElimBase.comparison_comp_i2_comp_k1 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : CategoryTheory.CategoryStruct.comp ie.comparison (CategoryTheory.CategoryStruct.comp ie.i2 ii.k1) = CategoryTheory.CategoryStruct.id M.Tm

theorem NaturalModel.Universe.IdElimBase.comparison_comp_i2_comp_k1_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Z : CategoryTheory.Psh Ctx} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp ie.comparison (CategoryTheory.CategoryStruct.comp ie.i2 (CategoryTheory.CategoryStruct.comp ii.k1 h)) = h

@[simp]

theorem NaturalModel.Universe.IdElimBase.comparison_comp_i2_comp_k2 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : CategoryTheory.CategoryStruct.comp ie.comparison (CategoryTheory.CategoryStruct.comp ie.i2 ii.k2) = CategoryTheory.CategoryStruct.id M.Tm

theorem NaturalModel.Universe.IdElimBase.comparison_comp_i2_comp_k2_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Z : CategoryTheory.Psh Ctx} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp ie.comparison (CategoryTheory.CategoryStruct.comp ie.i2 (CategoryTheory.CategoryStruct.comp ii.k2 h)) = h

def NaturalModel.Universe.IdElimBase.iUvPoly {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : CategoryTheory.UvPoly ie.i M.Tm

i over Tm can be informally thought of as the context extension (A : Ty).(a b : A).(p : Id(a,b)) ->> (A : Ty) (a : A) which is defined by the composition of (maps informally thought of as) context extensions (A : Ty).(a b : A).(p : Id(a,b)) ->> (A : Ty).(a b : A) ->> (A : Ty).(a : A) This is the signature for a polynomial functor iUvPoly on the presheaf category Psh Ctx.

Equations

• ie.iUvPoly = { p := CategoryTheory.CategoryStruct.comp ie.i2 ii.k2, exp := ⋯ }

@[simp]

theorem NaturalModel.Universe.IdElimBase.iUvPoly_p {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : ie.iUvPoly.p = CategoryTheory.CategoryStruct.comp ie.i2 ii.k2

@[reducible, inline]

abbrev NaturalModel.Universe.IdElimBase.iFunctor {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : CategoryTheory.Functor (CategoryTheory.Psh Ctx) (CategoryTheory.Psh Ctx)

The functor part of the polynomial endofunctor iOverUvPoly

Equations

• ie.iFunctor = ie.iUvPoly.functor

def NaturalModel.Universe.IdElimBase.verticalNatTrans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) : ie.iFunctor ⟶ (CategoryTheory.UvPoly.id M.Tm).functor

Consider the comparison map comparison : Tm ⟶ i in the slice over Tm. Then the contravariant action UVPoly.verticalNatTrans of taking UvPoly on a slice results in a natural transformation P_iOver ⟶ P_(𝟙 Tm) between the polynomial endofunctors iUvPoly and UvPoly.id M.Tm respectively. comparison Tm ----> i \ / 𝟙\ /i2 ≫ k2 \ / VV Tm

Equations

• ie.verticalNatTrans = (CategoryTheory.UvPoly.id M.Tm).verticalNatTrans ie.iUvPoly ie.comparison ⋯

theorem NaturalModel.Universe.IdElimBase.reflCase_aux {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.obj Γ)) a a (CategoryTheory.UvPoly.id M.Tm).p

def NaturalModel.Universe.IdElimBase.reflCase {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm

The variable r witnesses the motive for the case refl, This gives a map (a,r) : Γ ⟶ P_𝟙Tm Tm ≅ Tm × Tm where

    fst ≫ r
N.Tm <--   Γ  --------> Tm
    <      ‖            ‖
     \     ‖   (pb)     ‖ 𝟙_Tm
    r \    ‖            ‖
       \   ‖            ‖
        \  Γ  --------> Tm
                 a

Equations

• NaturalModel.Universe.IdElimBase.reflCase a r = CategoryTheory.UvPoly.Equiv.mk' (CategoryTheory.UvPoly.id M.Tm) N.Tm a ⋯ r

theorem NaturalModel.Universe.IdElimBase.toK_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {Δ : Ctx} (σ : Δ ⟶ Γ) : ii.toK (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.substWk σ (CategoryTheory.CategoryStruct.comp a M.tp) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (CategoryTheory.CategoryStruct.comp a M.tp)) ⋯)) (ii.toK a)

def NaturalModel.Universe.IdElimBase.toI {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ ie.i

Equations

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

theorem NaturalModel.Universe.IdElimBase.toI_comp_i1 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (ie.toI a) ie.i1 = M.var (ii.mkId (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp))) a) (M.var (CategoryTheory.CategoryStruct.comp a M.tp)) ⋯)

theorem NaturalModel.Universe.IdElimBase.toI_comp_i2 {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.CategoryStruct.comp (ie.toI a) ie.i2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (ii.mkId (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp))) a) (M.var (CategoryTheory.CategoryStruct.comp a M.tp)) ⋯))) (ii.toK a)

theorem NaturalModel.Universe.IdElimBase.toI_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) {Δ : Ctx} (σ : Δ ⟶ Γ) : ie.toI (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ a)) (ie.toI a)

theorem NaturalModel.Universe.IdElimBase.motiveCtx_isPullback {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.IsPullback (ie.toI a) (CategoryTheory.yoneda.map (M.disp (ii.mkId (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp))) a) (M.var (CategoryTheory.CategoryStruct.comp a M.tp)) ⋯))) ie.i2 (ii.toK a)

theorem NaturalModel.Universe.IdElimBase.motiveCtx_isPullback' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.IsPullback (ie.toI a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (ii.mkId (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp))) a) (M.var (CategoryTheory.CategoryStruct.comp a M.tp)) ⋯))) (CategoryTheory.yoneda.map (M.disp (CategoryTheory.CategoryStruct.comp a M.tp)))) ie.iUvPoly.p a

def NaturalModel.Universe.IdElimBase.equivMk {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (x : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ X) : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X

Equations

• ie.equivMk a x = CategoryTheory.UvPoly.Equiv.mk' ie.iUvPoly X a ⋯ x

def NaturalModel.Universe.IdElimBase.equivFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) : CategoryTheory.yoneda.obj Γ ⟶ M.Tm

Equations

• ie.equivFst pair = CategoryTheory.UvPoly.Equiv.fst ie.iUvPoly X pair

theorem NaturalModel.Universe.IdElimBase.equivFst_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) {Δ : Ctx} (σ : Δ ⟶ Γ) : ie.equivFst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (ie.equivFst pair)

def NaturalModel.Universe.IdElimBase.equivSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) : CategoryTheory.yoneda.obj (ii.motiveCtx (ie.equivFst pair)) ⟶ X

Equations

• ie.equivSnd pair = CategoryTheory.UvPoly.Equiv.snd' ie.iUvPoly X pair ⋯

theorem NaturalModel.Universe.IdElimBase.equivSnd_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) {Δ : Ctx} (σ : Δ ⟶ Γ) : ie.equivSnd (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) pair) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ (ie.equivFst pair))) (ie.equivSnd pair)

theorem NaturalModel.Universe.IdElimBase.equivFst_verticalNatTrans_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) : ie.equivFst pair = CategoryTheory.UvPoly.Equiv.fst (CategoryTheory.UvPoly.id M.Tm) X (CategoryTheory.CategoryStruct.comp pair (ie.verticalNatTrans.app X))

theorem NaturalModel.Universe.IdElimBase.equivSnd_verticalNatTrans_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (pair : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj X) : CategoryTheory.UvPoly.Equiv.snd' (CategoryTheory.UvPoly.id M.Tm) X (CategoryTheory.CategoryStruct.comp pair (ie.verticalNatTrans.app X)) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst (ie.equivFst pair))) (ie.equivSnd pair)

theorem NaturalModel.Universe.IdElimBase.equivMk_comp_verticalNatTrans_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (x : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ X) : CategoryTheory.CategoryStruct.comp (ie.equivMk a x) (ie.verticalNatTrans.app X) = CategoryTheory.UvPoly.Equiv.mk' (CategoryTheory.UvPoly.id M.Tm) X a ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) x)

structure NaturalModel.Universe.Id {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) (N : Universe Ctx) : Type (u + 1)

In the high-tech formulation by Richard Garner and Steve Awodey: The full structure interpreting the natural model semantics for identity types requires an IdIntro, (and IdElimBase which can be generated by pullback in the presheaf category,) and that the following commutative square generated by IdBaseComparison.verticalNatTrans is a weak pullback.

  verticalNatTrans.app Tm
iFunctor Tm --------> P_𝟙Tm Tm
  |                    |
  |                    |
iFunctor tp           P_𝟙Tm tp
  |                    |
  |                    |
  V                    V
iFunctor Ty --------> P_𝟙Tm Ty
  verticalNatTrans.app Ty

This can be thought of as saying the following. Fix A : Ty and a : A - we are working in the slice over M.Tm. For any context Γ, any map (a, r) : Γ → P_𝟙Tm Tm and (a, C) : Γ ⟶ iFunctor Ty such that r ≫ M.tp = C[x/y, refl_x/p], there is a map (a,c) : Γ ⟶ iFunctor Tm such that c ≫ M.tp = C and c[a/y, refl_a/p] = r. Here we are thinking Γ (y : A) (p : A) ⊢ C : Ty Γ ⊢ r : C[a/y, refl_a/p] Γ (y : A) (p : A) ⊢ c : Ty This witnesses the elimination principle for identity types since we can take J (y.p.C;x.r) := c.

• weakPullback : CategoryTheory.WeakPullback (ie.verticalNatTrans.app N.Tm) (ie.iFunctor.map N.tp) ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) (ie.verticalNatTrans.app N.Ty)

theorem NaturalModel.Universe.Id.reflCase_aux {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.obj Γ)) a a (CategoryTheory.UvPoly.id M.Tm).p

def NaturalModel.Universe.Id.reflCase {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm

The variable r witnesses the motive for the case refl, This gives a map (a,r) : Γ ⟶ P_𝟙Tm Tm ≅ Tm × Tm where

    fst ≫ r
Tm <--   Γ  --------> Tm
  <      ‖            ‖
   \     ‖   (pb)     ‖ 𝟙_Tm
  r \    ‖            ‖
     \   ‖            ‖
      \  Γ  --------> Tm
              a

Equations

• NaturalModel.Universe.Id.reflCase a r = CategoryTheory.UvPoly.Equiv.mk' (CategoryTheory.UvPoly.id M.Tm) N.Tm a ⋯ r

@[reducible, inline]

abbrev NaturalModel.Universe.Id.motive {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} (ie : IdElimBase ii) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty

The variable C is the motive for elimination, This gives a map (a, C) : Γ ⟶ iFunctor Ty

    C
Ty <-- y(motiveCtx) ----> i
             |            |
             |            | i2 ≫ k2
             |            |
             V            V
             Γ  --------> Tm
                  a

Equations

• NaturalModel.Universe.Id.motive ie a C = ie.equivMk a C

theorem NaturalModel.Universe.Id.motive_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (motive ie a C) = motive ie (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ a)) C)

def NaturalModel.Universe.Id.lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Tm

Equations

• i.lift a C r r_tp = i.weakPullback.coherentLift (NaturalModel.Universe.Id.reflCase a r) (NaturalModel.Universe.Id.motive ie a C) ⋯

theorem NaturalModel.Universe.Id.lift_comp_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) {Δ : Ctx} (σ : Δ ⟶ Γ) : i.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ a)) C) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) r) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (i.lift a C r r_tp)

theorem NaturalModel.Universe.Id.equivFst_lift_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : ie.equivFst (i.lift a C r r_tp) = a

def NaturalModel.Universe.Id.j {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Tm

The elimination rule for identity types. Γ ⊢ A is the type with a term Γ ⊢ a : A. Γ (y : A) (h : Id(A,a,y)) ⊢ C is the motive for the elimination. Then we obtain a section of the motive Γ (y : A) (h : Id(A,a,y)) ⊢ mkJ : A

Equations

• i.j a C r r_tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (ie.equivSnd (i.lift a C r r_tp))

theorem NaturalModel.Universe.Id.j_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (i.j a C r r_tp) N.tp = C

Typing for elimination rule J

theorem NaturalModel.Universe.Id.comp_j {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ a)) (i.j a C r r_tp) = i.j (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ a)) C) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) r) ⋯

theorem NaturalModel.Universe.Id.reflSubst_j {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) {Γ : Ctx} (a : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (C : CategoryTheory.yoneda.obj (ii.motiveCtx a) ⟶ N.Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ N.Tm) (r_tp : CategoryTheory.CategoryStruct.comp r N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst a)) (i.j a C r r_tp) = r

β rule for identity types. Substituting J with refl gives the user-supplied value r

def NaturalModel.Universe.Id.endPtSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {Γ : Ctx} (a b : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b M.tp = CategoryTheory.CategoryStruct.comp a M.tp) (h : CategoryTheory.yoneda.obj Γ ⟶ M.Tm) (h_tp : CategoryTheory.CategoryStruct.comp h M.tp = CategoryTheory.CategoryStruct.comp (⋯.lift b a ⋯) ii.Id) : Γ ⟶ ii.motiveCtx a

Equations

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

def NaturalModel.Universe.Id.toId' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} (i : Id ie N) : M.Id' ii N

Id is equivalent to Id (one half).

Equations

• i.toId' = { j := fun {Γ : Ctx} => i.j, j_tp := ⋯, comp_j := ⋯, reflSubst_j := ⋯ }

theorem NaturalModel.Universe.Id'.fst_eq_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) : CategoryTheory.UvPoly.Equiv.fst (CategoryTheory.UvPoly.id M.Tm) N.Tm ar = ie.equivFst aC

@[reducible, inline]

abbrev NaturalModel.Universe.Id'.motive {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} {Γ : Ctx} (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) : CategoryTheory.yoneda.obj (ii.motiveCtx (ie.equivFst aC)) ⟶ N.Ty

Equations

• NaturalModel.Universe.Id'.motive aC = ie.equivSnd aC

theorem NaturalModel.Universe.Id'.comp_motive {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} {Γ : Ctx} (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) {Δ : Ctx} (σ : Δ ⟶ Γ) : motive (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) aC) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.motiveSubst σ (ie.equivFst aC))) (motive aC)

@[reducible, inline]

abbrev NaturalModel.Universe.Id'.reflCase {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) : CategoryTheory.yoneda.obj Γ ⟶ N.Tm

Equations

• NaturalModel.Universe.Id'.reflCase ar = CategoryTheory.UvPoly.Equiv.snd' (CategoryTheory.UvPoly.id M.Tm) N.Tm ar ⋯

theorem NaturalModel.Universe.Id'.comp_reflCase {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) {Δ : Ctx} (σ : Δ ⟶ Γ) : reflCase (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ar) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (reflCase ar)

theorem NaturalModel.Universe.Id'.reflCase_comp_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) : CategoryTheory.CategoryStruct.comp (reflCase ar) N.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (ii.reflSubst (ie.equivFst aC))) (motive aC)

def NaturalModel.Universe.Id'.lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} (i : M.Id' ii N) {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Tm

Equations

• i.lift ar aC hrC = ie.equivMk (ie.equivFst aC) (i.j (ie.equivFst aC) (NaturalModel.Universe.Id'.motive aC) (NaturalModel.Universe.Id'.reflCase ar) ⋯)

theorem NaturalModel.Universe.Id'.lift_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} (i : M.Id' ii N) {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) : CategoryTheory.CategoryStruct.comp (i.lift ar aC hrC) (ie.verticalNatTrans.app N.Tm) = ar

theorem NaturalModel.Universe.Id'.lift_snd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} (i : M.Id' ii N) {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) : CategoryTheory.CategoryStruct.comp (i.lift ar aC hrC) (ie.iFunctor.map N.tp) = aC

theorem NaturalModel.Universe.Id'.comp_lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} (i : M.Id' ii N) {Γ : Ctx} (ar : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.UvPoly.id M.Tm).functor.obj N.Tm) (aC : CategoryTheory.yoneda.obj Γ ⟶ ie.iFunctor.obj N.Ty) (hrC : CategoryTheory.CategoryStruct.comp ar ((CategoryTheory.UvPoly.id M.Tm).functor.map N.tp) = CategoryTheory.CategoryStruct.comp aC (ie.verticalNatTrans.app N.Ty)) {Δ : Ctx} (σ : Δ ⟶ Γ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (i.lift ar aC hrC) = i.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ar) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) aC) ⋯

def NaturalModel.Universe.Id'.toId {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M : Universe Ctx} {ii : M.IdIntro} {ie : IdElimBase ii} {N : Universe Ctx} (i : M.Id' ii N) : Id ie N

Equations

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