---

Step * of Lemma sigma_comp-sq

∀[X,A,cA,cB:Top].
  (sigma_comp(cA;cB) ~ λH,sigma,phi,u,a0. let a = cA H.𝕀 (λx,x@0. (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)))))) in
                                           let b = cB H (λx,x@0. <sigma x x@0, a x x@0>) phi (λI,a. (snd((u I a)))) 
                                                   (λI,a. (snd((a0 I a)))) in
                                           λI,a@0. <a I <a@0, 1>, b I a@0>)
BY
{ (Auto
   THEN RepUR ``sigma_comp fill_term comp-to-fill comp_term csm-comp-structure`` 0
   THEN RepUR ``csm-comp compose csm+ csm-id csm-adjoin cc-snd cc-fst csm-ap csm-id-adjoin`` 0
   THEN RepUR ``csm-ap-term csm-ap interval-1 cubical-pair cubical-fst cubical-snd`` 0
   THEN RepUR ``case-term cubical-term-at face-or face-zero`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``sigma\_comp  fill\_term  comp-to-fill  comp\_term  csm-comp-structure``  0
  THEN  RepUR  ``csm-comp  compose  csm+  csm-id  csm-adjoin  cc-snd  cc-fst  csm-ap  csm-id-adjoin``  0
  THEN  RepUR  ``csm-ap-term  csm-ap  interval-1  cubical-pair  cubical-fst  cubical-snd``  0
  THEN  RepUR  ``case-term  cubical-term-at  face-or  face-zero``  0
  THEN  Auto)

---

Home Index