---

Step * of Lemma refl-path-app

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[r:{X ⊢ _:𝕀}].  (refl(a) @ r = a ∈ {X ⊢ _:A})
BY
{ (Intros THEN RepUR ``cubical-refl cubical-path-app cubicalpath-app term-to-path`` 0) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. r : {X ⊢ _:𝕀}
⊢ app((λ(a)p); r) = a ∈ {X ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[r:\{X  \mvdash{}  \_:\mBbbI{}\}].    (refl(a)  @  r  =  a)


By

---

Latex:
(Intros  THEN  RepUR  ``cubical-refl  cubical-path-app  cubicalpath-app  term-to-path``  0)

---

Home Index