def tacticSimp_part_ : Lean.ParserDescr

Equations

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

Extension sequences

inductive NaturalModelBase.UHomSeq.ExtSeq {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] (s : UHomSeq 𝒞) (Γ : 𝒞) : 𝒞 → Type u

s.ExtSeq Γ Γ' is a diff from the semantic context Γ to Γ', where Γ is a prefix of Γ'. It witnesses a sequence of context extension operations in s that built Γ' on top of Γ. We write Γ ≤ Γ'.

• nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ : 𝒞} : s.ExtSeq Γ Γ
• snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} {l : ℕ} (d : s.ExtSeq Γ Γ') (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ' ⟶ s[l].Ty) : s.ExtSeq Γ (s[l].ext A)

def NaturalModelBase.UHomSeq.ExtSeq.length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} : s.ExtSeq Γ Γ' → ℕ

Equations

• NaturalModelBase.UHomSeq.ExtSeq.nil.length = 0
• (d.snoc llen A).length = d.length + 1

def NaturalModelBase.UHomSeq.ExtSeq.append {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ₁ Γ₂ Γ₃ : 𝒞} : s.ExtSeq Γ₁ Γ₂ → s.ExtSeq Γ₂ Γ₃ → s.ExtSeq Γ₁ Γ₃

Equations

• x✝.append NaturalModelBase.UHomSeq.ExtSeq.nil = x✝
• x✝.append (e.snoc llen A) = (x✝.append e).snoc llen A

theorem NaturalModelBase.UHomSeq.ExtSeq.append_assoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ₁ Γ₂ Γ₃ Γ₄ : 𝒞} (d₁ : s.ExtSeq Γ₁ Γ₂) (d₂ : s.ExtSeq Γ₂ Γ₃) (d₃ : s.ExtSeq Γ₃ Γ₄) : d₁.append (d₂.append d₃) = (d₁.append d₂).append d₃

def NaturalModelBase.UHomSeq.ExtSeq.disp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} : s.ExtSeq Γ Γ' → (Γ' ⟶ Γ)

The composite display map associated to a sequence.

Equations

• NaturalModelBase.UHomSeq.ExtSeq.nil.disp = CategoryTheory.CategoryStruct.id Γ
• (d.snoc llen A).disp = CategoryTheory.CategoryStruct.comp (s[l].disp A) d.disp

def NaturalModelBase.UHomSeq.ExtSeq.substWk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) : s.ExtSeq Γ Γ' → (Δ' : 𝒞) × s.ExtSeq Δ Δ' × (Δ' ⟶ Γ')

Weaken a substitution and its domain by an extension sequence.

Δ ⊢ σ : Γ  d : Γ ≤ Γ'
-----------------------------
Δ ≤ Δ.d[σ]  Δ.d[σ] ⊢ σ.d : Γ'

where

Δ ⊢ σ : Γ  d : Γ ≤ Γ.Aₙ.….A₁
-----------------------------
Δ.d[σ] ≡ Δ.Aₙ[σ].….A₁[⋯]

Equations

• One or more equations did not get rendered due to their size.
• NaturalModelBase.UHomSeq.ExtSeq.substWk σ NaturalModelBase.UHomSeq.ExtSeq.nil = ⟨Δ, (NaturalModelBase.UHomSeq.ExtSeq.nil, σ)⟩

@[simp]

theorem NaturalModelBase.UHomSeq.ExtSeq.substWk_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') : (substWk σ d).snd.1.length = d.length

theorem NaturalModelBase.UHomSeq.ExtSeq.substWk_disp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') : CategoryTheory.CategoryStruct.comp (substWk σ d).snd.2 d.disp = CategoryTheory.CategoryStruct.comp (substWk σ d).snd.1.disp σ

def NaturalModelBase.UHomSeq.ExtSeq.var {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} {l : ℕ} (llen : l < s.length + 1) : s.ExtSeq Γ Γ' → ℕ → Part (CategoryTheory.yoneda.obj Γ' ⟶ s[l].Tm)

Γ.Aₖ.….A₀ ⊢ vₙ : Aₙ[↑ⁿ⁺¹]

Equations

• One or more equations did not get rendered due to their size.
• NaturalModelBase.UHomSeq.ExtSeq.var llen NaturalModelBase.UHomSeq.ExtSeq.nil x✝ = Part.none
• NaturalModelBase.UHomSeq.ExtSeq.var llen (d.snoc llen_1 A) n.succ = do let v ← NaturalModelBase.UHomSeq.ExtSeq.var llen d n pure (s[l'].wk A v)

def NaturalModelBase.UHomSeq.ExtSeq.tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} {l : ℕ} (llen : l < s.length + 1) : s.ExtSeq Γ Γ' → ℕ → Part (CategoryTheory.yoneda.obj Γ' ⟶ s[l].Ty)

Γ.Aₖ.….A₀ ⊢ Aₙ[↑ⁿ⁺¹]

Equations

• One or more equations did not get rendered due to their size.
• NaturalModelBase.UHomSeq.ExtSeq.tp llen NaturalModelBase.UHomSeq.ExtSeq.nil x✝ = Part.none
• NaturalModelBase.UHomSeq.ExtSeq.tp llen (d.snoc llen_1 A) n.succ = do let v ← NaturalModelBase.UHomSeq.ExtSeq.tp llen d n pure (s[l'].wk A v)

theorem NaturalModelBase.UHomSeq.ExtSeq.var_tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} {l : ℕ} (d : s.ExtSeq Γ Γ') (llen : l < s.length + 1) (n : ℕ) : Part.map (fun (x : CategoryTheory.yoneda.obj Γ' ⟶ s[l].Tm) => CategoryTheory.CategoryStruct.comp x s[l].tp) (ExtSeq.var llen d n) = ExtSeq.tp llen d n

theorem NaturalModelBase.UHomSeq.ExtSeq.var_eq_of_lt_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {l i : ℕ} {llen : l < s.length + 1} {sΓ sΓ' sΓ'' : 𝒞} (d : s.ExtSeq sΓ sΓ') (e : s.ExtSeq sΓ' sΓ'') : i < e.length → ExtSeq.var llen (d.append e) i = ExtSeq.var llen e i

theorem NaturalModelBase.UHomSeq.ExtSeq.var_append_add_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {l i : ℕ} {llen : l < s.length + 1} {sΓ sΓ' sΓ'' : 𝒞} (d : s.ExtSeq sΓ sΓ') (e : s.ExtSeq sΓ' sΓ'') : ExtSeq.var llen (d.append e) (i + e.length) = Part.map (fun (x : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Tm) => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map e.disp) x) (ExtSeq.var llen d i)

theorem NaturalModelBase.UHomSeq.ExtSeq.var_substWk_add_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {l i : ℕ} {llen : l < s.length + 1} {sΔ sΔ' sΓ sΓ' : 𝒞} (d : s.ExtSeq sΔ sΔ') (σ : sΔ' ⟶ sΓ) (e : s.ExtSeq sΓ sΓ') : match substWk σ e with | ⟨fst, (d', snd)⟩ => ExtSeq.var llen (d.append d') (i + e.length) = Part.map (fun (x : CategoryTheory.yoneda.obj sΔ' ⟶ s[l].Tm) => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map d'.disp) x) (ExtSeq.var llen d i)

theorem NaturalModelBase.UHomSeq.ExtSeq.var_substWk_of_lt_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {l i : ℕ} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') (llen : l < s.length + 1) {st : CategoryTheory.yoneda.obj Γ' ⟶ s[l].Tm} (st_mem : st ∈ ExtSeq.var llen d i) : i < d.length → CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (substWk σ d).snd.2) st ∈ ExtSeq.var llen (substWk σ d).snd.1 i

theorem NaturalModelBase.UHomSeq.ExtSeq.mem_var_liftVar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} {l : ℕ} {llen : l < s.length + 1} {sΓ sΓ' sΓ'' sΘ : 𝒞} {st : CategoryTheory.yoneda.obj sΓ'' ⟶ s[l].Tm} (i : ℕ) (c : s.ExtSeq sΓ sΓ') (d : s.ExtSeq sΓ' sΘ) (e : s.ExtSeq sΓ' sΓ'') (st_mem : st ∈ ExtSeq.var llen (c.append e) i) : match substWk d.disp e with | ⟨fst, (d', σ)⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) st ∈ ExtSeq.var llen ((c.append d).append d') (liftVar d.length i e.length)

Contextual objects

def NaturalModelBase.UHomSeq.CObj {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] (s : UHomSeq 𝒞) : Type u

A "contextual" object (as in Cartmell's contextual categories), i.e., one of the form 1.Aₙ₋₁.….A₀, together with the extension sequence [Aₙ₋₁ :: … :: A₀].

This kind of object can be destructured.

Equations

• s.CObj = ((Γ : 𝒞) × s.ExtSeq (⊤_ 𝒞) Γ)

def NaturalModelBase.UHomSeq.nilCObj {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] (s : UHomSeq 𝒞) : s.CObj

Equations

• s.nilCObj = ⟨⊤_ 𝒞, NaturalModelBase.UHomSeq.ExtSeq.nil⟩

def NaturalModelBase.UHomSeq.CObj.snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) : s.CObj

Equations

• Γ.snoc llen A = ⟨s[l].ext A, Γ.snd.snoc llen A⟩

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.snoc_fst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) : (Γ.snoc llen A).fst = s[l].ext A

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.snoc_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) : (Γ.snoc llen A).snd = Γ.snd.snoc llen A

def NaturalModelBase.UHomSeq.CObj.append {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') : s.CObj

Equations

• Γ.append d = ⟨sΓ', Γ.snd.append d⟩

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.append_fst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') : (Γ.append d).fst = sΓ'

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.append_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') : (Γ.append d).snd = Γ.snd.append d

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.append_nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} (Γ : s.CObj) : Γ.append ExtSeq.nil = Γ

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.append_snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} {l : ℕ} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Ty) : Γ.append (d.snoc llen A) = (Γ.append d).snoc llen A

def NaturalModelBase.UHomSeq.CObj.substWk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ sΓ' : 𝒞} (Δ : s.CObj) (σ : Δ.fst ⟶ sΓ) (d : s.ExtSeq sΓ sΓ') : (Δ' : s.CObj) × (Δ'.fst ⟶ sΓ')

Equations

• Δ.substWk σ d = match NaturalModelBase.UHomSeq.ExtSeq.substWk σ d with | ⟨Δ', (d', σ')⟩ => ⟨⟨Δ', Δ.snd.append d'⟩, σ'⟩

@[simp]

theorem NaturalModelBase.UHomSeq.CObj.substWk_nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ : 𝒞} (Δ : s.CObj) (σ : Δ.fst ⟶ sΓ) : Δ.substWk σ ExtSeq.nil = ⟨Δ, σ⟩

theorem NaturalModelBase.UHomSeq.CObj.substWk_snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ sΓ' : 𝒞} {l : ℕ} (Δ : s.CObj) (σ : Δ.fst ⟶ sΓ) (d : s.ExtSeq sΓ sΓ') (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Ty) : Δ.substWk σ (d.snoc llen A) = match Δ.substWk σ d with | ⟨Δ', σ'⟩ => ⟨Δ'.snoc llen (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ') A), s[l].substWk σ' A⟩

def NaturalModelBase.UHomSeq.CObj.var {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (i : ℕ) : Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)

Equations

• Γ.var llen i = NaturalModelBase.UHomSeq.ExtSeq.var llen Γ.snd i

def NaturalModelBase.UHomSeq.CObj.tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (i : ℕ) : Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)

Equations

• Γ.tp llen i = NaturalModelBase.UHomSeq.ExtSeq.tp llen Γ.snd i

theorem NaturalModelBase.UHomSeq.CObj.var_tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (i : ℕ) : Part.map (fun (x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm) => CategoryTheory.CategoryStruct.comp x s[l].tp) (Γ.var llen i) = Γ.tp llen i

theorem NaturalModelBase.UHomSeq.CObj.mem_var_liftVar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] [CategoryTheory.Limits.HasTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} {llen : l < s.length + 1} {sΓ : s.CObj} {sΘ sΓ' : 𝒞} {st : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Tm} (i : ℕ) (d : s.ExtSeq sΓ.fst sΘ) (e : s.ExtSeq sΓ.fst sΓ') (st_mem : st ∈ (sΓ.append e).var llen i) : match (sΓ.append d).substWk d.disp e with | ⟨sΔ, σ⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) st ∈ sΔ.var llen (liftVar d.length i e.length)

theorem NaturalModelBase.UHomSeq.lt_slen_of_eqTp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeq 𝒞} (slen : univMax ≤ s.length) {Γ : Ctx} {A B : Expr} {l : ℕ} : Γ ⊢[l] A ≡ B → l < s.length + 1

Interpretation

def NaturalModelBase.UHomSeqPis.ofType {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} (Γ : s.CObj) (l : ℕ) : Expr → (x : autoParam (l < s.length + 1) _auto✝) → Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)

def NaturalModelBase.UHomSeqPis.ofTerm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} (Γ : s.CObj) (l : ℕ) : Expr → (x : autoParam (l < s.length + 1) _auto✝) → Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)

Equations

• One or more equations did not get rendered due to their size.
• NaturalModelBase.UHomSeqPis.ofTerm Γ l (Expr.bvar i) x = Γ.var x i
• NaturalModelBase.UHomSeqPis.ofTerm Γ l t.code x = Part.assert (0 < l) fun (lpos : 0 < l) => do let A ← NaturalModelBase.UHomSeqPis.ofType Γ (l - 1) t ⋯ pure (cast ⋯ (s.code ⋯ A))
• NaturalModelBase.UHomSeqPis.ofTerm Γ l x x_1 = Part.none

def NaturalModelBase.UHomSeqPis.ofCtx {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] (s : UHomSeqPis 𝒞) : Ctx → Part s.CObj

Equations

• One or more equations did not get rendered due to their size.
• s.ofCtx [] = pure s.nilCObj

theorem NaturalModelBase.UHomSeqPis.snoc_mem_ofCtx {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {Γ : Ctx} {A : Expr} {l : ℕ} {llen : l < s.length + 1} {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Ty} : sΓ ∈ s.ofCtx Γ → sA ∈ ofType sΓ l A llen → sΓ.snoc llen sA ∈ s.ofCtx ((A, l) :: Γ)

Admissibility of thinning

theorem NaturalModelBase.UHomSeqPis.mem_ofType_liftN {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {A : Expr} {l : ℕ} {llen : l < s.length + 1} {sΓ : s.CObj} {sΘ sΓ' : 𝒞} {sA : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Ty} (d : s.ExtSeq sΓ.fst sΘ) (e : s.ExtSeq sΓ.fst sΓ') (sA_mem : sA ∈ ofType (sΓ.append e) l A llen) : match (sΓ.append d).substWk d.disp e with | ⟨sΔ, σ⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) sA ∈ ofType sΔ l (Expr.liftN d.length A e.length) llen

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_liftN {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {t : Expr} {l : ℕ} {llen : l < s.length + 1} {sΓ : s.CObj} {sΘ sΓ' : 𝒞} {st : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Tm} (d : s.ExtSeq sΓ.fst sΘ) (e : s.ExtSeq sΓ.fst sΓ') (st_mem : st ∈ ofTerm (sΓ.append e) l t llen) : match (sΓ.append d).substWk d.disp e with | ⟨sΔ, σ⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) st ∈ ofTerm sΔ l (Expr.liftN d.length t e.length) llen

theorem NaturalModelBase.UHomSeqPis.mem_ofType_lift {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {A : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Ty} (sB : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l'].Ty) (sA_mem : sA ∈ ofType sΓ l A llen) : s[l'].wk sB sA ∈ ofType (sΓ.snoc l'len sB) l A.lift llen

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_lift {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {t : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {st : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Tm} (sB : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l'].Ty) (st_mem : st ∈ ofTerm sΓ l t llen) : s[l'].wk sB st ∈ ofTerm (sΓ.snoc l'len sB) l t.lift llen

Admissibility of instantiation

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_instVar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {a : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sΓ' : 𝒞} {st : CategoryTheory.yoneda.obj sΓ' ⟶ s[l].Tm} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l'].Tm} (i : ℕ) (sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l'].Ty) (d : s.ExtSeq (s[l'].ext sA) sΓ') (st_mem : st ∈ ((sΓ.snoc l'len sA).append d).var llen i) (sa_mem : sa ∈ ofTerm sΓ l' a l'len) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[l'].tp = sA) : let σ := s[l'].substCons (CategoryTheory.CategoryStruct.id sΓ.fst) sA sa ⋯; match sΓ.substWk σ d with | ⟨sΔ, σ'⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ') st ∈ ofTerm sΔ l (instVar i a d.length) llen

theorem NaturalModelBase.UHomSeqPis.mem_ofType_inst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {B a : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sΓ' : 𝒞} {sB : CategoryTheory.yoneda.obj sΓ' ⟶ s[l'].Ty} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Tm} (sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Ty) (d : s.ExtSeq (sΓ.snoc llen sA).fst sΓ') (sB_mem : sB ∈ ofType ((sΓ.snoc llen sA).append d) l' B l'len) (sa_mem : sa ∈ ofTerm sΓ l a llen) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[l].tp = sA) : let σ := s[l].substCons (CategoryTheory.CategoryStruct.id sΓ.fst) sA sa ⋯; match sΓ.substWk σ d with | ⟨sΔ, σ'⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ') sB ∈ ofType sΔ l' (B.inst a d.length) l'len

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_inst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {t a : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sΓ' : 𝒞} {st : CategoryTheory.yoneda.obj sΓ' ⟶ s[l'].Tm} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Tm} (sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Ty) (d : s.ExtSeq (sΓ.snoc llen sA).fst sΓ') (st_mem : st ∈ ofTerm ((sΓ.snoc llen sA).append d) l' t l'len) (sa_mem : sa ∈ ofTerm sΓ l a llen) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[l].tp = sA) : let σ := s[l].substCons (CategoryTheory.CategoryStruct.id sΓ.fst) sA sa ⋯; match sΓ.substWk σ d with | ⟨sΔ, σ'⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ') st ∈ ofTerm sΔ l' (t.inst a d.length) l'len

theorem NaturalModelBase.UHomSeqPis.mem_ofType_inst0 {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {B a : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s.toUHomSeq[l].Ty} {sB : CategoryTheory.yoneda.obj (sΓ.snoc llen sA).fst ⟶ s[l'].Ty} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Tm} (sB_mem : sB ∈ ofType (sΓ.snoc llen sA) l' B l'len) (sa_mem : sa ∈ ofTerm sΓ l a llen) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[l].tp = sA) : s[l].inst sA sB sa sa_tp ∈ ofType sΓ l' (B.inst a) l'len

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_inst0 {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {t a : Expr} {l l' : ℕ} {llen : l < s.length + 1} {l'len : l' < s.length + 1} {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s.toUHomSeq[l].Ty} {st : CategoryTheory.yoneda.obj (sΓ.snoc llen sA).fst ⟶ s[l'].Tm} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Tm} (st_mem : st ∈ ofTerm (sΓ.snoc llen sA) l' t l'len) (sa_mem : sa ∈ ofTerm sΓ l a llen) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[l].tp = sA) : s[l].inst sA st sa sa_tp ∈ ofTerm sΓ l' (t.inst a) l'len

Soundness of interpretation

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_app {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {B f a : Expr} {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i].Ty} {sB : CategoryTheory.yoneda.obj (sΓ.snoc ilen sA).fst ⟶ s[j].Ty} {sf : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i ⊔ j].Tm} {sa : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i].Tm} (sB_mem : sB ∈ ofType (sΓ.snoc ilen sA) j B jlen) (sf_mem : sf ∈ ofTerm sΓ (i ⊔ j) f ⋯) (sf_tp : CategoryTheory.CategoryStruct.comp sf s[i ⊔ j].tp = s.mkPi ilen jlen sA sB) (sa_mem : sa ∈ ofTerm sΓ i a ilen) (sa_tp : CategoryTheory.CategoryStruct.comp sa s[i].tp = sA) : s.mkApp ilen jlen sA sB sf sf_tp sa sa_tp ∈ ofTerm sΓ j (Expr.app i j B f a) jlen

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_lam {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {A t : Expr} {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i].Ty} {st : CategoryTheory.yoneda.obj (sΓ.snoc ilen sA).fst ⟶ s[j].Tm} (sA_mem : sA ∈ ofType sΓ i A ilen) (st_mem : st ∈ ofTerm (sΓ.snoc ilen sA) j t jlen) : s.mkLam ilen jlen sA st ∈ ofTerm sΓ (i ⊔ j) (Expr.lam i j A t) ⋯

theorem NaturalModelBase.UHomSeqPis.mem_ofTerm_etaExpand {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} {A B f : Expr} {i j : ℕ} (ilen : i < s.length + 1) (jlen : j < s.length + 1) {sΓ : s.CObj} {sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i].Ty} {sB : CategoryTheory.yoneda.obj (sΓ.snoc ilen sA).fst ⟶ s[j].Ty} {sf : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[i ⊔ j].Tm} (sA_mem : sA ∈ ofType sΓ i A ilen) (sB_mem : sB ∈ ofType (sΓ.snoc ilen sA) j B jlen) (sf_mem : sf ∈ ofTerm sΓ (i ⊔ j) f ⋯) (sf_tp : CategoryTheory.CategoryStruct.comp sf s[i ⊔ j].tp = s.mkPi ilen jlen sA sB) : s.etaExpand ilen jlen sA sB sf sf_tp ∈ ofTerm sΓ (i ⊔ j) (Expr.lam i j A (Expr.app i j (Expr.liftN 1 B 1) f.lift (Expr.bvar 0))) ⋯

theorem NaturalModelBase.UHomSeqPis.ofType_ofTerm_sound {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenFiniteProducts 𝒞] {s : UHomSeqPis 𝒞} (slen : univMax ≤ s.length) : (∀ {Γ : Ctx} {l : ℕ} {A B : Expr} (Aeq : Γ ⊢[l] A ≡ B) {sΓ : s.CObj}, sΓ ∈ s.ofCtx Γ → let_fun llen := ⋯; ∃ sA ∈ ofType sΓ l A llen, sA ∈ ofType sΓ l B llen) ∧ ∀ {Γ : Ctx} {l : ℕ} {t u A : Expr} (teq : Γ ⊢[l] t ≡ u : A) {sΓ : s.CObj}, sΓ ∈ s.ofCtx Γ → let_fun llen := ⋯; ∃ sA ∈ ofType sΓ l A llen, ∃ st ∈ ofTerm sΓ l t llen, st ∈ ofTerm sΓ l u llen ∧ CategoryTheory.CategoryStruct.comp st s[l].tp = sA