---

Step * 2 of Lemma ps_context-ext

.....wf..... 
1. C : SmallCategory
⊢ ps_context{j:l}(C) ∈ 𝕌{[j 2 | i]}
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  C  :  SmallCategory
\mvdash{}  ps\_context\{j:l\}(C)  \mmember{}  \mBbbU{}\{[j  2  |  i]\}


By

---

Latex:
Auto

---

Home Index