---

Step * 1 1 of Lemma csm-universe-type

.....assertion..... 
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. K : fset(ℕ)
6. f : K ⟶ I
7. (t(a) a f) = t(f(a)) ∈ (A:{formal-cube(K) ⊢ _} × formal-cube(K) ⊢ CompOp(A))
8. (fst((t(a) a f))) = (fst(t(f(a)))) ∈ {formal-cube(K) ⊢ _}
⊢ (fst(t(a)))<f> = (fst((t(a) a f))) ∈ {formal-cube(K) ⊢ _}
BY
{ ((Assert t(a) ∈ c𝕌(a) BY
          ((Assert X ⊢' c𝕌 BY Auto) THEN Auto))
   THEN (RWO "cubical-universe-at" (-1) THENA Auto)
   THEN (GenConclTerm ⌜t(a)⌝⋅ THENA Auto)) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. K : fset(ℕ)
6. f : K ⟶ I
7. (t(a) a f) = t(f(a)) ∈ (A:{formal-cube(K) ⊢ _} × formal-cube(K) ⊢ CompOp(A))
8. (fst((t(a) a f))) = (fst(t(f(a)))) ∈ {formal-cube(K) ⊢ _}
9. t(a) ∈ A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A)
10. v : A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A)
11. t(a) = v ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
⊢ (fst(v))<f> = (fst((v a f))) ∈ {formal-cube(K) ⊢ _}

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  X(I)
5.  K  :  fset(\mBbbN{})
6.  f  :  K  {}\mrightarrow{}  I
7.  (t(a)  a  f)  =  t(f(a))
8.  (fst((t(a)  a  f)))  =  (fst(t(f(a))))
\mvdash{}  (fst(t(a)))<f>  =  (fst((t(a)  a  f)))


By

---

Latex:
((Assert  t(a)  \mmember{}  c\mBbbU{}(a)  BY
                ((Assert  X  \mvdash{}'  c\mBbbU{}  BY  Auto)  THEN  Auto))
  THEN  (RWO  "cubical-universe-at"  (-1)  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}t(a)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index