Morphisms of natural models, and Russell-universe embeddings.

def NaturalModelBase.isTerminal_yUnit {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] : CategoryTheory.Limits.IsTerminal (CategoryTheory.yoneda.obj (𝟙_ Ctx))

Equations

• NaturalModelBase.isTerminal_yUnit = CategoryTheory.Limits.IsTerminal.isTerminalObj CategoryTheory.yoneda (𝟙_ Ctx) (CategoryTheory.Limits.IsTerminal.ofUnique (𝟙_ Ctx))

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.ChosenFiniteProducts Ctx] (M N : NaturalModelBase Ctx) extends M.Hom N : Type u

A Russell 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.

• 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 (𝟙_ 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.ChosenFiniteProducts Ctx] {M N : NaturalModelBase Ctx} (H : M.Hom N) {U : CategoryTheory.yoneda.obj (𝟙_ 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts Ctx] (M : NaturalModelBase Ctx) (U : CategoryTheory.yoneda.obj (𝟙_ 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 := ⋯ }

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

A sequence of Russell 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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)

def NaturalModelBase.UHomSeq.el {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts 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) ⋯

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

The data of Π and λ term formers for every i, j ≤ length + 1, interpreting

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

and

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

This amounts to O(length²) data. One might object that the same formation rules could be modeled with O(length) data: etc etc

However, with O(length²) data we can use Lean's own type formers directly, rather than using Π (ULift A) (ULift B). The interpretations of types are thus more direct.

• length : ℕ
• objs (i : ℕ) (h : i < self.length + 1) : NaturalModelBase Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)
• Pis' (i : ℕ) (ilen : i < self.length + 1) : self.toUHomSeq[i].NaturalModelPi

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

• length : ℕ
• objs (i : ℕ) (h : i < self.length + 1) : NaturalModelBase Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)
• Sigmas' (i : ℕ) (ilen : i < self.length + 1) : self.toUHomSeq[i].NaturalModelSigma

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

Equations

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

@[simp]

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

def NaturalModelBase.UHomSeqPis.Pis {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : s[i].Ptp.obj s[i].Ty ⟶ s[i].Ty

Equations

• s.Pis i ilen = (s.Pis' i ilen).Pi

def NaturalModelBase.UHomSeqPis.lams {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : s[i].Ptp.obj s[i].Tm ⟶ s[i].Tm

Equations

• s.lams i ilen = (s.Pis' i ilen).lam

def NaturalModelBase.UHomSeqPis.Pi_pbs {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) (i : ℕ) (ilen : i < s.length + 1 := by get_elem_tactic) : CategoryTheory.IsPullback (s.lams i ilen) (s[i].Ptp.map s[i].tp) s[i].tp (s.Pis i ilen)

Equations

• ⋯ = ⋯

def NaturalModelBase.UHomSeqPis.PisPoly {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].Ptp.obj s[j].Ty ⟶ s[i ⊔ j].Ty

Equations

• s.PisPoly ilen jlen = CategoryTheory.CategoryStruct.comp sorry (s.Pis (i ⊔ j) ⋯)

def NaturalModelBase.UHomSeqPis.lamsPoly {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : s[i].Ptp.obj s[j].Tm ⟶ s[i ⊔ j].Tm

Equations

• s.lamsPoly ilen jlen = sorry

def NaturalModelBase.UHomSeqPis.PisPoly_pbs {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis Ctx) {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) : CategoryTheory.IsPullback (s.lamsPoly ilen jlen) (s[i].Ptp.map s[j].tp) s[i ⊔ j].tp (s.PisPoly ilen jlen)

Equations

• ⋯ = ⋯

def NaturalModelBase.UHomSeqPis.mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Ty

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

Equations

• s.mkPi ilen jlen A B = CategoryTheory.CategoryStruct.comp (s[i].Ptp_equiv ⟨A, B⟩) (s.PisPoly ilen jlen)

theorem NaturalModelBase.UHomSeqPis.comp_mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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.UHomSeqPis.mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[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 ⟨A, t⟩) (s.lamsPoly ilen jlen)

@[simp]

theorem NaturalModelBase.UHomSeqPis.mkLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].tp = s.mkPi ilen jlen A B

theorem NaturalModelBase.UHomSeqPis.comp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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.UHomSeqPis.unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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.symm (⋯.lift f (s[i].Ptp_equiv ⟨A, B⟩) f_tp)).snd

@[simp]

theorem NaturalModelBase.UHomSeqPis.unLam_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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.UHomSeqPis.mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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 = s[i].inst A (s.unLam ilen jlen A B f f_tp) a a_tp

@[simp]

theorem NaturalModelBase.UHomSeqPis.mkApp_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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 = s[i].inst A B a a_tp

theorem NaturalModelBase.UHomSeqPis.comp_mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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.UHomSeqPis.mkLam_unLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[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.UHomSeqPis.unLam_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[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.UHomSeqPis.etaExpand {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[i ⊔ j].tp = s.mkPi ilen jlen A B) : CategoryTheory.yoneda.obj Γ ⟶ s[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.UHomSeqPis.etaExpand_eq {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[i ⊔ j].Tm) (f_tp : CategoryTheory.CategoryStruct.comp f s[i ⊔ j].tp = s.mkPi ilen jlen A B) : s.etaExpand ilen jlen A B f f_tp = f

@[simp]

theorem NaturalModelBase.UHomSeqPis.mkApp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.ChosenFiniteProducts Ctx] (s : UHomSeqPis 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[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 = s[i].inst A t a a_tp

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