---

Step * 1 of Lemma universe-encode_wf


1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. a : G(I)
⊢ <(T)<a>, (cT)<a>> ∈ A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A)
BY
{ Auto }

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  T  :  \{G  \mvdash{}  \_\}
3.  cT  :  G  \mvdash{}  CompOp(T)
4.  G  \mvdash{}'  c\mBbbU{}
5.  I  :  fset(\mBbbN{})
6.  a  :  G(I)
\mvdash{}  <(T)<a>,  (cT)<a>>  \mmember{}  A:\{formal-cube(I)  \mvdash{}  \_\}  \mtimes{}  formal-cube(I)  \mvdash{}  CompOp(A)


By

---

Latex:
Auto

---

Home Index