---

Step * of Lemma path-type-at

∀[X,A,a,b,I,alpha:Top].
  ((Path_A a b)(alpha) ~ {p:{w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:Point(dM(J)) ⟶ A(f(alpha))| 
                             ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:Point(dM(J)).
                               ((w J f u f(alpha) g) = (w K f ⋅ g (u f(alpha) g)) ∈ A(g(f(alpha))))} | 
                          ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))} )
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``path-type pathtype cubical-subset cubical-fun`` 0
   THEN RepUR ``cubical-fun-family`` 0
   THEN (RWO "interval-type-at" 0 THENA Auto)
   THEN RepUR ``interval-presheaf`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,A,a,b,I,alpha:Top].
    ((Path\_A  a  b)(alpha)  \msim{}  \{p:\{w:J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  u:Point(dM(J))  {}\mrightarrow{}  A(f(alpha))| 
                                                          \mforall{}J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}u:Point(dM(J)).
                                                              ((w  J  f  u  f(alpha)  g)  =  (w  K  f  \mcdot{}  g  (u  f(alpha)  g)))\}  | 
                                                    ((p  I  1  0)  =  a(alpha))  \mwedge{}  ((p  I  1  1)  =  b(alpha))\}  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``path-type  pathtype  cubical-subset  cubical-fun``  0
  THEN  RepUR  ``cubical-fun-family``  0
  THEN  (RWO  "interval-type-at"  0  THENA  Auto)
  THEN  RepUR  ``interval-presheaf``  0
  THEN  Auto)

---

Home Index