---

Step * of Lemma transEquiv-trans-eq-path-trans

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 A B)}].
  (transEquivFun(p) = (PathTransport(p) o ConstTrans(decode(A))) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
BY
{ (Intros⋅
   THEN (InstLemma  `cubical-term-at_wf`  [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENA Auto)
   THEN (InstLemma `transEquiv-trans-eq2` [⌜G⌝;⌜A⌝;⌜B⌝;⌜p⌝]⋅ THENA Auto)
   THEN NthHypEqTrans (-1)
   THEN (Assert λI,a,J,h,u. ((snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅) 
                             (compOp(A) J new-name(J) s(h(a)) 0 ⋅ u)) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))} BY
               Eq)
   THEN Thin (-2)
   THEN (BLemma `cubical-fun-equal` THENA Auto)
   THEN Intros⋅
   THEN Unfold `cubical-term-at` 0
   THEN Reduce 0
   THEN (Subst' p J+new-name(J) s(h(a)) ~ p(s(h(a))) 0 THENA (CsmUnfolding THEN Auto))
   THEN RepUR ``cubical-fun-comp cubical-app cubical-lambda`` 0
   THEN RepUR ``const-transport-fun csm-ap-term transport-const cubical-lam cubical-lambda`` 0
   THEN (RWO "path-trans-sq2" 0 THENA Auto)
   THEN RepUR ``transport composition-term csm-composition cc-snd cc-adjoin-cube`` 0
   THEN RepUR ``csm-ap-term discrete-cubical-term csm-ap cc-fst face-0 cubical-term-at`` 0
   THEN RepUR ``cube-context-adjoin`` 0) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. ∀[I:fset(ℕ)]. ∀[a:G(I)].  (p(a) ∈ (Path_c𝕌 A B)(a))
6. λI,a,J,h,u. ((snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅) 
                (compOp(A) J new-name(J) s(h(a)) 0 ⋅ u)) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
7. I : fset(ℕ)
8. a : G(I)
9. J : fset(ℕ)
10. h : J ⟶ I
11. u : decode(A)(h(a))
⊢ ((snd((p J+new-name(J) s(h(a)) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅) 
   (compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
= ((snd((p J+new-name(J) s(1(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅) 
   (compOp(A) J new-name(J) s(1(h(a))) 0 (λI@0,a@0. ⋅) u))
∈ decode(B)(h(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}].
    (transEquivFun(p)  =  (PathTransport(p)  o  ConstTrans(decode(A))))


By

---

Latex:
(Intros\mcdot{}
  THEN  (InstLemma    `cubical-term-at\_wf`    [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{}  A  B)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `transEquiv-trans-eq2`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypEqTrans  (-1)
  THEN  (Assert  \mlambda{}I,a,J,h,u.  ((snd((p(s(h(a)))  J+new-name(J)  1  <new-name(J)>)))  J  new-name(J)  1  0 
                                                      discr(\mcdot{}) 
                                                      (compOp(A)  J  new-name(J)  s(h(a))  0  \mcdot{}  u))  \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B)\000C)\}  BY
                          Eq)
  THEN  Thin  (-2)
  THEN  (BLemma  `cubical-fun-equal`  THENA  Auto)
  THEN  Intros\mcdot{}
  THEN  Unfold  `cubical-term-at`  0
  THEN  Reduce  0
  THEN  (Subst'  p  J+new-name(J)  s(h(a))  \msim{}  p(s(h(a)))  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  RepUR  ``cubical-fun-comp  cubical-app  cubical-lambda``  0
  THEN  RepUR  ``const-transport-fun  csm-ap-term  transport-const  cubical-lam  cubical-lambda``  0
  THEN  (RWO  "path-trans-sq2"  0  THENA  Auto)
  THEN  RepUR  ``transport  composition-term  csm-composition  cc-snd  cc-adjoin-cube``  0
  THEN  RepUR  ``csm-ap-term  discrete-cubical-term  csm-ap  cc-fst  face-0  cubical-term-at``  0
  THEN  RepUR  ``cube-context-adjoin``  0)

---

Home Index