Proof of Nuprl Lemma : contractible

Step * of Lemma contractible_comp-apply-sq

∀[X,A,cA,B,a,b,c,d,J,x:Top].
(contractible_comp(X;A;cA) B (λx,y. a[x;y]) (λx,y. b[x;y]) (λx,y. c[x;y]) (λx,y. d[x;y]) J x

  ~ <cA <λI.(alpha:B(I) × 𝕀(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>> (λx,x@0. a[x;m x x@0])

(λI,rho. b[I;fst(rho)] ∨ dM-to-FL(I;¬(snd(rho))))

     (λI,rho. if (b[I;fst((m I rho))]==1) then fst(c[I;m I rho]) else fst(d[I;fst((m I rho))]) fi )

     (λI,a. (fst(d[I;fst(a)])))
     J
     <x, 1>
    , λJ@0,f,u@0,J@1,f@0,u@1. (cA

                               <λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))

                               , λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>, (snd(p) fst(p) f)>

>
(λx,x@0. a[x;<fst(fst(fst(x@0))), snd(x@0)>])

                               (λI,rho. b[I;fst(fst(rho))] ∨ dM-to-FL(I;¬(snd(rho))) ∨ dM-to-FL(I;snd(rho)))

(λI,rho. if (b[I;fst(fst(fst(rho)))]==1)

                                          then (snd(c[I;<fst(fst(fst(rho))), snd(rho)>])) I 1

(cA

                                                <λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))

                                                , λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>

                                                            , (snd(p) fst(p) f)

>

                                                (λx,x@0. a[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

                                                <fst(fst(rho)), ¬(snd(rho))>)

                                               I
                                               1
                                               (snd(fst(rho)))
                                       if (dM-to-FL(I;¬(snd(fst(rho))))==1)

                                         then cA <λI.(alpha:B(I) × 𝕀(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>

(λx,x@0. a[x;m x x@0])

                                              (λI,rho. b[I;fst(rho)] ∨ dM-to-FL(I;¬(snd(rho))))

                                              (λI,rho. if (b[I;fst((m I rho))]==1)

                                                      then fst(c[I;m I rho])

                                                      else fst(d[I;fst((m I rho))])

fi )

                                              (λI,a. (fst(d[I;fst(a)])))

I

                                              <fst(fst(fst(rho))), snd(rho)>

else cA

                                            <λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))

                                            , λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>

                                                        , (snd(p) fst(p) f)

>
>

                                            (λx,x@0. a[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
                                            <fst(fst(rho)), ¬(snd(rho))>
                                       fi )
                               (λI,a@0. ((snd(d[I;fst(fst(a@0))])) I 1
                                         (cA

                                          <λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))

                                          , λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>, (snd(p) fst(p) f)>

>

                                          (λx,x@0. a[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
                                          <fst(a@0), ¬(0)>)
                                         I
                                         1
                                         (snd(a@0))))
                               J@1
                               <<f@0(f(x)), (u@0 f(x) f@0)>, u@1>)
    >)
BY
{ (((UnivCD THENA Auto) THEN SqEqualTopToBase)
   THEN (RWO "contractible_comp-sq" 0 THENA Auto)
   THEN Reduce 0
   THEN RepUR ``let`` 0
   THEN ((RWO "fl-eq-0-1-false" 0 THENA Auto) THEN Reduce 0)
   THEN RepUR ``cube-context-adjoin cc-adjoin-cube cubical-pair interval-1`` 0
   THEN Auto) }

Latex:

Latex:
\mforall{}[X,A,cA,B,a,b,c,d,J,x:Top]. (contractible\_comp(X;A;cA) B (\mlambda{}x,y. a[x;y]) (\mlambda{}x,y. b[x;y]) (\mlambda{}x,y. c[x;y]) (\mlambda{}x,y. d[x;y]) J x \msim{} <cA <\mlambda{}I.(alpha:B(I) \mtimes{} \mBbbI{}(alpha)), \mlambda{}I,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>> (\mlambda{}x,x@0. a[x;m x x@0]\000C) (\mlambda{}I,rho. b[I;fst(rho)] \mvee{} dM-to-FL(I;\mneg{}(snd(rho)))) (\mlambda{}I,rho. if (b[I;fst((m I rho))]==1) then fst(c[I;m I rho]) else fst(d[I;fst((m I rho))]) fi ) (\mlambda{}I,a. (fst(d[I;fst(a)]))) J <x, 1> , \mlambda{}J@0,f,u@0,J@1,f@0,u@1. (cA <\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alpha) \mtimes{} \mBbbI{}(alpha)\000C) , \mlambda{}I,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)> , (snd(p) fst(p) f) > > (\mlambda{}x,x@0. a[x;<fst(fst(fst(x@0))), snd(x@0)>]) (\mlambda{}I,rho. b [I;fst(fst(rho))] \mvee{} dM-to-FL(I;\mneg{}(snd(rho))) \mvee{} dM-to-FL(I;...))\000C (\mlambda{}I,rho. if (b[I;fst(fst(fst(rho)))]==1) then (snd(c[I;<fst(fst(fst(rho))), snd(rho)>])) I 1 (cA <\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](\000Calpha) \mtimes{} \mBbbI{}(alpha)) , \mlambda{}I,J,f,p. <<f(fst(fst(p))) , (snd(fst(p)) fst(fst(p)) f) > , (snd(p) fst(p) f) > > (\mlambda{}x,x@0. a[x;<fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>\000C]) (\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 <fst(fst(rho)), \mneg{}(snd(rho))>) I 1 (snd(fst(rho))) if (dM-to-FL(I;\mneg{}(snd(fst(rho))))==1) then cA <\mlambda{}I.(alpha:B(I) \mtimes{} \mBbbI{}(alpha)) , \mlambda{}I,J,f,p. <f(fst(p)), (snd(p) fst(p) f)> > (\mlambda{}x,x@0. a[x;m x x@0]) (\mlambda{}I,rho. b[I;fst(rho)] \mvee{} dM-to-FL(I;\mneg{}(snd(rho)))) (\mlambda{}I,rho. if (b[I;fst((m I rho))]==1) then fst(c[I;m I rho]) else fst(d[I;fst((m I rho))]) fi ) (\mlambda{}I,a. (fst(d[I;fst(a)]))) I <fst(fst(fst(rho))), snd(rho)> else cA <\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alph\000Ca) \mtimes{} \mBbbI{}(alpha)) , \mlambda{}I,J,f,p. <<f(fst(fst(p))) , (snd(fst(p)) fst(fst(p)) f) > , (snd(p) fst(p) f) > > (\mlambda{}x,x@0. a[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 <fst(fst(rho)), \mneg{}(snd(rho))> fi ) (\mlambda{}I,a@0. ((snd(d[I;fst(fst(a@0))])) I 1 (cA <\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alpha) \mtimes{} \mBbbI{}(alpha)) , \mlambda{}I,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)> , (snd(p) fst(p) f) > > (\mlambda{}x,x@0. a[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 <fst(a@0), \mneg{}(0)>) I 1 (snd(a@0)))) J@1 <<f@0(f(x)), (u@0 f(x) f@0)>, u@1>) >) By Latex: (((UnivCD THENA Auto) THEN SqEqualTopToBase) THEN (RWO "contractible\_comp-sq" 0 THENA Auto) THEN Reduce 0 THEN RepUR ``let`` 0 THEN ((RWO "fl-eq-0-1-false" 0 THENA Auto) THEN Reduce 0) THEN RepUR ``cube-context-adjoin cc-adjoin-cube cubical-pair interval-1`` 0 THEN Auto) Home Index