---

Step * 1 of Lemma csm-equiv_comp


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))
⊢ 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 ⊢ _}
BY
{ (Symmetry THEN (InstLemmaIJ `csm-cubical-fiber` [H.(A ⟶ E).(E)p;⌜((A)p)p⌝;⌜((E)p)p⌝]⋅ THENA Auto)) }

1
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. ∀[w:{H.(A ⟶ E).(E)p ⊢ _:(((A)p)p ⟶ ((E)p)p)}]. ∀[a:{H.(A ⟶ E).(E)p ⊢ _:((E)p)p}]. ∀[Z:ij⊢].
    ∀[s:Z ij⟶ H.(A ⟶ E).(E)p].
      ((Fiber(w;a))s = Z ⊢ Fiber((w)s;(a)s) ∈ {Z ⊢ _})
⊢ (Fiber((q)p;q))tau++ = K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}

---

Latex:

---

Latex:

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
\mvdash{}  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  Fiber((q)p;q)  =  (Fiber((q)p;q))tau++


By

---

Latex:
(Symmetry  THEN  (InstLemmaIJ  `csm-cubical-fiber`  [H.(A  {}\mrightarrow{}  E).(E)p;\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((E)p)p\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index