---

Step * of Lemma rev-path_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[b,a:{X ⊢ _:A}]. ∀[pth:{X ⊢ _:(Path_A a b)}].  (rev-path(X;pth) ∈ {X ⊢ _:(Path_A b a)})
BY
{ (InstLemma `path-type-ext-eq` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Intro
   THEN (Assert ⌜rev-path(X;pth) ∈ {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = b ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = a ∈ {X ⊢ _:A})} ⌝⋅
   THENM (D -3 THEN DoSubsume THEN Auto)
   )
   THEN Thin (-2)
   THEN Unhide) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. b : {X ⊢ _:A}
4. a : {X ⊢ _:A}
5. pth : {X ⊢ _:(Path_A a b)}
⊢ rev-path(X;pth) ∈ {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = b ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = a ∈ {X ⊢ _:A})} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[b,a:\{X  \mvdash{}  \_:A\}].  \mforall{}[pth:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].
    (rev-path(X;pth)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  b  a)\})


By

---

Latex:
(InstLemma  `path-type-ext-eq`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intro
  THEN  (Assert  \mkleeneopen{}rev-path(X;pth)  \mmember{}  \{t:\{X  \mvdash{}  \_:Path(A)\}|  (t  @  0(\mBbbI{})  =  b)  \mwedge{}  (t  @  1(\mBbbI{})  =  a)\}  \mkleeneclose{}\mcdot{}
  THENM  (D  -3  THEN  DoSubsume  THEN  Auto)
  )
  THEN  Thin  (-2)
  THEN  Unhide)

---

Home Index