---

Step * 1 of Lemma ss-homotopic_weakening


1. X : SeparationSpace@i'
2. [x0] : Point(X)
3. [x1] : Point(X)
4. a : Point(Path(X))@i
5. b : Point(Path(X))@i
6. b@r1 ≡ x1
7. b@r0 ≡ x0
8. a ≡ b
9. λt.b ∈ Point(Path(Path(X)))
⊢ ss-homotopic(X;x0;x1;a;b)
BY
{ (D 0 With ⌜λt.b⌝  THEN Auto THEN RepUR ``path-at`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace@i'
2.  [x0]  :  Point(X)
3.  [x1]  :  Point(X)
4.  a  :  Point(Path(X))@i
5.  b  :  Point(Path(X))@i
6.  b@r1  \mequiv{}  x1
7.  b@r0  \mequiv{}  x0
8.  a  \mequiv{}  b
9.  \mlambda{}t.b  \mmember{}  Point(Path(Path(X)))
\mvdash{}  ss-homotopic(X;x0;x1;a;b)


By

---

Latex:
(D  0  With  \mkleeneopen{}\mlambda{}t.b\mkleeneclose{}    THEN  Auto  THEN  RepUR  ``path-at``  0  THEN  Auto)

---

Home Index