---

Step * 1 of Lemma csm-cubical-fiber


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. Z : CubicalSet{j}
7. s : Z j⟶ X
8. (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)}
9. ((w)s)p ∈ {Z.(T)s ⊢ _:(((T ⟶ A))s)p}
10. (((T ⟶ A))s)p = (Z.(T)s ⊢ ((T)s)p ⟶ ((A)s)p) ∈ {Z.(T)s ⊢ _}
⊢ Σ (T)s ((Path_(A)p (a)p app((w)p; q)))(s o p;q) = Σ (T)s (Path_((A)s)p ((a)s)p app(((w)s)p; q)) ∈ {Z ⊢ _}
BY
{ (InstLemmaIJ `csm-ap-comp-type` [⌜X⌝;⌜Z⌝;⌜Z.(T)s⌝;⌜p⌝;⌜s⌝;⌜A⌝]⋅ THENA Auto) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. Z : CubicalSet{j}
7. s : Z j⟶ X
8. (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)}
9. ((w)s)p ∈ {Z.(T)s ⊢ _:(((T ⟶ A))s)p}
10. (((T ⟶ A))s)p = (Z.(T)s ⊢ ((T)s)p ⟶ ((A)s)p) ∈ {Z.(T)s ⊢ _}
11. (A)s o p = ((A)s)p ∈ {Z.(T)s ⊢ _}
⊢ Σ (T)s ((Path_(A)p (a)p app((w)p; q)))(s o p;q) = Σ (T)s (Path_((A)s)p ((a)s)p app(((w)s)p; q)) ∈ {Z ⊢ _}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  w  :  \{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  Z  :  CubicalSet\{j\}
7.  s  :  Z  j{}\mrightarrow{}  X
8.  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T)p  {}\mrightarrow{}  (A)p)\}
9.  ((w)s)p  \mmember{}  \{Z.(T)s  \mvdash{}  \_:(((T  {}\mrightarrow{}  A))s)p\}
10.  (((T  {}\mrightarrow{}  A))s)p  =  (Z.(T)s  \mvdash{}  ((T)s)p  {}\mrightarrow{}  ((A)s)p)
\mvdash{}  \mSigma{}  (T)s  ((Path\_(A)p  (a)p  app((w)p;  q)))(s  o  p;q)  =  \mSigma{}  (T)s  (Path\_((A)s)p  ((a)s)p  app(((w)s)p;  q))


By

---

Latex:
(InstLemmaIJ  `csm-ap-comp-type`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}Z.(T)s\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index