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

.....subterm..... T:t
1:n
1. fset(ℕ)
2. Top
3. {formal-cube(I) ⊢ _}
4. x1 formal-cube(I) ⊢ CompOp(A)
⊢ formal-cube(I) ⊢A
BY
Thin (-1) }

1
1. fset(ℕ)
2. Top
3. {formal-cube(I) ⊢ _}
⊢ formal-cube(I) ⊢A


Latex:


Latex:
.....subterm.....  T:t
1:n
1.  I  :  fset(\mBbbN{})
2.  a  :  Top
3.  A  :  \{formal-cube(I)  \mvdash{}  \_\}
4.  x1  :  formal-cube(I)  \mvdash{}  CompOp(A)
\mvdash{}  formal-cube(I)  \mvdash{}'  A


By


Latex:
Thin  (-1)




Home Index