---

Step * 3 of Lemma ss-free-homotopic_inversion


1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
7. λt.p@r1 - t@r0 ≡ b
⊢ λt.p@r1 - t@r1 ≡ a
BY
{ (RepUR ``path-at`` 0 THEN Fold `path-at` 0 THEN RepeatFor 2 ((nRNorm 0 THEN Auto THEN MemTypeCD THEN Auto))) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace@i'
2.  a  :  Point(X)@i
3.  b  :  Point(X)@i
4.  p  :  Point(Path(X))@i
5.  p@r0  \mequiv{}  a
6.  p@r1  \mequiv{}  b
7.  \mlambda{}t.p@r1  -  t@r0  \mequiv{}  b
\mvdash{}  \mlambda{}t.p@r1  -  t@r1  \mequiv{}  a


By

---

Latex:
(RepUR  ``path-at``  0
  THEN  Fold  `path-at`  0
  THEN  RepeatFor  2  ((nRNorm  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto)))

---

Home Index