---

Step * 1 of Lemma equiv_comp-apply-sq


1. H : Top
2. A : Top
3. E : Top
4. cA : Top
5. cE : Top
6. I : Top
7. a : Top
8. b : Top
9. c : Top
10. d : Top
11. J : Base
12. f : Base
13. u@0 : Base
⊢ 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)>)\000C)))) 
                                                          (λI,rho.
                                                                  phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(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(fst(rho))))==1)
                                                                    then snd((sigma I <fst(fst(rho)), snd(rho)>))
                                                                  else (snd(fst((sigma I <fst(fst(rho)), snd(rho)>)))) I\000C 1 
                                                                       (cA H@0.𝕀 
                                                                        (λx,x@0. (fst(fst((sigma x (m x x@0)))))) 
                                                                        (λI,a. (phi I (fst(a))) ∨ (λI,p. (snd(p))=0)) 
                                                                        (λ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 
                                                                        <fst(fst(rho)), snd(rho)>)
                                                                  fi ) 
                                                          (λI,a. ((snd((a0 I (fst(a))))) I 1 (snd(a)))) 
                                                          J 
                                                          (f(a@0);u@0))
                                              >) 
  <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.(((E)λI,p. (fst(p)))
                         λx,x@0. <<a[x;x@0], b[x;x@0]>
                                 , λJ,f,u@0. (cE <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0], b[x;m x x@0]>\000C)[1(𝕀)] 
                                              (λx,x@0. <a[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                       , b[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                       >) 
                                              (λI,a. c[I;fst(fst(a))] ∨ dM-to-FL(I;¬(snd(fst(a))))) 
                                              (λI@0,a@0. (if (c[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))]==1)
                                                          then fst(⋅)
                                                          else fst(d[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))])
                                                          fi  
                                                          I@0 
                                                          1 
                                                          (cA 
                                                           <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0]
                                                                                              , b[x;m x x@0]
                                                                                              >)[1(𝕀)].𝕀 
                                                           (λx,x@0. <a[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
                                                                    , b[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
                                                                    >) 
                                                           (λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho)))) 
                                                           (λI,rho. (snd(fst((m I rho))))) 
                                                           (λI,a. (snd(fst(a)))) 
                                                           I@0 
                                                           <fst(a@0), ¬(snd(a@0))>))) 
                                              (λI@0,a@0. ((fst(d[I@0;fst(fst(a@0))])) I@0 1 
                                                          (cA 
                                                           <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0]
                                                                                              , b[x;m x x@0]
                                                                                              >)[1(𝕀)].𝕀 
                                                           (λx,x@0. <a[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
                                                                    , b[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
                                                                    >) 
                                                           (λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho)))) 
                                                           (λI,rho. (snd(fst((m I rho))))) 
                                                           (λI,a. (snd(fst(a)))) 
                                                           ... 
                                                           ...))) 
                                              ... 
                                              ...)
                                 >)... 
  ... 
  ... 
  ... 
  ... 
  ... 
  ... ~ ...
BY
{ ((RWO  "contractible_comp-sq" 0 THENA Auto) THEN Reduce 0) }

1
1. H : Top
2. A : Top
3. E : Top
4. cA : Top
5. cE : Top
6. I : Top
7. a : Top
8. b : Top
9. c : Top
10. d : Top
11. J : Base
12. f : Base
13. u@0 : Base
⊢ let a@0 = λI@0,a@0.
                     <cA 
                      <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.(((E)λI,p. (fst(p)))
                                             λx,x@0. <<a[x;x@0], b[x;x@0]>
                                                     , λJ,f,u@0. (cE 
                                                                  <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@\000C0]
                                                                                                     , b[x;m x x@0]
                                                                                                     >)[1(𝕀)] 
                                                                  (λx,x@0. <a[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                                           , b[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                                           >) 
                                                                  (λI,a. c[I;fst(fst(a))] ∨ dM-to-FL(I;¬(snd(fst(a))))) 
                                                                  (λI@0,a@0. (if (c[I@0;
                                                                                   fst((m I@0 <fst(fst(a@0)), snd(a@0)>)\000C)]==1)
                                                                              then fst(⋅)
                                                                              else fst(d[I@0;fst((m I@0 
                                                                                                  <fst(fst(a@0))
                                                                                                  , snd(a@0)
                                                                                                  >))])
                                                                              fi  
                                                                              I@0 
                                                                              1 
                                                                              (cA 
                                                                               <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)
                                                                                                        λx,x@0. <a[x;
                                                                                                                  m x 
                                                                                                                  x@0]
                                                                                                                , b[x;
                                                                                                                   m x 
                                                                                                                   x@0]
                                                                                                                >)[1(𝕀)]\000C.𝕀 
                                                                               (λx,x@0. <a[x;m x 
                                                                                             <fst(fst((m x x@0)))
                                                                                             , ¬(snd((m x x@0)))
                                                                                             >]
                                                                                        , b[x;m x 
                                                                                              <fst(fst((m x x@0)))
                                                                                              , ¬(snd((m x x@0)))
                                                                                              >]
                                                                                        >) 
                                                                               (λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho)))) 
                                                                               (λI,rho. (snd(fst((m I rho))))) 
                                                                               (λI,a. (snd(fst(a)))) 
                                                                               I@0 
                                                                               <fst(a@0), ¬(snd(a@0))>))) 
                                                                  (λI@0,a@0. ((fst(d[I@0;fst(fst(a@0))])) I@0 1 
                                                                              (cA 
                                                                               <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)
                                                                                                        λx,x@0. <a[x;
                                                                                                                  m x 
                                                                                                                  x@0]
                                                                                                                , b[x;
                                                                                                                   m x 
                                                                                                                   x@0]
                                                                                                                >)[1(𝕀)]\000C.𝕀 
                                                                               (λx,x@0. <a[x;m x 
                                                                                             <fst(fst((m x x@0)))
                                                                                             , ¬(snd((m x x@0)))
                                                                                             >]
                                                                                        , b[x;m x 
                                                                                              <fst(fst((m x x@0)))
                                                                                              , ¬(snd((m x x@0)))
                                                                                              >]
                                                                                        >) 
                                                                               (λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho)))) 
                                                                               (λI,rho. (snd(fst((m I rho))))) 
                                                                               (λI,a. (snd(fst(a)))) 
                                                                               I@0 
                                                                               <a@0, ¬(0)>))) 
                                                                  J 
                                                                  (f(x@0);u@0))
                                                     >)[1(𝕀)].𝕀.𝕀 
                      (λx,x@0. <a[x;<fst(fst((m x (m x x@0)))), snd((m x (m x x@0)))>]
                               , b[x;<fst(fst((m x (m x x@0)))), snd((m x (m x x@0)))>]
                               >) 
                      (λI,rho. c[I;fst(fst(fst(rho)))] ∨ dM-to-FL(I;¬(snd(fst(rho)))) ∨ dM-to-FL(I;¬(snd(rho)))) 
                      (λI@0,rho. if (c[I@0;fst(fst(fst((m I@0 rho))))] ∨ dM-to-FL(I@0;¬(snd(fst((m I@0 rho)))))==1)
                                then fst(if (c[I@0;fst(fst((m I@0 (m I@0 rho))))]==1)
                                     then fst(((snd(⋅)) I@0 1 
                                               (cE 
                                                <λJ.J ⟶ I
                                                , λI,J,f,g. g ⋅ f
                                                >.(((E)λI,p. (fst(p)))
                                                    λx,x@0.
                                                           <<a[x;x@0], b[x;x@0]>
                                                           , λJ,f,u@0.
                                                                      (cE 
                                                                       <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m\000C x x@0]
                                                                                                          , b[x;m x x@0]
                                                                                                          >)[1(𝕀)] 
                                                                       (λx,x@0. <a[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                                                , b[x;m x <fst(fst(x@0)), snd(x@0)>]
                                                                                >) 
                                                                       (λI,a. c[I;
                                                                               fst(fst(a))] ∨ dM-to-FL(I;¬(snd(fst(a))))\000C) 
                                                                       (λI@0,a@0.
                                                                                 (if (c[I@0;fst((m I@0 
                                                                                                 <fst(fst(a@0))
                                                                                                 , snd(a@0)
                                                                                                 >))]==1)
                                                                                  then fst(⋅)
                                                                                  else fst(d[I@0;fst((m I@0 
                                                                                                      <fst(fst(a@0))
                                                                                                      , snd(a@0)
                                                                                                      >))])
                                                                                  fi  
                                                                                  I@0 
                                                                                  1 
                                                                                  (cA 
                                                                                   <λJ.J ⟶ I
                                                                                   , λI,J,f,g. g ⋅ f
                                                                                   >.𝕀.((A)λx,x@0. <a[x;m x ...], ...>).\000C...... 
                                                                                   ... 
                                                                                   ... 
                                                                                   ... 
                                                                                   ... 
                                                                                   ... 
                                                                                   ...))) 
                                                                       ... 
                                                                       ... 
                                                                       ...)
                                                           >)....... 
                                                ... 
                                                ... 
                                                ... 
                                                ... 
                                                ... 
                                                ...)))
                                     else ...
                                     fi )
                                else ...
                                fi ) 
                      ... 
                      ... 
                      ...
                     , ...
                     > in
   ... 
  ... 
  ... ~ ...

---

Latex:

---

Latex:

1.  H  :  Top
2.  A  :  Top
3.  E  :  Top
4.  cA  :  Top
5.  cE  :  Top
6.  I  :  Top
7.  a  :  Top
8.  b  :  Top
9.  c  :  Top
10.  d  :  Top
11.  J  :  Base
12.  f  :  Base
13.  u@0  :  Base
\mvdash{}  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)))))) 
                                                                                              (\mlambda{}I,rho.  phi  I  (fst(rho))  \mvee{}  dM-to-FL(I;\mneg{}(snd(rho)))) 
                                                                                              (\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((sigma  x 
                                                                                                                                                          <fst(fst(x@0))
                                                                                                                                                          ,  snd(x@0)
                                                                                                                                                          >))))) 
                                                                                                                    (\mlambda{}I,rho.
                                                                                                                                    phi  I  (fst(rho))  \mvee{}  ...  \mvee{}  (...=1) 
                                                                                                                                                                                      I 
                                                                                                                                                                                      rho) 
                                                                                                                    (\mlambda{}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;\mneg{}(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.\mBbbI{} 
                                                                                                                                                (\mlambda{}x,x@0.  (fst(fst((sigma  x 
                                                                                                                                                                                      (m  x 
                                                                                                                                                                                        x@0)))))\000C) 
                                                                                                                                                (\mlambda{}I,a.
                                                                                                                                                            (phi  I 
                                                                                                                                                              (fst(a)))  \mvee{}  (\mlambda{}I,p.  ..\000C.=0)) 
                                                                                                                                                (\mlambda{}I,rho.
                                                                                                                                                                if  (phi  I 
                                                                                                                                                                        (fst((m  I 
                                                                                                                                                                                    rho)))==1)
                                                                                                                                                                then  fst((u  I 
                                                                                                                                                                                    (m  I 
                                                                                                                                                                                      rho)))
                                                                                                                                                                else  fst(...)
                                                                                                                                                                fi  ) 
                                                                                                                                                (\mlambda{}I,a.  (fst((a0  I 
                                                                                                                                                                          (fst(a)))))) 
                                                                                                                                                I 
                                                                                                                                                <fst(fst(rho)),  snd(rho)>)
                                                                                                                                    fi  ) 
                                                                                                                    (\mlambda{}I,a.  ((snd((a0  I  (fst(a)))))  I  1 
                                                                                                                                    (snd(a)))) 
                                                                                                                    J 
                                                                                                                    (f(a@0);u@0))
                                                                                            >) 
    <\mlambda{}J.J  {}\mrightarrow{}  I,  \mlambda{}I,J,f,g.  g  \mcdot{}  f>.(((E)\mlambda{}I,p.  (fst(p)))
                                                  \mlambda{}x,x@0.  <<a[x;x@0],  b[x;x@0]>
                                                                  ,  \mlambda{}J,f,u@0.  (cE 
                                                                                            <\mlambda{}J.J  {}\mrightarrow{}  I,  \mlambda{}I,J,f,g.  g  \mcdot{}  f>.\mBbbI{}.((A)\mlambda{}x,x@0.  <a[x;m  x  x@\000C0]
                                                                                                                                                                  ,  b[x;m  x  x@0]
                                                                                                                                                                  >)[1(\mBbbI{})] 
                                                                                            (\mlambda{}x,x@0.  <a[x;m  x  <fst(fst(x@0)),  snd(x@0)>]
                                                                                                              ,  b[x;m  x  <fst(fst(x@0)),  snd(x@0)>]
                                                                                                              >) 
                                                                                            (\mlambda{}I,a.  c[I;fst(fst(a))]  \mvee{}  dM-to-FL(I;\mneg{}(snd(fst(a))))) 
                                                                                            (\mlambda{}I@0,a@0.  (if  (c[I@0;
                                                                                                                              fst((m  I@0  <fst(fst(a@0)),  snd(a@0)>)\000C)]==1)
                                                                                                                    then  fst(\mcdot{})
                                                                                                                    else  fst(d[I@0;fst((m  I@0 
                                                                                                                                                            <fst(fst(a@0))
                                                                                                                                                            ,  snd(a@0)
                                                                                                                                                            >))])
                                                                                                                    fi   
                                                                                                                    I@0 
                                                                                                                    1 
                                                                                                                    (cA 
                                                                                                                      <\mlambda{}J.J  {}\mrightarrow{}  I,  \mlambda{}I,J,f,g.  g  \mcdot{}  f>.\mBbbI{}.((A)
                                                                                                                                                                        \mlambda{}x,x@0.  <a[x;
                                                                                                                                                                                            m  x 
                                                                                                                                                                                            x@0]
                                                                                                                                                                                        ,  b[x;
                                                                                                                                                                                              m  x 
                                                                                                                                                                                              x@0]
                                                                                                                                                                                        >)[1(\mBbbI{})]\000C.\mBbbI{} 
                                                                                                                      (\mlambda{}x,x@0.  <a[x;m  x 
                                                                                                                                                  <fst(fst((m  x  x@0)))
                                                                                                                                                  ,  \mneg{}(snd((m  x  x@0)))
                                                                                                                                                  >]
                                                                                                                                        ,  b[x;m  x 
                                                                                                                                                    <fst(fst((m  x  x@0)))
                                                                                                                                                    ,  \mneg{}(snd((m  x  x@0)))
                                                                                                                                                    >]
                                                                                                                                        >) 
                                                                                                                      (\mlambda{}I,rho.  0  \mvee{}  dM-to-FL(I;\mneg{}(snd(rho)))) 
                                                                                                                      (\mlambda{}I,rho.  (snd(fst((m  I  rho))))) 
                                                                                                                      (\mlambda{}I,a.  (snd(fst(a)))) 
                                                                                                                      I@0 
                                                                                                                      <fst(a@0),  \mneg{}(snd(a@0))>))) 
                                                                                            (\mlambda{}I@0,a@0.  ((fst(d[I@0;fst(fst(a@0))]))  I@0  1 
                                                                                                                    (cA 
                                                                                                                      <\mlambda{}J.J  {}\mrightarrow{}  I,  \mlambda{}I,J,f,g.  g  \mcdot{}  f>.\mBbbI{}.((A)
                                                                                                                                                                        \mlambda{}x,x@0.  <a[x;
                                                                                                                                                                                            m  x 
                                                                                                                                                                                            x@0]
                                                                                                                                                                                        ,  b[x;
                                                                                                                                                                                              m  x 
                                                                                                                                                                                              x@0]
                                                                                                                                                                                        >)[1(\mBbbI{})]\000C.\mBbbI{} 
                                                                                                                      (\mlambda{}x,x@0.  <a[x;m  x 
                                                                                                                                                  <fst(fst((m  x  x@0)))
                                                                                                                                                  ,  \mneg{}(snd((m  x  x@0)))
                                                                                                                                                  >]
                                                                                                                                        ,  b[x;m  x 
                                                                                                                                                    <fst(fst((m  x  x@0)))
                                                                                                                                                    ,  \mneg{}(snd((m  x  x@0)))
                                                                                                                                                    >]
                                                                                                                                        >) 
                                                                                                                      (\mlambda{}I,rho.  0  \mvee{}  dM-to-FL(I;\mneg{}(snd(rho)))) 
                                                                                                                      (\mlambda{}I,rho.  (snd(fst((m  I  rho))))) 
                                                                                                                      (\mlambda{}I,a.  (snd(fst(a)))) 
                                                                                                                      I@0 
                                                                                                                      <a@0,  \mneg{}(0)>))) 
                                                                                            J 
                                                                                            (f(x@0);u@0))
                                                                  >)... 
    ... 
    ... 
    ... 
    ... 
    ... 
    ...  \msim{}  ...


By

---

Latex:
((RWO    "contractible\_comp-sq"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index