---

Step * 1 of Lemma csm-contractible_comp


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))
BY
{ ((InstLemma `csm-pi_comp` [⌜X.A⌝;⌜H.(A)tau⌝]⋅ 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+))
7. ∀[tau@0,A@0,cA,cB:Top].  ((pi_comp(X.A;A@0;cA;cB))tau@0 ~ pi_comp(H.(A)tau;(A@0)tau@0;(cA)tau@0;(cB)tau@0+))
⊢ ((A)p)tau+ ~ ((A)tau)p

2
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+))
7. ∀[tau@0,A@0,cA,cB:Top].  ((pi_comp(X.A;A@0;cA;cB))tau@0 ~ pi_comp(H.(A)tau;(A@0)tau@0;(cA)tau@0;(cB)tau@0+))
⊢ ((cA)p)tau+ ~ ((cA)tau)p

3
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+))
7. ∀[tau@0,A@0,cA,cB:Top].  ((pi_comp(X.A;A@0;cA;cB))tau@0 ~ pi_comp(H.(A)tau;(A@0)tau@0;(cA)tau@0;(cB)tau@0+))
⊢ (path_comp(X.A.(A)p;((A)p)p;(q)p;q;
             ((cA)p)p))tau++ ~ path_comp(H.(A)tau.((A)tau)p;(((A)tau)p)p;(q)p;q;
                                         (((cA)tau)p)p)

---

Latex:

---

Latex:

1.  X  :  Top
2.  H  :  Top
3.  cA  :  Top
4.  A  :  Top
5.  tau  :  Top
6.  \mforall{}[cA,cB,A,tau:Top].    ((sigma\_comp(cA;cB))tau  \msim{}  sigma\_comp((cA)tau;(cB)tau+))
\mvdash{}  (pi\_comp(X.A;(A)p;(cA)p;path\_comp(X.A.(A)p;((A)p)p;(q)p;q;
                                                                        ((cA)p)p)))tau+ 
\msim{}  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))


By

---

Latex:
((InstLemma  `csm-pi\_comp`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}H.(A)tau\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index