---

Step * 2 of Lemma ctt-term-meaning-subtype

.....eq aux..... 
1. X : CubicalSet'''
2. Y : CubicalSet'''
3. sub_cubical_set{i''':l}(Y; X)
4. lvl : ℕ4
5. T : {X ⊢lvl _}
6. x2 : {X ⊢ _:T}
7. l1 : ℕ4
⊢ istype(T:{Y ⊢l1 _} × {Y ⊢ _:T})
BY
{ (IntSegCases (-1) THEN RepUR ``ctt-level-type`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  X  :  CubicalSet'''
2.  Y  :  CubicalSet'''
3.  sub\_cubical\_set\{i''':l\}(Y;  X)
4.  lvl  :  \mBbbN{}4
5.  T  :  \{X  \mvdash{}lvl  \_\}
6.  x2  :  \{X  \mvdash{}  \_:T\}
7.  l1  :  \mBbbN{}4
\mvdash{}  istype(T:\{Y  \mvdash{}l1  \_\}  \mtimes{}  \{Y  \mvdash{}  \_:T\})


By

---

Latex:
(IntSegCases  (-1)  THEN  RepUR  ``ctt-level-type``  0  THEN  Auto)

---

Home Index