---

Step * 1 of Lemma fiber-path_wf


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)))}
BY
{ Unfolds ``fiber-path fiber-member`` 0 }

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))}
⊢ p.2 ∈ {X ⊢ _:(Path_A a app(w; p.1))}

---

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


By

---

Latex:
Unfolds  ``fiber-path  fiber-member``  0

---

Home Index