---

Step * 1 of Lemma mk-ctt-term-mng_wf


1. [X] : CubicalSet'''
2. [lvl] : ℕ4
3. [T] : {X ⊢lvl _}
4. {X ⊢ _:T} ∈ 𝕌{i''''}
5. [t] : {X ⊢ _:T}
⊢ <lvl, T, t> ∈ lvl:ℕ4 × T:{X ⊢lvl _} × {X ⊢ _:T}
BY
{ (MemCD
   THENL [Auto
         ; (MemCD THENL [Auto; Auto; (InstLemma `cubical-term_wf-level-type` [⌜X⌝;⌜lvl⌝;⌜T1⌝]⋅ THEN Auto)])
         ; (D 0 THENL [Auto; (InstLemma `cubical-term_wf-level-type` [⌜X⌝;⌜l1⌝;⌜T1⌝]⋅ THEN Auto)])]
) }

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet'''
2.  [lvl]  :  \mBbbN{}4
3.  [T]  :  \{X  \mvdash{}lvl  \_\}
4.  \{X  \mvdash{}  \_:T\}  \mmember{}  \mBbbU{}\{i''''\}
5.  [t]  :  \{X  \mvdash{}  \_:T\}
\mvdash{}  <lvl,  T,  t>  \mmember{}  lvl:\mBbbN{}4  \mtimes{}  T:\{X  \mvdash{}lvl  \_\}  \mtimes{}  \{X  \mvdash{}  \_:T\}


By

---

Latex:
(MemCD
  THENL  [Auto
              ;  (MemCD
                    THENL  [Auto;  Auto;  (InstLemma  `cubical-term\_wf-level-type`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}lvl\mkleeneclose{};\mkleeneopen{}T1\mkleeneclose{}]\mcdot{}  THEN  Auto)]
              )
              ;  (D  0  THENL  [Auto;  (InstLemma  `cubical-term\_wf-level-type`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}T1\mkleeneclose{}]\mcdot{}  THEN  Auto)])]
)

---

Home Index