Morphisms of unstructured models, and Russell-universe embeddings.

def Model.UnstructuredUniverse.«termBy>_» : Lean.ParserDescr

Equations

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

structure Model.UnstructuredUniverse.Hom {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M N : UnstructuredUniverse Ctx) : Type u_1

• mapTm : M.Tm ⟶ N.Tm
• mapTy : M.Ty ⟶ N.Ty
• pb : CategoryTheory.IsPullback self.mapTm M.tp N.tp self.mapTy

def Model.UnstructuredUniverse.Hom.id {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) : M.Hom M

Equations

• Model.UnstructuredUniverse.Hom.id M = { mapTm := CategoryTheory.CategoryStruct.id M.Tm, mapTy := CategoryTheory.CategoryStruct.id M.Ty, pb := ⋯ }

def Model.UnstructuredUniverse.Hom.comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {M N O : UnstructuredUniverse Ctx} (α : M.Hom N) (β : N.Hom O) : M.Hom O

Equations

• α.comp β = { mapTm := CategoryTheory.CategoryStruct.comp α.mapTm β.mapTm, mapTy := CategoryTheory.CategoryStruct.comp α.mapTy β.mapTy, pb := ⋯ }

def Model.UnstructuredUniverse.Hom.comp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {M N O P : UnstructuredUniverse Ctx} (α : M.Hom N) (β : N.Hom O) (γ : O.Hom P) : (α.comp β).comp γ = α.comp (β.comp γ)

Equations

• ⋯ = ⋯

def Model.UnstructuredUniverse.pullbackHom {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) : (M.pullback A).Hom M

Morphism into the representable natural transformation M from the pullback of M along a type.

Equations

• M.pullbackHom A = { mapTm := M.var A, mapTy := A, pb := ⋯ }

def Model.UnstructuredUniverse.Hom.subst {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ Δ : Ctx} (A : Γ ⟶ M.Ty) (σ : Δ ⟶ Γ) : (M.pullback (CategoryTheory.CategoryStruct.comp σ A)).Hom (M.pullback A)

Given M : Universe, a semantic type A : (Γ) ⟶ M.Ty, and a substitution σ : Δ ⟶ Γ, construct a Hom for the substitution A[σ].

Equations

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

def Model.UnstructuredUniverse.Hom.extIsoExt {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {M N : UnstructuredUniverse Ctx} (h : M.Hom N) {Γ : Ctx} (A : Γ ⟶ M.Ty) : N.ext (CategoryTheory.CategoryStruct.comp A h.mapTy) ≅ M.ext A

Equations

• h.extIsoExt A = CategoryTheory.IsPullback.isoIsPullback N.Tm Γ ⋯ ⋯

structure Model.UnstructuredUniverse.UHom {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (M N : UnstructuredUniverse Ctx) extends M.Hom N : Type u_1

A Russell universe embedding is a hom of natural models M ⟶ N such that types in M correspond to terms of a universe U in N.

These don't form a category since UHom.id M is essentially Type : Type in M.

Note this doesn't need to extend Hom as none of its fields are used; it's just convenient to pack up the data.

• mapTm : M.Tm ⟶ N.Tm
• mapTy : M.Ty ⟶ N.Ty
• pb : CategoryTheory.IsPullback self.mapTm M.tp N.tp self.mapTy
• U : CategoryTheory.ChosenTerminal.terminal ⟶ N.Ty
• asTm : M.Ty ⟶ N.Tm
• U_pb : CategoryTheory.IsPullback self.asTm (CategoryTheory.ChosenTerminal.isTerminal.from M.Ty) N.tp self.U

def Model.UnstructuredUniverse.UHom.ofTyIsoExt {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : UnstructuredUniverse Ctx} (H : M.Hom N) {U : CategoryTheory.ChosenTerminal.terminal ⟶ N.Ty} (i : M.Ty ≅ N.ext U) : M.UHom N

Equations

• Model.UnstructuredUniverse.UHom.ofTyIsoExt H i = { toHom := H, U := U, asTm := CategoryTheory.CategoryStruct.comp i.hom (N.var U), U_pb := ⋯ }

def Model.UnstructuredUniverse.UHom.comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N O : UnstructuredUniverse Ctx} (α : M.UHom N) (β : N.UHom O) : M.UHom O

Equations

• α.comp β = { toHom := α.comp β.toHom, U := CategoryTheory.CategoryStruct.comp α.U β.mapTy, asTm := CategoryTheory.CategoryStruct.comp α.asTm β.mapTm, U_pb := ⋯ }

def Model.UnstructuredUniverse.UHom.comp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N O P : UnstructuredUniverse Ctx} (α : M.UHom N) (β : N.UHom O) (γ : O.UHom P) : (α.comp β).comp γ = α.comp (β.comp γ)

Equations

• ⋯ = ⋯

def Model.UnstructuredUniverse.UHom.wkU {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : UnstructuredUniverse Ctx} (Γ : Ctx) (α : M.UHom N) : Γ ⟶ N.Ty

Equations

• Model.UnstructuredUniverse.UHom.wkU Γ α = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenTerminal.isTerminal.from Γ) α.U

@[simp]

theorem Model.UnstructuredUniverse.UHom.comp_wkU {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : UnstructuredUniverse Ctx} {Δ Γ : Ctx} (α : M.UHom N) (f : Δ ⟶ Γ) : CategoryTheory.CategoryStruct.comp f (wkU Γ α) = wkU Δ α

@[simp]

theorem Model.UnstructuredUniverse.UHom.comp_wkU_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {M N : UnstructuredUniverse Ctx} {Δ Γ : Ctx} (α : M.UHom N) (f : Δ ⟶ Γ) {Z : Ctx} (h : N.Ty ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (wkU Γ α) h) = CategoryTheory.CategoryStruct.comp (wkU Δ α) h

def Model.UnstructuredUniverse.UHom.ofTarskiU {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (M : UnstructuredUniverse Ctx) (U : CategoryTheory.ChosenTerminal.terminal ⟶ M.Ty) (El : M.ext U ⟶ M.Ty) : (M.pullback El).UHom M

Equations

• Model.UnstructuredUniverse.UHom.ofTarskiU M U El = { toHom := M.pullbackHom El, U := U, asTm := M.var U, U_pb := ⋯ }

Universe embeddings

structure Model.UnstructuredUniverse.UHomSeq (Ctx : Type u) [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] : Type (max u u_1)

A sequence of Russell universe embeddings.

• length : ℕ

  Number of embeddings in the sequence, or one less than the number of models in the sequence.

• objs (i : ℕ) (h : i < self.length + 1) : UnstructuredUniverse Ctx
• homSucc' (i : ℕ) (h : i < self.length) : (self.objs i ⋯).UHom (self.objs (i + 1) ⋯)

instance Model.UnstructuredUniverse.UHomSeq.instGetElemNatLtHAddLengthOfNat {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] : GetElem (UHomSeq Ctx) ℕ (UnstructuredUniverse Ctx) fun (s : UHomSeq Ctx) (i : ℕ) => i < s.length + 1

Equations

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

def Model.UnstructuredUniverse.UHomSeq.homSucc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i : ℕ) (h : i < s.length := by get_elem_tactic) : s[i].UHom s[i + 1]

Equations

• s.homSucc i h = s.homSucc' i h

@[irreducible]

def Model.UnstructuredUniverse.UHomSeq.hom {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i < j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) : s[i].UHom s[j]

Composition of embeddings between i and j in the chain.

Equations

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

def Model.UnstructuredUniverse.UHomSeq.homOfLe {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) : s[i].Hom s[j]

Equations

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

def Model.UnstructuredUniverse.UHomSeq.unlift {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) {Γ : Ctx} (A : Γ ⟶ s[i].Ty) (t : Γ ⟶ s[j].Tm) (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : Γ ⟶ s[i].Tm

For i ≤ j and a term t at level j, if the type of t is lifted from level i, then t is a lift of a term at level i.

Equations

• s.unlift i j ij jlen A t eq = ⋯.lift t A eq

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.unlift_tp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : Γ ⟶ s[i].Ty} {t : Γ ⟶ s[j].Tm} (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : CategoryTheory.CategoryStruct.comp (s.unlift i j ij jlen A t eq) s[i].tp = A

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.unlift_lift {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : Γ ⟶ s[i].Ty} {t : Γ ⟶ s[j].Tm} (eq : CategoryTheory.CategoryStruct.comp t s[j].tp = CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy) : CategoryTheory.CategoryStruct.comp (s.unlift i j ij jlen A t eq) (s.homOfLe i j ij jlen).mapTm = t

def Model.UnstructuredUniverse.UHomSeq.unliftVar {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j : ℕ) (ij : i ≤ j := by omega) (jlen : j < s.length + 1 := by get_elem_tactic) {Γ : Ctx} (A : Γ ⟶ s[i].Ty) {A' : Γ ⟶ s[j].Ty} (eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A') : s[j].ext A' ⟶ s[i].Tm

Equations

• s.unliftVar i j ij jlen A eq = s.unlift i j ij jlen (CategoryTheory.CategoryStruct.comp (s[j].disp A') A) (s[j].var A') ⋯

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.unliftVar_tp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : Γ ⟶ s[i].Ty} {A' : Γ ⟶ s[j].Ty} (eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A') : CategoryTheory.CategoryStruct.comp (s.unliftVar i j ij jlen A eq) s[i].tp = CategoryTheory.CategoryStruct.comp (s[j].disp A') A

theorem Model.UnstructuredUniverse.UHomSeq.substCons_unliftVar {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {i j : ℕ} {ij : i ≤ j} {jlen : j < s.length + 1} {Γ : Ctx} {A : Γ ⟶ s[i].Ty} {A' : Γ ⟶ s[j].Ty} {eq : CategoryTheory.CategoryStruct.comp A (s.homOfLe i j ij jlen).mapTy = A'} {Δ : Ctx} {σ : Δ ⟶ Γ} {t : Δ ⟶ s[i].Tm} (t_tp : CategoryTheory.CategoryStruct.comp t s[i].tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp (s[j].substCons σ A' (CategoryTheory.CategoryStruct.comp t (s.homOfLe i j ij jlen).mapTm) ⋯) (s.unliftVar i j ij jlen A eq) = t

def Model.UnstructuredUniverse.UHomSeq.code {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : Γ ⟶ s[i].Ty) : Γ ⟶ s[i + 1].Tm

TODO: Consider generalising to just UHom? Convert a map into the ith type classifier into a a term of the i+1th term classifier, that is a term of the ith universe. It is defined by composition with the first projection of the pullback square v s[i].Ty ----> s[i+1].Tm ^ | | A / | p.b. | / | | / V V (Γ) ---> 1 -----> s[i+1].Ty U_i

Equations

• s.code ilen A = CategoryTheory.CategoryStruct.comp A (s.homSucc i ilen).asTm

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.code_tp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : Γ ⟶ s[i].Ty) : CategoryTheory.CategoryStruct.comp (s.code ilen A) s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)

theorem Model.UnstructuredUniverse.UHomSeq.comp_code {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {Δ Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (σ : Δ ⟶ Γ) (A : Γ ⟶ s[i].Ty) : CategoryTheory.CategoryStruct.comp σ (s.code ilen A) = s.code ilen (CategoryTheory.CategoryStruct.comp σ A)

theorem Model.UnstructuredUniverse.UHomSeq.comp_code_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {Δ Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (σ : Δ ⟶ Γ) (A : Γ ⟶ s[i].Ty) {Z : Ctx} (h : s[i + 1].Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (s.code ilen A) h) = CategoryTheory.CategoryStruct.comp (s.code ilen (CategoryTheory.CategoryStruct.comp σ A)) h

def Model.UnstructuredUniverse.UHomSeq.el {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Γ : Ctx} {i : ℕ} (ilen : i < s.length) (a : Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : Γ ⟶ s[i].Ty

TODO: Consider generalising to just UHom? Convert a a term of the ith universe (it is a i+1 level term) into a map into the ith type classifier. It is the unique map into the pullback a (Γ) -----------------¬ ‖ --> v V ‖ s[i].Ty ----> s[i+1].Tm ‖ | | ‖ | p.b. | ‖ | | ‖ V V (Γ) ---> 1 -----> s[i+1].Ty U_i

Equations

• s.el ilen a a_tp = ⋯.lift a (CategoryTheory.ChosenTerminal.isTerminal.from Γ) ⋯

theorem Model.UnstructuredUniverse.UHomSeq.comp_el {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Δ Γ : Ctx} {i : ℕ} (ilen : i < s.length) (σ : Δ ⟶ Γ) (a : Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : CategoryTheory.CategoryStruct.comp σ (s.el ilen a a_tp) = s.el ilen (CategoryTheory.CategoryStruct.comp σ a) ⋯

theorem Model.UnstructuredUniverse.UHomSeq.comp_el_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Δ Γ : Ctx} {i : ℕ} (ilen : i < s.length) (σ : Δ ⟶ Γ) (a : Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) {Z : Ctx} (h : s[i].Ty ⟶ Z) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (s.el ilen a a_tp) h) = CategoryTheory.CategoryStruct.comp (s.el ilen (CategoryTheory.CategoryStruct.comp σ a) ⋯) h

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.el_code {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] {Γ : Ctx} {i : ℕ} (s : UHomSeq Ctx) (ilen : i < s.length) (A : Γ ⟶ s[i].Ty) : s.el ilen (s.code ilen A) ⋯ = A

@[simp]

theorem Model.UnstructuredUniverse.UHomSeq.code_el {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) {Γ : Ctx} {i : ℕ} (ilen : i < s.length) (a : Γ ⟶ s[i + 1].Tm) (a_tp : CategoryTheory.CategoryStruct.comp a s[i + 1].tp = UHom.wkU Γ (s.homSucc i ilen)) : s.code ilen (s.el ilen a a_tp) = a

@[irreducible]

theorem Model.UnstructuredUniverse.UHomSeq.hom_comp_trans {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] [CategoryTheory.ChosenTerminal Ctx] (s : UHomSeq Ctx) (i j k : ℕ) (ij : i < j) (jk : j < k) (klen : k < s.length + 1) : (s.hom i j ij ⋯).comp (s.hom j k jk klen) = s.hom i k ⋯ klen