---

Step * 2 of Lemma csm-equiv_comp

.....aux..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
6. cA : H +⊢ Compositon(A)
7. cE : H +⊢ Compositon(E)
8. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau ⟶ (E)tau))p)p}
9. (((A)tau ⟶ (E)tau))p = (K.((A)tau ⟶ (E)tau) ⊢ ((A)tau)p ⟶ ((E)tau)p) ∈ {K.((A)tau ⟶ (E)tau) ⊢ _}
10. ((((A)tau)p ⟶ ((E)tau)p))p
= (K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ (((A)tau)p)p ⟶ (((E)tau)p)p)
∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
11. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau)p)p ⟶ (((E)tau)p)p)}
12. v : K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
13. fiber-comp(K.((A)tau ⟶ (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;(((cA)tau)p)p;(((cE)tau)p)p)
= v
∈ K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
14. K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) = (Fiber((q)p;q))tau++ ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
15. Z : {z:{K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}| 
         (z = K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _})
         ∧ (z = (Fiber((q)p;q))tau++ ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _})} 
⊢ pi_comp(K.((A)tau ⟶ (E)tau);((E)tau)p;((cE)tau)p;contractible_comp(K.((A)tau ⟶ (E)tau).((E)tau)p;Z;v))
  ∈ K.((A)tau ⟶ (E)tau) +⊢ Compositon(IsEquiv(((A)tau)p;((E)tau)p;q))
BY
{ (RepeatFor 2 (D -1)
   THEN (Assert v ∈ K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Z) BY
               (InferEqualTypeGen THENL [(EqCDA THEN Auto); Auto]))
   THEN (InstLemmaIJ `contractible_comp_wf` [⌜K.((A)tau ⟶ (E)tau).((E)tau)p⌝;⌜Z⌝;⌜v⌝]⋅ THENA Auto)
   THEN (InstLemmaIJ `pi_comp_wf2` [⌜K.((A)tau ⟶ (E)tau)⌝;⌜((E)tau)p⌝;⌜Contractible(Z)⌝;⌜((cE)tau)p⌝;
         ⌜contractible_comp(K.((A)tau ⟶ (E)tau).((E)tau)p;Z;v)⌝]⋅
         THENA Auto
         )
   THEN InferEqualTypeGen
   THEN RepUR ``is-cubical-equiv`` 0
   THEN RepeatFor 3 (EqCDA)
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  H  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  H
4.  A  :  \{H  \mvdash{}  \_\}
5.  E  :  \{H  \mvdash{}  \_\}
6.  cA  :  H  +\mvdash{}  Compositon(A)
7.  cE  :  H  +\mvdash{}  Compositon(E)
8.  (q)p  \mmember{}  \{K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  \_:((((A)tau  {}\mrightarrow{}  (E)tau))p)p\}
9.  (((A)tau  {}\mrightarrow{}  (E)tau))p  =  (K.((A)tau  {}\mrightarrow{}  (E)tau)  \mvdash{}  ((A)tau)p  {}\mrightarrow{}  ((E)tau)p)
10.  ((((A)tau)p  {}\mrightarrow{}  ((E)tau)p))p  =  (K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  (((A)tau)p)p  {}\mrightarrow{}  (((E)tau)p)p)
11.  (q)p  \mmember{}  \{K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  \_:((((A)tau)p)p  {}\mrightarrow{}  (((E)tau)p)p)\}
12.  v  :  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  +\mvdash{}  Compositon(Fiber((q)p;q))
13.  fiber-comp(K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;(((cA)tau)p)p;
                              (((cE)tau)p)p)
=  v
14.  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  Fiber((q)p;q)  =  (Fiber((q)p;q))tau++
15.  Z  :  \{z:\{K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  \_\}| 
                  (z  =  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  Fiber((q)p;q))  \mwedge{}  (z  =  (Fiber((q)p;q))tau++)\} 
\mvdash{}  pi\_comp(K.((A)tau  {}\mrightarrow{}  (E)tau);((E)tau)p;((cE)tau)p;
                    contractible\_comp(K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p;Z;v))
    \mmember{}  K.((A)tau  {}\mrightarrow{}  (E)tau)  +\mvdash{}  Compositon(IsEquiv(((A)tau)p;((E)tau)p;q))


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (Assert  v  \mmember{}  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  +\mvdash{}  Compositon(Z)  BY
                          (InferEqualTypeGen  THENL  [(EqCDA  THEN  Auto);  Auto]))
  THEN  (InstLemmaIJ  `contractible\_comp\_wf`  [\mkleeneopen{}K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemmaIJ  `pi\_comp\_wf2`  [\mkleeneopen{}K.((A)tau  {}\mrightarrow{}  (E)tau)\mkleeneclose{};\mkleeneopen{}((E)tau)p\mkleeneclose{};\mkleeneopen{}Contractible(Z)\mkleeneclose{};\mkleeneopen{}((cE)tau)p\mkleeneclose{};
              \mkleeneopen{}contractible\_comp(K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p;Z;v)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  InferEqualTypeGen
  THEN  RepUR  ``is-cubical-equiv``  0
  THEN  RepeatFor  3  (EqCDA)
  THEN  Auto)

---

Home Index