---

Step * of Lemma term-to-path-beta

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[b:{X.𝕀 ⊢ _:(A)p}]. ∀[r:{X ⊢ _:𝕀}].  (<>(b) @ r = (b)[r] ∈ {X ⊢ _:A})
BY
{ (Intros
   THEN RepUR ``term-to-path cubicalpath-app`` 0⋅
   THEN (InstLemma `cubical-beta` [⌜X⌝;⌜𝕀⌝;⌜(A)p⌝;⌜b⌝;⌜r⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN InferEqualType
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[b:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}].  \mforall{}[r:\{X  \mvdash{}  \_:\mBbbI{}\}].    (<>(b)  @  r  =  (b)[r])


By

---

Latex:
(Intros
  THEN  RepUR  ``term-to-path  cubicalpath-app``  0\mcdot{}
  THEN  (InstLemma  `cubical-beta`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  InferEqualType
  THEN  EqCDA
  THEN  Auto)

---

Home Index