Morphisms of natural models, and Russell-universe embeddings.

def NaturalModelBase.isTerminal_yUnit {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] : CategoryTheory.Limits.IsTerminal (CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Ctx))

Equations

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

structure NaturalModelBase.Hom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M N : NaturalModelBase 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 NaturalModelBase.Hom.id {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) : M.Hom M

Equations

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

def NaturalModelBase.Hom.comp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N O : NaturalModelBase 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 NaturalModelBase.Hom.comp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] {M N O P : NaturalModelBase Ctx} (α : M.Hom N) (β : N.Hom O) (γ : O.Hom P) : (α.comp β).comp γ = α.comp (β.comp γ)

Equations

• ⋯ = ⋯

def NaturalModelBase.pullbackHom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase 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 NaturalModelBase.Hom.subst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] (M : NaturalModelBase Ctx) {Γ Δ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ M.Ty) (σ : Δ ⟶ Γ) : (M.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)).Hom (M.pullback A)

Given M : NaturalModelBase, 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.

structure NaturalModelBase.UHom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (M N : NaturalModelBase 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.MonoidalCategoryStruct.tensorUnit Ctx) ⟶ N.Ty
• U_pb : ∃ (v : M.Ty ⟶ N.Tm), CategoryTheory.IsPullback v (isTerminal_yUnit.from M.Ty) N.tp self.U

def NaturalModelBase.UHom.ofTyIsoExt {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] {M N : NaturalModelBase Ctx} (H : M.Hom N) {U : CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Ctx) ⟶ N.Ty} (i : M.Ty ≅ CategoryTheory.yoneda.obj (N.ext U)) : M.UHom N

Equations

• NaturalModelBase.UHom.ofTyIsoExt H i = { toHom := H, U := U, U_pb := ⋯ }

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

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

@[simp]

theorem NaturalModelBase.UHom.comp_wkU_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] {M N : NaturalModelBase 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 NaturalModelBase.UHom.ofTarskiU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (M : NaturalModelBase Ctx) (U : CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Ctx) ⟶ M.Ty) (El : CategoryTheory.yoneda.obj (M.ext U) ⟶ M.Ty) : (M.pullback El).UHom M

Equations

• NaturalModelBase.UHom.ofTarskiU M U El = { toHom := M.pullbackHom El, U := U, U_pb := ⋯ }

Universe embeddings

structure NaturalModelBase.UHomSeq (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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) : NaturalModelBase Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)

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

Equations

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

def NaturalModelBase.UHomSeq.homSucc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.hom {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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.

@[irreducible]

theorem NaturalModelBase.UHomSeq.hom_comp_trans {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.code {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) : CategoryTheory.yoneda.obj Γ ⟶ s[i + 1].Tm

Equations

• s.code ilen A = sorry

@[simp]

theorem NaturalModelBase.UHomSeq.code_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.comp_code {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.comp_code_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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

Equations

• s.el ilen a a_tp = sorry

theorem NaturalModelBase.UHomSeq.comp_el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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 NaturalModelBase.UHomSeq.comp_el_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory 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

structure NaturalModelBase.UHomSeqPiSigma (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] extends NaturalModelBase.UHomSeq Ctx : Type (u + 1)

The data of type and term 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

• length : ℕ
• objs (i : ℕ) (h : i < self.length + 1) : NaturalModelBase Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)
• nmPi (i : ℕ) (ilen : i < self.length + 1 := by get_elem_tactic) : self.toUHomSeq[i].NaturalModelPi
• nmSigma (i : ℕ) (ilen : i < self.length + 1 := by get_elem_tactic) : self.toUHomSeq[i].NaturalModelSigma

instance NaturalModelBase.UHomSeqPiSigma.instGetElemNatLtHAddLengthOfNat {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] : GetElem (UHomSeqPiSigma Ctx) ℕ (NaturalModelBase Ctx) fun (s : UHomSeqPiSigma Ctx) (i : ℕ) => i < s.length + 1

Equations

• NaturalModelBase.UHomSeqPiSigma.instGetElemNatLtHAddLengthOfNat = { getElem := fun (s : NaturalModelBase.UHomSeqPiSigma Ctx) (i : ℕ) (h : i < s.length + 1) => s.toUHomSeq[i] }

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.getElem_toUHomSeq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) (i : ℕ) (ilen : i < s.length + 1) : s.toUHomSeq[i] = s[i]

Pi

def NaturalModelBase.UHomSeqPiSigma.Pi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].Ptp.obj s[j].Ty ⟶ s[max i j].Ty

Equations

• s.Pi ilen jlen = CategoryTheory.CategoryStruct.comp sorry (s.nmPi (max i j) ⋯).Pi

def NaturalModelBase.UHomSeqPiSigma.lam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].Ptp.obj s[j].Tm ⟶ s[max i j].Tm

Equations

• s.lam ilen jlen = sorry

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

Equations

• ⋯ = ⋯

def NaturalModelBase.UHomSeqPiSigma.mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 (s[i].Ptp_equiv.symm ⟨A, B⟩) (s.Pi ilen jlen)

theorem NaturalModelBase.UHomSeqPiSigma.comp_mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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.mkPi ilen jlen A B) = s.mkPi ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A)) B)

def NaturalModelBase.UHomSeqPiSigma.mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 (s[i].Ptp_equiv.symm ⟨A, t⟩) (s.lam ilen jlen)

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.comp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ s[i].Ty) (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 (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A)) t)

def NaturalModelBase.UHomSeqPiSigma.unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 = ⋯.mpr (s[i].Ptp_equiv (⋯.lift f (s[i].Ptp_equiv.symm ⟨A, B⟩) f_tp)).snd

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.unLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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

def NaturalModelBase.UHomSeqPiSigma.mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.mkApp_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.comp_mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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 (CategoryTheory.yoneda.map σ) (s.mkApp ilen jlen A B f f_tp a a_tp) = s.mkApp ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) f) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) a) ⋯

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkLam_unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.unLam_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.etaExpand {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.etaExpand_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.mkApp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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

def NaturalModelBase.UHomSeqPiSigma.Sig {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].Ptp.obj s[j].Ty ⟶ s[max i j].Ty

Equations

• s.Sig ilen jlen = CategoryTheory.CategoryStruct.comp sorry (s.nmSigma (max i j) ⋯).Sig

def NaturalModelBase.UHomSeqPiSigma.pair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].uvPolyTp.compDom s[j].uvPolyTp ⟶ s[max i j].Tm

Equations

• s.pair ilen jlen = sorry

def NaturalModelBase.UHomSeqPiSigma.Sig_pb {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : CategoryTheory.IsPullback (s.pair ilen jlen) (s[i].uvPolyTp.comp s[j].uvPolyTp).p s[max i j].tp (s.Sig ilen jlen)

Equations

• ⋯ = ⋯

def NaturalModelBase.UHomSeqPiSigma.mkSigma {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma ilen jlen A B = CategoryTheory.CategoryStruct.comp (s[i].Ptp_equiv.symm ⟨A, B⟩) (s.Sig ilen jlen)

theorem NaturalModelBase.UHomSeqPiSigma.comp_mkSigma {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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.mkSigma ilen jlen A B) = s.mkSigma ilen jlen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substWk σ A)) B)

def NaturalModelBase.UHomSeqPiSigma.mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 (NaturalModelBase.compDomEquiv.mk s[j] t (⋯ ▸ B) u ⋯) (s.pair ilen jlen)

theorem NaturalModelBase.UHomSeqPiSigma.comp_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) t) ⋯ (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) u) ⋯

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkPair_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma ilen jlen A B

def NaturalModelBase.UHomSeqPiSigma.mkFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[i].Tm

Equations

• s.mkFst ilen jlen A B p p_tp = NaturalModelBase.compDomEquiv.fst s[j] (⋯.lift p (s[i].Ptp_equiv.symm ⟨A, B⟩) p_tp)

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkFst_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma ilen jlen A B) : CategoryTheory.CategoryStruct.comp (s.mkFst ilen jlen A B p p_tp) s[i].tp = A

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkFst_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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 NaturalModelBase.UHomSeqPiSigma.comp_mkFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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.mkSigma 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)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) p) ⋯

def NaturalModelBase.UHomSeqPiSigma.mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[j].Tm

Equations

• s.mkSnd ilen jlen A B p p_tp = NaturalModelBase.compDomEquiv.snd s[j] (⋯.lift p (s[i].Ptp_equiv.symm ⟨A, B⟩) p_tp)

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkSnd_mkPair {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkSnd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma 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 NaturalModelBase.UHomSeqPiSigma.comp_mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Δ Γ : 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.mkSigma 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)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) p) ⋯

@[simp]

theorem NaturalModelBase.UHomSeqPiSigma.mkPair_mkFst_mkSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.CartesianMonoidalCategory Ctx] (s : UHomSeqPiSigma Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {Γ : 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.mkSigma 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