---

Step * of Lemma transEquiv-trans-sq

No Annotations
∀[G,A,p,I,a,J,f,u:Top].
  (transEquivFun(p) I a J f u ~ let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)> 
                                in cA J new-name(J) 
                                   1 ⋅ cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ <new-name(J)>> ⋅ 1 
                                   (0)<1 ⋅ f> ∨ 0 
                                   (λI@1,a@0. (if ((0)<1 ⋅ f ⋅ s ⋅ a@0>==1) then (fst(⋅)) I@1 1 else λu.u fi  
                                               ((snd((A I@1+new-name(I@1) 
                                                      cube+(I;new-name(I)) I@1+new-name(I@1) 
                                                      <1 ⋅ f ⋅ s ⋅ a@0 ⋅ s
                                                      , 1 ∧ ¬(dM-lift(I@1+new-name(I@1);I@1;s) 
                                                              ¬(dM-lift(I@1;J+new-name(J);a@0) 
                                                                <new-name(J)>) ∧ <new-name(I@1)>)
                                                      >(1(1(1(s(1(a))))))))) 
                                                I@1 
                                                new-name(I@1) 
                                                1 
                                                0 ∨ dM-to-FL(I@1;¬(¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>))) 
                                                (λI@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1)) 
                                                ((u 1 s) 1 a@0)))) 
                                   ((snd((A J+new-name(J) 
                                          cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ ¬(1 ∧ <new-name(J)>)>(1(1(1\000C(s(1(a))))))))) 
                                    J 
                                    new-name(J) 
                                    1 
                                    0 
                                    (λI@1,a@0. ((u 1 s) 1 a@0)) 
                                    u))
BY
{ (Intros
   THEN RepUR ``transEquiv-trans equiv-fun cubical-fst transEquiv cubical-subst cubical-app`` 0
   THEN RepUR ``cubical-id-equiv equiv-witness cubical-pair`` 0
   THEN RepUR ``path-trans univ-trans transprt-fun cubical-lambda`` 0
   THEN RepUR ``universe-decode universe-comp-op path-eta map-path cube-context-adjoin`` 0
   THEN ...
   THEN RepUR ``comp-op-to-comp-fun transprt csm-comp-structure cubical-app`` 0
   THEN ...
   THEN RepUR ``universe-decode universe-comp-op path-eta map-path cube-context-adjoin`` 0
   THEN ...
   THEN RepUR ``comp-op-to-comp-fun transprt csm-comp-structure cubical-app`` 0
   THEN ...
   THEN RepUR ``discrete-cubical-term csm-ap-term csm-comp cc-adjoin-cube compose`` 0
   THEN ...
   THEN RepUR ``cube-context-adjoin`` 0
   THEN ...
   THEN ...
   THEN (InstLemma `equiv_comp-apply-sq` [⌜<λI.(alpha:G(I) × c𝕌(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>⌝;
         ⌜decode(λI,a. (A I (fst(a))))⌝;⌜decode(λI,p. (snd(p)))⌝
         ;⌜λH,sigma,phi,u,a0,I,rho. ((snd((A I+new-name(I) (fst((sigma I+new-name(I) (s(rho);<new-name(I)>))))))) I 
                                     new-name(I) 
                                     1 
                                     (phi I rho) 
                                     (λI@0,a. (u I@0 (H.𝕀 I+new-name(I) I@0 (iota I@0 a) (s(rho);<new-name(I)>)))) 
                                     (a0 I rho))⌝
         ;⌜λH,sigma,phi,u,a0,I,rho. ((snd(snd((sigma I+new-name(I) (s(rho);<new-name(I)>))))) I new-name(I) 1 
                                     (phi I rho) 
                                     (λI@0,a. (u I@0 (H.𝕀 I+new-name(I) I@0 (iota I@0 a) (s(rho);<new-name(I)>)))) 
                                     (a0 I rho))⌝
         ;⌜I⌝]⋅
         THENA Auto
         )
   THEN ((InstHyp [⌜λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a))))))⌝] (-1)⋅ THENA Auto) THEN Thin (-2))
   THEN ((InstHyp [⌜λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 
                              <new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) cube+(I;new-name(I)) x x@0)⌝] (-1)⋅
          THENA Auto
          )
         THEN Thin (-2)
         )
   THEN (InstHyp [⌜λ2K f.(0 ⋅ f)⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN (InstHyp [
         ⌜λ2K f.(<λJ,f,u. u, cubical-id-is-equiv(G;<λI,a. fst((A I a))(1), λI,J,f,a,x. (x 1 f)>) I a> <(new-name(I)0)(1(\000C1(1(s(1(a))))))
                                                     , ((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 
                                                         <new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) (new-name(I)0))
                                                     > f)⌝] (-1)⋅
         THENA Auto
         )
   THEN Thin (-2)
   THEN RWO "-1" 0
   THEN Thin (-1)) }

1
1. [G] : Top
2. [A] : Top
3. [p] : Top
4. [I] : Top
5. [a] : Top
6. [J] : Top
7. [f] : Top
8. [u] : Top
⊢ (fst(equiv_comp_apply(<λI.(alpha:G(I) × c𝕌(alpha))
                        , λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>
                        >;decode(λI,a.
                (A I 
                 (fst(a))));decode(λI,p.
                                    (snd(p)));λH,sigma,phi,u,a0,I,rho.
                                                                  ((snd((A I+new-name(I) 
                                                                         (fst((sigma I+new-name(I) 
                                                                               (s(rho);<new-name(I)>))))))) 
                                                                   I 
                                                                   new-name(I) 
                                                                   1 
                                                                   (phi I rho) 
                                                                   (λI@0,a. (u I@0 
                                                                             (H.𝕀 I+new-name(I) I@0 (iota I@0 a) 
                                                                              (s(rho);<new-name(I)>)))) 
                                                                   (a0 I rho));λH,sigma,phi,u,a0,I,rho. ((snd(snd((sigma\000C I+new-name(I) 
                                                                                            (s(rho);<new-name(I)>))))) 
                                                                                  I 
                                                                                  new-name(I) 
                                                                                  1 
                                                                                  (phi I rho) 
                                                                                  (λI@0,a. (u I@0 
                                                                                            (H.𝕀 I+new-name(I) I@0 
                                                                                             (iota I@0 a) 
                                                                                             (s(rho);<new-name(I)>)))) 
                                                                                  (a0 I 
                                                                                   rho));I;λ2x x@0.cube+(I;new-name(I)) \000Cx 
                                                                            x@0(1(1(1(s(1(a))))));...;λ2K f....;...))) 
  J 
  f 
  u ~ let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)> 
      in cA J new-name(J) 1 ⋅ cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ <new-name(J)>> ⋅ 1 (0)<1 ⋅ f> ∨ 0 
         (λI@1,a@0. (if ((0)<1 ⋅ f ⋅ s ⋅ a@0>==1) then (fst(⋅)) I@1 1 else λu.u fi  
                     ((snd((A I@1+new-name(I@1) 
                            cube+(I;new-name(I)) I@1+new-name(I@1) 
                            <1 ⋅ f ⋅ s ⋅ a@0 ⋅ s
                            , 1 ∧ ¬(dM-lift(I@1+new-name(I@1);I@1;s) 
                                    ¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>) ∧ <new-name(I@1)>)
                            >(1(1(1(s(1(a))))))))) 
                      I@1 
                      new-name(I@1) 
                      1 
                      0 ∨ dM-to-FL(I@1;¬(¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>))) 
                      (λI@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1)) 
                      ((u 1 s) 1 a@0)))) 
         ((snd((A J+new-name(J) cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ ¬(1 ∧ <new-name(J)>)>(1(1(1(s(1(a))))\000C))))) J new-name(J) 1 0 
          (λI@1,a@0. ((u 1 s) 1 a@0)) 
          u)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,A,p,I,a,J,f,u:Top].
    (transEquivFun(p)  I  a  J  f  u 
    \msim{}  let  x,cA  =  p  I+new-name(I)  1(s(1(a)))  I+new-name(I)  1  <new-name(I)> 
        in  cA  J  new-name(J)  1  \mcdot{}  cube+(I;new-name(I))  J+new-name(J)  ə  \mcdot{}  f  \mcdot{}  s,  1  \mwedge{}  <new-name(J)>>  \mcdot{}  1  (0\000C)ə  \mcdot{}  f>  \mvee{}  0 
              (\mlambda{}I@1,a@0.  (if  ((0)ə  \mcdot{}  f  \mcdot{}  s  \mcdot{}  a@0>==1)  then  (fst(\mcdot{}))  I@1  1  else  \mlambda{}u.u  fi   
                                      ((snd((A  I@1+new-name(I@1) 
                                                    cube+(I;new-name(I))  I@1+new-name(I@1) 
                                                    ə  \mcdot{}  f  \mcdot{}  s  \mcdot{}  a@0  \mcdot{}  s
                                                    ,  1  \mwedge{}  \mneg{}(dM-lift(I@1+new-name(I@1);I@1;s) 
                                                                    \mneg{}(dM-lift(I@1;J+new-name(J);a@0)  <new-name(J)>)  \mwedge{}  <new-name(I@1)>)
                                                    >(1(1(1(s(1(a))))))))) 
                                        I@1 
                                        new-name(I@1) 
                                        1 
                                        0  \mvee{}  dM-to-FL(I@1;\mneg{}(\mneg{}(dM-lift(I@1;J+new-name(J);a@0)  <new-name(J)>))) 
                                        (\mlambda{}I@0,a@1.  ((((u  1  s)  1  a@0)  1  s)  1  a@1)) 
                                        ((u  1  s)  1  a@0)))) 
              ((snd((A  J+new-name(J) 
                            cube+(I;new-name(I))  J+new-name(J)  ə  \mcdot{}  f  \mcdot{}  s,  1  \mwedge{}  \mneg{}(1  \mwedge{}  <new-name(J)>)>(1(1(1(s(1(a))\000C))))))) 
                J 
                new-name(J) 
                1 
                0 
                (\mlambda{}I@1,a@0.  ((u  1  s)  1  a@0)) 
                u))


By

---

Latex:
(Intros
  THEN  RepUR  ``transEquiv-trans  equiv-fun  cubical-fst  transEquiv  cubical-subst  cubical-app``  0
  THEN  RepUR  ``cubical-id-equiv  equiv-witness  cubical-pair``  0
  THEN  RepUR  ``path-trans  univ-trans  transprt-fun  cubical-lambda``  0
  THEN  RepUR  ``universe-decode  universe-comp-op  path-eta  map-path  cube-context-adjoin``  0
  THEN  ...
  THEN  RepUR  ``comp-op-to-comp-fun  transprt  csm-comp-structure  cubical-app``  0
  THEN  ...
  THEN  RepUR  ``universe-decode  universe-comp-op  path-eta  map-path  cube-context-adjoin``  0
  THEN  ...
  THEN  RepUR  ``comp-op-to-comp-fun  transprt  csm-comp-structure  cubical-app``  0
  THEN  ...
  THEN  RepUR  ``discrete-cubical-term  csm-ap-term  csm-comp  cc-adjoin-cube  compose``  0
  THEN  ...
  THEN  RepUR  ``cube-context-adjoin``  0
  THEN  ...
  THEN  ...
  THEN  (InstLemma  `equiv\_comp-apply-sq`  [\mkleeneopen{}<\mlambda{}I.(alpha:G(I)  \mtimes{}  c\mBbbU{}(alpha))
                                                                                  ,  \mlambda{}I,J,f,p.  <f(fst(p)),  (snd(p)  fst(p)  f)>
                                                                                  >\mkleeneclose{};\mkleeneopen{}decode(\mlambda{}I,a.  (A  I  (fst(a))))\mkleeneclose{};\mkleeneopen{}decode(\mlambda{}I,p.  (snd(p)))\mkleeneclose{}
              ;\mkleeneopen{}\mlambda{}H,sigma,phi,u,a0,I,rho.  ((snd((A  I+new-name(I) 
                                                                                  (fst((sigma  I+new-name(I)  (s(rho);<new-name(I)>))))))) 
                                                                      I 
                                                                      new-name(I) 
                                                                      1 
                                                                      (phi  I  rho) 
                                                                      (\mlambda{}I@0,a.  (u  I@0 
                                                                                          (H.\mBbbI{}  I+new-name(I)  I@0  (iota  I@0  a) 
                                                                                            (s(rho);<new-name(I)>)))) 
                                                                      (a0  I  rho))\mkleeneclose{}
              ;\mkleeneopen{}\mlambda{}H,sigma,phi,u,a0,I,rho.  ((snd(snd((sigma  I+new-name(I)  (s(rho);<new-name(I)>)))))  I 
                                                                      new-name(I) 
                                                                      1 
                                                                      (phi  I  rho) 
                                                                      (\mlambda{}I@0,a.  (u  I@0 
                                                                                          (H.\mBbbI{}  I+new-name(I)  I@0  (iota  I@0  a) 
                                                                                            (s(rho);<new-name(I)>)))) 
                                                                      (a0  I  rho))\mkleeneclose{}
              ;\mkleeneopen{}I\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  ((InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x  x@0.cube+(I;new-name(I))  x  x@0(1(1(1(s(1(a))))))\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
              THEN  Thin  (-2)
              )
  THEN  ((InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x  x@0.((p  I+new-name(I)  1(s(1(a)))  I+new-name(I)  1 
                                                        <new-name(I)>  1(1(s(1(a))))  1)  1(1(1(s(1(a)))))  cube+(I;new-name(I))  x 
                                                                                                                                                        x@0)\mkleeneclose{}]  (-1)\mcdot{}
                THENA  Auto
                )
              THEN  Thin  (-2)
              )
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}K  f.(0  \mcdot{}  f)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  (InstHyp  [
              \mkleeneopen{}\mlambda{}\msubtwo{}K  f.(<\mlambda{}J,f,u.  u
                              ,  cubical-id-is-equiv(G;<\mlambda{}I,a.  fst((A  I  a))(1),  \mlambda{}I,J,f,a,x.  (x  1  f)>)  I  a
                              >  <(new-name(I)0)(1(1(1(s(1(a))))))
                    ,  ((p  I+new-name(I)  1(s(1(a)))  I+new-name(I)  1 
                            <new-name(I)>  1(1(s(1(a))))  1)  1(1(1(s(1(a)))))  (new-name(I)0))
                    >  f)\mkleeneclose{}]  (-1)\mcdot{}
              THENA  Auto
              )
  THEN  Thin  (-2)
  THEN  RWO  "-1"  0
  THEN  Thin  (-1))

---

Home Index