---

Step * 1 of Lemma csm-pi_comp


1. [X] : Top
2. [Y] : Top
3. [tau] : Top
4. [A] : Top
5. [cA] : Top
6. [cB] : Top
⊢ (pi_comp(X;A;cA;cB))tau ~ pi_comp(Y;(A)tau;(cA)tau;(cB)tau+)
BY
{ ((RepUR ``pi_comp csm-comp-structure let`` 0 THEN RepUR ``cubical-lambda`` 0)
   THEN RepeatFor 10 (EqCD)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))) }

1
1. X : Top
2. Y : Top
3. tau : Top
4. A : Top
5. cA : Top
6. cB : Top
7. H : Base
8. sigma : Base
9. phi : Base
10. u : Base
11. a0 : Base
12. I : Base
13. a : Base
14. J : Base
15. f : Base
16. u@0 : Base
⊢ comp λH@0,sigma@0,phi,u,a0. (cB H@0 
                               (tau o sigma o p+;revfill(H.((A)tau o sigma)
                                                            [1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 
                                                                                           tau o sigma o p+ o sigma@0 
                                                                                           phi 
                                                                                           u 
                                                                                           a0);q)) o sigma@0 
                               phi 
                               u 
                               a0) [(phi)p ⟶ app((u)p+; revfill(H.((A)tau o sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0\000C 
                                                                                             tau o sigma o p+ o sigma@0 
                                                                                             phi 
                                                                                             u 
                                                                                             a0);q))]
      app((a0)p; (revfill(H.((A)tau o sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ o sigma@0 phi u a0);q\000C))[0(𝕀)]) 
~ comp λH@0,sigma@0,phi,u,a0. (cB H@0 
                               tau+ o (sigma o p+;revfill(H.(((A)tau)sigma)
                                                             [1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 
                                                                                            tau o sigma o p+ o sigma@0 
                                                                                            phi 
                                                                                            u 
                                                                                            a0);q)) o sigma@0 
                               phi 
                               u 
                               a0) [(phi)p ⟶ app((u)p+; revfill(H.(((A)tau)sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 
                                                                                            tau o sigma o p+ o sigma@0 
                                                                                            phi 
                                                                                            u 
                                                                                            a0);q))]
      app((a0)p; (revfill(H.(((A)tau)sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ o sigma@0 phi u a0);q)\000C)[0(𝕀)])

---

Latex:

---

Latex:

1.  [X]  :  Top
2.  [Y]  :  Top
3.  [tau]  :  Top
4.  [A]  :  Top
5.  [cA]  :  Top
6.  [cB]  :  Top
\mvdash{}  (pi\_comp(X;A;cA;cB))tau  \msim{}  pi\_comp(Y;(A)tau;(cA)tau;(cB)tau+)


By

---

Latex:
((RepUR  ``pi\_comp  csm-comp-structure  let``  0  THEN  RepUR  ``cubical-lambda``  0)
  THEN  RepeatFor  10  (EqCD)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial))))

---

Home Index