---

Step * 1 of Lemma path-type_wf

.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : fset(ℕ)
6. alpha : X(I)
7. p : Path(A)(alpha)
⊢ ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha)) ∈ ℙ
BY
{ (OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family``) THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  fset(\mBbbN{})
6.  alpha  :  X(I)
7.  p  :  Path(A)(alpha)
\mvdash{}  ((p  I  1  0)  =  a(alpha))  \mwedge{}  ((p  I  1  1)  =  b(alpha))  \mmember{}  \mBbbP{}


By

---

Latex:
(OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)

---

Home Index