---

Step * 1 of Lemma csm-equivU


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(𝕀)]})
⊢ (transport(G;IdEquiv(G;(E)[0(𝕀)])))tau
= transport(K;IdEquiv(K;((E)tau+)[0(𝕀)]))
∈ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])}
BY
{ (Assert ⌜{K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])} = {K ⊢ _:((Equiv(((E)[0(𝕀)])p;E))[1(𝕀)])tau} ∈ 𝕌{[i' | j']}⌝⋅
THENM (RWO "csm-transport" 0 THENA (Try ((Unfold `label` 0 THEN Eq)) THEN Try (Fold `equivU` 0) THEN Auto))
) }

1
.....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']}

2
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(𝕀)]})
8. {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])} = {K ⊢ _:((Equiv(((E)[0(𝕀)])p;E))[1(𝕀)])tau} ∈ 𝕌{[i' | j']}
⊢ transport(K;(IdEquiv(G;(E)[0(𝕀)]))tau)
= transport(K;IdEquiv(K;((E)tau+)[0(𝕀)]))
∈ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])}

---

Latex:

---

Latex:

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{}  (transport(G;IdEquiv(G;(E)[0(\mBbbI{})])))tau  =  transport(K;IdEquiv(K;((E)tau+)[0(\mBbbI{})]))


By

---

Latex:
(Assert  \mkleeneopen{}\{K  \mvdash{}  \_:Equiv(((E)tau+)[0(\mBbbI{})];((E)tau+)[1(\mBbbI{})])\}
                  =  \{K  \mvdash{}  \_:((Equiv(((E)[0(\mBbbI{})])p;E))[1(\mBbbI{})])tau\}\mkleeneclose{}\mcdot{}
THENM  (RWO  "csm-transport"  0
              THENA  (Try  ((Unfold  `label`  0  THEN  Eq))  THEN  Try  (Fold  `equivU`  0)  THEN  Auto)
              )
)

---

Home Index