---

Step * of Lemma fiber-path_wf

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[p:{X ⊢ _:Fiber(w;a)}].
  (fiber-path(p) ∈ {X ⊢ _:(Path_A a app(w; fiber-member(p)))})
BY
{ (Intros THEN Unhide THEN Unfold `cubical-fiber` -1) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. p : {X ⊢ _:Σ T (Path_(A)p (a)p app((w)p; q))}
⊢ fiber-path(p) ∈ {X ⊢ _:(Path_A a app(w; fiber-member(p)))}

---

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{}[p:\{X  \mvdash{}  \_:Fiber(w;a)\}].
    (fiber-path(p)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  a  app(w;  fiber-member(p)))\})


By

---

Latex:
(Intros  THEN  Unhide  THEN  Unfold  `cubical-fiber`  -1)

---

Home Index