---

Step * of Lemma path-trans-sq

No Annotations
∀[G,pth,I,a,J,h,u:Top].  (PathTransport(pth) I a J h u ~ compOp(path-eta(pth)) J new-name(J) <s(h(a)), <new-name(J)>> 0 \000Cdiscr(⋅) u)
BY
{ (Intros
   THEN RepUR ``path-trans univ-trans transprt-fun cubical-lambda`` 0
   THEN (RWO "csm-universe-decode" 0 THENA Auto)
   THEN (RWO "csm-path-eta" 0 THENA Auto)
   THEN (Subst' ((pth)p)[0(𝕀)] @ (q)[0(𝕀)] ~ pth @ 0(𝕀) 0
         THENA (CsmUnfolding THEN RepUR ``cubicalpath-app cubical-app`` 0 THEN Auto)
         )
   THEN RepUR ``transprt comp_term csm-id csm-comp-structure csm-comp compose csm+`` 0
   THEN RepUR ``cc-fst csm-adjoin cc-snd comp-op-to-comp-fun csm-composition`` 0
   THEN RepUR ``csm-ap composition-term cc-adjoin-cube face-0`` 0
   THEN RepUR ``cubical-term-at csm-ap-term discrete-cubical-term`` 0
   THEN Fold `discrete-cubical-term` 0
   THEN RepUR ``cube-context-adjoin`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,pth,I,a,J,h,u:Top].
    (PathTransport(pth)  I  a  J  h  u  \msim{}  compOp(path-eta(pth))  J  new-name(J)  <s(h(a)),  <new-name(J)>>  0  dis\000Ccr(\mcdot{})  u)


By

---

Latex:
(Intros
  THEN  RepUR  ``path-trans  univ-trans  transprt-fun  cubical-lambda``  0
  THEN  (RWO  "csm-universe-decode"  0  THENA  Auto)
  THEN  (RWO  "csm-path-eta"  0  THENA  Auto)
  THEN  (Subst'  ((pth)p)[0(\mBbbI{})]  @  (q)[0(\mBbbI{})]  \msim{}  pth  @  0(\mBbbI{})  0
              THENA  (CsmUnfolding  THEN  RepUR  ``cubicalpath-app  cubical-app``  0  THEN  Auto)
              )
  THEN  RepUR  ``transprt  comp\_term  csm-id  csm-comp-structure  csm-comp  compose  csm+``  0
  THEN  RepUR  ``cc-fst  csm-adjoin  cc-snd  comp-op-to-comp-fun  csm-composition``  0
  THEN  RepUR  ``csm-ap  composition-term  cc-adjoin-cube  face-0``  0
  THEN  RepUR  ``cubical-term-at  csm-ap-term  discrete-cubical-term``  0
  THEN  Fold  `discrete-cubical-term`  0
  THEN  RepUR  ``cube-context-adjoin``  0
  THEN  Auto)

---

Home Index