---

Step * 1 of Lemma equiv_comp-sq


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))
                                                                 >)))
BY
{ ... }

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. ...\000C=1) 
                                                                                                              I 
                                                                                                              rho ⊢→
                                                                              λI,rho.
                                                                                     if (phi I (fst(fst(rho)))==1)
                                                                                       then u I 
                                                                                            <fst(fst(rho)), snd(rho)> 
                                                                                            I 
                                                                                            1 
                                                                                            (snd(fst(rho)))
                                                                                     if (dM-to-FL(I;¬(snd(...)))==1)
                                                                                       then snd(fst((sigma I 
                                                                                                     <fst(fst(rho))
                                                                                                     , snd(rho)
                                                                                                     >)))
                                                                                     else (snd(fst(fst((sigma I 
                                                                                                        <fst(fst(rho))
                                                                                                        , snd(rho)
                                                                                                        >))))) 
                                                                                          I 
                                                                                          1 
                                                                                          (snd((sigma I 
                                                                                                <fst(fst(rho))
                                                                                                , snd(rho)
                                                                                                >)))
                                                                                     fi ] λI,a. (a0 I (fst(a)) I 1 (snd(\000Ca)))))))) 
~ 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 ... ∨ ...) 
                                                                                           (λ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:

1.  cE  :  Base
2.  cA  :  Base
3.  E  :  Base
4.  A  :  Base
5.  H  :  Base
\mvdash{}  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));
                          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)))) 
                                                                                                                                        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.  \000C(snd(p)));
                                                                              sigma\_comp(\mlambda{}H@0,sigma,phi,u,a0.  (cA  H@0 
                                                                                                                                                (\mlambda{}x,x@0.  (fst(fst((sigma  x 
                                                                                                                                                                                      x@0))))) 
                                                                                                                                                phi 
                                                                                                                                                u 
                                                                                                                                                a0);
                                                                                                    \mlambda{}H@0,sigma,phi,u,a0.
                                                                                                                                            <>(comp  \mlambda{}H@1,sigma@0,phi,u,...
                                                                                                                                                          [\mlambda{}I,rho.
                                                                                                                                                                          phi  I 
                                                                                                                                                                          ...  \mvee{}  (...=0) 
                                                                                                                                                                                      I 
                                                                                                                                                                                      rho  \mvee{}  ...\000C  \mvdash{}\mrightarrow{}
                                                                                                                                                            path\_term
                                                                                                                                                                (\mlambda{}I,a.  (phi  I 
                                                                                                                                                                                (fst(a)));
                                                                                                                                                                  \mlambda{}I,a.  (u  I 
                                                                                                                                                                                <fst(fst(a))
                                                                                                                                                                                ,  snd(a)
                                                                                                                                                                                >);
                                                                                                                                                                  \mlambda{}I,a.  (snd(...));
                                                                                                                                                                  \mlambda{}I,a.
                                                                                                                                                                            ((snd(...)) 
                                                                                                                                                                              I 
                                                                                                                                                                              1 
                                                                                                                                                                              (snd((...  I 
                                                                                                                                                                                          <...
                                                                                                                                                                                          ,  ...
                                                                                                                                                                                          >))));
                                                                                                                                                                  \mlambda{}I,p.  (snd(p)))]
                                                                                                                                                          \mlambda{}I,a.
                                                                                                                                                                    (a0  I 
                                                                                                                                                                      (fst(a)))  @  \mlambda{}I,p.\000C  ...))))) 
\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));
                          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)))) 
                                                                                                                                        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.  \000C(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)))))) 
                                                                                                                                    (\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(fst((... 
                                                                                                                                                                                              x 
                                                                                                                                                                                              <...
                                                                                                                                                                                              ,  ...
                                                                                                                                                                                              >))))\000C) 
                                                                                                                                                          (\mlambda{}I,rho.
                                                                                                                                                                          phi  I 
                                                                                                                                                                          ...  \mvee{}  ...  \mvee{}  ...\000C) 
                                                                                                                                                          (\mlambda{}I,rho.
                                                                                                                                                                          if  (...==1)
                                                                                                                                                                              then  ... 
                                                                                                                                                                                        I 
                                                                                                                                                                                        1 
                                                                                                                                                                                        ...
                                                                                                                                                                          if  (...==1)
                                                                                                                                                                              then  snd(...)
                                                                                                                                                                          else  ... 
                                                                                                                                                                                    I 
                                                                                                                                                                                    1 
                                                                                                                                                                                    (cA  H@0.\mBbbI{} 
                                                                                                                                                                                      (\mlambda{}x,...) 
                                                                                                                                                                                      (\mlambda{}I,...) 
                                                                                                                                                                                      (\mlambda{}I,...) 
                                                                                                                                                                                      (\mlambda{}I,...) 
                                                                                                                                                                                      I 
                                                                                                                                                                                      <fst(...)
                                                                                                                                                                                      ,  ...
                                                                                                                                                                                      >)
                                                                                                                                                                          fi  ) 
                                                                                                                                                          (\mlambda{}I,a.
                                                                                                                                                                      ((snd(...)) 
                                                                                                                                                                        I 
                                                                                                                                                                        1 
                                                                                                                                                                        (snd(a)))) 
                                                                                                                                                          J 
                                                                                                                                                          (f(a@0);u@0))
                                                                                                                                  >)))


By

---

Latex:
...

---

Home Index