---

Step * of Lemma csm-equivU

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[E:{G.𝕀 ⊢ _}]. ∀[cE:G.𝕀 ⊢ CompOp(E)].
  ((equivU(G;E;cE))tau = equivU(K;(E)tau+;(cE)tau+) ∈ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])})
BY
{ (Intros
   THEN (InstLemma `csm-ap-type_wf` [⌜G⌝;⌜G.𝕀⌝;⌜(E)[0(𝕀)]⌝;⌜p⌝]⋅ THENA Auto)
   THEN (InstLemma `transport_wf` [⌜G⌝;⌜Equiv(((E)[0(𝕀)])p;E)⌝]⋅ THENA Auto)
   THEN (InstLemma `csm-cubical-equiv` [⌜G.𝕀⌝;⌜G⌝;⌜[0(𝕀)]⌝;⌜((E)[0(𝕀)])p⌝;⌜E⌝]⋅ THENA Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)
   THEN (Subst' (((E)[0(𝕀)])p)[1(𝕀)] ~ (E)[0(𝕀)] -1 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' (((E)[0(𝕀)])p)[0(𝕀)] ~ (E)[0(𝕀)] -1 THENA (CsmUnfolding THEN Auto))
   THEN Unfold `equivU` 0) }

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(𝕀)]})
⊢ (transport(G;IdEquiv(G;(E)[0(𝕀)])))tau
= transport(K;IdEquiv(K;((E)tau+)[0(𝕀)]))
∈ {K ⊢ _:Equiv(((E)tau+)[0(𝕀)];((E)tau+)[1(𝕀)])}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  G].  \mforall{}[E:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cE:G.\mBbbI{}  \mvdash{}  CompOp(E)].
    ((equivU(G;E;cE))tau  =  equivU(K;(E)tau+;(cE)tau+))


By

---

Latex:
(Intros
  THEN  (InstLemma  `csm-ap-type\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(E)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `transport\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}Equiv(((E)[0(\mBbbI{})])p;E)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `csm-cubical-equiv`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}((E)[0(\mBbbI{})])p\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (Subst'  (((E)[0(\mBbbI{})])p)[1(\mBbbI{})]  \msim{}  (E)[0(\mBbbI{})]  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  (((E)[0(\mBbbI{})])p)[0(\mBbbI{})]  \msim{}  (E)[0(\mBbbI{})]  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  Unfold  `equivU`  0)

---

Home Index