---

Step * of Lemma equiv_comp-sq

No Annotations
∀[H,A,E,cA,cE:Top].
  (equiv_comp(H;A;E;cA;cE) 
  ~ sigma_comp(pi_comp(H;A;cA;λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0));
               pi_comp(H.(A ⟶ E);(E)λI,p. (fst(p));λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0\000C);
                       contractible_comp(H.(A ⟶ E).(E)λI,p. (fst(p));Fiber(λI,a. (snd(fst(a)));λI,p. (snd(p)));
                                         λH@0,sigma,phi,u,a0,I,a@0.
                                                                   <cA H@0.𝕀 (λx,x@0. (fst(fst((sigma x (m x x@0)))))) 
                                                                    (λI,rho. phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(rho))))\000C 
                                                                    (λI,rho. if (phi I (fst((m I rho)))==1)
                                                                            then fst((u I (m I rho)))
                                                                            else fst((a0 I (fst((m I rho)))))
                                                                            fi ) 
                                                                    (λI,a. (fst((a0 I (fst(a)))))) 
                                                                    I 
                                                                    <a@0, 1>
                                                                   , λJ,f,u@0.
                                                                              (cE H@0.𝕀 
                                                                               (λx,x@0. (fst(fst((sigma x 
                                                                                                  <fst(fst(x@0))
                                                                                                  , snd(x@0)
                                                                                                  >))))) 
                                                                               (λI,rho.
                                                                                       phi I (fst(rho)) ∨ ... ∨ (...=1) 
                                                                                                                I 
                                                                                                                rho) 
                                                                               (λI,rho.
                                                                                       if (phi I (fst(fst(rho)))==1)
                                                                                         then (snd((u I 
                                                                                                    <fst(fst(rho))
                                                                                                    , snd(rho)
                                                                                                    >))) 
                                                                                              I 
                                                                                              1 
                                                                                              (snd(fst(rho)))
                                                                                       if (dM-to-FL(I;¬(snd(...)))==1)
                                                                                         then snd((sigma I 
                                                                                                   <fst(fst(rho))
                                                                                                   , snd(rho)
                                                                                                   >))
                                                                                       else (snd(fst((sigma I 
                                                                                                      <fst(fst(rho))
                                                                                                      , snd(rho)
                                                                                                      >)))) 
                                                                                            I 
                                                                                            1 
                                                                                            (cA H@0.𝕀 
                                                                                             (λx,x@0.
                                                                                                     (fst(fst((sigma x 
                                                                                                               (m x 
                                                                                                                x@0)))))\000C) 
                                                                                             (λI,a.
                                                                                                   (phi I 
                                                                                                    (fst(a))) ∨ (λI,p. .\000C..=0)) 
                                                                                             (λI,rho.
                                                                                                     if (...==1)
                                                                                                     then fst((u I 
                                                                                                               (m I 
                                                                                                                rho)))
                                                                                                     else fst((a0 I 
                                                                                                               ...))
                                                                                                     fi ) 
                                                                                             (λI,a. (fst((a0 I 
                                                                                                          (fst(a)))))) 
                                                                                             I 
                                                                                             <fst(fst(rho)), snd(rho)>)
                                                                                       fi ) 
                                                                               (λI,a. ((snd((a0 I (fst(a))))) I 1 
                                                                                       (snd(a)))) 
                                                                               J 
                                                                               (f(a@0);u@0))
                                                                   >))))
BY
{ ((UnivCD THENA Auto)
   THEN (SqEqualTopToBase THEN Unfold `equiv_comp` 0 THEN Unfold `fiber-comp` 0 THEN Unfold `path_comp` 0)
   THEN ...) }

1
1. cE : Base
2. cA : Base
3. E : Base
4. A : Base
5. H : Base
⊢ sigma_comp(pi_comp(H;A;cA;λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0));
             pi_comp(H.(A ⟶ E);(E)λI,p. (fst(p));λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0);
                     contractible_comp(H.(A ⟶ E).(E)λI,p. (fst(p));Fiber(λI,a. (snd(fst(a)));λI,p. (snd(p)));
                                       sigma_comp(λH@0,sigma,phi,u,a0. (cA H@0 (λx,x@0. (fst(fst((sigma x x@0))))) phi u\000C a0);
                                                  λH@0,sigma,phi,u,a0.
                                                                      <>(comp λH@1,sigma@0,phi,u,a0.
                                                                                                    (cE H@1 
                                                                                                     (λx,x@0. (fst(...))\000C) 
                                                                                                     phi 
                                                                                                     u 
                                                                                                     a0)
                                                                             [λI,rho. phi I 
                                                                                      (fst(rho)) ∨ (λI,p. (snd(p))=0) I 
                                                                                                   rho ∨ (λI,p. (snd(p))\000C=1) 
                                                                                                         I 
                                                                                                         rho ⊢→
                                                                              path_term
                                                                                (λI,a. (phi I (fst(a)));
                                                                                 λI,a. (u I <fst(fst(a)), snd(a)>);
                                                                                 λI,a.
                                                                                      (snd(fst(...)));
                                                                                 λI,a. ((snd(fst(fst((sigma I 
                                                                                                      <fst(fst(a))
                                                                                                      , snd(a)
                                                                                                      >))))) 
                                                                                        I 
                                                                                        1 
                                                                                        (snd((sigma I 
                                                                                              <fst(fst(a)), snd(a)>))));
                                                                                 λI,p. (snd(p)))]
                                                                             λI,a. (a0 I (fst(a))) @ λI,p. (snd(p)))))))\000C 
~ sigma_comp(pi_comp(H;A;cA;λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0));
             pi_comp(H.(A ⟶ E);(E)λI,p. (fst(p));λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0);
                     contractible_comp(H.(A ⟶ E).(E)λI,p. (fst(p));Fiber(λI,a. (snd(fst(a)));λI,p. (snd(p)));
                                       λH@0,sigma,phi,u,a0,I,a@0.
                                                                 <cA H@0.𝕀 (λx,x@0. (fst(fst((sigma x (m x x@0)))))) 
                                                                  (λI,rho. phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(rho)))) 
                                                                  (λI,rho. if (phi I (fst((m I rho)))==1)
                                                                          then fst((u I (m I rho)))
                                                                          else fst((a0 I (fst((m I rho)))))
                                                                          fi ) 
                                                                  (λI,a. (fst((a0 I (fst(a)))))) 
                                                                  I 
                                                                  <a@0, 1>
                                                                 , λJ,f,u@0.
                                                                            (cE H@0.𝕀 
                                                                             (λx,x@0. (fst(fst((sigma x 
                                                                                                <fst(fst(x@0))
                                                                                                , snd(x@0)
                                                                                                >))))) 
                                                                             (λI,rho.
                                                                                     phi I (fst(rho)) ∨ ... ∨ (λI,p. ...\000C=1) 
                                                                                                              I 
                                                                                                              rho) 
                                                                             (λI,rho.
                                                                                     if (phi I (fst(fst(rho)))==1)
                                                                                       then (snd((u I 
                                                                                                  <fst(fst(rho))
                                                                                                  , snd(rho)
                                                                                                  >))) 
                                                                                            I 
                                                                                            1 
                                                                                            (snd(fst(rho)))
                                                                                     if (dM-to-FL(I;¬(snd(...)))==1)
                                                                                       then snd((sigma I 
                                                                                                 <fst(fst(rho))
                                                                                                 , snd(rho)
                                                                                                 >))
                                                                                     else (snd(fst((sigma I 
                                                                                                    <fst(fst(rho))
                                                                                                    , snd(rho)
                                                                                                    >)))) 
                                                                                          I 
                                                                                          1 
                                                                                          (cA H@0.𝕀 
                                                                                           (λx,x@0. (fst(fst((sigma x 
                                                                                                              (m x 
                                                                                                               x@0))))))\000C 
                                                                                           (λI,rho.
                                                                                                   phi I ... ∨ (...=0) 
                                                                                                               I 
                                                                                                               rho) 
                                                                                           (λI,rho. if (phi I 
                                                                                                        (fst((m I 
                                                                                                              rho)))==1)
                                                                                                   then fst((u I 
                                                                                                             (m I rho)))
                                                                                                   else fst(...)
                                                                                                   fi ) 
                                                                                           (λI,a. (fst((a0 I (fst(a)))))\000C) 
                                                                                           I 
                                                                                           <fst(fst(rho)), snd(rho)>)
                                                                                     fi ) 
                                                                             (λI,a. ((snd((a0 I (fst(a))))) I 1 
                                                                                     (snd(a)))) 
                                                                             J 
                                                                             (f(a@0);u@0))
                                                                 >)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,A,E,cA,cE:Top].
    (equiv\_comp(H;A;E;cA;cE) 
    \msim{}  sigma\_comp(pi\_comp(H;A;cA;\mlambda{}H@0,sigma,phi,u,a0.  (cE  H@0  (\mlambda{}x,x@0.  (fst((sigma  x  x@0))))  phi  u  a0))\000C;
                              pi\_comp(H.(A  {}\mrightarrow{}  E);(E)\mlambda{}I,p.  (fst(p));\mlambda{}H@0,sigma,phi,u,a0.  (cE  H@0 
                                                                                                                                            (\mlambda{}x,x@0.  (fst((sigma  x  x@0))))\000C 
                                                                                                                                            phi 
                                                                                                                                            u 
                                                                                                                                            a0);
                                              contractible\_comp(H.(A  {}\mrightarrow{}  E).(E)\mlambda{}I,p.  (fst(p));
                                                                                  Fiber(\mlambda{}I,a.  (snd(fst(a)));\mlambda{}I,p.  (snd(p)));
                                                                                  \mlambda{}H@0,sigma,phi,u,a0,I,a@0.
                                                                                                                                      <cA  H@0.\mBbbI{} 
                                                                                                                                        (\mlambda{}x,x@0.  (fst(fst((sigma  x 
                                                                                                                                                                              (m  x  x@0)))))\000C) 
                                                                                                                                        (\mlambda{}I,rho.
                                                                                                                                                        phi  I  (fst(rho))  \mvee{}  ...) 
                                                                                                                                        (\mlambda{}I,rho.  if  (phi  I 
                                                                                                                                                                  (fst((m  I 
                                                                                                                                                                              rho)))==1)
                                                                                                                                                        then  fst((u  I 
                                                                                                                                                                            (m  I  rho)))
                                                                                                                                                        else  fst((a0  I 
                                                                                                                                                                            (fst((m  I 
                                                                                                                                                                                        rho)))))
                                                                                                                                                        fi  ) 
                                                                                                                                        (\mlambda{}I,a.  (fst((a0  I  (fst(a)))))) 
                                                                                                                                        I 
                                                                                                                                        <a@0,  1>
                                                                                                                                      ,  \mlambda{}J,f,u@0.
                                                                                                                                                            (cE  H@0.\mBbbI{} 
                                                                                                                                                              (\mlambda{}x,x@0.  (fst(...))) 
                                                                                                                                                              (\mlambda{}I,rho.
                                                                                                                                                                              phi  I 
                                                                                                                                                                              ...  \mvee{}  ...) 
                                                                                                                                                              (\mlambda{}I,rho.
                                                                                                                                                                              if  (phi  I 
                                                                                                                                                                                      ...==1)
                                                                                                                                                                                  then  ... 
                                                                                                                                                                                            I 
                                                                                                                                                                                            1 
                                                                                                                                                                                            ...
                                                                                                                                                                              ...) 
                                                                                                                                                              (\mlambda{}I,a.
                                                                                                                                                                          ((snd(...)) 
                                                                                                                                                                            I 
                                                                                                                                                                            1 
                                                                                                                                                                            (snd(a)))) 
                                                                                                                                                              J 
                                                                                                                                                              (f(a@0);u@0))
                                                                                                                                      >))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (SqEqualTopToBase
              THEN  Unfold  `equiv\_comp`  0
              THEN  Unfold  `fiber-comp`  0
              THEN  Unfold  `path\_comp`  0)
  THEN  ...)

---

Home Index