---

Step * 1 1 of Lemma csm-equivU

.....assertion..... 
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. E : {G.𝕀 ⊢ _}
5. cE : G.𝕀 ⊢ CompOp(E)
6. G.𝕀 ⊢ ((E)[0(𝕀)])p
7. ∀[cA:G.𝕀 ⊢ CompOp(Equiv(((E)[0(𝕀)])p;E))]. ∀[a:{G ⊢ _:Equiv((E)[0(𝕀)];(E)[0(𝕀)])}].
     (transport(G;a) ∈ {G ⊢ _:(Equiv(((E)[0(𝕀)])p;E))[1(𝕀)]})
⊢ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])} = {K ⊢ _:((Equiv(((E)[0(𝕀)])p;E))[1(𝕀)])tau} ∈ 𝕌{[i' | j']}
BY
{ EqCDA }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. E : {G.𝕀 ⊢ _}
5. cE : G.𝕀 ⊢ CompOp(E)
6. G.𝕀 ⊢ ((E)[0(𝕀)])p
7. ∀[cA:G.𝕀 ⊢ CompOp(Equiv(((E)[0(𝕀)])p;E))]. ∀[a:{G ⊢ _:Equiv((E)[0(𝕀)];(E)[0(𝕀)])}].
     (transport(G;a) ∈ {G ⊢ _:(Equiv(((E)[0(𝕀)])p;E))[1(𝕀)]})
⊢ Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)]) = ((Equiv(((E)[0(𝕀)])p;E))[1(𝕀)])tau ∈ {K ⊢ _}

---

Latex:

---

Latex:
.....assertion..... 
1.  G  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  G
4.  E  :  \{G.\mBbbI{}  \mvdash{}  \_\}
5.  cE  :  G.\mBbbI{}  \mvdash{}  CompOp(E)
6.  G.\mBbbI{}  \mvdash{}  ((E)[0(\mBbbI{})])p
7.  \mforall{}[cA:G.\mBbbI{}  \mvdash{}  CompOp(Equiv(((E)[0(\mBbbI{})])p;E))].  \mforall{}[a:\{G  \mvdash{}  \_:Equiv((E)[0(\mBbbI{})];(E)[0(\mBbbI{})])\}].
          (transport(G;a)  \mmember{}  \{G  \mvdash{}  \_:(Equiv(((E)[0(\mBbbI{})])p;E))[1(\mBbbI{})]\})
\mvdash{}  \{K  \mvdash{}  \_:Equiv(((E)tau+)[0(\mBbbI{})];((E)tau+)[1(\mBbbI{})])\}  =  \{K  \mvdash{}  \_:((Equiv(((E)[0(\mBbbI{})])p;E))[1(\mBbbI{})])tau\}


By

---

Latex:
EqCDA

---

Home Index