---

Step * 1 1 of Lemma cubical-universe_wf

.....subterm..... T:t
1:n
λI.{unit-cube(I) ⊢ _(Kan)} ∈ L:(Cname List) ⟶ 𝕌'
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
\mlambda{}I.\{unit-cube(I)  \mvdash{}  \_(Kan)\}  \mmember{}  L:(Cname  List)  {}\mrightarrow{}  \mBbbU{}'


By

---

Latex:
Auto

---

Home Index