---

Step * of Lemma path-trans-sq2

No Annotations
∀[G,pth,I,a,J,h,u:Top].
  (PathTransport(pth) I a J h u ~ (snd((pth(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅) u)
BY
{ (Intros
   THEN (RWO "path-trans-sq" 0 THENA Auto)
   THEN RepUR ``universe-comp-op path-eta cubicalpath-app cubical-app cubical-term-at cc-fst cc-snd`` 0
   THEN RepUR ``csm-ap-term csm-ap`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,pth,I,a,J,h,u:Top].
    (PathTransport(pth)  I  a  J  h  u  \msim{}  (snd((pth(s(h(a)))  J+new-name(J)  1  <new-name(J)>)))  J  new-name(J) 
                                                                    1 
                                                                    0 
                                                                    discr(\mcdot{}) 
                                                                    u)


By

---

Latex:
(Intros
  THEN  (RWO  "path-trans-sq"  0  THENA  Auto)
  THEN  ...
  THEN  RepUR  ``csm-ap-term  csm-ap``  0
  THEN  Auto)

---

Home Index