---

Step * of Lemma cubical-path-app-1

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[t:{X ⊢ _:(Path_A a b)}].  (t @ 1(𝕀) = b ∈ {X ⊢ _:A})
BY
{ (Auto
   THEN BLemma `cubical-term-equal2`
   THEN Auto
   THEN RepUR ``cubical-path-app cubicalpath-app cubical-app interval-1`` 0) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. t : {X ⊢ _:(Path_A a b)}
6. I : fset(ℕ)
7. a1 : X(I)
⊢ (t I a1 I 1 1) = (b I a1) ∈ A(a1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[t:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].    (t  @  1(\mBbbI{})  =  b)


By

---

Latex:
(Auto
  THEN  BLemma  `cubical-term-equal2`
  THEN  Auto
  THEN  RepUR  ``cubical-path-app  cubicalpath-app  cubical-app  interval-1``  0)

---

Home Index