---

Step * 1 of Lemma singleton-contraction_wf

.....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]}
⊢ cubical-pair((pth)p @ q;path-contraction(X;pth)) ∈ {X.𝕀 ⊢ _:(Σ T (Path_(T)p (a)p q))p}
BY
{ (GenConclTerm ⌜path-contraction(X;pth)⌝⋅ THENA Auto) }

1
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]}
8. v : {X.𝕀 ⊢ _:(Path_(T)p (a)p path-point(pth))}
9. path-contraction(X;pth) = v ∈ {X.𝕀 ⊢ _:(Path_(T)p (a)p path-point(pth))}
⊢ cubical-pair((pth)p @ q;v) ∈ {X.𝕀 ⊢ _:(Σ T (Path_(T)p (a)p q))p}

---

Latex:

---

Latex:
.....wf..... 
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{}  cubical-pair((pth)p  @  q;path-contraction(X;pth))  \mmember{}  \{X.\mBbbI{}  \mvdash{}  \_:(\mSigma{}  T  (Path\_(T)p  (a)p  q))p\}


By

---

Latex:
(GenConclTerm  \mkleeneopen{}path-contraction(X;pth)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index