---

Step * of Lemma path-contraction_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[pth:{X ⊢ _:(Path_A a b)}].
  (path-contraction(X;pth) ∈ {X.𝕀 ⊢ _:(Path_(A)p (a)p path-point(pth))})
BY
{ (Auto
   THEN Unfold `path-contraction` 0
   THEN (InstLemma `cubical-path-app_wf`  [⌜X.𝕀.𝕀⌝;⌜((A)p)p⌝;⌜((a)p)p⌝;⌜((b)p)p⌝;⌜((pth)p)p⌝;⌜(q)p ∧ q⌝]⋅ THENA Auto)) }

1
.....wf..... 
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. pth : {X ⊢ _:(Path_A a b)}
⊢ ((pth)p)p ∈ {X.𝕀.𝕀 ⊢ _:(Path_((A)p)p ((a)p)p ((b)p)p)}

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. pth : {X ⊢ _:(Path_A a b)}
6. ((pth)p)p @ (q)p ∧ q ∈ {X.𝕀.𝕀 ⊢ _:((A)p)p}
⊢ <>(((pth)p)p @ (q)p ∧ q) ∈ {X.𝕀 ⊢ _:(Path_(A)p (a)p path-point(pth))}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `path-contraction`  0
  THEN  (InstLemma  `cubical-path-app\_wf` 
              [\mkleeneopen{}X.\mBbbI{}.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((a)p)p\mkleeneclose{};\mkleeneopen{}((b)p)p\mkleeneclose{};\mkleeneopen{}((pth)p)p\mkleeneclose{};\mkleeneopen{}(q)p  \mwedge{}  q\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index