---

Step * of Lemma discrete-path-endpoints

No Annotations
∀[X:j⊢]. ∀[T:Type].
  ∀a:{X ⊢ _:discr(T)}. ∀[b:{X ⊢ _:discr(T)}]. ∀[p:{X ⊢ _:(Path_discr(T) a b)}].  (a = b ∈ {X ⊢ _:discr(T)})
BY
{ (Auto
   THEN (InstLemma `path-eta_wf` [⌜X⌝;⌜discr(T)⌝;⌜p⌝]⋅ THENA Auto)
   THEN (RWO "csm-discrete-cubical-type" (-1) THENA Auto)) }

1
1. X : CubicalSet{j}
2. T : Type
3. a : {X ⊢ _:discr(T)}
4. b : {X ⊢ _:discr(T)}
5. p : {X ⊢ _:(Path_discr(T) a b)}
6. path-eta(p) ∈ {X.𝕀 ⊢ _:discr(T)}
⊢ a = b ∈ {X ⊢ _:discr(T)}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}discr(T)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "csm-discrete-cubical-type"  (-1)  THENA  Auto))

---

Home Index