---

Step * of Lemma equivU_wf

No Annotations
∀[G:j⊢]. ∀[E:{G.𝕀 ⊢ _}]. ∀[cE:G.𝕀 ⊢ CompOp(E)].  (equivU(G;E;cE) ∈ {G ⊢ _:Equiv((E)[0(𝕀)];(E)[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
   THEN BHyp -1
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[E:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cE:G.\mBbbI{}  \mvdash{}  CompOp(E)].
    (equivU(G;E;cE)  \mmember{}  \{G  \mvdash{}  \_:Equiv((E)[0(\mBbbI{})];(E)[1(\mBbbI{})])\})


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
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index