---

Step * of Lemma equiv_comp-apply-sq

No Annotations
∀[H,A,E,cA,cE,I,a,b,c,d:Top].
  (equiv_comp(H;A;E;cA;cE) formal-cube(I) (λx,y. <a[x;y], b[x;y]>) (λK,f. c[K;f]) (λI@0,a. ⋅) (λK,f. d[K;f]) I 1 
  ~ equiv_comp_apply(H;A;E;cA;cE;I;a;b;c;d))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "equiv_comp-sq" 0 THENA Auto)
   THEN ((RWO "sigma_comp-sq" 0 THENA Auto) THEN Reduce 0)
   THEN (RWO "pi_comp-sq" 0 THENA Auto)
   THEN RepUR ``let cubical-lambda formal-cube`` 0
   THEN Unfold `equiv_comp_apply` 0
   THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))) }

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
⊢ 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)))) 
                                                           ... 
                                                           ...))) 
                                              ... 
                                              ...)
                                 >)... 
  ... 
  ... 
  ... 
  ... 
  ... 
  ... ~ ...

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,A,E,cA,cE,I,a,b,c,d:Top].
    (equiv\_comp(H;A;E;cA;cE)  formal-cube(I)  (\mlambda{}x,y.  <a[x;y],  b[x;y]>)  (\mlambda{}K,f.  c[K;f])  (\mlambda{}I@0,a.  \mcdot{})  (\mlambda{}K,f.\000C  d[K;f])  I  1 
    \msim{}  equiv\_comp\_apply(H;A;E;cA;cE;I;a;b;c;d))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "equiv\_comp-sq"  0  THENA  Auto)
  THEN  ((RWO  "sigma\_comp-sq"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (RWO  "pi\_comp-sq"  0  THENA  Auto)
  THEN  RepUR  ``let  cubical-lambda  formal-cube``  0
  THEN  Unfold  `equiv\_comp\_apply`  0
  THEN  RepeatFor  4  ((EqCD  THEN  Try  (Trivial))))

---

Home Index