inductive TyExpr : Type

• univ: TyExpr
• el: Expr → TyExpr
• pi: TyExpr → TyExpr → TyExpr

instance instReprExpr : Repr Expr

Equations

• instReprExpr = { reprPrec := reprExpr✝ }

instance instReprTyExpr : Repr TyExpr

Equations

• instReprTyExpr = { reprPrec := reprTyExpr✝ }

inductive Expr : Type

• bvar: ℕ → Expr

  A de Bruijn index.

• app: TyExpr → Expr → Expr → Expr
• lam: TyExpr → Expr → Expr
• pi: Expr → Expr → Expr

In this section we compute the action of substitutions.

Write ↑ⁿ for the n-fold weakening substitution {n+i/i}. Write σ:k for σ.vₖ₋₁.….v₁.v₀.

The substitution ↑ⁿ⁺ᵏ:k, i.e., {0/0,…,k-1/k-1, k+n/k,k+1+n/k+1,…}, arises by starting with ↑ⁿ and traversing under k binders: for example, (ΠA. B)[↑¹] = ΠA[↑¹]. B[↑².v₀].

The substitution ↑ᵏ.e[↑ᵏ]:k, i.e., {0/0,…,k-1/k-1, e[↑ᵏ]/k, k/k+1,k+2/k+3,…}, arises by starting with id.e and traversing under k binders: for example (ΠA. B)[id.e] = ΠA[id.e]. B[↑.e[↑].v₀].

The substitution id.e is used in β-reduction: (λa) b ↝ a[id.b].

def liftVar (n : ℕ) (i : ℕ) (k : optParam ℕ 0) : ℕ

Evaluate ↑ⁿ⁺ᵏ:k at a de Bruijn index i.

Equations

• liftVar n i k = if i < k then i else n + i

theorem liftVar_lt {i : ℕ} {k : ℕ} {n : ℕ} (h : i < k) : liftVar n i k = i

theorem liftVar_le {k : ℕ} {i : ℕ} {n : ℕ} (h : k ≤ i) : liftVar n i k = n + i

theorem liftVar_base {n : ℕ} {i : ℕ} : liftVar n i = n + i

@[simp]

theorem liftVar_base' {n : ℕ} {i : ℕ} : liftVar n i = i + n

@[simp]

theorem liftVar_zero {n : ℕ} {k : ℕ} : liftVar n 0 (k + 1) = 0

@[simp]

theorem liftVar_succ {n : ℕ} {i : ℕ} {k : ℕ} : liftVar n (i + 1) (k + 1) = liftVar n i k + 1

theorem liftVar_lt_add {i : ℕ} {k : ℕ} {n : ℕ} {j : ℕ} (self : i < k) : liftVar n i j < k + n

def TyExpr.liftN (n : ℕ) : TyExpr → optParam ℕ 0 → TyExpr

Evaluate ↑ⁿ⁺ᵏ:k at a type expression.

Equations

• TyExpr.liftN n TyExpr.univ x = TyExpr.univ
• TyExpr.liftN n (TyExpr.el A) x = TyExpr.el (Expr.liftN n A x)
• TyExpr.liftN n (ty.pi body) x = (TyExpr.liftN n ty x).pi (TyExpr.liftN n body (x + 1))

def Expr.liftN (n : ℕ) : Expr → optParam ℕ 0 → Expr

Evaluate ↑ⁿ⁺ᵏ:k at an expression.

Equations

• Expr.liftN n (Expr.bvar i) x = Expr.bvar (liftVar n i x)
• Expr.liftN n (Expr.app B fn arg) x = Expr.app (TyExpr.liftN n B (x + 1)) (Expr.liftN n fn x) (Expr.liftN n arg x)
• Expr.liftN n (Expr.lam ty body) x = Expr.lam (TyExpr.liftN n ty x) (Expr.liftN n body (x + 1))
• Expr.liftN n (ty.pi body) x = (Expr.liftN n ty x).pi (Expr.liftN n body (x + 1))

@[reducible, inline]

abbrev TyExpr.lift : TyExpr → TyExpr

Evaluate ↑¹ at a type expression.

Equations

• a.lift = TyExpr.liftN 1 a

@[reducible, inline]

abbrev Expr.lift : Expr → Expr

Evaluate ↑¹ at an expression.

Equations

• a.lift = Expr.liftN 1 a

def instVar (i : ℕ) (e : Expr) (k : optParam ℕ 0) : Expr

Evaluate ↑ᵏ.e[↑ᵏ]:k at a de Bruijn index i.

Equations

• instVar i e k = if i < k then Expr.bvar i else if i = k then Expr.liftN k e else Expr.bvar (i - 1)

def TyExpr.inst : TyExpr → Expr → optParam ℕ 0 → TyExpr

Evaluate ↑ᵏ.e[↑ᵏ]:k at a type expression.

Equations

• TyExpr.univ.inst x✝ x = TyExpr.univ
• (TyExpr.el a).inst x✝ x = TyExpr.el (a.inst x✝ x)
• (ty.pi body).inst x✝ x = (ty.inst x✝ x).pi (body.inst x✝ (x + 1))

def Expr.inst : Expr → Expr → optParam ℕ 0 → Expr

Evaluate ↑ᵏ.e[↑ᵏ]:k at an expression.

Equations

• (Expr.bvar i).inst x✝ x = instVar i x✝ x
• (Expr.app B fn arg).inst x✝ x = Expr.app (B.inst x✝ (x + 1)) (fn.inst x✝ x) (arg.inst x✝ x)
• (Expr.lam ty body).inst x✝ x = Expr.lam (ty.inst x✝ x) (body.inst x✝ (x + 1))
• (ty.pi body).inst x✝ x = (ty.inst x✝ x).pi (body.inst x✝ (x + 1))

In this section we specify typing judgments of the type theory as Prop-valued relations.

inductive HasType : List TyExpr → Expr → TyExpr → Prop

• weak: ∀ {e : Expr} {A : TyExpr} {Γ : List TyExpr}, HasType Γ e A → HasType (A :: Γ) e.lift A.lift
• bvar: ∀ {A : TyExpr} {Γ : List TyExpr}, HasType (A :: Γ) (Expr.bvar 0) A.lift
• app: ∀ {A B : TyExpr} {f a : Expr} {Γ : List TyExpr}, IsType (A :: Γ) B → HasType Γ f (A.pi B) → HasType Γ a A → HasType Γ (Expr.app B f a) (B.inst a)
• lam: ∀ {A B : TyExpr} {e : Expr} {Γ : List TyExpr}, IsType Γ A → HasType (A :: Γ) e B → HasType Γ (Expr.lam A e) (A.pi B)

inductive IsType : List TyExpr → TyExpr → Prop

• univ: ∀ {Γ : List TyExpr}, IsType Γ TyExpr.univ
• el: ∀ {A : Expr} {Γ : List TyExpr}, HasType Γ A TyExpr.univ → IsType Γ (TyExpr.el A)
• pi: ∀ {A B : TyExpr} {Γ : List TyExpr}, IsType Γ A → IsType (A :: Γ) B → IsType Γ (A.pi B)

def wU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty

Equations

• wU = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (CategoryTheory.Limits.terminal.from Γ)) CategoryTheory.NaturalModel.U

@[simp]

theorem comp_wU {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Δ : Ctx) (Γ : Ctx) (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) : CategoryTheory.CategoryStruct.comp σ wU = wU

inductive CtxStack {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] : Ctx → Type u

CtxStack Γ witnesses that the semantic context Γ is built by successive context extension operations.

• nil: {Ctx : Type u} → [inst : CategoryTheory.SmallCategory Ctx] → [inst_1 : CategoryTheory.Limits.HasTerminal Ctx] → [M : CategoryTheory.NaturalModel Ctx] → CtxStack (⊤_ Ctx)
• cons: {Ctx : Type u} → [inst : CategoryTheory.SmallCategory Ctx] → [inst_1 : CategoryTheory.Limits.HasTerminal Ctx] → [M : CategoryTheory.NaturalModel Ctx] → {Γ : Ctx} → (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) → CtxStack Γ → CtxStack (CategoryTheory.NaturalModel.ext Γ A)

def Context (Ctx : Type u) [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] : Type u

Equations

• Context Ctx = ((Γ : Ctx) × CtxStack Γ)

@[reducible, inline]

abbrev Context.ty {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) : Type u

Equations

• Γ.ty = (CategoryTheory.yoneda.obj Γ.fst ⟶ CategoryTheory.NaturalModel.Ty)

@[reducible, inline]

abbrev Context.tm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) : Type u

Equations

• Γ.tm = (CategoryTheory.yoneda.obj Γ.fst ⟶ CategoryTheory.NaturalModel.Tm)

def Context.typed {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (A : Γ.ty) : Type (max 0 u)

Equations

• Γ.typed A = { x : Γ.tm // CategoryTheory.CategoryStruct.comp x CategoryTheory.NaturalModel.tp = A }

def Context.typed.cast {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {A : Γ.ty} {B : Γ.ty} (h : A = B) (x : Γ.typed A) : Γ.typed B

Equations

• Context.typed.cast h x = ⟨↑x, ⋯⟩

@[simp]

theorem Context.typed.val_cast {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {A : Γ.ty} {B : Γ.ty} (h : A = B) (x : Γ.typed A) : ↑(Context.typed.cast h x) = ↑x

def Context.nil {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] : Context Ctx

Equations

• Context.nil = ⟨⊤_ Ctx, CtxStack.nil⟩

def Context.cons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (A : Γ.ty) : Context Ctx

Equations

• Γ.cons A = ⟨CategoryTheory.NaturalModel.ext Γ.fst A, CtxStack.cons A Γ.snd⟩

@[simp]

theorem Context.cons_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (A : Γ.ty) : (Γ.cons A).fst = CategoryTheory.NaturalModel.ext Γ.fst A

def Context.weak {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (A : Γ.ty) {P : CategoryTheory.Psh Ctx} (f : CategoryTheory.yoneda.obj Γ.fst ⟶ P) : CategoryTheory.yoneda.obj (Γ.cons A).fst ⟶ P

Equations

• Γ.weak A f = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Γ.fst A)) f

def CtxStack.var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} : CtxStack Γ → ℕ → Part (CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm)

Equations

• CtxStack.nil.var x = Part.none
• (CtxStack.cons A a).var 0 = pure (CategoryTheory.NaturalModel.var Γ_2 A)
• (CtxStack.cons A S).var n.succ = Context.weak ⟨Γ_2, S⟩ A <$> S.var n

def Context.var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (i : ℕ) : Part Γ.tm

Equations

• Γ.var i = Γ.snd.var i

def substCons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A)

Equations

• substCons σ e A eTy = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift e σ eTy) ⋯.isoPullback.inv

@[simp]

theorem substCons_var {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp (substCons σ e A eTy) (CategoryTheory.NaturalModel.var Δ A) = e

@[simp]

theorem substCons_var_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : CategoryTheory.NaturalModel.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp (substCons σ e A eTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NaturalModel.var Δ A) h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem substCons_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp (substCons σ e A eTy) (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Δ A)) = σ

@[simp]

theorem substCons_disp_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : CategoryTheory.yoneda.obj Δ ⟶ Z) : CategoryTheory.CategoryStruct.comp (substCons σ e A eTy) (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Δ A)) h) = CategoryTheory.CategoryStruct.comp σ h

theorem comp_substUnit {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Ctx} {Γ : Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (f : Γ ⟶ ⊤_ Ctx) (f' : Δ ⟶ ⊤_ Ctx) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.yoneda.map f) = CategoryTheory.yoneda.map f'

theorem comp_substCons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Γ' : Ctx} {Δ : Ctx} (τ : CategoryTheory.yoneda.obj Γ' ⟶ CategoryTheory.yoneda.obj Γ) (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp τ (substCons σ e A eTy) = substCons (CategoryTheory.CategoryStruct.comp τ σ) (CategoryTheory.CategoryStruct.comp τ e) A ⋯

theorem comp_substCons_assoc {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Γ' : Ctx} {Δ : Ctx} (τ : CategoryTheory.yoneda.obj Γ' ⟶ CategoryTheory.yoneda.obj Γ) (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ) (e : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty) (eTy : CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp σ A) {Z : CategoryTheory.Functor Ctxᵒᵖ (Type u)} (h : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A) ⟶ Z) : CategoryTheory.CategoryStruct.comp τ (CategoryTheory.CategoryStruct.comp (substCons σ e A eTy) h) = CategoryTheory.CategoryStruct.comp (substCons (CategoryTheory.CategoryStruct.comp τ σ) (CategoryTheory.CategoryStruct.comp τ e) A ⋯) h

def substFst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} {A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A)) : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj Δ

Equations

• substFst σ = CategoryTheory.CategoryStruct.comp σ (CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp Δ A))

def substSnd {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} {A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A)) : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm

Equations

• substSnd σ = CategoryTheory.CategoryStruct.comp σ (CategoryTheory.NaturalModel.var Δ A)

theorem substSnd_ty {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {Δ : Ctx} {A : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty} (σ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A)) : CategoryTheory.CategoryStruct.comp (substSnd σ) CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (substFst σ) A

def weakSubst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Ctx} {Γ : Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ (CategoryTheory.CategoryStruct.comp σ A)) ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A)

Equations

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

def weakSubst' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Ctx} {Γ : Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) {A' : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.NaturalModel.Ty} (e : CategoryTheory.CategoryStruct.comp σ A = A') : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ A') ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A)

Equations

• weakSubst' σ A e = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (weakSubst σ A)

def Context.typed.subst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) {A : Γ.ty} (x : Γ.typed A) : Δ.typed (CategoryTheory.CategoryStruct.comp σ A)

Equations

• Context.typed.subst σ x = ⟨CategoryTheory.CategoryStruct.comp σ ↑x, ⋯⟩

@[simp]

theorem Context.typed.subst_coe {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) {A : Γ.ty} (x : Γ.typed A) : ↑(Context.typed.subst σ x) = CategoryTheory.CategoryStruct.comp σ ↑x

def mkEl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.typed wU) : Γ.ty

Equations

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

theorem comp_mkEl {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Context Ctx} {Γ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.typed wU) : CategoryTheory.CategoryStruct.comp σ (mkEl A) = mkEl (Context.typed.cast ⋯ (Context.typed.subst σ A))

def mkP_equiv {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {X : CategoryTheory.Psh Ctx} : (CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj X) ≃ (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) × (CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ X)

Equations

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

theorem mkP_equiv_naturality_left {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Ctx} {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (f : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj X) : mkP_equiv (CategoryTheory.CategoryStruct.comp σ f) = match mkP_equiv f with | ⟨A, a⟩ => ⟨CategoryTheory.CategoryStruct.comp σ A, CategoryTheory.CategoryStruct.comp (weakSubst σ A) a⟩

def mkP {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {X : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ X) : CategoryTheory.yoneda.obj Γ ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj X

Equations

• mkP A B = mkP_equiv.symm ⟨A, B⟩

theorem mkP_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {X : CategoryTheory.Psh Ctx} {Y : CategoryTheory.Psh Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (F : X ⟶ Y) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ X) : CategoryTheory.CategoryStruct.comp (mkP A B) ((CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).map F) = mkP A (CategoryTheory.CategoryStruct.comp B F)

theorem comp_mkP {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {X : CategoryTheory.Functor Ctxᵒᵖ (Type u)} {Δ : Ctx} {Γ : Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ X) : CategoryTheory.CategoryStruct.comp σ (mkP A B) = mkP (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B)

def mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.ty) (B : (Γ.cons A).ty) : Γ.ty

Equations

• mkPi A B = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi

theorem comp_mkPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.ty) (B : (Γ.cons A).ty) : CategoryTheory.CategoryStruct.comp σ (mkPi A B) = mkPi (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B)

def mkLam' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.ty) (e : (Γ.cons A).tm) : Γ.tm

Equations

• mkLam' A e = CategoryTheory.CategoryStruct.comp (mkP A e) CategoryTheory.NaturalModel.NaturalModelPi.lam

theorem comp_mkLam' {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.ty) (B : (Γ.cons A).tm) : CategoryTheory.CategoryStruct.comp σ (mkLam' A B) = mkLam' (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B)

def Context.subst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {X : CategoryTheory.Psh Ctx} (A : Γ.ty) (B : CategoryTheory.yoneda.obj (Γ.cons A).fst ⟶ X) (a : Γ.typed A) : CategoryTheory.yoneda.obj Γ.fst ⟶ X

Equations

• Context.subst A B a = CategoryTheory.CategoryStruct.comp (substCons (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.obj Γ.fst)) (↑a) A ⋯) B

theorem Context.comp_subst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) {X : CategoryTheory.Psh Ctx} (A : Γ.ty) (B : CategoryTheory.yoneda.obj (Γ.cons A).fst ⟶ X) (a : Γ.typed A) : CategoryTheory.CategoryStruct.comp σ (Context.subst A B a) = Context.subst (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B) (Context.typed.subst σ a)

def mkTyped {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} {A : Δ.ty} (σ : CategoryTheory.yoneda.obj Γ.fst ⟶ CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Δ.fst A)) {Aσ : CategoryTheory.yoneda.obj Γ.fst ⟶ CategoryTheory.NaturalModel.Ty} (eq : CategoryTheory.CategoryStruct.comp (substFst σ) A = Aσ) : Γ.typed Aσ

Equations

• mkTyped σ eq = ⟨substSnd σ, ⋯⟩

def mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.ty) (B : (Γ.cons A).ty) (e : (Γ.cons A).typed B) : Γ.typed (mkPi A B)

Equations

• mkLam A B e = ⟨mkLam' A ↑e, ⋯⟩

theorem comp_mkLam {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.ty) (B : (Γ.cons A).ty) (e : (Γ.cons A).typed B) : CategoryTheory.CategoryStruct.comp σ ↑(mkLam A B e) = ↑(mkLam (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B) (Context.typed.subst (weakSubst σ A) e))

def mkPApp'_aux {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi) : (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) × (CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Tm)

Equations

• mkPApp'_aux A B f f_tp = mkP_equiv (⋯.isLimit.lift (CategoryTheory.Limits.PullbackCone.mk f (mkP A B) f_tp))

theorem mkPApp'_aux_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi) : let p := mkPApp'_aux A B f f_tp; ⟨p.fst, CategoryTheory.CategoryStruct.comp p.snd CategoryTheory.NaturalModel.tp⟩ = ⟨A, B⟩

@[simp]

theorem mkPApp'_aux_fst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi) : (mkPApp'_aux A B f f_tp).fst = A

@[simp]

theorem mkPApp'_aux_snd_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi) : CategoryTheory.CategoryStruct.comp (mkPApp'_aux A B f f_tp).snd CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) B

def comp_mkPApp'_aux {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Δ : Ctx} {Γ : Ctx} (σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Ty) (B : CategoryTheory.yoneda.obj (CategoryTheory.NaturalModel.ext Γ A) ⟶ CategoryTheory.NaturalModel.Ty) (f : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.NaturalModel.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f CategoryTheory.NaturalModel.tp = CategoryTheory.CategoryStruct.comp (mkP A B) CategoryTheory.NaturalModel.NaturalModelPi.Pi) : mkPApp'_aux (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B) (CategoryTheory.CategoryStruct.comp σ f) ⋯ = match mkPApp'_aux A B f f_tp with | ⟨A, a⟩ => ⟨CategoryTheory.CategoryStruct.comp σ A, CategoryTheory.CategoryStruct.comp (weakSubst σ A) a⟩

Equations

• ⋯ = ⋯

def mkPApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.ty) (B : (Γ.cons A).ty) (f : Γ.typed (mkPi A B)) : (Γ.cons A).typed B

Equations

• mkPApp A B f = ⟨CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (mkPApp'_aux A B ↑f ⋯).snd, ⋯⟩

theorem comp_mkPApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.ty) (B : (Γ.cons A).ty) (f : Γ.typed (mkPi A B)) : CategoryTheory.CategoryStruct.comp (weakSubst σ A) ↑(mkPApp A B f) = ↑(mkPApp (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B) (Context.typed.cast ⋯ (Context.typed.subst σ f)))

def mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.ty) (B : (Γ.cons A).ty) (f : Γ.typed (mkPi A B)) (a : Γ.typed A) : Γ.typed (Context.subst A B a)

Equations

• mkApp A B f a = ⟨Context.subst A (↑(mkPApp A B f)) a, ⋯⟩

theorem comp_mkApp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.ty) (B : (Γ.cons A).ty) (f : Γ.typed (mkPi A B)) (a : Γ.typed A) : CategoryTheory.CategoryStruct.comp σ ↑(mkApp A B f a) = ↑(mkApp (CategoryTheory.CategoryStruct.comp σ A) (CategoryTheory.CategoryStruct.comp (weakSubst σ A) B) (Context.typed.cast ⋯ (Context.typed.subst σ f)) (Context.typed.subst σ a))

def mkSmallPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} (A : Γ.typed wU) (B : (Γ.cons (mkEl A)).typed wU) : Γ.typed wU

Equations

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

theorem comp_mkSmallPi {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {Δ : Context Ctx} (σ : CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ.fst) (A : Γ.typed wU) (B : (Γ.cons (mkEl A)).typed wU) : CategoryTheory.CategoryStruct.comp σ ↑(mkSmallPi A B) = ↑(mkSmallPi (Context.typed.cast ⋯ (Context.typed.subst σ A)) (Context.typed.cast ⋯ (Context.typed.subst (weakSubst' σ (mkEl A) ⋯) B)))

def ofType {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) : TyExpr → Part Γ.ty

Equations

• One or more equations did not get rendered due to their size.
• ofType Γ TyExpr.univ = pure wU
• ofType Γ (A.pi B) = do let A ← ofType Γ A let B ← ofType (Γ.cons A) B pure (mkPi A B)

def ofTerm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) : Expr → Part Γ.tm

Equations

• One or more equations did not get rendered due to their size.
• ofTerm Γ (Expr.bvar i) = Γ.var i
• ofTerm Γ (Expr.lam A e) = do let A ← ofType Γ A let e ← ofTerm (Γ.cons A) e pure ↑(mkLam A (CategoryTheory.CategoryStruct.comp e CategoryTheory.NaturalModel.tp) ⟨e, ⋯⟩)

def ofCtx {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] : List TyExpr → Part (Context Ctx)

Equations

• ofCtx [] = pure Context.nil
• ofCtx (A :: Γ) = do let Γ ← ofCtx Γ let __do_lift ← ofType Γ A ↑(some (Γ.cons __do_lift))

theorem ofTerm_app {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {B : TyExpr} (Γ : Context Ctx) {f : Expr} {a : Expr} {e' : Γ.tm} : e' ∈ ofTerm Γ (Expr.app B f a) ↔ ∃ f' ∈ ofTerm Γ f, ∃ a' ∈ ofTerm Γ a, ∃ (t' : CategoryTheory.yoneda.obj Γ.fst ⟶ CategoryTheory.NaturalModel.Ty) (ht' : CategoryTheory.CategoryStruct.comp a' CategoryTheory.NaturalModel.tp = t'), ∃ B' ∈ ofType (Γ.cons t') B, ∃ (hB : CategoryTheory.CategoryStruct.comp f' CategoryTheory.NaturalModel.tp = mkPi t' B'), e' = ↑(mkApp t' B' ⟨f', hB⟩ ⟨a', ht'⟩)

def CtxStack.size {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} : CtxStack Γ → ℕ

Equations

• CtxStack.nil.size = 0
• (CtxStack.cons A S).size = S.size + 1

def CtxStack.dropN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (k : ℕ) (S : CtxStack Γ) : k ≤ S.size → Context Ctx

Equations

• CtxStack.dropN 0 x x_1 = ⟨Γ, x⟩
• CtxStack.dropN n.succ (CtxStack.cons A a) h = CtxStack.dropN n a ⋯

def CtxStack.dropN_disp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} (k : ℕ) (S : CtxStack Γ) (h : k ≤ S.size) : Γ ⟶ (CtxStack.dropN k S h).fst

Equations

• CtxStack.dropN_disp 0 x x_1 = CategoryTheory.CategoryStruct.id Γ
• CtxStack.dropN_disp n.succ (CtxStack.cons A a) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NaturalModel.disp Γ_2 A) (CtxStack.dropN_disp n a ⋯)

def CtxStack.extN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Ctx} {k : ℕ} {S : CtxStack Γ} {h : k ≤ S.size} : (CtxStack.dropN k S h).ty → (Δ : Context Ctx) × (CategoryTheory.yoneda.obj Δ.fst ⟶ CategoryTheory.yoneda.obj Γ)

Equations

• CtxStack.extN x_2 = ⟨(CtxStack.dropN 0 x x_1).cons x_2, CategoryTheory.yoneda.map (CategoryTheory.NaturalModel.disp (CtxStack.dropN 0 x x_1).fst x_2)⟩
• CtxStack.extN X = match CtxStack.extN X with | ⟨Δ, wk⟩ => ⟨Δ.cons (CategoryTheory.CategoryStruct.comp wk A), weakSubst wk A⟩

def Context.tyN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] (Γ : Context Ctx) (k : ℕ) : Type u

Equations

• Γ.tyN k = ((h : k ≤ Γ.snd.size) ×' (CtxStack.dropN k Γ.snd h).ty)

def Context.tyN.up {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {k : ℕ} {A : Γ.ty} : Γ.tyN k → (Γ.cons A).tyN (k + 1)

Equations

• Context.tyN.up ⟨h, X⟩ = ⟨⋯, X⟩

def Context.tyN.down {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {k : ℕ} {A : Γ.ty} : (Γ.cons A).tyN (k + 1) → Γ.tyN k

Equations

• Context.tyN.down ⟨h, X⟩ = ⟨⋯, X⟩

def Context.consN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} (Γ : Context Ctx) (A : Γ.tyN k) : Context Ctx

Equations

• Γ.consN A = (CtxStack.extN A.snd).fst

def Context.dispN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} (Γ : Context Ctx) (A : Γ.tyN k) : CategoryTheory.yoneda.obj (Γ.consN A).fst ⟶ CategoryTheory.yoneda.obj Γ.fst

Equations

• Γ.dispN A = (CtxStack.extN A.snd).snd

@[simp]

theorem Context.dispN_cons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} (Γ : Context Ctx) (A : Γ.ty) (X : Γ.tyN k) : (Γ.cons A).dispN X.up = weakSubst (Γ.dispN X) A

@[simp]

theorem Context.consN_cons {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} (Γ : Context Ctx) (A : Γ.ty) (X : Γ.tyN k) : (Γ.cons A).consN X.up = (Γ.consN X).cons (CategoryTheory.CategoryStruct.comp (Γ.dispN X) A)

theorem ofType_liftN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} {Γ : Context Ctx} {A : TyExpr} {A' : Γ.ty} (X : Γ.tyN k) : A' ∈ ofType Γ A → CategoryTheory.CategoryStruct.comp (Γ.dispN X) A' ∈ ofType (Γ.consN X) (TyExpr.liftN 1 A k)

theorem ofTerm_liftN {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {k : ℕ} {Γ : Context Ctx} {e : Expr} {e' : Γ.tm} (X : Γ.tyN k) : e' ∈ ofTerm Γ e → CategoryTheory.CategoryStruct.comp (Γ.dispN X) e' ∈ ofTerm (Γ.consN X) (Expr.liftN 1 e k)

theorem ofType_lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {A : TyExpr} {A' : Γ.ty} (X : Γ.ty) (H : A' ∈ ofType Γ A) : Γ.weak X A' ∈ ofType (Γ.cons X) A.lift

theorem ofTerm_lift {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {e : Expr} {e' : Γ.tm} (X : Γ.ty) (H : e' ∈ ofTerm Γ e) : Γ.weak X e' ∈ ofTerm (Γ.cons X) e.lift

theorem ofType_inst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {X : Γ.ty} {x : Expr} {A : TyExpr} {A' : (Γ.cons X).ty} (x' : Γ.typed X) (Hx : ↑x' ∈ ofTerm Γ x) (He : A' ∈ ofType (Γ.cons X) A) : Context.subst X A' x' ∈ ofType Γ (A.inst x)

theorem ofTerm_inst {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : Context Ctx} {X : Γ.ty} {x : Expr} {e : Expr} {e' : (Γ.cons X).tm} (x' : Γ.typed X) (Hx : ↑x' ∈ ofTerm Γ x) (He : e' ∈ ofTerm (Γ.cons X) e) : Context.subst X e' x' ∈ ofTerm Γ (e.inst x)

theorem ofTerm_ofType_correct {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] : (∀ {Γ : List TyExpr} {e : Expr} {A : TyExpr}, HasType Γ e A → ∀ {Γ' : Context Ctx}, Γ' ∈ ofCtx Γ → ∃ A' ∈ ofType Γ' A, ∃ e' ∈ ofTerm Γ' e, CategoryTheory.CategoryStruct.comp e' CategoryTheory.NaturalModel.tp = A') ∧ ∀ {Γ : List TyExpr} {A : TyExpr}, IsType Γ A → ∀ {Γ' : Context Ctx}, Γ' ∈ ofCtx Γ → (ofType Γ' A).Dom

theorem ofTerm_correct {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : List TyExpr} {e : Expr} {A : TyExpr} (H : HasType Γ e A) {Γ' : Context Ctx} (hΓ : Γ' ∈ ofCtx Γ) : ∃ A' ∈ ofType Γ' A, ∃ e' ∈ ofTerm Γ' e, CategoryTheory.CategoryStruct.comp e' CategoryTheory.NaturalModel.tp = A'

theorem ofTerm_correct_ty {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : List TyExpr} {e : Expr} {A : TyExpr} (H : HasType Γ e A) {Γ' : Context Ctx} (hΓ : Γ' ∈ ofCtx Γ) : (ofType Γ' A).Dom

theorem ofTerm_correct_tm {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : List TyExpr} {e : Expr} {A : TyExpr} (H : HasType Γ e A) {Γ' : Context Ctx} (hΓ : Γ' ∈ ofCtx Γ) : (ofTerm Γ' e).Dom

theorem ofTerm_correct_tp {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {e : Expr} {Γ : List TyExpr} {A : TyExpr} (H : HasType Γ e A) {Γ' : Context Ctx} (hΓ : Γ' ∈ ofCtx Γ) : CategoryTheory.CategoryStruct.comp ((ofTerm Γ' e).get ⋯) CategoryTheory.NaturalModel.tp = (ofType Γ' A).get ⋯

theorem ofType_correct {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {Γ : List TyExpr} {A : TyExpr} (H : IsType Γ A) {Γ' : Context Ctx} (hΓ : Γ' ∈ ofCtx Γ) : (ofType Γ' A).Dom

def Typed (Γ : List TyExpr) (A : TyExpr) : Type

Equations

• Typed Γ A = { e : Expr // HasType Γ e A }

def toModelType {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {A : TyExpr} (e : Typed [] A) : CategoryTheory.yoneda.obj (⊤_ Ctx) ⟶ CategoryTheory.NaturalModel.Ty

Equations

• toModelType e = (ofType Context.nil A).get ⋯

def toModel {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {A : TyExpr} (e : Typed [] A) : CategoryTheory.yoneda.obj (⊤_ Ctx) ⟶ CategoryTheory.NaturalModel.Tm

Equations

• toModel e = (ofTerm Context.nil ↑e).get ⋯

theorem toModel_type {Ctx : Type u} [CategoryTheory.SmallCategory Ctx] [CategoryTheory.Limits.HasTerminal Ctx] [M : CategoryTheory.NaturalModel Ctx] {A : TyExpr} (e : Typed [] A) : CategoryTheory.CategoryStruct.comp (toModel e) CategoryTheory.NaturalModel.tp = toModelType e