---

Step * of Lemma fiber-member_wf

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

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))}
⊢ app((w)p; q) ∈ {X.T ⊢ _:(A)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-member(p)  \mmember{}  \{X  \mvdash{}  \_:T\})


By

---

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

---

Home Index