---

Step * 1 2 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(𝕀)]})
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(𝕀)])}
BY
{ (Assert ⌜((λcA,a. transport(K;a)) (equiv-comp(G.𝕀;((E)[0(𝕀)])p;E;((cE)[0(𝕀)])p;cE))tau+ (IdEquiv(G;(E)[0(𝕀)]))tau)
           = ((λcA,a. transport(K;a)) equiv-comp(K.𝕀;(((E)tau+)[0(𝕀)])p;(E)tau+;(((cE)tau+)[0(𝕀)])p;(cE)tau+) 
              IdEquiv(K;((E)tau+)[0(𝕀)]))
           ∈ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])}⌝⋅
THENM (Reduce -1 THEN Trivial)
) }

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(𝕀)]})
8. {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])} = {K ⊢ _:((Equiv(((E)[0(𝕀)])p;E))[1(𝕀)])tau} ∈ 𝕌{[i' | j']}
⊢ ((λcA,a. transport(K;a)) (equiv-comp(G.𝕀;((E)[0(𝕀)])p;E;((cE)[0(𝕀)])p;cE))tau+ (IdEquiv(G;(E)[0(𝕀)]))tau)
= ((λcA,a. transport(K;a)) equiv-comp(K.𝕀;(((E)tau+)[0(𝕀)])p;(E)tau+;(((cE)tau+)[0(𝕀)])p;(cE)tau+) 
   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{})]\})
8.  \{K  \mvdash{}  \_:Equiv(((E)tau+)[0(\mBbbI{})];((E)tau+)[1(\mBbbI{})])\}  =  \{K  \mvdash{}  \_:((Equiv(((E)[0(\mBbbI{})])p;E))[1(\mBbbI{})])tau\}
\mvdash{}  transport(K;(IdEquiv(G;(E)[0(\mBbbI{})]))tau)  =  transport(K;IdEquiv(K;((E)tau+)[0(\mBbbI{})]))


By

---

Latex:
(Assert  \mkleeneopen{}((\mlambda{}cA,a.  transport(K;a))  (equiv-comp(G.\mBbbI{};((E)[0(\mBbbI{})])p;E;((cE)[0(\mBbbI{})])p;cE))tau+ 
                    (IdEquiv(G;(E)[0(\mBbbI{})]))tau)
                  =  ((\mlambda{}cA,a.  transport(K;a)) 
                        equiv-comp(K.\mBbbI{};(((E)tau+)[0(\mBbbI{})])p;(E)tau+;(((cE)tau+)[0(\mBbbI{})])p;(cE)tau+) 
                        IdEquiv(K;((E)tau+)[0(\mBbbI{})]))\mkleeneclose{}\mcdot{}
THENM  (Reduce  -1  THEN  Trivial)
)

---

Home Index