Morphisms of natural models, and Russell-universe embeddings.

def NaturalModel.Universe.«termBy>_» : Lean.ParserDescr

Equations

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

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

• mapTm : M.Tm ⟶ N.Tm
• mapTy : M.Ty ⟶ N.Ty
• pb : CategoryTheory.IsPullback self.mapTm M.tp N.tp self.mapTy

def NaturalModel.Universe.Hom.id {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) : M.Hom M

Equations

• NaturalModel.Universe.Hom.id M = { mapTm := CategoryTheory.CategoryStruct.id M.Tm, mapTy := CategoryTheory.CategoryStruct.id M.Ty, pb := ⋯ }

def NaturalModel.Universe.Hom.comp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N O : Universe Ctx} (α : M.Hom N) (β : N.Hom O) : M.Hom O

Equations

• α.comp β = { mapTm := CategoryTheory.CategoryStruct.comp α.mapTm β.mapTm, mapTy := CategoryTheory.CategoryStruct.comp α.mapTy β.mapTy, pb := ⋯ }

def NaturalModel.Universe.Hom.comp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N O P : Universe Ctx} (α : M.Hom N) (β : N.Hom O) (γ : O.Hom P) : (α.comp β).comp γ = α.comp (β.comp γ)

Equations

• ⋯ = ⋯

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

Morphism into the representable natural transformation M from the pullback of M along a type.

Equations

• M.pullbackHom A = { mapTm := M.var A, mapTy := A, pb := ⋯ }

def NaturalModel.Universe.Hom.subst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : Universe Ctx) {Γ Δ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σ : Δ ⟶ Γ) : (M.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)).Hom (M.pullback A)

Given M : Universe, a semantic type A : y(Γ) ⟶ M.Ty, and a substitution σ : Δ ⟶ Γ, construct a Hom for the substitution A[σ].

Equations

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

def NaturalModel.Universe.Hom.cartesianNatTrans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} (h : M.Hom N) : M.Ptp ⟶ N.Ptp

Equations

• h.cartesianNatTrans = M.uvPolyTp.cartesianNatTrans N.uvPolyTp h.mapTy h.mapTm ⋯

def NaturalModel.Universe.Hom.extIsoExt {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} (h : M.Hom N) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) : CategoryTheory.yoneda.obj (N.ext (CategoryTheory.CategoryStruct.comp A h.mapTy)) ≅ CategoryTheory.yoneda.obj (M.ext A)

Equations

• h.extIsoExt A = CategoryTheory.IsPullback.isoIsPullback N.Tm (CategoryTheory.yoneda.obj Γ) ⋯ ⋯

theorem NaturalModel.Universe.Hom.mk_comp_cartesianNatTrans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} (h : M.Hom N) {Γ : Ctx} {X : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk M A B) (h.cartesianNatTrans.app X) = PtpEquiv.mk N (CategoryTheory.CategoryStruct.comp A h.mapTy) (CategoryTheory.CategoryStruct.comp (h.extIsoExt A).hom B)

theorem NaturalModel.Universe.Hom.mk_comp_cartesianNatTrans_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N : Universe Ctx} (h : M.Hom N) {Γ : Ctx} {X : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (B : CategoryTheory.yoneda.obj (M.ext A) ⟶ X) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h✝ : N.Ptp.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk M A B) (CategoryTheory.CategoryStruct.comp (h.cartesianNatTrans.app X) h✝) = CategoryTheory.CategoryStruct.comp (PtpEquiv.mk N (CategoryTheory.CategoryStruct.comp A h.mapTy) (CategoryTheory.CategoryStruct.comp (h.extIsoExt A).hom B)) h✝

structure NaturalModel.Universe.UHom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (M N : Universe Ctx) extends M.Hom N : Type u

A Russell universe embedding is a hom of natural models M ⟶ N such that types in M correspond to terms of a universe U in N.

These don't form a category since UHom.id M is essentially Type : Type in M.

Note this doesn't need to extend Hom as none of its fields are used; it's just convenient to pack up the data.

• mapTm : M.Tm ⟶ N.Tm
• mapTy : M.Ty ⟶ N.Ty
• pb : CategoryTheory.IsPullback self.mapTm M.tp N.tp self.mapTy
• U : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ N.Ty
• asTm : M.Ty ⟶ N.Tm
• U_pb : CategoryTheory.IsPullback self.asTm (CategoryTheory.ChosenTerminal.isTerminal_yUnit.from M.Ty) N.tp self.U

def NaturalModel.Universe.UHom.ofTyIsoExt {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : Universe Ctx} (H : M.Hom N) {U : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ N.Ty} (i : M.Ty ≅ CategoryTheory.yoneda.obj (N.ext U)) : M.UHom N

Equations

• NaturalModel.Universe.UHom.ofTyIsoExt H i = { toHom := H, U := U, asTm := CategoryTheory.CategoryStruct.comp i.hom (N.var U), U_pb := ⋯ }

def NaturalModel.Universe.UHom.comp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N O : Universe Ctx} (α : M.UHom N) (β : N.UHom O) : M.UHom O

Equations

• α.comp β = { toHom := α.comp β.toHom, U := CategoryTheory.CategoryStruct.comp α.U β.mapTy, asTm := CategoryTheory.CategoryStruct.comp α.asTm β.mapTm, U_pb := ⋯ }

def NaturalModel.Universe.UHom.comp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N O P : Universe Ctx} (α : M.UHom N) (β : N.UHom O) (γ : O.UHom P) : (α.comp β).comp γ = α.comp (β.comp γ)

Equations

• ⋯ = ⋯

def NaturalModel.Universe.UHom.wkU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : Universe Ctx} (Γ : Ctx) (α : M.UHom N) : CategoryTheory.yoneda.obj Γ ⟶ N.Ty

Equations

• NaturalModel.Universe.UHom.wkU Γ α = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenTerminal.isTerminal_yUnit.from (CategoryTheory.yoneda.obj Γ)) α.U

@[simp]

theorem NaturalModel.Universe.UHom.comp_wkU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : Universe Ctx} {Δ Γ : Ctx} (α : M.UHom N) (f : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) : CategoryTheory.CategoryStruct.comp f (wkU Γ α) = wkU Δ α

@[simp]

theorem NaturalModel.Universe.UHom.comp_wkU_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : Universe Ctx} {Δ Γ : Ctx} (α : M.UHom N) (f : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : N.Ty ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (wkU Γ α) h) = CategoryTheory.CategoryStruct.comp (wkU Δ α) h

def NaturalModel.Universe.UHom.ofTarskiU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (M : Universe Ctx) (U : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ M.Ty) (El : CategoryTheory.yoneda.obj (M.ext U) ⟶ M.Ty) : (M.pullback El).UHom M

Equations

• NaturalModel.Universe.UHom.ofTarskiU M U El = { toHom := M.pullbackHom El, U := U, asTm := M.var U, U_pb := ⋯ }

Universe embeddings

structure NaturalModel.Universe.UHomSeq (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] : Type (u + 1)

A sequence of Russell universe embeddings.

• length : ℕ

  Number of embeddings in the sequence, or one less than the number of models in the sequence.

• objs (i : ℕ) (h : i < self.length + 1) : Universe Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)

instance NaturalModel.Universe.UHomSeq.instGetElemNatLtHAddLengthOfNat {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] : GetElem (UHomSeq Ctx) ℕ (Universe Ctx) fun (s : UHomSeq Ctx) (i : ℕ) => i < s.length + 1

Equations

• NaturalModel.Universe.UHomSeq.instGetElemNatLtHAddLengthOfNat = { getElem := fun (s : NaturalModel.Universe.UHomSeq Ctx) (i : ℕ) (h : i < s.length + 1) => s.objs i h }

def NaturalModel.Universe.UHomSeq.homSucc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i : ℕ) (h : i < s.length := by get_elem_tactic) : s[i].UHom s[i + 1]

Equations

• s.homSucc i h = s.homSucc' i h

@[irreducible]

def NaturalModel.Universe.UHomSeq.hom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i < j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) : s[i].UHom s[j]

Composition of embeddings between i and j in the chain.

Equations

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

def NaturalModel.Universe.UHomSeq.homOfLe {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) : s[i].Hom s[j]

Equations

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

def NaturalModel.Universe.UHomSeq.unlift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) {Γ : CategoryTheory.Psh Ctx} (A : Γ ⟶ s[i].Ty) (t : Γ ⟶ s[j].Tm) (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : Γ ⟶ s[i].Tm

For i ≤ j and a term t at level j, if the type of t is lifted from level i, then t is a lift of a term at level i.

Equations

• s.unlift i j ij jlen A t eq = ⋯.lift t A eq

@[simp]

theorem NaturalModel.Universe.UHomSeq.unlift_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty} {t : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm} (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : CategoryTheory.CategoryStruct.comp (s.unlift i j ij jlen A t eq) s[i].tp = A

@[simp]

theorem NaturalModel.Universe.UHomSeq.unlift_lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty} {t : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm} (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : CategoryTheory.CategoryStruct.comp (s.unlift i j ij jlen A t eq) (s.homOfLe i j ij jlen).mapTm = t

def NaturalModel.Universe.UHomSeq.unliftVar {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) {A' : CategoryTheory.yoneda.obj Γ ⟶ s[j].Ty} (eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A') : CategoryTheory.yoneda.obj (s[j].ext A') ⟶ s[i].Tm

Equations

• s.unliftVar i j ij jlen A eq = s.unlift i j ij jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[j].disp A')) A) (s[j].var A') ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.unliftVar_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty} {A' : CategoryTheory.yoneda.obj Γ ⟶ s[j].Ty} (eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A') : CategoryTheory.CategoryStruct.comp (s.unliftVar i j ij jlen A eq) s[i].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[j].disp A')) A

theorem NaturalModel.Universe.UHomSeq.substCons_unliftVar {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty} {A' : CategoryTheory.yoneda.obj Γ ⟶ s[j].Ty} {eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A'} {Δ : Ctx} {σ : Δ ⟶ Γ} {t : CategoryTheory.yoneda.obj Δ ⟶ s[i].Tm} (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[j].substCons σ A' (CategoryTheory.CategoryStruct.comp t (s.homOfLe i j ij jlen).mapTm) ⋯)) (s.unliftVar i j ij jlen A eq) = t

def NaturalModel.Universe.UHomSeq.cartesianNatTrans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by get_elem_tactic) (jlen : j < s.length + 1 := by get_elem_tactic) : s[i].Ptp ⟶ s[j].Ptp

If s is a sequence of universe homomorphisms then for i ≤ j we get a polynomial endofunctor natural transformation s[i].Ptp ⟶ s[j].Ptp.

Equations

• s.cartesianNatTrans i j ij jlen = (s.homOfLe i j ij jlen).cartesianNatTrans

theorem NaturalModel.Universe.UHomSeq.mk_comp_cartesianNatTrans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {X : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ X) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk s[i] A B) ((s.cartesianNatTrans i j ij jlen).app X) = PtpEquiv.mk s[j] (CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[j].disp (CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy)) A (s.unliftVar i j ij jlen A ⋯) ⋯)) B)

theorem NaturalModel.Universe.UHomSeq.mk_comp_cartesianNatTrans_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {X : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ X) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : s[j].Ptp.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk s[i] A B) (CategoryTheory.CategoryStruct.comp ((s.cartesianNatTrans i j ij jlen).app X) h) = CategoryTheory.CategoryStruct.comp (PtpEquiv.mk s[j] (CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[j].disp (CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy)) A (s.unliftVar i j ij jlen A ⋯) ⋯)) B)) h

theorem NaturalModel.Universe.UHomSeq.cartesianNatTrans_fstProj {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {X : CategoryTheory.Psh Ctx} : CategoryTheory.CategoryStruct.comp ((s.cartesianNatTrans i j ij jlen).app X) (s[j].uvPolyTp.fstProj X) = CategoryTheory.CategoryStruct.comp (s[i].uvPolyTp.fstProj X) (s.homOfLe i j ij jlen).mapTy

def NaturalModel.Universe.UHomSeq.cartesianNatTransTm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i0 i1 j0 j1 : ℕ) (ii : i0 ≤ i1 := by get_elem_tactic) (ilen : i1 < s.length + 1 := by get_elem_tactic) (jj : j0 ≤ j1 := by get_elem_tactic) (jlen : j1 < s.length + 1 := by get_elem_tactic) : s[i0].Ptp.obj s[j0].Tm ⟶ s[i1].Ptp.obj s[j1].Tm

This is one side of the commutative square

s[i0].Ptp.obj s[j0].Tm ⟶ s[i1].Ptp.obj s[j1].Tm
  |                           |
  |                           |
  |                           |
  |                           |
  V                           V
s[i0].Ptp.obj s[j0].Tm ⟶ s[i1].Ptp.obj s[j0].Tm

Given i0 ≤ i1 and j0 ≤ j1

Equations

• s.cartesianNatTransTm i0 i1 j0 j1 ii ilen jj jlen = CategoryTheory.CategoryStruct.comp ((s.cartesianNatTrans i0 i1 ii ilen).app s[j0].Tm) (s[i1].Ptp.map (s.homOfLe j0 j1 jj jlen).mapTm)

theorem NaturalModel.Universe.UHomSeq.mk_comp_cartesianNatTransTm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i0 i1 j0 j1 : ℕ} {ii : i0 ≤ i1} {ilen : i1 < s.length + 1} {jj : j0 ≤ j1} {jlen : j1 < s.length + 1} {Γ : Ctx} {X : i0 < s.length + 1} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i0].Ty) (B : CategoryTheory.yoneda.obj (s[i0].ext A) ⟶ s[j0].Tm) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk s[i0] A B) (s.cartesianNatTransTm i0 i1 j0 j1 ii ilen jj jlen) = PtpEquiv.mk s[i1] (CategoryTheory.CategoryStruct.comp A (s.homOfLe i0 i1 ii ilen).mapTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i0].substCons (s[i1].disp (CategoryTheory.CategoryStruct.comp A (s.homOfLe i0 i1 ii ilen).mapTy)) A (s.unliftVar i0 i1 ii ilen A ⋯) ⋯)) (CategoryTheory.CategoryStruct.comp B (s.homOfLe j0 j1 jj jlen).mapTm))

theorem NaturalModel.Universe.UHomSeq.cartesianNatTransTm_fstProj {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i0 i1 j0 j1 : ℕ} {ii : i0 ≤ i1} {ilen : i1 < s.length + 1} {jj : j0 ≤ j1} {jlen : j1 < s.length + 1} : CategoryTheory.CategoryStruct.comp (s.cartesianNatTransTm i0 i1 j0 j1 ii ilen jj jlen) (s[i1].uvPolyTp.fstProj s[j1].Tm) = CategoryTheory.CategoryStruct.comp (s[i0].uvPolyTp.fstProj s[j0].Tm) (s.homOfLe i0 i1 ii ilen).mapTy

def NaturalModel.Universe.UHomSeq.cartesianNatTransTy {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i0 i1 j0 j1 : ℕ) (i0len : i0 ≤ i1 := by get_elem_tactic) (i1len : i1 < s.length + 1 := by get_elem_tactic) (j0len : j0 ≤ j1 := by get_elem_tactic) (j1len : j1 < s.length + 1 := by get_elem_tactic) : s[i0].Ptp.obj s[j0].Ty ⟶ s[i1].Ptp.obj s[j1].Ty

Equations

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

theorem NaturalModel.Universe.UHomSeq.mk_comp_cartesianNatTransTy {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i0 i1 j0 j1 : ℕ} {ii : i0 ≤ i1} {ilen : i1 < s.length + 1} {jj : j0 ≤ j1} {jlen : j1 < s.length + 1} {Γ : Ctx} {X : i0 < s.length + 1} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i0].Ty) (B : CategoryTheory.yoneda.obj (s[i0].ext A) ⟶ s[j0].Ty) : CategoryTheory.CategoryStruct.comp (PtpEquiv.mk s[i0] A B) (s.cartesianNatTransTy i0 i1 j0 j1 ii ilen jj jlen) = PtpEquiv.mk s[i1] (CategoryTheory.CategoryStruct.comp A (s.homOfLe i0 i1 ii ilen).mapTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i0].substCons (s[i1].disp (CategoryTheory.CategoryStruct.comp A (s.homOfLe i0 i1 ii ilen).mapTy)) A (s.unliftVar i0 i1 ii ilen A ⋯) ⋯)) (CategoryTheory.CategoryStruct.comp B (s.homOfLe j0 j1 jj jlen).mapTy))

theorem NaturalModel.Universe.UHomSeq.cartesianNatTransTy_fstProj {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i0 i1 j0 j1 : ℕ} {ii : i0 ≤ i1} {ilen : i1 < s.length + 1} {jj : j0 ≤ j1} {jlen : j1 < s.length + 1} : CategoryTheory.CategoryStruct.comp (s.cartesianNatTransTy i0 i1 j0 j1 ii ilen jj jlen) (s[i1].uvPolyTp.fstProj s[j1].Ty) = CategoryTheory.CategoryStruct.comp (s[i0].uvPolyTp.fstProj s[j0].Ty) (s.homOfLe i0 i1 ii ilen).mapTy

@[irreducible]

theorem NaturalModel.Universe.UHomSeq.hom_comp_trans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j k : ℕ) (ij : i < j) (jk : j < k) (klen : k < s.length + 1) : (s.hom i j ij ⋯).comp (s.hom j k jk klen) = s.hom i k ⋯ klen

def NaturalModel.Universe.UHomSeq.code {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm

TODO: Consider generalising to just UHom? Convert a map into the ith type classifier into a a term of the i+1th term classifier, that is a term of the ith universe. It is defined by composition with the first projection of the pullback square v s[i].Ty ----> s[i+1].Tm ^ | | A / | p.b. | / | | / V V y(Γ) ---> 1 -----> s[i+1].Ty U_i

Equations

• s.code ilen A = CategoryTheory.CategoryStruct.comp A (s.homSucc i ilen).asTm

@[simp]

theorem NaturalModel.Universe.UHomSeq.code_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) : CategoryTheory.CategoryStruct.comp (s.code ilen A) s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)

theorem NaturalModel.Universe.UHomSeq.comp_code {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {Δ Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) : CategoryTheory.CategoryStruct.comp σ (s.code ilen A) = s.code ilen (CategoryTheory.CategoryStruct.comp σ A)

theorem NaturalModel.Universe.UHomSeq.comp_code_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {Δ Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : s[i + 1].Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (s.code ilen A) h) = CategoryTheory.CategoryStruct.comp (s.code ilen (CategoryTheory.CategoryStruct.comp σ A)) h

def NaturalModel.Universe.UHomSeq.el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Γ : Ctx} {i : ℕ} (ilen : i < s.length) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty

TODO: Consider generalising to just UHom? Convert a a term of the ith universe (it is a i+1 level term) into a map into the ith type classifier. It is the unique map into the pullback a y(Γ) -----------------¬ ‖ --> v V ‖ s[i].Ty ----> s[i+1].Tm ‖ | | ‖ | p.b. | ‖ | | ‖ V V y(Γ) ---> 1 -----> s[i+1].Ty U_i

Equations

• s.el ilen a a_tp = ⋯.lift a (CategoryTheory.ChosenTerminal.isTerminal_yUnit.from (CategoryTheory.yoneda.obj Γ)) ⋯

theorem NaturalModel.Universe.UHomSeq.comp_el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Δ Γ : Ctx} {i : ℕ} (ilen : i < s.length) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : CategoryTheory.CategoryStruct.comp σ (s.el ilen a a_tp) = s.el ilen (CategoryTheory.CategoryStruct.comp σ a) ⋯

theorem NaturalModel.Universe.UHomSeq.comp_el_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Δ Γ : Ctx} {i : ℕ} (ilen : i < s.length) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : s[i].Ty ⟶ Z) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (s.el ilen a a_tp) h) = CategoryTheory.CategoryStruct.comp (s.el ilen (CategoryTheory.CategoryStruct.comp σ a) ⋯) h

@[simp]

theorem NaturalModel.Universe.UHomSeq.el_code {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) : s.el ilen (s.code ilen A) ⋯ = A

@[simp]

theorem NaturalModel.Universe.UHomSeq.code_el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Γ : Ctx} {i : ℕ} (ilen : i < s.length) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : s.code ilen (s.el ilen a a_tp) = a

Pi

class NaturalModel.Universe.UHomSeq.PiSeq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) : Type u

The data of Pi and lam formers at each universe s[i].tp.

This data is universe-monomorphic, but we can use it to construct universe-polymorphic formation in a model-independent manner. For example, universe-monomorphic Pi

Γ ⊢ᵢ A type  Γ.A ⊢ᵢ B type
--------------------------
Γ ⊢ᵢ ΠA. B type

can be extended to

Γ ⊢ᵢ A type  Γ.A ⊢ⱼ B type
--------------------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ ΠA. B type

• nmPi (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : s[i].Pi

def NaturalModel.Universe.UHomSeq.Pi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] : s[i].Ptp.obj s[j].Ty ⟶ s[max i j].Ty

Equations

• s.Pi ilen jlen = CategoryTheory.CategoryStruct.comp (s.cartesianNatTransTy i (max i j) j (max i j) ⋯ ⋯ ⋯ ⋯) (NaturalModel.Universe.UHomSeq.PiSeq.nmPi (max i j) ⋯).Pi

def NaturalModel.Universe.UHomSeq.lam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] : s[i].Ptp.obj s[j].Tm ⟶ s[max i j].Tm

Equations

• s.lam ilen jlen = CategoryTheory.CategoryStruct.comp (s.cartesianNatTransTm i (max i j) j (max i j) ⋯ ⋯ ⋯ ⋯) (NaturalModel.Universe.UHomSeq.PiSeq.nmPi (max i j) ⋯).lam

def NaturalModel.Universe.UHomSeq.Pi_pb {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] : CategoryTheory.IsPullback (s.lam ilen jlen) (s[i].Ptp.map s[j].tp) s[max i j].tp (s.Pi ilen jlen)

Equations

• ⋯ = ⋯

def NaturalModel.Universe.UHomSeq.mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Ty

Γ ⊢ᵢ A  Γ.A ⊢ⱼ B
-----------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ ΠA. B

Equations

• s.mkPi ilen jlen A B = CategoryTheory.CategoryStruct.comp (NaturalModel.Universe.PtpEquiv.mk s[i] A B) (s.Pi ilen jlen)

theorem NaturalModel.Universe.UHomSeq.comp_mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkPi ilen jlen A B) = s.mkPi ilen jlen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA eq)) B)

def NaturalModel.Universe.UHomSeq.mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (t : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm) : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm

Γ ⊢ᵢ A  Γ.A ⊢ⱼ t : B
-------------------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ λA. t : ΠA. B

Equations

• s.mkLam ilen jlen A t = CategoryTheory.CategoryStruct.comp (NaturalModel.Universe.PtpEquiv.mk s[i] A t) (s.lam ilen jlen)

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[j].tp = B) : CategoryTheory.CategoryStruct.comp (s.mkLam ilen jlen A t) s[max i j].tp = s.mkPi ilen jlen A B

theorem NaturalModel.Universe.UHomSeq.comp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (t : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkLam ilen jlen A t) = s.mkLam ilen jlen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA eq)) t)

def NaturalModel.Universe.UHomSeq.unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm

Γ ⊢ᵢ A  Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ f : ΠA. B
-----------------------------
Γ.A ⊢ⱼ unlam f : B

Equations

• s.unLam ilen jlen A B f f_tp = NaturalModel.Universe.PtpEquiv.snd s[i] (⋯.lift f (NaturalModel.Universe.PtpEquiv.mk s[i] A B) f_tp) A ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.unLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : CategoryTheory.CategoryStruct.comp (s.unLam ilen jlen A B f f_tp) s[j].tp = B

theorem NaturalModel.Universe.UHomSeq.comp_unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA eq)) (s.unLam ilen jlen A B f f_tp) = s.unLam ilen jlen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA eq)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) f) ⋯

def NaturalModel.Universe.UHomSeq.mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i].tp = A) : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm

Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ f : ΠA. B  Γ ⊢ᵢ a : A
---------------------------------
Γ ⊢ⱼ f a : B[id.a]

Equations

• s.mkApp ilen jlen A B f f_tp a a_tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A a a_tp)) (s.unLam ilen jlen A B f f_tp)

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkApp_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i].tp = A) : CategoryTheory.CategoryStruct.comp (s.mkApp ilen jlen A B f f_tp a a_tp) s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A a a_tp)) B

theorem NaturalModel.Universe.UHomSeq.comp_mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i].tp = A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkApp ilen jlen A B f f_tp a a_tp) = s.mkApp ilen jlen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA eq)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) f) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkLam_unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : s.mkLam ilen jlen A (s.unLam ilen jlen A B f f_tp) = f

@[simp]

theorem NaturalModel.Universe.UHomSeq.unLam_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[j].tp = B) (lam_tp : CategoryTheory.CategoryStruct.comp (s.mkLam ilen jlen A t) s[max i j].tp = s.mkPi ilen jlen A B) : s.unLam ilen jlen A B (s.mkLam ilen jlen A t) lam_tp = t

def NaturalModel.Universe.UHomSeq.etaExpand {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm

Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ f : ΠA. B
--------------------------------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ λA. f[↑] v₀ : ΠA. B

Equations

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

theorem NaturalModel.Universe.UHomSeq.etaExpand_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[max i j].tp = s.mkPi ilen jlen A B) : s.etaExpand ilen jlen A B f f_tp = f

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkApp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.PiSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[j].tp = B) (lam_tp : CategoryTheory.CategoryStruct.comp (s.mkLam ilen jlen A t) s[max i j].tp = s.mkPi ilen jlen A B) (a : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i].tp = A) : s.mkApp ilen jlen A B (s.mkLam ilen jlen A t) lam_tp a a_tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A a a_tp)) t

Γ ⊢ᵢ A  Γ.A ⊢ⱼ t : B  Γ ⊢ᵢ a : A
--------------------------------
Γ.A ⊢ⱼ (λA. t) a ≡ t[a] : B[a]

Sigma

class NaturalModel.Universe.UHomSeq.SigSeq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) : Type u

The data of Sig and pair formers at each universe s[i].tp.

• nmSig (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : s[i].Sigma

def NaturalModel.Universe.UHomSeq.Sig {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] : s[i].Ptp.obj s[j].Ty ⟶ s[max i j].Ty

Equations

• s.Sig ilen jlen = CategoryTheory.CategoryStruct.comp (s.cartesianNatTransTy i (max i j) j (max i j) ⋯ ⋯ ⋯ ⋯) (NaturalModel.Universe.UHomSeq.SigSeq.nmSig (max i j) ⋯).Sig

def NaturalModel.Universe.UHomSeq.pair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] : s[i].uvPolyTp.compDom s[j].uvPolyTp ⟶ s[max i j].Tm

Equations

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

def NaturalModel.Universe.UHomSeq.Sig_pb {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] : CategoryTheory.IsPullback (s.pair ilen jlen) (s[i].uvPolyTp.compP s[j].uvPolyTp) s[max i j].tp (s.Sig ilen jlen)

Equations

• ⋯ = ⋯

def NaturalModel.Universe.UHomSeq.mkSig {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Ty

Γ ⊢ᵢ A  Γ.A ⊢ⱼ B
-----------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ ΣA. B

Equations

• s.mkSig ilen jlen A B = CategoryTheory.CategoryStruct.comp (NaturalModel.Universe.PtpEquiv.mk s[i] A B) (s.Sig ilen jlen)

theorem NaturalModel.Universe.UHomSeq.comp_mkSig {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkSig ilen jlen A B) = s.mkSig ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) ⋯)) B)

def NaturalModel.Universe.UHomSeq.mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (u : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A t t_tp)) B) : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm

Γ ⊢ᵢ t : A  Γ ⊢ⱼ u : B[t]
--------------------------
Γ ⊢ₘₐₓ₍ᵢ,ⱼ₎ ⟨t, u⟩ : ΣA. B

Equations

• s.mkPair ilen jlen A B t t_tp u u_tp = CategoryTheory.CategoryStruct.comp (NaturalModel.Universe.compDomEquiv.mk t t_tp B u u_tp) (s.pair ilen jlen)

theorem NaturalModel.Universe.UHomSeq.comp_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (u : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A t t_tp)) B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkPair ilen jlen A B t t_tp u u_tp) = s.mkPair ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) ⋯)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) t) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) u) ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkPair_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (u : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A t t_tp)) B) : CategoryTheory.CategoryStruct.comp (s.mkPair ilen jlen A B t t_tp u u_tp) s[max i j].tp = s.mkSig ilen jlen A B

def NaturalModel.Universe.UHomSeq.mkFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm

Equations

• s.mkFst ilen jlen A B p p_tp = NaturalModel.Universe.compDomEquiv.fst (⋯.lift p (NaturalModel.Universe.PtpEquiv.mk s[i] A B) p_tp)

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkFst_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.CategoryStruct.comp (s.mkFst ilen jlen A B p p_tp) s[i].tp = A

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkFst_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (u : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A t t_tp)) B) : s.mkFst ilen jlen A B (s.mkPair ilen jlen A B t t_tp u u_tp) ⋯ = t

theorem NaturalModel.Universe.UHomSeq.comp_mkFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkFst ilen jlen A B p p_tp) = s.mkFst ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) ⋯)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) p) ⋯

def NaturalModel.Universe.UHomSeq.mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm

Equations

• s.mkSnd ilen jlen A B p p_tp = NaturalModel.Universe.compDomEquiv.snd (⋯.lift p (NaturalModel.Universe.PtpEquiv.mk s[i] A B) p_tp)

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkSnd_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (u : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A t t_tp)) B) : s.mkSnd ilen jlen A B (s.mkPair ilen jlen A B t t_tp u u_tp) ⋯ = u

theorem NaturalModel.Universe.UHomSeq.dependent_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : compDomEquiv.dependent (⋯.lift p (PtpEquiv.mk s[i] A B) p_tp) A ⋯ = B

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkSnd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.CategoryStruct.comp (s.mkSnd ilen jlen A B p p_tp) s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A (s.mkFst ilen jlen A B p p_tp) ⋯)) B

theorem NaturalModel.Universe.UHomSeq.comp_mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkSnd ilen jlen A B p p_tp) = s.mkSnd ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) ⋯)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) p) ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkPair_mkFst_mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.SigSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[j].Ty) (p : CategoryTheory.yoneda.obj Γ ⟶ s[max i j].Tm) (p_tp : CategoryTheory.CategoryStruct.comp p s[max i j].tp = s.mkSig ilen jlen A B) : s.mkPair ilen jlen A B (s.mkFst ilen jlen A B p p_tp) ⋯ (s.mkSnd ilen jlen A B p p_tp) ⋯ = p

Identity types

class NaturalModel.Universe.UHomSeq.IdSeq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) : Type (u + 1)

• nmII (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : s[i].IdIntro
• nmIEB (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : IdElimBase (nmII i ilen)
• nmId (i j : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) (jlen : j < s.length + 1 := by get_elem_tactic) : Id (nmIEB i ilen) s[j]

def NaturalModel.Universe.UHomSeq.mkId {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i : ℕ} (ilen : i < s.length + 1) [s.IdSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (a0 a1 : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a0_tp : CategoryTheory.CategoryStruct.comp a0 s[i].tp = A) (a1_tp : CategoryTheory.CategoryStruct.comp a1 s[i].tp = A) : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty

Γ ⊢ᵢ A  Γ ⊢ᵢ a0, a1 : A
-----------------------
Γ ⊢ᵢ Id(A, a0, a1)

Equations

• s.mkId ilen A a0 a1 a0_tp a1_tp = (NaturalModel.Universe.UHomSeq.IdSeq.nmII i ilen).mkId a0 a1 ⋯

theorem NaturalModel.Universe.UHomSeq.comp_mkId {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i : ℕ} (ilen : i < s.length + 1) [s.IdSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (a0 a1 : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (a0_tp : CategoryTheory.CategoryStruct.comp a0 s[i].tp = A) (a1_tp : CategoryTheory.CategoryStruct.comp a1 s[i].tp = A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkId ilen A a0 a1 a0_tp a1_tp) = s.mkId ilen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a1) ⋯ ⋯

def NaturalModel.Universe.UHomSeq.mkRefl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i : ℕ} (ilen : i < s.length + 1) [s.IdSeq] {Γ : Ctx} (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm

Γ ⊢ᵢ t : A
-----------------------
Γ ⊢ᵢ refl(t) : Id(A, t, t)

Equations

• s.mkRefl ilen t = (NaturalModel.Universe.UHomSeq.IdSeq.nmII i ilen).mkRefl t

theorem NaturalModel.Universe.UHomSeq.comp_mkRefl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i : ℕ} (ilen : i < s.length + 1) [s.IdSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkRefl ilen t) = s.mkRefl ilen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) t)

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkRefl_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i : ℕ} (ilen : i < s.length + 1) [s.IdSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) : CategoryTheory.CategoryStruct.comp (s.mkRefl ilen t) s[i].tp = s.mkId ilen A t t t_tp t_tp

def NaturalModel.Universe.UHomSeq.mkIdRec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.IdSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[i].Ty) (B_eq : s.mkId ilen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) t) (s[i].var A) ⋯ ⋯ = B) (M : CategoryTheory.yoneda.obj (s[i].ext B) ⟶ s[j].Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (r_tp : CategoryTheory.CategoryStruct.comp r s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A t t_tp) B (s.mkRefl ilen t) ⋯)) M) (u : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[i].tp = A) (h : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (h_tp : CategoryTheory.CategoryStruct.comp h s[i].tp = s.mkId ilen A t u t_tp u_tp) : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm

Γ ⊢ᵢ t : A
-----------------------
Γ ⊢ᵢ idRec(t) : Id(A, t, t)

Equations

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

theorem NaturalModel.Universe.UHomSeq.comp_mkIdRec {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.IdSeq] {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (σA : CategoryTheory.yoneda.obj Δ ⟶ s[i].Ty) (σA_eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = σA) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[i].Ty) (B_eq : s.mkId ilen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) t) (s[i].var A) ⋯ ⋯ = B) (σB : CategoryTheory.yoneda.obj (s[i].ext σA) ⟶ s[i].Ty) (σB_eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A σA σA_eq)) B = σB) (M : CategoryTheory.yoneda.obj (s[i].ext B) ⟶ s[j].Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (r_tp : CategoryTheory.CategoryStruct.comp r s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A t t_tp) B (s.mkRefl ilen t) ⋯)) M) (u : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[i].tp = A) (h : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (h_tp : CategoryTheory.CategoryStruct.comp h s[i].tp = s.mkId ilen A t u t_tp u_tp) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (s.mkIdRec ilen jlen A t t_tp B B_eq M r r_tp u u_tp h h_tp) = s.mkIdRec ilen jlen σA (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) t) ⋯ σB ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk (s[i].substWk σ A σA σA_eq) B σB σB_eq)) M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) r) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) u) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) h) ⋯

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkIdRec_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.IdSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[i].Ty) (B_eq : s.mkId ilen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) t) (s[i].var A) ⋯ ⋯ = B) (M : CategoryTheory.yoneda.obj (s[i].ext B) ⟶ s[j].Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (r_tp : CategoryTheory.CategoryStruct.comp r s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A t t_tp) B (s.mkRefl ilen t) ⋯)) M) (u : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (u_tp : CategoryTheory.CategoryStruct.comp u s[i].tp = A) (h : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (h_tp : CategoryTheory.CategoryStruct.comp h s[i].tp = s.mkId ilen A t u t_tp u_tp) : CategoryTheory.CategoryStruct.comp (s.mkIdRec ilen jlen A t t_tp B B_eq M r r_tp u u_tp h h_tp) s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A u u_tp) B h ⋯)) M

@[simp]

theorem NaturalModel.Universe.UHomSeq.mkIdRec_mkRefl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) [s.IdSeq] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (t : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm) (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = A) (B : CategoryTheory.yoneda.obj (s[i].ext A) ⟶ s[i].Ty) (B_eq : s.mkId ilen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].disp A)) t) (s[i].var A) ⋯ ⋯ = B) (M : CategoryTheory.yoneda.obj (s[i].ext B) ⟶ s[j].Ty) (r : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm) (r_tp : CategoryTheory.CategoryStruct.comp r s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A t t_tp) B (s.mkRefl ilen t) ⋯)) M) : s.mkIdRec ilen jlen A t t_tp B B_eq M r r_tp t t_tp (s.mkRefl ilen t) ⋯ = r