---

Step * of Lemma csm-contractible_comp

∀[X,H,cA,A,tau:Top].  ((contractible_comp(X;A;cA))tau ~ contractible_comp(H;(A)tau;(cA)tau))
BY
{ (Auto
   THEN RepUR ``contractible_comp`` 0
   THEN (InstLemma `csm-sigma_comp2` [⌜X⌝;⌜H⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)) }

1
1. X : Top
2. H : Top
3. cA : Top
4. A : Top
5. tau : Top
6. ∀[cA,cB,A,tau:Top].  ((sigma_comp(cA;cB))tau ~ sigma_comp((cA)tau;(cB)tau+))
⊢ (pi_comp(X.A;(A)p;(cA)p;path_comp(X.A.(A)p;((A)p)p;(q)p;q;
                                    ((cA)p)p)))tau+ 
~ pi_comp(H.(A)tau;((A)tau)p;((cA)tau)p;path_comp(H.(A)tau.((A)tau)p;(((A)tau)p)p;(q)p;q;
                                                  (((cA)tau)p)p))

---

Latex:

---

Latex:
\mforall{}[X,H,cA,A,tau:Top].    ((contractible\_comp(X;A;cA))tau  \msim{}  contractible\_comp(H;(A)tau;(cA)tau))


By

---

Latex:
(Auto
  THEN  RepUR  ``contractible\_comp``  0
  THEN  (InstLemma  `csm-sigma\_comp2`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index