---

Step * of Lemma presheaf-type-cumulativity

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  ({X ⊢ _} ⊆r {X ⊢' _})
BY
{ (Auto THEN At ⌜𝕌''⌝ (D 0)⋅) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. x : {X ⊢ _}
⊢ x ∈ X ⊢' 

2
.....eq aux..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
⊢ istype({X ⊢ _})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].    (\{X  \mvdash{}  \_\}  \msubseteq{}r  \{X  \mvdash{}'  \_\})


By

---

Latex:
(Auto  THEN  At  \mkleeneopen{}\mBbbU{}''\mkleeneclose{}  (D  0)\mcdot{})

---

Home Index