---

Step * of Lemma pi_comp-sq

∀[X,A,cA,cB:Top].
  (pi_comp(X;A;cA;cB) ~ λH,sigma,phi,u,a0. let v = λI,a. (cA H.((A)sigma)[1(𝕀)].𝕀 
                                                          (λx,x@0. (sigma 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), ¬(snd(a))>) in
                                               (λcB H.((A)sigma)[1(𝕀)] (λx,x@0. <sigma x <fst(fst(x@0)), snd(x@0)>, v x \000Cx@0>) 
                                                 (λI,a. (phi I (fst(a)))) 
                                                 (λI,a. (u I <fst(fst(a)), snd(a)> I 1 (v I a))) 
                                                 (λI,a. (a0 I (fst(a)) I 1 (v I <a, 0>)))))
BY
{ (Auto
   THEN SqEqualTopToBase
   THEN RepUR ``pi_comp revfill rev_fill_term rev-type-comp fill_term comp-to-fill`` 0
   THEN ...
   THEN RepUR ``interval-0 csm-id interval-rev case-term case_term face-0 cubical-term-at`` 0
   THEN (RWO  "fl-eq-0-1-false" 0 THENA Auto)
   THEN RepUR ``face-or cubical-term-at face-zero`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,A,cA,cB:Top].
    (pi\_comp(X;A;cA;cB)  \msim{}  \mlambda{}H,sigma,phi,u,a0.  let  v  =  \mlambda{}I,a.  (cA  H.((A)sigma)[1(\mBbbI{})].\mBbbI{} 
                                                                                                                    (\mlambda{}x,x@0.  (sigma  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),  \mneg{}(snd(a))>)  in
                                                                                              (\mlambda{}cB  H.((A)sigma)[1(\mBbbI{})] 
                                                                                                  (\mlambda{}x,x@0.  <sigma  x  <fst(fst(x@0)),  snd(x@0)>,  v  x  x@\000C0>) 
                                                                                                  (\mlambda{}I,a.  (phi  I  (fst(a)))) 
                                                                                                  (\mlambda{}I,a.  (u  I  <fst(fst(a)),  snd(a)>  I  1  (v  I  a))) 
                                                                                                  (\mlambda{}I,a.  (a0  I  (fst(a))  I  1  (v  I  <a,  0>)))))


By

---

Latex:
(Auto
  THEN  SqEqualTopToBase
  THEN  RepUR  ``pi\_comp  revfill  rev\_fill\_term  rev-type-comp  fill\_term  comp-to-fill``  0
  THEN  ...
  THEN  RepUR  ``interval-0  csm-id  interval-rev  case-term  case\_term  face-0  cubical-term-at``  0
  THEN  (RWO    "fl-eq-0-1-false"  0  THENA  Auto)
  THEN  RepUR  ``face-or  cubical-term-at  face-zero``  0
  THEN  Auto)

---

Home Index