---

Step * 3 of Lemma singleton-contraction_wf


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. a : {X ⊢ _:T}
4. b : {X ⊢ _:T}
5. pth : {X ⊢ _:(Path_T a b)}
6. refl(a) ∈ {X ⊢ _:((Path_(T)p (a)p q))[a]}
7. pth ∈ {X ⊢ _:((Path_(T)p (a)p q))[b]}
⊢ X ⊢ (cubical-pair((pth)p @ q;path-contraction(X;pth)))[0(𝕀)]=cubical-pair(a;refl(a)):Σ T (Path_(T)p (a)p q)
BY
{ ((RWW "csm-cubical-pair cubical-path-ap-id-adjoin" 0 THENA Auto)
   THEN Unfold `same-cubical-term` 0
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:T\}
4.  b  :  \{X  \mvdash{}  \_:T\}
5.  pth  :  \{X  \mvdash{}  \_:(Path\_T  a  b)\}
6.  refl(a)  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (a)p  q))[a]\}
7.  pth  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (a)p  q))[b]\}
\mvdash{}  X  \mvdash{}  (cubical-pair((pth)p  @  q;path-contraction(X;pth)))[0(\mBbbI{})]=cubical-pair(a;refl(a)):
    \mSigma{}  T  (Path\_(T)p  (a)p  q)


By

---

Latex:
((RWW  "csm-cubical-pair  cubical-path-ap-id-adjoin"  0  THENA  Auto)
  THEN  Unfold  `same-cubical-term`  0
  THEN  EqCDA
  THEN  Auto)

---

Home Index