---

Step * of Lemma path-point-0

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[pth:{X ⊢ _:(Path_A a b)}].  ((path-point(pth))[0(𝕀)] = a ∈ {X ⊢ _:A})
BY
{ (Auto
   THEN RepUR ``path-point`` 0
   THEN (RWO "csm-cubical-path-app" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst' (0(𝕀))1(X) ~ 0(𝕀) 0 THENA (CsmUnfolding THEN Auto))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. pth : {X ⊢ _:(Path_A a b)}
⊢ (pth)1(X) @ 0(𝕀) = a ∈ {X ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[pth:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].    ((path-point(pth))[0(\mBbbI{})]  =  a)


By

---

Latex:
(Auto
  THEN  RepUR  ``path-point``  0
  THEN  (RWO  "csm-cubical-path-app"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst'  (0(\mBbbI{}))1(X)  \msim{}  0(\mBbbI{})  0  THENA  (CsmUnfolding  THEN  Auto)))

---

Home Index