---

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

.....subterm..... T:t
2:n
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}
⊢ <T, x2> ∈ T:{Y ⊢lvl _} × {Y ⊢ _:T}
BY
{ (IntSegCases (-3) THEN Eliminate ⌜lvl⌝⋅ THEN RepUR ``ctt-level-type`` -3 THEN RepUR ``ctt-level-type`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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\}
\mvdash{}  <T,  x2>  \mmember{}  T:\{Y  \mvdash{}lvl  \_\}  \mtimes{}  \{Y  \mvdash{}  \_:T\}


By

---

Latex:
(IntSegCases  (-3)
  THEN  Eliminate  \mkleeneopen{}lvl\mkleeneclose{}\mcdot{}
  THEN  RepUR  ``ctt-level-type``  -3
  THEN  RepUR  ``ctt-level-type``  0
  THEN  Auto)

---

Home Index