Universe level bounds

theorem le_univMax_all {χ : Type u_1} {E : Axioms χ} : (∀ {Γ : Ctx χ}, WfCtx E Γ → ∀ {A : Expr χ} {i l : ℕ}, Lookup Γ i A l → l ≤ univMax) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A : Expr χ}, E ∣ Γ ⊢[l] A → l ≤ univMax) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A B : Expr χ}, E ∣ Γ ⊢[l] A ≡ B → l ≤ univMax) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A t : Expr χ}, E ∣ Γ ⊢[l] t : A → l ≤ univMax) ∧ ∀ {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ}, E ∣ Γ ⊢[l] t ≡ u : A → l ≤ univMax

theorem WfCtx.le_univMax_of_lookup {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {i l : ℕ} : WfCtx E Γ → Lookup Γ i A l → l ≤ univMax

theorem EqTp.le_univMax {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ B → l ≤ univMax

theorem WfTp.le_univMax {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → l ≤ univMax

theorem WfTm.le_univMax {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → l ≤ univMax

theorem EqTm.le_univMax {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ u : A → l ≤ univMax

Admissibility of renaming

@[irreducible]

def WfRen {χ : Type u_1} (Δ : Ctx χ) (ξ : ℕ → ℕ) (Γ : Ctx χ) : Prop

The renaming ξ : Δ ⟶ Γ is well-formed.

This notion is only useful as an intermediate step in establishing admissibility of substitution. After that, use WfSb and EqSb.

Equations

• WfRen Δ ξ Γ = ∀ {i : ℕ} {A : Expr χ} {l : ℕ}, Lookup Γ i A l → Lookup Δ (ξ i) (Expr.rename ξ A) l

theorem WfRen.lookup {χ : Type u_1} {Δ Γ : Ctx χ} {A : Expr χ} {ξ : ℕ → ℕ} {i l : ℕ} : WfRen Δ ξ Γ → Lookup Γ i A l → Lookup Δ (ξ i) (Expr.rename ξ A) l

theorem WfRen.id {χ : Type u_1} (Γ : Ctx χ) : WfRen Γ _root_.id Γ

theorem WfRen.wk {χ : Type u_1} (Γ : Ctx χ) (A : Expr χ) (l : ℕ) : WfRen ((A, l) :: Γ) Nat.succ Γ

theorem WfRen.comp {χ : Type u_1} {Θ Δ Γ : Ctx χ} {ξ ξ' : ℕ → ℕ} : WfRen Θ ξ Δ → WfRen Δ ξ' Γ → WfRen Θ (ξ ∘ ξ') Γ

theorem WfRen.upr {χ : Type u_1} {Δ Γ : Ctx χ} {A : Expr χ} {ξ : ℕ → ℕ} {l : ℕ} : WfRen Δ ξ Γ → WfRen ((Expr.rename ξ A, l) :: Δ) (Expr.upr ξ) ((A, l) :: Γ)

theorem rename_all {χ : Type u_1} {E : Axioms χ} : (∀ {Γ : Ctx χ} {l : ℕ} {A : Expr χ}, E ∣ Γ ⊢[l] A → ∀ {Δ : Ctx χ} {ξ : ℕ → ℕ}, WfCtx E Δ → WfRen Δ ξ Γ → E ∣ Δ ⊢[l] Expr.rename ξ A) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A B : Expr χ}, E ∣ Γ ⊢[l] A ≡ B → ∀ {Δ : Ctx χ} {ξ : ℕ → ℕ}, WfCtx E Δ → WfRen Δ ξ Γ → E ∣ Δ ⊢[l] Expr.rename ξ A ≡ Expr.rename ξ B) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A t : Expr χ}, E ∣ Γ ⊢[l] t : A → ∀ {Δ : Ctx χ} {ξ : ℕ → ℕ}, WfCtx E Δ → WfRen Δ ξ Γ → E ∣ Δ ⊢[l] Expr.rename ξ t : Expr.rename ξ A) ∧ ∀ {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ}, E ∣ Γ ⊢[l] t ≡ u : A → ∀ {Δ : Ctx χ} {ξ : ℕ → ℕ}, WfCtx E Δ → WfRen Δ ξ Γ → E ∣ Δ ⊢[l] Expr.rename ξ t ≡ Expr.rename ξ u : Expr.rename ξ A

Lookup well-formedness

theorem WfCtx.lookup_wf {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {i l : ℕ} : WfCtx E Γ → Lookup Γ i A l → E ∣ Γ ⊢[l] A

Admissibility of substitution

@[irreducible]

def EqSb {χ : Type u_1} (E : Axioms χ) (Δ : Ctx χ) (σ σ' : ℕ → Expr χ) (Γ : Ctx χ) : Prop

The substitutions σ σ' : Δ ⟶ Γ are judgmentally equal.

This is a functional definition similar to that in the Autosubst paper, but with a lot of preservation data added so that we can use this before proving admissibility of substitution and inversion.

The additional data is an implementation detail; EqSb should not be unfolded outside of this module.

A common alternative is to use an inductive characterization.

Equations

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

@[irreducible]

def WfSb {χ : Type u_1} (E : Axioms χ) (Δ : Ctx χ) (σ : ℕ → Expr χ) (Γ : Ctx χ) : Prop

The substitution σ : Δ ⟶ Γ is well-formed.

Equations

• WfSb E Δ σ Γ = EqSb E Δ σ σ Γ

theorem EqSb.refl {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ : ℕ → Expr χ} : WfSb E Δ σ Γ → EqSb E Δ σ σ Γ

theorem EqSb.symm {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → EqSb E Δ σ' σ Γ

theorem EqSb.trans {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' σ'' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → EqSb E Δ σ' σ'' Γ → EqSb E Δ σ σ'' Γ

theorem EqSb.lookup {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ σ' : ℕ → Expr χ} {i l : ℕ} : EqSb E Δ σ σ' Γ → Lookup Γ i A l → E ∣ Δ ⊢[l] σ i ≡ σ' i : Expr.subst σ A

theorem EqSb.wf_dom {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → WfCtx E Δ

theorem EqSb.wf_cod {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → WfCtx E Γ

theorem EqSb.wf_left {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → WfSb E Δ σ Γ

theorem EqSb.wf_right {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : EqSb E Δ σ σ' Γ → WfSb E Δ σ' Γ

theorem WfSb.eq_self {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ : ℕ → Expr χ} : WfSb E Δ σ Γ → EqSb E Δ σ σ Γ

theorem WfSb.ofRen {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {ξ : ℕ → ℕ} : WfCtx E Δ → WfCtx E Γ → WfRen Δ ξ Γ → WfSb E Δ (Expr.ofRen χ ξ) Γ

theorem WfSb.id {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} : WfCtx E Γ → WfSb E Γ Expr.bvar Γ

theorem WfSb.lookup {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ : ℕ → Expr χ} {i l : ℕ} : WfSb E Δ σ Γ → Lookup Γ i A l → E ∣ Δ ⊢[l] σ i : Expr.subst σ A

theorem WfSb.wf_dom {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ : ℕ → Expr χ} : WfSb E Δ σ Γ → WfCtx E Δ

theorem WfSb.wf_cod {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ : ℕ → Expr χ} : WfSb E Δ σ Γ → WfCtx E Γ

theorem SubstProof.tp_wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l'] B → E ∣ (A, l) :: Γ ⊢[l'] Expr.subst Expr.wk B

theorem SubstProof.eqTp_wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B B' : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l'] B ≡ B' → E ∣ (A, l) :: Γ ⊢[l'] Expr.subst Expr.wk B ≡ Expr.subst Expr.wk B'

theorem SubstProof.tm_wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B b : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l'] b : B → E ∣ (A, l) :: Γ ⊢[l'] Expr.subst Expr.wk b : Expr.subst Expr.wk B

theorem SubstProof.eqTm_wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B b b' : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l'] b ≡ b' : B → E ∣ (A, l) :: Γ ⊢[l'] Expr.subst Expr.wk b ≡ Expr.subst Expr.wk b' : Expr.subst Expr.wk B

theorem SubstProof.eqSb_snoc {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t t' : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} : EqSb E Δ σ σ' Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] Expr.subst σ A → E ∣ Δ ⊢[l] Expr.subst σ' A → E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' A → E ∣ Δ ⊢[l] t : Expr.subst σ A → E ∣ Δ ⊢[l] t' : Expr.subst σ' A → E ∣ Δ ⊢[l] t ≡ t' : Expr.subst σ A → EqSb E Δ (Expr.snoc σ t) (Expr.snoc σ' t') ((A, l) :: Γ)

theorem SubstProof.eqSb_toSb {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t t' : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] t' : A → E ∣ Γ ⊢[l] t ≡ t' : A → EqSb E Γ t.toSb t'.toSb ((A, l) :: Γ)

theorem SubstProof.wfSb_snoc {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} : WfSb E Δ σ Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] Expr.subst σ A → E ∣ Δ ⊢[l] t : Expr.subst σ A → WfSb E Δ (Expr.snoc σ t) ((A, l) :: Γ)

theorem SubstProof.wfSb_toSb {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → WfSb E Γ t.toSb ((A, l) :: Γ)

theorem SubstProof.eqSb_up {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} : EqSb E Δ σ σ' Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] Expr.subst σ A → E ∣ Δ ⊢[l] Expr.subst σ' A → E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' A → EqSb E ((Expr.subst σ A, l) :: Δ) (Expr.up σ) (Expr.up σ') ((A, l) :: Γ)

theorem SubstProof.wfSb_wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → WfSb E ((A, l) :: Γ) Expr.wk Γ

theorem SubstProof.wfSb_up {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} : WfSb E Δ σ Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] Expr.subst σ A → WfSb E ((Expr.subst σ A, l) :: Δ) (Expr.up σ) ((A, l) :: Γ)

theorem SubstProof.Id_bvar {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ (A, l) :: Γ ⊢[l] Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0)

theorem SubstProof.subst_all {χ : Type u_1} {E : Axioms χ} : (∀ {Γ : Ctx χ} {l : ℕ} {A : Expr χ}, E ∣ Γ ⊢[l] A → (∀ {Δ : Ctx χ} {σ : ℕ → Expr χ}, WfSb E Δ σ Γ → E ∣ Δ ⊢[l] Expr.subst σ A) ∧ ∀ {Δ : Ctx χ} {σ σ' : ℕ → Expr χ}, EqSb E Δ σ σ' Γ → E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' A) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A B : Expr χ}, E ∣ Γ ⊢[l] A ≡ B → ∀ {Δ : Ctx χ} {σ σ' : ℕ → Expr χ}, EqSb E Δ σ σ' Γ → E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' B) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A t : Expr χ}, E ∣ Γ ⊢[l] t : A → (∀ {Δ : Ctx χ} {σ : ℕ → Expr χ}, WfSb E Δ σ Γ → E ∣ Δ ⊢[l] Expr.subst σ t : Expr.subst σ A) ∧ ∀ {Δ : Ctx χ} {σ σ' : ℕ → Expr χ}, EqSb E Δ σ σ' Γ → E ∣ Δ ⊢[l] Expr.subst σ t ≡ Expr.subst σ' t : Expr.subst σ A) ∧ ∀ {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ}, E ∣ Γ ⊢[l] t ≡ u : A → ∀ {Δ : Ctx χ} {σ σ' : ℕ → Expr χ}, EqSb E Δ σ σ' Γ → E ∣ Δ ⊢[l] Expr.subst σ t ≡ Expr.subst σ' u : Expr.subst σ A

Substitution helper lemmas

theorem WfTp.subst_eq {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] A) (hσσ' : EqSb E Δ σ σ' Γ) : E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' A

theorem EqTp.subst_eq {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A B : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] A ≡ B) (hσσ' : EqSb E Δ σ σ' Γ) : E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' B

theorem WfTm.subst_eq {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] t : A) (hσσ' : EqSb E Δ σ σ' Γ) : E ∣ Δ ⊢[l] Expr.subst σ t ≡ Expr.subst σ' t : Expr.subst σ A

theorem EqTm.subst_eq {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t u : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] t ≡ u : A) (hσσ' : EqSb E Δ σ σ' Γ) : E ∣ Δ ⊢[l] Expr.subst σ t ≡ Expr.subst σ' u : Expr.subst σ A

theorem WfTp.subst {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] A) (hσ : WfSb E Δ σ Γ) : E ∣ Δ ⊢[l] Expr.subst σ A

theorem EqTp.subst {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A B : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] A ≡ B) (hσ : WfSb E Δ σ Γ) : E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ B

theorem WfTm.subst {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] t : A) (hσ : WfSb E Δ σ Γ) : E ∣ Δ ⊢[l] Expr.subst σ t : Expr.subst σ A

theorem EqTm.subst {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t u : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} (h : E ∣ Γ ⊢[l] t ≡ u : A) (hσ : WfSb E Δ σ Γ) : E ∣ Δ ⊢[l] Expr.subst σ t ≡ Expr.subst σ u : Expr.subst σ A

Consequences of substitution

theorem WfSb.snoc {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} : WfSb E Δ σ Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] t : Expr.subst σ A → WfSb E Δ (Expr.snoc σ t) ((A, l) :: Γ)

theorem WfSb.up {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ : ℕ → Expr χ} {l : ℕ} : WfSb E Δ σ Γ → E ∣ Γ ⊢[l] A → WfSb E ((Expr.subst σ A, l) :: Δ) (Expr.up σ) ((A, l) :: Γ)

theorem EqSb.up {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} : EqSb E Δ σ σ' Γ → E ∣ Γ ⊢[l] A → EqSb E ((Expr.subst σ A, l) :: Δ) (Expr.up σ) (Expr.up σ') ((A, l) :: Γ)

theorem Axioms.Wf.atCtx {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {c : χ} {Al : { Al : Expr χ × ℕ // Expr.isClosed 0 Al.fst = true ∧ Al.snd ≤ univMax }} : E.Wf → WfCtx E Γ → E c = some Al → E ∣ Γ ⊢[Al.val.snd] Al.val.fst

The type of any axiom is closed, so can be used in any context without weakening.