---

Step * of Lemma transEquiv-trans-eq2

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 A B)}].
  (transEquivFun(p)
  = (λ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
{ (Intros⋅
   THEN (InstLemma  `cubical-term-at_wf`  [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENA Auto)
   THEN CubicalFunEqual
   THEN (Intros THEN RW (AddrC [3;1;1;1] UnfoldTopAbC) 0)
   THEN Reduce 0
   THEN (InstLemma `transEquiv-trans-eq` [⌜G⌝;⌜A⌝;⌜B⌝;⌜p⌝]⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z(a) J h u⌝ ⌜decode(B)(h(a))⌝ (-1)⋅
         THENA (Fold `member` 0
                THEN (GenConclTerm ⌜Z(a)⌝⋅ THENA Auto)
                THEN (RepUR ``cubical-fun cubical-fun-family`` -2 THEN D -2)
                THEN Auto)
         )
   THEN NthHypEqTrans (-1)
   THEN Unfold `cubical-term-at` 0
   THEN Reduce 0
   THEN (Subst' p I+new-name(I) s(a) ~ p(s(a)) 0 THENA (CsmUnfolding THEN Auto))
   THEN RepeatFor 2 (Thin (-1))) }

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 : fset(ℕ)
7. a : G(I)
8. J : fset(ℕ)
9. h : J ⟶ I
10. u : decode(A)(h(a))
⊢ ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) h,new-name(I)=new-name(J) 0 ⋅ 
   (compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
= ((snd((p J+new-name(J) 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))
∈ 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)
    =  (\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))))


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  CubicalFunEqual
  THEN  (Intros  THEN  RW  (AddrC  [3;1;1;1]  UnfoldTopAbC)  0)
  THEN  Reduce  0
  THEN  (InstLemma  `transEquiv-trans-eq`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z(a)  J  h  u\mkleeneclose{}  \mkleeneopen{}decode(B)(h(a))\mkleeneclose{}  (-1)\mcdot{}
              THENA  (Fold  `member`  0
                            THEN  (GenConclTerm  \mkleeneopen{}Z(a)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (RepUR  ``cubical-fun  cubical-fun-family``  -2  THEN  D  -2)
                            THEN  Auto)
              )
  THEN  NthHypEqTrans  (-1)
  THEN  Unfold  `cubical-term-at`  0
  THEN  Reduce  0
  THEN  (Subst'  p  I+new-name(I)  s(a)  \msim{}  p(s(a))  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index