GroupoidModel.Syntax.Interpretation

Equations

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

Instances For

Universe level bound helpers #

theorem EqTp.lt_slen {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : NaturalModel.Universe.UHomSeq 𝒞} (slen : univMax ≤ s.length) {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] A ≡ B) :

l < s.length + 1

source

theorem WfTp.lt_slen {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : NaturalModel.Universe.UHomSeq 𝒞} (slen : univMax ≤ s.length) {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] A) :

l < s.length + 1

source

theorem EqTm.lt_slen {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : NaturalModel.Universe.UHomSeq 𝒞} (slen : univMax ≤ s.length) {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t ≡ u : A) :

l < s.length + 1

source

theorem WfTm.lt_slen {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : NaturalModel.Universe.UHomSeq 𝒞} (slen : univMax ≤ s.length) {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t : A) :

l < s.length + 1

Extension sequences #

source

inductive NaturalModel.Universe.UHomSeq.ExtSeq {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] (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.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ : 𝒞} : s.ExtSeq Γ Γ
snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} {l : ℕ} (d : s.ExtSeq Γ Γ') (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ' ⟶ s[l].Ty) : s.ExtSeq Γ (s[l].ext A)

Instances For

source

def NaturalModel.Universe.UHomSeq.ExtSeq.length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} :

s.ExtSeq Γ Γ' → ℕ

Equations

NaturalModel.Universe.UHomSeq.ExtSeq.nil.length = 0
(d.snoc llen A).length = d.length + 1

Instances For

source

def NaturalModel.Universe.UHomSeq.ExtSeq.append {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ₁ Γ₂ Γ₃ : 𝒞} :

s.ExtSeq Γ₁ Γ₂ → s.ExtSeq Γ₂ Γ₃ → s.ExtSeq Γ₁ Γ₃

Equations

x✝.append NaturalModel.Universe.UHomSeq.ExtSeq.nil = x✝
x✝.append (e.snoc llen A) = (x✝.append e).snoc llen A

Instances For

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.append_assoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ₁ Γ₂ Γ₃ Γ₄ : 𝒞} (d₁ : s.ExtSeq Γ₁ Γ₂) (d₂ : s.ExtSeq Γ₂ Γ₃) (d₃ : s.ExtSeq Γ₃ Γ₄) :

d₁.append (d₂.append d₃) = (d₁.append d₂).append d₃

source

def NaturalModel.Universe.UHomSeq.ExtSeq.disp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ Γ' : 𝒞} :

s.ExtSeq Γ Γ' → (Γ' ⟶ Γ)

The composite display map associated to a sequence.

Equations

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

Instances For

source

def NaturalModel.Universe.UHomSeq.ExtSeq.substWk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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.
NaturalModel.Universe.UHomSeq.ExtSeq.substWk σ NaturalModel.Universe.UHomSeq.ExtSeq.nil = ⟨Δ, (NaturalModel.Universe.UHomSeq.ExtSeq.nil , σ)⟩

Instances For

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.ExtSeq.substWk_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') :

(substWk σ d).snd.1.length = d.length

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.substWk_disp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') :

CategoryTheory.CategoryStruct.comp (substWk σ d).snd.2 d.disp = CategoryTheory.CategoryStruct.comp (substWk σ d).snd.1.disp σ

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.substWk_disp_functor_map {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') {D : Type _uniq.17897} [CategoryTheory.Category.{_uniq.17896, _uniq.17897} D] (F : CategoryTheory.Functor 𝒞 D) :

CategoryTheory.CategoryStruct.comp (F.map (substWk σ d).snd.2) (F.map d.disp) = CategoryTheory.CategoryStruct.comp (F.map (substWk σ d).snd.1.disp) (F.map σ)

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.substWk_disp_assoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') {Z : 𝒞} (h : Γ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (substWk σ d).snd.2 (CategoryTheory.CategoryStruct.comp d.disp h) = CategoryTheory.CategoryStruct.comp (substWk σ d).snd.1.disp (CategoryTheory.CategoryStruct.comp σ h)

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.substWk_disp_functor_map_assoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Δ Γ Γ' : 𝒞} (σ : Δ ⟶ Γ) (d : s.ExtSeq Γ Γ') {D : Type _uniq.17897} [CategoryTheory.Category.{_uniq.17896, _uniq.17897} D] (F : CategoryTheory.Functor 𝒞 D) {Z : D} (h : F.obj Γ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (substWk σ d).snd.2) (CategoryTheory.CategoryStruct.comp (F.map d.disp) h) = CategoryTheory.CategoryStruct.comp (F.map (substWk σ d).snd.1.disp) (CategoryTheory.CategoryStruct.comp (F.map σ) h)

source

def NaturalModel.Universe.UHomSeq.ExtSeq.var {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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.
NaturalModel.Universe.UHomSeq.ExtSeq.var llen NaturalModel.Universe.UHomSeq.ExtSeq.nil x✝ = Part.none

Instances For

source

def NaturalModel.Universe.UHomSeq.ExtSeq.tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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.
NaturalModel.Universe.UHomSeq.ExtSeq.tp llen NaturalModel.Universe.UHomSeq.ExtSeq.nil x✝ = Part.none

Instances For

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.var_tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.var_eq_of_lt_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.var_append_add_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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)

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.var_substWk_add_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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)

source

theorem NaturalModel.Universe.UHomSeq.ExtSeq.var_substWk_of_lt_length {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

Contextual objects #

source

def NaturalModel.Universe.UHomSeq.CObj {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] (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 CategoryTheory.ChosenTerminal.terminal Γ)

Instances For

source

def NaturalModel.Universe.UHomSeq.nilCObj {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] (s : UHomSeq 𝒞) :

s.CObj

Equations

s.nilCObj = ⟨CategoryTheory.ChosenTerminal.terminal, NaturalModel.Universe.UHomSeq.ExtSeq.nil ⟩

Instances For

source

def NaturalModel.Universe.UHomSeq.CObj.snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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⟩

Instances For

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.snoc_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.snoc_fst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

source

def NaturalModel.Universe.UHomSeq.CObj.append {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') :

s.CObj

Equations

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

Instances For

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.append_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') :

(Γ.append d).snd = Γ.snd.append d

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.append_fst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ' : 𝒞} (Γ : s.CObj) (d : s.ExtSeq Γ.fst sΓ') :

(Γ.append d).fst = sΓ'

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.append_nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} (Γ : s.CObj) :

Γ.append ExtSeq.nil = Γ

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.append_snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

source

def NaturalModel.Universe.UHomSeq.CObj.substWk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ sΓ' : 𝒞} (Δ : s.CObj) (σ : Δ.fst ⟶ sΓ) (d : s.ExtSeq sΓ sΓ') :

(Δ' : s.CObj) × (Δ'.fst ⟶ sΓ')

Equations

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

Instances For

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.substWk_nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {sΓ : 𝒞} (Δ : s.CObj) (σ : Δ.fst ⟶ sΓ) :

Δ.substWk σ ExtSeq.nil = ⟨Δ, σ⟩

source

theorem NaturalModel.Universe.UHomSeq.CObj.substWk_snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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 (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ') A) ⋯⟩

source

def NaturalModel.Universe.UHomSeq.CObj.var {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (i : ℕ) :

Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)

Equations

Γ.var llen i = NaturalModel.Universe.UHomSeq.ExtSeq.var llen Γ.snd i

Instances For

source

def NaturalModel.Universe.UHomSeq.CObj.tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {l : ℕ} (Γ : s.CObj) (llen : l < s.length + 1) (i : ℕ) :

Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)

Equations

Γ.tp llen i = NaturalModel.Universe.UHomSeq.ExtSeq.tp llen Γ.snd i

Instances For

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.mem_var_zero {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ : s.CObj} {l' : ℕ} {l'len : l' < s.length + 1} {A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {l : ℕ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj (Γ.snoc l'len A).fst ⟶ s[l].Tm} :

x ∈ (Γ.snoc l'len A).var llen 0 ↔ ∃ (l'l : l' = l), x = Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj (Γ.snoc l'len A).fst ⟶ s[l].Tm} → CategoryTheory.yoneda.obj (Γ.snoc l'len A).fst ⟶ s[l].Tm) (fun {llen : l' < s.length + 1} {x : CategoryTheory.yoneda.obj (Γ.snoc l'len A).fst ⟶ s[l'].Tm} => s[l'].var A) l'l

source

@[simp]

theorem NaturalModel.Universe.UHomSeq.CObj.mem_var_succ {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {Γ : s.CObj} {l' : ℕ} {l'len : l' < s.length + 1} {A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {l i : ℕ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj (Γ.snoc l'len A).fst ⟶ s[l].Tm} :

x ∈ (Γ.snoc l'len A).var llen (i + 1) ↔ ∃ a ∈ Γ.var llen i, x = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[l'].disp A)) a

source

theorem NaturalModel.Universe.UHomSeq.CObj.var_tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {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

Interpretation #

source

structure NaturalModel.Universe.Interpretation {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] (χ : Type u_1) (s : UHomSeq 𝒞) :

Type (max u u_1)

An interpretation of a signature consists of a semantic term for each named axiom. This is the semantic equivalent of Axioms χ.

ax (c : χ) (l : ℕ) (x✝ : l < s.length + 1 := by get_elem_tactic) : Option (CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ s[l].Tm)

Instances For

source

def NaturalModel.Universe.Interpretation.ofType {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : s.CObj) (l : ℕ) :

Expr χ → (x : autoParam (l < s.length + 1) _auto✝) → Part (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)

Equations

One or more equations did not get rendered due to their size.
I.ofType Γ l x x_1 = Part.none

Instances For

source

def NaturalModel.Universe.Interpretation.ofTerm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : 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.
I.ofTerm Γ l (Expr.bvar i) x = Γ.var x i
I.ofTerm Γ l (Expr.refl l_1 t) x = do let t ← I.ofTerm Γ l t x pure (s.mkRefl x t)
I.ofTerm Γ l t.code x = Part.assert (0 < l) fun (lpos : 0 < l) => do let A ← I.ofType Γ (l - 1) t ⋯ pure (cast ⋯ (s.code ⋯ A))
I.ofTerm Γ l x x_1 = Part.none

Instances For

source

def NaturalModel.Universe.Interpretation.ofCtx {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] :

Ctx χ → Part s.CObj

Equations

I.ofCtx [] = pure s.nilCObj
I.ofCtx ((A, l) :: Γ) = Part.assert (l < s.length + 1) fun (llen : l < s.length + 1) => do let sΓ ← I.ofCtx Γ let sA ← I.ofType sΓ l A llen pure (sΓ.snoc llen sA)

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofType_pi {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {A B : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} :

x ∈ I.ofType Γ l (Expr.pi i j A B) llen ↔ ∃ (lij : l = max i j), have ilen := ⋯; have jlen := ⋯; ∃ A' ∈ I.ofType Γ i A ilen, ∃ B' ∈ I.ofType (Γ.snoc ilen A') j B jlen, x = (fun (h : max i j = l) => (fun (h_1 : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Ty) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} → l = max i j → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)) (fun {llen : max i j < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Ty} (lij : max i j = max i j) => h_1) h lij) (s.mkPi ilen jlen A' B')) ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofType_sigma {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {A B : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} :

x ∈ I.ofType Γ l (Expr.sigma i j A B) llen ↔ ∃ (lij : l = max i j), have ilen := ⋯; have jlen := ⋯; ∃ A' ∈ I.ofType Γ i A ilen, ∃ B' ∈ I.ofType (Γ.snoc ilen A') j B jlen, x = (fun (h : max i j = l) => (fun (h_1 : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Ty) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} → l = max i j → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)) (fun {llen : max i j < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Ty} (lij : max i j = max i j) => h_1) h lij) (s.mkSig ilen jlen A' B')) ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofType_Id {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i : ℕ} {A a b : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} :

x ∈ I.ofType Γ l (Expr.Id i A a b) llen ↔ ∃ A' ∈ I.ofType Γ l A llen, ∃ a' ∈ I.ofTerm Γ l a llen, ∃ b' ∈ I.ofTerm Γ l b llen, ∃ (eq : CategoryTheory.CategoryStruct.comp a' s[l].tp = A') (eq' : CategoryTheory.CategoryStruct.comp b' s[l].tp = A'), x = s.mkId llen A' a' b' eq eq'

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofType_el {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l : ℕ} {t : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} :

x ∈ I.ofType Γ l t.el llen ↔ ∃ (llen_1 : l < s.length), ∃ A ∈ I.ofTerm Γ (l + 1) t ⋯, ∃ (A_tp : CategoryTheory.CategoryStruct.comp A s[l + 1].tp = UHom.wkU Γ.fst (s.homSucc l llen_1)), x = s.el llen_1 A A_tp

source

@[simp]

theorem NaturalModel.Universe.Interpretation.ofTerm_bvar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i : ℕ} {llen : l < s.length + 1} :

I.ofTerm Γ l (Expr.bvar i) llen = Γ.var llen i

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_ax {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {c : χ} {A : Expr χ} {l : ℕ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.ax c A) llen ↔ ∃ (sc : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ s[l].Tm), I.ax c l llen = some sc ∧ x = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenTerminal.isTerminal_yUnit.from (CategoryTheory.yoneda.obj Γ.fst)) sc

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_lam {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {A e : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.lam i j A e) llen ↔ ∃ (lij : l = max i j), have ilen := ⋯; have jlen := ⋯; ∃ A' ∈ I.ofType Γ i A ilen, ∃ e' ∈ I.ofTerm (Γ.snoc ilen A') j e jlen, x = (fun (h : max i j = l) => (fun (h_1 : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Tm) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} → l = max i j → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)) (fun {llen : max i j < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Tm} (lij : max i j = max i j) => h_1) h lij) (s.mkLam ilen jlen A' e')) ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_app {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {B f a : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.app i j B f a) llen ↔ ∃ (ilen : i < s.length + 1), ∃ f' ∈ I.ofTerm Γ (max i l) f ⋯, ∃ a' ∈ I.ofTerm Γ i a ilen, ∃ (A' : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp a' s[i].tp = A'), ∃ B' ∈ I.ofType (Γ.snoc ilen A') l B llen, ∃ (h : CategoryTheory.CategoryStruct.comp f' s[max i l].tp = s.mkPi ilen llen A' B'), x = s.mkApp ilen llen A' B' f' h a' eq

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_pair {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {B t u : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.pair i j B t u) llen ↔ ∃ (lij : l = max i j), have ilen := ⋯; have jlen := ⋯; ∃ t' ∈ I.ofTerm Γ i t ilen, ∃ (A' : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i].Ty) (eq : CategoryTheory.CategoryStruct.comp t' s[i].tp = A'), ∃ B' ∈ I.ofType (Γ.snoc ilen A') j B jlen, ∃ u' ∈ I.ofTerm Γ j u jlen, ∃ (u_tp : CategoryTheory.CategoryStruct.comp u' s[j].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].sec A' t' eq)) B'), x = (fun (h : max i j = l) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} → l = max i j → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)) (fun {llen : max i j < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[max i j].Tm} (lij : max i j = max i j) => s.mkPair ilen jlen A' B' t' eq u' u_tp) h lij) ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_fst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {A B p : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.fst i j A B p) llen ↔ have ilen := ⋯; ∃ (jlen : j < s.length + 1), ∃ A' ∈ I.ofType Γ l A ilen, ∃ B' ∈ I.ofType (Γ.snoc llen A') j B jlen, ∃ p' ∈ I.ofTerm Γ (max l j) p ⋯, ∃ (p_tp : CategoryTheory.CategoryStruct.comp p' s[max l j].tp = s.mkSig llen jlen A' B'), x = s.mkFst llen jlen A' B' p' p_tp

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {A B p : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.snd i j A B p) llen ↔ have llen_1 := ⋯; ∃ (ilen : i < s.length + 1), ∃ A' ∈ I.ofType Γ i A ilen, ∃ B' ∈ I.ofType (Γ.snoc ilen A') l B llen_1, ∃ p' ∈ I.ofTerm Γ (max i l) p ⋯, ∃ (p_tp : CategoryTheory.CategoryStruct.comp p' s[max i l].tp = s.mkSig ilen llen_1 A' B'), x = s.mkSnd ilen llen_1 A' B' p' p_tp

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_refl {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i : ℕ} {t : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.refl i t) llen ↔ ∃ t' ∈ I.ofTerm Γ l t llen, x = s.mkRefl llen t'

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_idRec {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i j : ℕ} {t M r u h : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l (Expr.idRec i j t M r u h) llen ↔ ∃ (ilen : i < s.length + 1), ∃ t' ∈ I.ofTerm Γ i t ilen, ∃ (A' : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i].Ty) (t_tp : CategoryTheory.CategoryStruct.comp t' s[i].tp = A') (B' : CategoryTheory.yoneda.obj (Γ.snoc ilen A').fst ⟶ 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' ∈ I.ofType ((Γ.snoc ilen A').snoc ilen B') l M llen, ∃ r' ∈ I.ofTerm Γ l r llen, ∃ (r_tp : CategoryTheory.CategoryStruct.comp r' s[l].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[i].substCons (s[i].sec A' t' t_tp) B' (s.mkRefl ilen t') ⋯)) M'), ∃ u' ∈ I.ofTerm Γ i u ilen, ∃ (u_tp : CategoryTheory.CategoryStruct.comp u' s[i].tp = A'), ∃ h' ∈ I.ofTerm Γ i h ilen, ∃ (h_tp : CategoryTheory.CategoryStruct.comp h' s[i].tp = s.mkId ilen A' t' u' t_tp u_tp), x = s.mkIdRec ilen llen A' t' t_tp B' B_eq M' r' r_tp u' u_tp h' h_tp

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_code {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l : ℕ} {t : Expr χ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} :

x ∈ I.ofTerm Γ l t.code llen ↔ ∃ (i : ℕ) (li : l = i + 1), ∃ t' ∈ I.ofType Γ i t ⋯, x = (fun (h : i + 1 = l) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} → (li : l = i + 1) → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[i].Ty) → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm)) (fun {llen : i + 1 < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i + 1].Tm} (li : i + 1 = i + 1) (t' : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i].Ty) => s.code ⋯ t') h li t') ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofType_univ {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l i : ℕ} {llen : l < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} :

x ∈ I.ofType Γ l (Expr.univ i) llen ↔ ∃ (li : l = i + 1), x = (fun (h : i + 1 = l) => Eq.ndrec (motive := fun {l : ℕ} => {llen : l < s.length + 1} → {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} → l = i + 1 → (CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty)) (fun {llen : i + 1 < s.length + 1} {x : CategoryTheory.yoneda.obj Γ.fst ⟶ s[i + 1].Ty} (li : i + 1 = i + 1) => UHom.wkU Γ.fst (s.homSucc i ⋯)) h li) ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.ofCtx_nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] :

I.ofCtx [] = ↑(some s.nilCObj)

source

@[simp]

theorem NaturalModel.Universe.Interpretation.mem_ofCtx_snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : List (Expr χ × ℕ)} {A : Expr χ} {l : ℕ} {sΓ' : s.CObj} :

sΓ' ∈ I.ofCtx ((A, l) :: Γ) ↔ ∃ sΓ ∈ I.ofCtx Γ, ∃ (llen : l < s.length + 1), ∃ sA ∈ I.ofType sΓ l A llen, sΓ' = sΓ.snoc llen sA

Semantic substitutions #

source

inductive NaturalModel.Universe.Interpretation.CSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Δ Γ : s.CObj) :

(Δ.fst ⟶ Γ.fst) → (full : optParam Bool true) → Type (max u u_1)

An inductive characterization of those semantic substitutions that appear in syntactic operations. We use this as an auxiliary device in the proof of semantic substitution admissibility.

The family with full = false characterizes renamings, whereas full = true contains general substitutions but where composition is limited to renamings on the left.

id {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : s.CObj) (full : Bool := true) : I.CSb Γ Γ (CategoryTheory.CategoryStruct.id Γ.fst) full
wk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : s.CObj} {l : ℕ} (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (full : Bool := true) : I.CSb (Γ.snoc llen A) Γ (s[l].disp A) full
comp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Θ Δ Γ : s.CObj} {σ : Θ.fst ⟶ Δ.fst} {τ : Δ.fst ⟶ Γ.fst} {full : Bool} : I.CSb Θ Δ σ false → I.CSb Δ Γ τ full → I.CSb Θ Γ (CategoryTheory.CategoryStruct.comp σ τ) full
snoc' {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} {full : Bool} : I.CSb Δ Γ σ full → {l : ℕ} → (llen : l < s.length + 1) → (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) → (e : Expr χ) → (hf : ¬full = true → ∃ (i : ℕ), e = Expr.bvar i) → {se : CategoryTheory.yoneda.obj Δ.fst ⟶ s[l].Tm} → (eq : CategoryTheory.CategoryStruct.comp se s[l].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) → (H : se ∈ I.ofTerm Δ l e llen) → I.CSb Δ (Γ.snoc llen A) (s[l].substCons σ A se eq) full

Instances For

source

def NaturalModel.Universe.Interpretation.CSb.toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} {full : Bool} :

I.CSb Δ Γ σ full → ℕ → Expr χ

Equations

(NaturalModel.Universe.Interpretation.CSb.id Δ full).toSb = Expr.bvar
(NaturalModel.Universe.Interpretation.CSb.wk llen A full).toSb = Expr.wk
(σ_3.comp τ_1).toSb = Expr.comp σ_3.toSb τ_1.toSb
(σ_3.snoc' llen A e hf eq H).toSb = Expr.snoc σ_3.toSb e

Instances For

source

@[irreducible]

theorem NaturalModel.Universe.Interpretation.CSb.toSb_is_bvar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} (sσ : I.CSb Δ Γ σ false) (i : ℕ) :

∃ (j : ℕ), sσ.toSb i = Expr.bvar j

source

def NaturalModel.Universe.Interpretation.CSb.snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} (sσ : I.CSb Δ Γ σ) {l : ℕ} (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (e : Expr χ) {se : CategoryTheory.yoneda.obj Δ.fst ⟶ s[l].Tm} (eq : CategoryTheory.CategoryStruct.comp se s[l].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (H : se ∈ I.ofTerm Δ l e llen) :

I.CSb Δ (Γ.snoc llen A) (s[l].substCons σ A se eq)

Equations

sσ.snoc llen A e eq H = sσ.snoc' llen A e ⋯ eq H

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.CSb.snoc_toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} (sσ : I.CSb Δ Γ σ) {l : ℕ} (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (e : Expr χ) {se : CategoryTheory.yoneda.obj Δ.fst ⟶ s[l].Tm} (eq : CategoryTheory.CategoryStruct.comp se s[l].tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (H : se ∈ I.ofTerm Δ l e llen) :

(sσ.snoc llen A e eq H).toSb = Expr.snoc sσ.toSb e

source

def NaturalModel.Universe.Interpretation.CSb.sub1 {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Γ : s.CObj} {l : ℕ} (llen : l < s.length + 1) {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (e : Expr χ) (eq : CategoryTheory.CategoryStruct.comp se s[l].tp = A) (H : se ∈ I.ofTerm Γ l e llen) :

I.CSb Γ (Γ.snoc llen A) (s[l].sec A se eq)

Equations

NaturalModel.Universe.Interpretation.CSb.sub1 llen A e eq H = (NaturalModel.Universe.Interpretation.CSb.id Γ).snoc llen A e ⋯ H

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.CSb.sub1_toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Γ : s.CObj} {l : ℕ} (llen : l < s.length + 1) {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (e : Expr χ) (eq : CategoryTheory.CategoryStruct.comp se s[l].tp = A) (H : se ∈ I.ofTerm Γ l e llen) :

(sub1 llen A e eq H).toSb = e.toSb

source

def NaturalModel.Universe.Interpretation.CSb.up {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} {full : Bool} (sσ : I.CSb Δ Γ σ full) {l : ℕ} (llen : l < s.length + 1) (A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty) (A' : CategoryTheory.yoneda.obj Δ.fst ⟶ s[l].Ty := CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) (eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A' := by rfl) :

I.CSb (Δ.snoc llen A') (Γ.snoc llen A) (s[l].substWk σ A A' eq) full

Equations

sσ.up llen A A' eq = ((NaturalModel.Universe.Interpretation.CSb.wk llen A' false).comp sσ).snoc' llen A (Expr.bvar 0) ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.CSb.up_toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] {I : Interpretation χ s} {Δ Γ : s.CObj} {σ : Δ.fst ⟶ Γ.fst} {full : Bool} (sσ : I.CSb Δ Γ σ full) {l : ℕ} {llen : l < s.length + 1} {A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} {A' : CategoryTheory.yoneda.obj Δ.fst ⟶ s[l].Ty} {eq : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A = A'} :

(sσ.up llen A A' eq).toSb = Expr.up sσ.toSb

Admissibility of substitution #

source

theorem NaturalModel.Universe.Interpretation.mem_ofType_ofTerm_subst' {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {full : Bool} (IH : full = true → ∀ {Δ Γ : s.CObj} {l : ℕ} (llen : l < s.length + 1) {sσ : Δ.fst ⟶ Γ.fst} (σ : I.CSb Δ Γ sσ false) {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} {e : Expr χ}, se ∈ I.ofTerm Γ l e llen → CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map sσ) se ∈ I.ofTerm Δ l (Expr.subst σ.toSb e) llen) {e : Expr χ} {l : ℕ} (llen : l < s.length + 1) {Δ Γ : s.CObj} {sσ : Δ.fst ⟶ Γ.fst} (σ : I.CSb Δ Γ sσ full) {σ' : ℕ → Expr χ} (eq : σ.toSb = σ') :

(∀ {sA : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty}, sA ∈ I.ofType Γ l e llen → CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map sσ) sA ∈ I.ofType Δ l (Expr.subst σ' e) llen) ∧ ∀ {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm}, se ∈ I.ofTerm Γ l e llen → CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map sσ) se ∈ I.ofTerm Δ l (Expr.subst σ' e) llen

source

theorem NaturalModel.Universe.Interpretation.mem_ofType_ofTerm_subst {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l : ℕ} (llen : l < s.length + 1) {Δ Γ : s.CObj} {sσ : Δ.fst ⟶ Γ.fst} {full : Bool} (σ : I.CSb Δ Γ sσ full) {σ' : ℕ → Expr χ} (eq : σ.toSb = σ') :

source

theorem NaturalModel.Universe.Interpretation.mem_ofType_wk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l l' : ℕ} {hl : l < s.length + 1} (hl' : l' < s.length + 1) {Γ : s.CObj} {X : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Ty} (H : se ∈ I.ofType Γ l e hl) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[l'].disp X)) se ∈ I.ofType (Γ.snoc hl' X) l (Expr.subst Expr.wk e) hl

source

theorem NaturalModel.Universe.Interpretation.mem_ofType_of_isClosed {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l : ℕ} (e_cl : Expr.isClosed 0 e = true) (Γ : s.CObj) (hl : l < s.length + 1) {se : CategoryTheory.yoneda.obj s.nilCObj.fst ⟶ s[l].Ty} (se_mem : se ∈ I.ofType s.nilCObj l e hl) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenTerminal.isTerminal_yUnit.from (CategoryTheory.yoneda.obj Γ.fst)) se ∈ I.ofType Γ l e hl

source

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_wk {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l l' : ℕ} {hl : l < s.length + 1} (hl' : l' < s.length + 1) {Γ : s.CObj} {X : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {se : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l].Tm} (H : se ∈ I.ofTerm Γ l e hl) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[l'].disp X)) se ∈ I.ofTerm (Γ.snoc hl' X) l (Expr.subst Expr.wk e) hl

source

theorem NaturalModel.Universe.Interpretation.mem_ofType_toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l l' : ℕ} {hl : l < s.length + 1} (hl' : l' < s.length + 1) {Γ : s.CObj} {A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {a : Expr χ} {sa : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Tm} (ha : sa ∈ I.ofTerm Γ l' a hl') (eq : CategoryTheory.CategoryStruct.comp sa s[l'].tp = A) {se : CategoryTheory.yoneda.obj (Γ.snoc hl' A).fst ⟶ s[l].Ty} (H : se ∈ I.ofType (Γ.snoc hl' A) l e hl) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[l'].sec A sa eq)) se ∈ I.ofType Γ l (Expr.subst a.toSb e) hl

source

theorem NaturalModel.Universe.Interpretation.mem_ofTerm_toSb {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {e : Expr χ} {l l' : ℕ} {hl : l < s.length + 1} (hl' : l' < s.length + 1) {Γ : s.CObj} {A : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Ty} {a : Expr χ} {sa : CategoryTheory.yoneda.obj Γ.fst ⟶ s[l'].Tm} (ha : sa ∈ I.ofTerm Γ l' a hl') (eq : CategoryTheory.CategoryStruct.comp sa s[l'].tp = A) {se : CategoryTheory.yoneda.obj (Γ.snoc hl' A).fst ⟶ s[l].Tm} (H : se ∈ I.ofTerm (Γ.snoc hl' A) l e hl) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (s[l'].sec A sa eq)) se ∈ I.ofTerm Γ l (Expr.subst a.toSb e) hl

Soundness of interpretation #

source

theorem NaturalModel.Universe.Interpretation.tp_sound {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {i : ℕ} {A : Expr χ} {l : ℕ} (H : Lookup Γ i A l) {sΓ : s.CObj} (hΓ : sΓ ∈ I.ofCtx Γ) :

∃ (llen : l < s.length + 1), ∃ sA ∈ sΓ.tp llen i, sA ∈ I.ofType sΓ l A llen

source

theorem NaturalModel.Universe.Interpretation.var_sound {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {i : ℕ} {A : Expr χ} {l : ℕ} (H : Lookup Γ i A l) {sΓ : s.CObj} (hΓ : sΓ ∈ I.ofCtx Γ) :

∃ (llen : l < s.length + 1), ∃ st ∈ sΓ.var llen i, CategoryTheory.CategoryStruct.comp st s[l].tp ∈ I.ofType sΓ l A llen

source

def NaturalModel.Universe.Interpretation.WfCtxIH {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : Ctx χ) :

Prop

Equations

I.WfCtxIH Γ = ∃ (sΓ : s.CObj), sΓ ∈ I.ofCtx Γ

Instances For

source

def NaturalModel.Universe.Interpretation.WfTpIH {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : Ctx χ) (l : ℕ) (A : Expr χ) :

Prop

Equations

I.WfTpIH Γ l A = ∃ sΓ ∈ I.ofCtx Γ, ∃ (llen : l < s.length + 1) (sA : CategoryTheory.yoneda.obj sΓ.fst ⟶ s[l].Ty), sA ∈ I.ofType sΓ l A llen

Instances For

source

def NaturalModel.Universe.Interpretation.EqTpIH {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : Ctx χ) (l : ℕ) (A B : Expr χ) :

Prop

Equations

I.EqTpIH Γ l A B = ∃ sΓ ∈ I.ofCtx Γ, ∃ (llen : l < s.length + 1), ∃ sA ∈ I.ofType sΓ l A llen, sA ∈ I.ofType sΓ l B llen

Instances For

source

def NaturalModel.Universe.Interpretation.WfTmIH {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : Ctx χ) (l : ℕ) (A t : Expr χ) :

Prop

Equations

I.WfTmIH Γ l A t = ∃ sΓ ∈ I.ofCtx Γ, ∃ (llen : l < s.length + 1), ∃ sA ∈ I.ofType sΓ l A llen, ∃ st ∈ I.ofTerm sΓ l t llen, CategoryTheory.CategoryStruct.comp st s[l].tp = sA

Instances For

source

def NaturalModel.Universe.Interpretation.EqTmIH {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} (I : Interpretation χ s) [s.PiSeq] [s.SigSeq] [s.IdSeq] (Γ : Ctx χ) (l : ℕ) (A t u : Expr χ) :

Prop

Equations

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

Instances For

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.left {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {l : ℕ} {A B : Expr χ} :

I.EqTpIH Γ l A B → I.WfTpIH Γ l A

source

theorem NaturalModel.Universe.Interpretation.WfTpIH.refl {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {l : ℕ} {A : Expr χ} :

I.WfTpIH Γ l A → I.EqTpIH Γ l A A

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.symm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} :

I.EqTpIH Γ l A A' → I.EqTpIH Γ l A' A

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.left {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ} :

I.EqTmIH Γ l A t u → I.WfTmIH Γ l A t

source

theorem NaturalModel.Universe.Interpretation.WfTmIH.refl {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {l : ℕ} {A t : Expr χ} :

I.WfTmIH Γ l A t → I.EqTmIH Γ l A t t

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.symm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ} :

I.EqTmIH Γ l A t u → I.EqTmIH Γ l A u t

source

theorem NaturalModel.Universe.Interpretation.WfCtxIH.nil {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] :

I.WfCtxIH []

source

theorem NaturalModel.Universe.Interpretation.WfCtxIH.snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A : Expr χ} {l : ℕ} :

I.WfTpIH Γ l A → I.WfCtxIH ((A, l) :: Γ)

source

theorem NaturalModel.Universe.Interpretation.WfTpIH.univ {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] (slen : univMax ≤ s.length) {Γ : Ctx χ} {l : ℕ} :

l < univMax → I.WfCtxIH Γ → I.WfTpIH Γ (l + 1) (Expr.univ l)

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.pi {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' B B' : Expr χ} {l l' : ℕ} :

I.EqTpIH Γ l A A' → I.EqTpIH ((A, l) :: Γ) l' B B' → I.EqTpIH Γ (max l l') (Expr.pi l l' A B) (Expr.pi l l' A' B')

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.sigma {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' B B' : Expr χ} {l l' : ℕ} :

I.EqTpIH Γ l A A' → I.EqTpIH ((A, l) :: Γ) l' B B' → I.EqTpIH Γ (max l l') (Expr.sigma l l' A B) (Expr.sigma l l' A' B')

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.Id {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' t t' u u' : Expr χ} {l : ℕ} :

I.EqTpIH Γ l A A' → I.EqTmIH Γ l A t t' → I.EqTmIH Γ l A u u' → I.EqTpIH Γ l (Expr.Id l A t u) (Expr.Id l A' t' u')

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.el {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} :

I.EqTmIH Γ (l + 1) (Expr.univ l) A A' → I.EqTpIH Γ l A.el A'.el

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.el_code {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] (slen : univMax ≤ s.length) {Γ : Ctx χ} {A : Expr χ} {l : ℕ} :

l < univMax → I.WfTpIH Γ l A → I.EqTpIH Γ l A.code.el A

source

theorem NaturalModel.Universe.Interpretation.EqTpIH.trans {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' A'' : Expr χ} {l : ℕ} :

I.EqTpIH Γ l A A' → I.EqTpIH Γ l A' A'' → I.EqTpIH Γ l A A''

source

theorem NaturalModel.Universe.Interpretation.WfTmIH.bvar {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A : Expr χ} {i l : ℕ} (H : Lookup Γ i A l) :

I.WfCtxIH Γ → I.WfTmIH Γ l A (Expr.bvar i)

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.lam {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' B t t' : Expr χ} {l l' : ℕ} :

I.EqTpIH Γ l A A' → I.EqTmIH ((A, l) :: Γ) l' B t t' → I.EqTmIH Γ (max l l') (Expr.pi l l' A B) (Expr.lam l l' A t) (Expr.lam l l' A' t')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.app {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : List (Expr χ × ℕ)} {A B B' f f' a a' : Expr χ} {l l' : ℕ} :

I.EqTpIH ((A, l) :: Γ) l' B B' → I.EqTmIH Γ (max l l') (Expr.pi l l' A B) f f' → I.EqTmIH Γ l A a a' → I.EqTmIH Γ l' (Expr.subst a.toSb B) (Expr.app l l' B f a) (Expr.app l l' B' f' a')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.pair {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : List (Expr χ × ℕ)} {A B B' t t' u u' : Expr χ} {l l' : ℕ} :

I.EqTpIH ((A, l) :: Γ) l' B B' → I.EqTmIH Γ l A t t' → I.EqTmIH Γ l' (Expr.subst t.toSb B) u u' → I.EqTmIH Γ (max l l') (Expr.sigma l l' A B) (Expr.pair l l' B t u) (Expr.pair l l' B' t' u')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.fst_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' B B' p p' : Expr χ} {l l' : ℕ} :

I.EqTpIH Γ l A A' → I.EqTpIH ((A, l) :: Γ) l' B B' → I.EqTmIH Γ (max l l') (Expr.sigma l l' A B) p p' → I.EqTmIH Γ l A (Expr.fst l l' A B p) (Expr.fst l l' A' B' p') ∧ I.EqTmIH Γ l' (Expr.subst (Expr.fst l l' A B p).toSb B) (Expr.snd l l' A B p) (Expr.snd l l' A' B' p')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.refl_tm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A t t' : Expr χ} {l : ℕ} :

I.EqTmIH Γ l A t t' → I.EqTmIH Γ l (Expr.Id l A t t) (Expr.refl l t) (Expr.refl l t')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.idRec {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A M M' t t' r r' u u' h h' : Expr χ} {l l' : ℕ} :

I.EqTmIH Γ l A t t' → I.EqTpIH ((Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0), l) :: (A, l) :: Γ) l' M M' → I.EqTmIH Γ l' (Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M) r r' → I.EqTmIH Γ l A u u' → I.EqTmIH Γ l (Expr.Id l A t u) h h' → I.EqTmIH Γ l' (Expr.subst (Expr.snoc u.toSb h) M) (Expr.idRec l l' t M r u h) (Expr.idRec l l' t' M' r' u' h')

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.code {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] (slen : univMax ≤ s.length) {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} :

l < univMax → I.EqTpIH Γ l A A' → I.EqTmIH Γ (l + 1) (Expr.univ l) A.code A'.code

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.app_lam {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : List (Expr χ × ℕ)} {A B t u : Expr χ} {l l' : ℕ} :

I.WfTmIH ((A, l) :: Γ) l' B t → I.WfTmIH Γ l A u → I.EqTmIH Γ l' (Expr.subst u.toSb B) (Expr.app l l' B (Expr.lam l l' A t) u) (Expr.subst u.toSb t)

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.fst_snd_pair {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : List (Expr χ × ℕ)} {A B t u : Expr χ} {l l' : ℕ} :

I.WfTpIH ((A, l) :: Γ) l' B → I.WfTmIH Γ l A t → I.WfTmIH Γ l' (Expr.subst t.toSb B) u → I.EqTmIH Γ l A (Expr.fst l l' A B (Expr.pair l l' B t u)) t ∧ I.EqTmIH Γ l' (Expr.subst t.toSb B) (Expr.snd l l' A B (Expr.pair l l' B t u)) u

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.idRec_refl {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A M t r : Expr χ} {l l' : ℕ} :

I.WfTmIH Γ l A t → I.WfTpIH ((Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0), l) :: (A, l) :: Γ) l' M → I.WfTmIH Γ l' (Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M) r → I.EqTmIH Γ l' (Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M) (Expr.idRec l l' t M r t (Expr.refl l t)) r

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.lam_app {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A B f : Expr χ} {l l' : ℕ} :

I.WfTmIH Γ (max l l') (Expr.pi l l' A B) f → I.EqTmIH Γ (max l l') (Expr.pi l l' A B) f (Expr.lam l l' A (Expr.app l l' (Expr.subst (Expr.up Expr.wk) B) (Expr.subst Expr.wk f) (Expr.bvar 0)))

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.pair_fst_snd {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A B p : Expr χ} {l l' : ℕ} :

I.WfTmIH Γ (max l l') (Expr.sigma l l' A B) p → I.EqTmIH Γ (max l l') (Expr.sigma l l' A B) p (Expr.pair l l' B (Expr.fst l l' A B p) (Expr.snd l l' A B p))

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.code_el {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {a : Expr χ} {l : ℕ} :

I.WfTmIH Γ (l + 1) (Expr.univ l) a → I.EqTmIH Γ (l + 1) (Expr.univ l) a a.el.code

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.conv {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A A' t t' : Expr χ} {l : ℕ} :

I.EqTmIH Γ l A t t' → I.EqTpIH Γ l A A' → I.EqTmIH Γ l A' t t'

source

theorem NaturalModel.Universe.Interpretation.EqTmIH.trans {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {Γ : Ctx χ} {A t t' t'' : Expr χ} {l : ℕ} :

I.EqTmIH Γ l A t t' → I.EqTmIH Γ l A t' t'' → I.EqTmIH Γ l A t t''

source

structure NaturalModel.Universe.Interpretation.Wf {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [s.PiSeq] [s.SigSeq] [s.IdSeq] (slen : univMax ≤ s.length) (I : Interpretation χ s) (E : Axioms χ) :

Prop

I is a well-formed interpretation of the axiom environment E.

ax {c : χ} {Al : { Al : Expr χ × ℕ // Expr.isClosed 0 Al.1 = true ∧ Al.2 ≤ univMax }} (Ec : E c = some Al) : ∃ (sc : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ s[(↑Al).2].Tm), I.ax c (↑Al).2 ⋯ = some sc ∧ ∃ sA ∈ I.ofType s.nilCObj (↑Al).2 (↑Al).1 ⋯, CategoryTheory.CategoryStruct.comp sc s[(↑Al).2].tp = sA

Instances For

source

theorem NaturalModel.Universe.Interpretation.WfTmIH.ax {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {c : χ} {Al : { Al : Expr χ × ℕ // Expr.isClosed 0 Al.1 = true ∧ Al.2 ≤ univMax }} (Ec : E c = some Al) :

I.WfCtxIH Γ → I.WfTmIH Γ (↑Al).2 (↑Al).1 (Expr.ax c (↑Al).1)

source

theorem NaturalModel.Universe.Interpretation.ofType_ofTerm_sound {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] :

(∀ {Γ : Ctx χ}, WfCtx E Γ → I.WfCtxIH Γ) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A : Expr χ}, E ∣ Γ ⊢[l] A → I.WfTpIH Γ l A) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A B : Expr χ}, E ∣ Γ ⊢[l] A ≡ B → I.EqTpIH Γ l A B) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A t : Expr χ}, E ∣ Γ ⊢[l] t : A → I.WfTmIH Γ l A t) ∧ ∀ {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ}, E ∣ Γ ⊢[l] t ≡ u : A → I.EqTmIH Γ l A t u

Interpretation API #

source

def NaturalModel.Universe.Interpretation.interpCtx {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} (H : WfCtx E Γ) :

s.CObj

Given Γ s.t. WfCtx Γ, return ⟦Γ⟧.

Equations

NaturalModel.Universe.Interpretation.interpCtx H = (I.ofCtx Γ).get ⋯

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.interpCtx_mem {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} (H : WfCtx E Γ) :

interpCtx H ∈ I.ofCtx Γ

source

def NaturalModel.Universe.Interpretation.interpTy {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] A) :

CategoryTheory.yoneda.obj (interpCtx ⋯).fst ⟶ s[l].Ty

Given Γ, l, A s.t. Γ ⊢[l] A, return ⟦A⟧_⟦Γ⟧.

Equations

NaturalModel.Universe.Interpretation.interpTy H = (I.ofType (NaturalModel.Universe.Interpretation.interpCtx ⋯) l A ⋯).get ⋯

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.interpTy_mem {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] A) :

interpTy H ∈ I.ofType (interpCtx ⋯) l A ⋯

source

theorem NaturalModel.Universe.Interpretation.interpTy_eq {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] A ≡ B) :

interpTy ⋯ = interpTy ⋯

source

def NaturalModel.Universe.Interpretation.interpTm {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t : A) :

CategoryTheory.yoneda.obj (interpCtx ⋯).fst ⟶ s[l].Tm

Given Γ, l, t, A s.t. Γ ⊢[l] t : A, return ⟦t⟧_⟦Γ⟧.

Equations

NaturalModel.Universe.Interpretation.interpTm H = (I.ofTerm (NaturalModel.Universe.Interpretation.interpCtx ⋯) l t ⋯).get ⋯

Instances For

source

@[simp]

theorem NaturalModel.Universe.Interpretation.interpTm_mem {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t : A) :

interpTm H ∈ I.ofTerm (interpCtx ⋯) l t ⋯

source

@[simp]

theorem NaturalModel.Universe.Interpretation.interpTm_tp {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t : A) :

CategoryTheory.CategoryStruct.comp (interpTm H) s[l].tp = interpTy ⋯

source

theorem NaturalModel.Universe.Interpretation.interpTm_eq {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} {I : Interpretation χ s} [s.PiSeq] [s.SigSeq] [s.IdSeq] {slen : univMax ≤ s.length} {E : Axioms χ} [Iwf : Fact (Wf slen I E)] {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} (H : E ∣ Γ ⊢[l] t ≡ u : A) :

interpTm ⋯ = interpTm ⋯

source

def NaturalModel.Universe.Interpretation.empty {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] (χ : Type u_2) (s : UHomSeq 𝒞) :

Interpretation χ s

Equations

NaturalModel.Universe.Interpretation.empty χ s = { ax := fun (x : χ) (x : ℕ) (x_1 : autoParam (x < s.length + 1) _auto✝) => none }

Instances For

source

def NaturalModel.Universe.Interpretation.snoc {𝒞 : Type u} [CategoryTheory.SmallCategory 𝒞] [CategoryTheory.ChosenTerminal 𝒞] {s : UHomSeq 𝒞} {χ : Type u_1} [DecidableEq χ] (I : Interpretation χ s) (c : χ) (l : ℕ) (l_lt : l < s.length) (sc : CategoryTheory.yoneda.obj CategoryTheory.ChosenTerminal.terminal ⟶ s[l].Tm) :

Interpretation χ s

Equations

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

Instances For