---

Step * of Lemma mk-ctt-term-mng_wf

No Annotations
∀[X:⊢''']. ∀[lvl:ℕ4]. ∀[T:{X ⊢lvl _}]. ∀[t:{X ⊢ _:T}].  (mk-ctt-term-mng(lvl; T; t) ∈ cttTerm(X))
BY
{ (InstLemma `cubical-term_wf-level-type` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Intro
   THEN RepUR ``mk-ctt-term-mng ctt-term-meaning`` 0) }

1
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}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  \mforall{}[lvl:\mBbbN{}4].  \mforall{}[T:\{X  \mvdash{}lvl  \_\}].  \mforall{}[t:\{X  \mvdash{}  \_:T\}].    (mk-ctt-term-mng(lvl;  T;  t)  \mmember{}  cttTerm(X))


By

---

Latex:
(InstLemma  `cubical-term\_wf-level-type`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intro
  THEN  RepUR  ``mk-ctt-term-mng  ctt-term-meaning``  0)

---

Home Index