---

Step * of Lemma discrete-path

No Annotations
∀[T:Type]. ∀[X:j⊢]. ∀[a,b:{X ⊢ _:discr(T)}]. ∀[p:{X ⊢ _:(Path_discr(T) a b)}].
  (p = refl(a) ∈ {X ⊢ _:(Path_discr(T) a b)})
BY
{ (InstLemma `discrete-pathtype` [] THEN RepeatFor 2 (ParallelLast') THEN Intros THEN (InstHyp [⌜p⌝] 3⋅ THENA Auto)) }

1
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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[a,b:\{X  \mvdash{}  \_:discr(T)\}].  \mforall{}[p:\{X  \mvdash{}  \_:(Path\_discr(T)  a  b)\}].    (p  =  refl(a))


By

---

Latex:
(InstLemma  `discrete-pathtype`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intros
  THEN  (InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index