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

A natural model with support for dependent types (and nothing more). The data is a natural transformation with representable fibers, stored as a choice of representative for each fiber.

• Tm : Ctx
• Ty : Ctx
• tp : self.Tm ⟶ self.Ty
• ext {Γ : Ctx} (A : Γ ⟶ self.Ty) : Ctx
• disp {Γ : Ctx} (A : Γ ⟶ self.Ty) : self.ext A ⟶ Γ
• var {Γ : Ctx} (A : Γ ⟶ self.Ty) : self.ext A ⟶ self.Tm
• disp_pullback {Γ : Ctx} (A : Γ ⟶ self.Ty) : CategoryTheory.IsPullback (self.var A) (self.disp A) self.tp A

@[simp]

theorem Model.UnstructuredUniverse.var_tp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) : CategoryTheory.CategoryStruct.comp (M.var A) M.tp = CategoryTheory.CategoryStruct.comp (M.disp A) A

@[simp]

theorem Model.UnstructuredUniverse.var_tp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) {Z : Ctx} (h : M.Ty ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.var A) (CategoryTheory.CategoryStruct.comp M.tp h) = CategoryTheory.CategoryStruct.comp (M.disp A) (CategoryTheory.CategoryStruct.comp A h)

Pullback of representable natural transformation

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

Pull a natural model back along a type.

Equations

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

def Model.UnstructuredUniverse.ofIsPullback {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {U E : Ctx} {π : E ⟶ U} {toTy : U ⟶ M.Ty} {toTm : E ⟶ M.Tm} (pb : CategoryTheory.IsPullback toTm π M.tp toTy) : UnstructuredUniverse Ctx

Given the pullback square on the right, with a natural model structure on tp : Tm ⟶ Ty giving the outer pullback square.

Γ.A -.-.- var -.-,-> E ------ toTm ------> Tm | | | | | | M.disp π tp | | | V V V Γ ------- A -------> U ------ toTy ------> Ty

construct a natural model structure on π : E ⟶ U, by pullback pasting.

Equations

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

Substitutions

def Model.UnstructuredUniverse.substCons {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (t_tp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) : Δ ⟶ M.ext A

Δ ⊢ σ : Γ  Γ ⊢ A type  Δ ⊢ t : A[σ]
-----------------------------------
Δ ⊢ σ.t : Γ.A

------ Δ ------ t --------¬ | ↓ substCons ↓ | M.ext A ---var A---> M.Tm | | | σ | | | disp A M.tp | | | | V V ---> Γ ------ A -----> M.Ty

Equations

• M.substCons σ A t t_tp = ⋯.lift t σ t_tp

@[simp]

theorem Model.UnstructuredUniverse.substCons_disp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (tTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp (M.substCons σ A t tTp) (M.disp A) = σ

@[simp]

theorem Model.UnstructuredUniverse.substCons_disp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (tTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) {Z : Ctx} (h : Γ ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substCons σ A t tTp) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = CategoryTheory.CategoryStruct.comp σ h

@[simp]

theorem Model.UnstructuredUniverse.substCons_var {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (aTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp (M.substCons σ A t aTp) (M.var A) = t

@[simp]

theorem Model.UnstructuredUniverse.substCons_var_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (aTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) {Z : Ctx} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substCons σ A t aTp) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp t h

@[simp]

theorem Model.UnstructuredUniverse.comp_substCons {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Θ Δ Γ : Ctx} (τ : Θ ⟶ Δ) (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (t : Δ ⟶ M.Tm) (aTp : CategoryTheory.CategoryStruct.comp t M.tp = CategoryTheory.CategoryStruct.comp σ A) : CategoryTheory.CategoryStruct.comp τ (M.substCons σ A t aTp) = M.substCons (CategoryTheory.CategoryStruct.comp τ σ) A (CategoryTheory.CategoryStruct.comp τ t) ⋯

@[simp]

theorem Model.UnstructuredUniverse.substCons_apply_comp_var {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (s : Δ ⟶ M.ext A) (s_tp : CategoryTheory.CategoryStruct.comp s (M.disp A) = σ) : M.substCons σ A (CategoryTheory.CategoryStruct.comp s (M.var A)) ⋯ = s

@[simp]

theorem Model.UnstructuredUniverse.substCons_apply_comp_var_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (s : Δ ⟶ M.ext A) (s_tp : CategoryTheory.CategoryStruct.comp s (M.disp A) = σ) {Z : Ctx} (h : M.ext A ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substCons σ A (CategoryTheory.CategoryStruct.comp s (M.var A)) ⋯) h = CategoryTheory.CategoryStruct.comp s h

def Model.UnstructuredUniverse.substFst {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} {A : Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) : Δ ⟶ Γ

Δ ⊢ σ : Γ.A
------------
Δ ⊢ ↑∘σ : Γ

Equations

• M.substFst σ = CategoryTheory.CategoryStruct.comp σ (M.disp A)

def Model.UnstructuredUniverse.substSnd {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} {A : Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) : Δ ⟶ M.Tm

Δ ⊢ σ : Γ.A
-------------------
Δ ⊢ v₀[σ] : A[↑∘σ]

Equations

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

theorem Model.UnstructuredUniverse.substSnd_tp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} {A : Γ ⟶ M.Ty} (σ : Δ ⟶ M.ext A) : CategoryTheory.CategoryStruct.comp (M.substSnd σ) M.tp = CategoryTheory.CategoryStruct.comp (M.substFst σ) A

def Model.UnstructuredUniverse.substWk {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (A' : Δ ⟶ M.Ty := CategoryTheory.CategoryStruct.comp σ A) (eq : CategoryTheory.CategoryStruct.comp σ A = A' := by rfl) : M.ext A' ⟶ M.ext A

Weaken a substitution.

Δ ⊢ σ : Γ  Γ ⊢ A type  A' = A[σ]
------------------------------------
Δ.A' ⊢ ↑≫σ : Γ  Δ.A' ⊢ v₀ : A[↑≫σ]
------------------------------------
Δ.A' ⊢ (↑≫σ).v₀ : Γ.A

Equations

• M.substWk σ A A' eq = M.substCons (CategoryTheory.CategoryStruct.comp (M.disp A') σ) A (M.var A') ⋯

@[simp]

theorem Model.UnstructuredUniverse.substWk_disp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (A' : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = A') : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (M.disp A) = CategoryTheory.CategoryStruct.comp (M.disp A') σ

@[simp]

theorem Model.UnstructuredUniverse.substWk_disp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (A' : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = A') {Z : Ctx} (h : Γ ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = CategoryTheory.CategoryStruct.comp (M.disp A') (CategoryTheory.CategoryStruct.comp σ h)

@[simp]

theorem Model.UnstructuredUniverse.substWk_var {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (A' : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = A') : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (M.var A) = M.var A'

@[simp]

theorem Model.UnstructuredUniverse.substWk_var_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (A' : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = A') {Z : Ctx} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.substWk σ A A' eq) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp (M.var A') h

theorem Model.UnstructuredUniverse.var_comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) : M.var (CategoryTheory.CategoryStruct.comp σ A) = CategoryTheory.CategoryStruct.comp (M.substWk σ A (CategoryTheory.CategoryStruct.comp σ A) ⋯) (M.var A)

def Model.UnstructuredUniverse.sec {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) : Γ ⟶ M.ext A

sec is the section of disp A corresponding to a.

===== Γ ------ a --------¬ ‖ ↓ sec V ‖ M.ext A -----------> M.Tm ‖ | | ‖ | | ‖ disp A M.tp ‖ | | ‖ V V ===== Γ ------ A -----> M.Ty

Equations

• M.sec A a a_tp = M.substCons (CategoryTheory.CategoryStruct.id Γ) A a ⋯

@[simp]

theorem Model.UnstructuredUniverse.sec_disp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) : CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (M.disp A) = CategoryTheory.CategoryStruct.id Γ

@[simp]

theorem Model.UnstructuredUniverse.sec_disp_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {Z : Ctx} (h : Γ ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (CategoryTheory.CategoryStruct.comp (M.disp A) h) = h

@[simp]

theorem Model.UnstructuredUniverse.sec_var {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) : CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (M.var A) = a

@[simp]

theorem Model.UnstructuredUniverse.sec_var_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {Z : Ctx} (h : M.Tm ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) (CategoryTheory.CategoryStruct.comp (M.var A) h) = CategoryTheory.CategoryStruct.comp a h

theorem Model.UnstructuredUniverse.comp_sec {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (σA : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) : CategoryTheory.CategoryStruct.comp σ (M.sec A a a_tp) = CategoryTheory.CategoryStruct.comp (M.sec σA (CategoryTheory.CategoryStruct.comp σ a) ⋯) (M.substWk σ A σA eq)

theorem Model.UnstructuredUniverse.comp_sec_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ M.Ty) (σA : Δ ⟶ M.Ty) (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (a : Γ ⟶ M.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a M.tp = A) {Z : Ctx} (h : M.ext A ⟶ Z) : CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (M.sec A a a_tp) h) = CategoryTheory.CategoryStruct.comp (M.sec σA (CategoryTheory.CategoryStruct.comp σ a) ⋯) (CategoryTheory.CategoryStruct.comp (M.substWk σ A σA eq) h)

@[simp]

theorem Model.UnstructuredUniverse.sec_apply_comp_var {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (s : Γ ⟶ M.ext A) (s_tp : CategoryTheory.CategoryStruct.comp s (M.disp A) = CategoryTheory.CategoryStruct.id Γ) : M.sec A (CategoryTheory.CategoryStruct.comp s (M.var A)) ⋯ = s

@[simp]

theorem Model.UnstructuredUniverse.sec_apply_comp_var_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (M : UnstructuredUniverse Ctx) {Γ : Ctx} (A : Γ ⟶ M.Ty) (s : Γ ⟶ M.ext A) (s_tp : CategoryTheory.CategoryStruct.comp s (M.disp A) = CategoryTheory.CategoryStruct.id Γ) {Z : Ctx} (h : M.ext A ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.sec A (CategoryTheory.CategoryStruct.comp s (M.var A)) ⋯) h = CategoryTheory.CategoryStruct.comp s h

structure Model.UnstructuredUniverse.PolymorphicSigma {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (U0 U1 U2 : UnstructuredUniverse Ctx) : Type (max u u_1)

• Sig {Γ : Ctx} {A : Γ ⟶ U0.Ty} : (U0.ext A ⟶ U1.Ty) → (Γ ⟶ U2.Ty)
• Sig_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ U0.Ty) {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty) : self.Sig (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) = CategoryTheory.CategoryStruct.comp σ (self.Sig B)
• pair {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (b : Γ ⟶ U1.Tm) : CategoryTheory.CategoryStruct.comp b U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A a a_tp) B → (Γ ⟶ U2.Tm)
• pair_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty) (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (b : Γ ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A a a_tp) B) : self.pair (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) (CategoryTheory.CategoryStruct.comp σ a) ⋯ (CategoryTheory.CategoryStruct.comp σ b) ⋯ = CategoryTheory.CategoryStruct.comp σ (self.pair B a a_tp b b_tp)
• pair_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (b : Γ ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A a a_tp) B) : CategoryTheory.CategoryStruct.comp (self.pair B a a_tp b b_tp) U2.tp = self.Sig B
• fst {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (s : Γ ⟶ U2.Tm) : CategoryTheory.CategoryStruct.comp s U2.tp = self.Sig B → (Γ ⟶ U0.Tm)
• fst_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (s : Γ ⟶ U2.Tm) (s_tp : CategoryTheory.CategoryStruct.comp s U2.tp = self.Sig B) : CategoryTheory.CategoryStruct.comp (self.fst B s s_tp) U0.tp = A
• snd {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (s : Γ ⟶ U2.Tm) : CategoryTheory.CategoryStruct.comp s U2.tp = self.Sig B → (Γ ⟶ U1.Tm)
• snd_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (s : Γ ⟶ U2.Tm) (s_tp : CategoryTheory.CategoryStruct.comp s U2.tp = self.Sig B) : CategoryTheory.CategoryStruct.comp (self.snd B s s_tp) U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A (self.fst B s s_tp) ⋯) B
• fst_pair {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (b : Γ ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A a a_tp) B) : self.fst B (self.pair B a a_tp b b_tp) ⋯ = a
• snd_pair {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (b : Γ ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = CategoryTheory.CategoryStruct.comp (U0.sec A a a_tp) B) : self.snd B (self.pair B a a_tp b b_tp) ⋯ = b
• eta {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (s : Γ ⟶ U2.Tm) (s_tp : CategoryTheory.CategoryStruct.comp s U2.tp = self.Sig B) : self.pair B (self.fst B s s_tp) ⋯ (self.snd B s s_tp) ⋯ = s

def Model.UnstructuredUniverse.PolymorphicSigma.mk' {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 U2 : UnstructuredUniverse Ctx} (Sig : {Γ : Ctx} → {A : Γ ⟶ U0.Ty} → (U0.ext A ⟶ U1.Ty) → (Γ ⟶ U2.Ty)) (Sig_comp : ∀ {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ U0.Ty) {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty), Sig (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) = CategoryTheory.CategoryStruct.comp σ (Sig B)) (assoc : {Γ : Ctx} → {A : Γ ⟶ U0.Ty} → (B : U0.ext A ⟶ U1.Ty) → U1.ext B ≅ U2.ext (Sig B)) (assoc_comp : ∀ {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty), CategoryTheory.CategoryStruct.comp (assoc (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B)).hom (U2.substWk σ (Sig B) (Sig (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B)) ⋯) = CategoryTheory.CategoryStruct.comp (U1.substWk (U0.substWk σ A σA eq) B (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) ⋯) (assoc B).hom) (assoc_disp : ∀ {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty), CategoryTheory.CategoryStruct.comp (assoc B).hom (U2.disp (Sig B)) = CategoryTheory.CategoryStruct.comp (U1.disp B) (U0.disp A)) : U0.PolymorphicSigma U1 U2

Equations

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

theorem Model.UnstructuredUniverse.PolymorphicSigma.fst_comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 U2 : UnstructuredUniverse Ctx} (S : U0.PolymorphicSigma U1 U2) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) {B : U0.ext A ⟶ U1.Ty} (s : Γ ⟶ U2.Tm) (s_tp : CategoryTheory.CategoryStruct.comp s U2.tp = S.Sig B) : S.fst (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) (CategoryTheory.CategoryStruct.comp σ s) ⋯ = CategoryTheory.CategoryStruct.comp σ (S.fst B s s_tp)

theorem Model.UnstructuredUniverse.PolymorphicSigma.snd_comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 U2 : UnstructuredUniverse Ctx} (S : U0.PolymorphicSigma U1 U2) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) {B : U0.ext A ⟶ U1.Ty} (s : Γ ⟶ U2.Tm) (s_tp : CategoryTheory.CategoryStruct.comp s U2.tp = S.Sig B) : S.snd (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) (CategoryTheory.CategoryStruct.comp σ s) ⋯ = CategoryTheory.CategoryStruct.comp σ (S.snd B s s_tp)

structure Model.UnstructuredUniverse.PolymorphicPi {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (U0 U1 U2 : UnstructuredUniverse Ctx) : Type (max u u_1)

• Pi {Γ : Ctx} {A : Γ ⟶ U0.Ty} : (U0.ext A ⟶ U1.Ty) → (Γ ⟶ U2.Ty)
• Pi_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ U0.Ty) {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty) : self.Pi (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) = CategoryTheory.CategoryStruct.comp σ (self.Pi B)
• lam {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (b : U0.ext A ⟶ U1.Tm) : CategoryTheory.CategoryStruct.comp b U1.tp = B → (Γ ⟶ U2.Tm)
• lam_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) (B : U0.ext A ⟶ U1.Ty) (b : U0.ext A ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = B) : self.lam (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) b) ⋯ = CategoryTheory.CategoryStruct.comp σ (self.lam B b b_tp)
• lam_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (b : U0.ext A ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = B) : CategoryTheory.CategoryStruct.comp (self.lam B b b_tp) U2.tp = self.Pi B
• unLam {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (f : Γ ⟶ U2.Tm) : CategoryTheory.CategoryStruct.comp f U2.tp = self.Pi B → (U0.ext A ⟶ U1.Tm)
• unLam_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (f : Γ ⟶ U2.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f U2.tp = self.Pi B) : CategoryTheory.CategoryStruct.comp (self.unLam B f f_tp) U1.tp = B
• unLam_lam {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (b : U0.ext A ⟶ U1.Tm) (b_tp : CategoryTheory.CategoryStruct.comp b U1.tp = B) : self.unLam B (self.lam B b b_tp) ⋯ = b
• lam_unLam {Γ : Ctx} {A : Γ ⟶ U0.Ty} (B : U0.ext A ⟶ U1.Ty) (f : Γ ⟶ U2.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f U2.tp = self.Pi B) : self.lam B (self.unLam B f f_tp) ⋯ = f

theorem Model.UnstructuredUniverse.PolymorphicPi.unLam_comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 U2 : UnstructuredUniverse Ctx} (P : U0.PolymorphicPi U1 U2) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} {σA : Δ ⟶ U0.Ty} (eq : CategoryTheory.CategoryStruct.comp σ A = σA) {B : U0.ext A ⟶ U1.Ty} (f : Γ ⟶ U2.Tm) (f_tp : CategoryTheory.CategoryStruct.comp f U2.tp = P.Pi B) : P.unLam (CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) B) (CategoryTheory.CategoryStruct.comp σ f) ⋯ = CategoryTheory.CategoryStruct.comp (U0.substWk σ A σA eq) (P.unLam B f f_tp)

structure Model.UnstructuredUniverse.PolymorphicIdIntro {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] (U0 U1 : UnstructuredUniverse Ctx) : Type (max u u_1)

• Id {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) : CategoryTheory.CategoryStruct.comp a0 U0.tp = A → CategoryTheory.CategoryStruct.comp a1 U0.tp = A → (Γ ⟶ U1.Ty)
• Id_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a0 a1 : Γ ⟶ U0.Tm) (a0_tp : CategoryTheory.CategoryStruct.comp a0 U0.tp = A) (a1_tp : CategoryTheory.CategoryStruct.comp a1 U0.tp = A) : self.Id (CategoryTheory.CategoryStruct.comp σ a0) (CategoryTheory.CategoryStruct.comp σ a1) ⋯ ⋯ = CategoryTheory.CategoryStruct.comp σ (self.Id a0 a1 a0_tp a1_tp)
• refl {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) : CategoryTheory.CategoryStruct.comp a U0.tp = A → (Γ ⟶ U1.Tm)
• refl_comp {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : self.refl (CategoryTheory.CategoryStruct.comp σ a) ⋯ = CategoryTheory.CategoryStruct.comp σ (self.refl a a_tp)
• refl_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : CategoryTheory.CategoryStruct.comp (self.refl a a_tp) U1.tp = self.Id a a a_tp a_tp

@[simp]

theorem Model.UnstructuredUniverse.PolymorphicIdIntro.refl_tp' {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : CategoryTheory.CategoryStruct.comp (i.refl a a_tp) U1.tp = i.Id a a a_tp a_tp

@[reducible, inline]

abbrev Model.UnstructuredUniverse.PolymorphicIdIntro.weakenId {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : U0.ext A ⟶ U1.Ty

Given Γ ⊢ a : A this is the identity type weakened to the context Γ.(x : A) ⊢ Id(a,x) : U1.Ty

Equations

• i.weakenId a a_tp = i.Id (CategoryTheory.CategoryStruct.comp (U0.disp A) a) (U0.var A) ⋯ ⋯

theorem Model.UnstructuredUniverse.PolymorphicIdIntro.weakenId_comp {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : i.weakenId (CategoryTheory.CategoryStruct.comp σ a) ⋯ = CategoryTheory.CategoryStruct.comp (U0.substWk σ A (CategoryTheory.CategoryStruct.comp σ A) ⋯) (i.weakenId a a_tp)

@[reducible, inline]

abbrev Model.UnstructuredUniverse.PolymorphicIdIntro.motiveCtx {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : Ctx

Given Γ ⊢ a : A this is the context Γ.(x : A).(h:Id(a,x))

Equations

• i.motiveCtx a a_tp = U1.ext (i.weakenId a a_tp)

@[reducible, inline]

abbrev Model.UnstructuredUniverse.PolymorphicIdIntro.reflSubst {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) : Γ ⟶ i.motiveCtx a a_tp

Given Γ ⊢ a : A, reflSubst is the substitution (a,refl) : Γ ⟶ Γ.(x:A).(h:Id(a,x)) appearing in identity elimination J so that we can write Γ ⊢ r : C(a,refl)

Equations

• i.reflSubst a a_tp = U1.substCons (U0.sec A a a_tp) (i.weakenId a a_tp) (i.refl a a_tp) ⋯

@[reducible, inline]

abbrev Model.UnstructuredUniverse.PolymorphicIdIntro.motiveSubst {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) {σA : Δ ⟶ U0.Ty} (eq : σA = CategoryTheory.CategoryStruct.comp σ A := by rfl) : i.motiveCtx (CategoryTheory.CategoryStruct.comp σ a) ⋯ ⟶ i.motiveCtx a a_tp

Given a substitution σ : Δ ⟶ Γ and Γ ⊢ a : A, this is the substitution Δ.(x: σ ≫ A).(h:Id(σ ≫ a,x)) ⟶ Γ.(x:A).(h:Id(a,x))

Equations

• i.motiveSubst σ a a_tp eq = U1.substWk (U0.substWk σ A σA ⋯) (i.weakenId a a_tp) (i.weakenId (CategoryTheory.CategoryStruct.comp σ a) ⋯) ⋯

@[simp]

theorem Model.UnstructuredUniverse.PolymorphicIdIntro.reflSubst_comp_motiveSubst {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) {σA : Δ ⟶ U0.Ty} (eq : σA = CategoryTheory.CategoryStruct.comp σ A := by rfl) : CategoryTheory.CategoryStruct.comp (i.reflSubst (CategoryTheory.CategoryStruct.comp σ a) ⋯) (i.motiveSubst σ a a_tp eq) = CategoryTheory.CategoryStruct.comp σ (i.reflSubst a a_tp)

@[simp]

theorem Model.UnstructuredUniverse.PolymorphicIdIntro.reflSubst_comp_motiveSubst_assoc {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) {σA : Δ ⟶ U0.Ty} (eq : σA = CategoryTheory.CategoryStruct.comp σ A := by rfl) {Z : Ctx} (h : i.motiveCtx a a_tp ⟶ Z) : CategoryTheory.CategoryStruct.comp (i.reflSubst (CategoryTheory.CategoryStruct.comp σ a) ⋯) (CategoryTheory.CategoryStruct.comp (i.motiveSubst σ a a_tp eq) h) = CategoryTheory.CategoryStruct.comp σ (CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) h)

structure Model.UnstructuredUniverse.PolymorphicIdElim {Ctx : Type u} [CategoryTheory.Category.{u_1, u} Ctx] {U0 U1 : UnstructuredUniverse Ctx} (i : U0.PolymorphicIdIntro U1) (U2 : UnstructuredUniverse Ctx) : Type (max u u_1)

• j {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (C : i.motiveCtx a a_tp ⟶ U2.Ty) (c : Γ ⟶ U2.Tm) : CategoryTheory.CategoryStruct.comp c U2.tp = CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) C → (i.motiveCtx a a_tp ⟶ U2.Tm)
• comp_j {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (C : i.motiveCtx a a_tp ⟶ U2.Ty) (c : Γ ⟶ U2.Tm) (c_tp : CategoryTheory.CategoryStruct.comp c U2.tp = CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) C) : self.j (CategoryTheory.CategoryStruct.comp σ a) ⋯ (CategoryTheory.CategoryStruct.comp (i.motiveSubst σ a a_tp ⋯) C) (CategoryTheory.CategoryStruct.comp σ c) ⋯ = CategoryTheory.CategoryStruct.comp (i.motiveSubst σ a a_tp ⋯) (self.j a a_tp C c c_tp)
• j_tp {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (C : i.motiveCtx a a_tp ⟶ U2.Ty) (c : Γ ⟶ U2.Tm) (c_tp : CategoryTheory.CategoryStruct.comp c U2.tp = CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) C) : CategoryTheory.CategoryStruct.comp (self.j a a_tp C c c_tp) U2.tp = C
• reflSubst_j {Γ : Ctx} {A : Γ ⟶ U0.Ty} (a : Γ ⟶ U0.Tm) (a_tp : CategoryTheory.CategoryStruct.comp a U0.tp = A) (C : i.motiveCtx a a_tp ⟶ U2.Ty) (c : Γ ⟶ U2.Tm) (c_tp : CategoryTheory.CategoryStruct.comp c U2.tp = CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) C) : CategoryTheory.CategoryStruct.comp (i.reflSubst a a_tp) (self.j a a_tp C c c_tp) = c