---

Step * 1 of Lemma csm-universe-type


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(f(a)))) ∈ {formal-cube(K) ⊢ _}
BY
{ (Assert ⌜(fst(t(a)))<f> = (fst((t(a) a f))) ∈ {formal-cube(K) ⊢ _}⌝⋅ THENM Eq) }

1
.....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) ⊢ _}

---

Latex:

---

Latex:

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(f(a))))


By

---

Latex:
(Assert  \mkleeneopen{}(fst(t(a)))<f>  =  (fst((t(a)  a  f)))\mkleeneclose{}\mcdot{}  THENM  Eq)

---

Home Index