---

Step * 1 of Lemma discrete-path


1. T : Type
2. X : CubicalSet{j}
3. ∀[pth:{X ⊢ _:Path(discr(T))}]. (pth = refl(pth @ 0(𝕀)) ∈ {X ⊢ _:Path(discr(T))})
4. a : {X ⊢ _:discr(T)}
5. b : {X ⊢ _:discr(T)}
6. p : {X ⊢ _:(Path_discr(T) a b)}
7. p = refl(p @ 0(𝕀)) ∈ {X ⊢ _:Path(discr(T))}
⊢ p = refl(a) ∈ {X ⊢ _:(Path_discr(T) a b)}
BY
{ ((Subst' p @ 0(𝕀) = a ∈ {X ⊢ _:discr(T)} -1 THENA Auto) THEN BLemma `paths-equal` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  X  :  CubicalSet\{j\}
3.  \mforall{}[pth:\{X  \mvdash{}  \_:Path(discr(T))\}].  (pth  =  refl(pth  @  0(\mBbbI{})))
4.  a  :  \{X  \mvdash{}  \_:discr(T)\}
5.  b  :  \{X  \mvdash{}  \_:discr(T)\}
6.  p  :  \{X  \mvdash{}  \_:(Path\_discr(T)  a  b)\}
7.  p  =  refl(p  @  0(\mBbbI{}))
\mvdash{}  p  =  refl(a)


By

---

Latex:
((Subst'  p  @  0(\mBbbI{})  =  a  -1  THENA  Auto)  THEN  BLemma  `paths-equal`  THEN  Auto)

---

Home Index