---

Step * of Lemma csm-cubical-fiber

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[Z:j⊢]. ∀[s:Z j⟶ X].
  ((Fiber(w;a))s = Z ⊢ Fiber((w)s;(a)s) ∈ {Z ⊢ _})
BY
{ (Auto
   THEN (Assert (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)} BY
               Auto)
   THEN (Assert ((w)s)p ∈ {Z.(T)s ⊢ _:(((T ⟶ A))s)p} BY
               Auto)
   THEN (Assert (((T ⟶ A))s)p = (Z.(T)s ⊢ ((T)s)p ⟶ ((A)s)p) ∈ {Z.(T)s ⊢ _} BY
               ((RWO "csm-cubical-fun" 0 THENA Auto) THEN InstLemmaIJ `csm-cubical-fun`  [] THEN BHyp -1 THEN Auto))
   THEN Unfold `cubical-fiber` 0
   THEN RWO "csm-cubical-sigma" 0
   THEN 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 ⊢ _}
⊢ Σ (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:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[Z:j\mvdash{}].  \mforall{}[s:Z  j{}\mrightarrow{}  X].
    ((Fiber(w;a))s  =  Z  \mvdash{}  Fiber((w)s;(a)s))


By

---

Latex:
(Auto
  THEN  (Assert  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T)p  {}\mrightarrow{}  (A)p)\}  BY
                          Auto)
  THEN  (Assert  ((w)s)p  \mmember{}  \{Z.(T)s  \mvdash{}  \_:(((T  {}\mrightarrow{}  A))s)p\}  BY
                          Auto)
  THEN  (Assert  (((T  {}\mrightarrow{}  A))s)p  =  (Z.(T)s  \mvdash{}  ((T)s)p  {}\mrightarrow{}  ((A)s)p)  BY
                          ((RWO  "csm-cubical-fun"  0  THENA  Auto)
                            THEN  InstLemmaIJ  `csm-cubical-fun`    []
                            THEN  BHyp  -1
                            THEN  Auto))
  THEN  Unfold  `cubical-fiber`  0
  THEN  RWO  "csm-cubical-sigma"  0
  THEN  Auto)

---

Home Index