---

Step * of Lemma cubical-universe-cumulativity2

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}].  (t ∈ {X ⊢ _:c𝕌'})
BY
{ (Intro
   THEN Intro
   THEN Try ((BLemma `istype-cubical-universe-term` THEN Auto))
   THEN Unhide
   THEN (Unfold `cubical-universe` -1 THEN Unfold `cubical-universe` 0)
   THEN D -1
   THEN MemTypeCD
   THEN All (RepUR ``closed-type-to-type closed-cubical-universe``)
   THEN Auto
   THEN RepeatFor 2 ((FunExt THENW Auto))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].    (t  \mmember{}  \{X  \mvdash{}  \_:c\mBbbU{}'\})


By

---

Latex:
(Intro
  THEN  Intro
  THEN  Try  ((BLemma  `istype-cubical-universe-term`  THEN  Auto))
  THEN  Unhide
  THEN  (Unfold  `cubical-universe`  -1  THEN  Unfold  `cubical-universe`  0)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  All  (RepUR  ``closed-type-to-type  closed-cubical-universe``)
  THEN  Auto
  THEN  RepeatFor  2  ((FunExt  THENW  Auto))
  THEN  Auto)

---

Home Index