---

Step * 1 of Lemma ctt-level-comp-cumulativity

.....wf..... 
1. X : CubicalSet'''
2. a : ℤ
3. T : {X ⊢ _}
4. b : ℤ
5. a = 0 ∈ ℤ
6. b = 2 ∈ ℤ
7. 0 ≤ 2
⊢ composition-structure{i''':l, i'':l}(X; T) ∈ 𝕌{i 5}
BY
{ ((MemCD THEN Auto) THEN SubsumeC ⌜{X ⊢' _}⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  CubicalSet'''
2.  a  :  \mBbbZ{}
3.  T  :  \{X  \mvdash{}  \_\}
4.  b  :  \mBbbZ{}
5.  a  =  0
6.  b  =  2
7.  0  \mleq{}  2
\mvdash{}  composition-structure\{i''':l,  i'':l\}(X;  T)  \mmember{}  \mBbbU{}\{i  5\}


By

---

Latex:
((MemCD  THEN  Auto)  THEN  SubsumeC  \mkleeneopen{}\{X  \mvdash{}'  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index