Step * 1 1 of Lemma cubical-universe-at-cumulativity


1. fset(ℕ)
2. Top
3. {formal-cube(I) ⊢ _}
⊢ formal-cube(I) ⊢A
BY
(RepeatFor (DVar `A') THEN MemTypeCD THEN Auto) }


Latex:


Latex:

1.  I  :  fset(\mBbbN{})
2.  a  :  Top
3.  A  :  \{formal-cube(I)  \mvdash{}  \_\}
\mvdash{}  formal-cube(I)  \mvdash{}'  A


By


Latex:
(RepeatFor  2  (DVar  `A')  THEN  MemTypeCD  THEN  Auto)




Home Index