---

Step * of Lemma singleton-contraction_wf

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[a,b:{X ⊢ _:T}]. ∀[pth:{X ⊢ _:(Path_T a b)}].
  (singleton-contraction(X;pth) ∈ {X ⊢ _:(Path_Σ T (Path_(T)p (a)p q) cubical-pair(a;refl(a)) cubical-pair(b;pth))})
BY
{ (Auto
   THEN Unfold `singleton-contraction` 0
   THEN (Assert refl(a) ∈ {X ⊢ _:((Path_(T)p (a)p q))[a]} BY
               ((InstLemma `cubical-refl_wf` [⌜X⌝;⌜T⌝;⌜a⌝]⋅ THENA Auto)
                THEN InferEqualType
                THEN Try (Trivial)
                THEN EqCDA
                THEN RWO "csm-path-type" 0
                THEN Auto))
   THEN (Assert pth ∈ {X ⊢ _:((Path_(T)p (a)p q))[b]} BY
               (InferEqualType THEN Try (Trivial) THEN EqCDA THEN RWO "csm-path-type" 0 THEN Auto))
   THEN BLemma `term-to-path-wf`
   THEN Auto) }

1
.....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}

2
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)))[1(𝕀)]=cubical-pair(b;pth):Σ T (Path_(T)p (a)p q)

3
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:T\}].  \mforall{}[pth:\{X  \mvdash{}  \_:(Path\_T  a  b)\}].
    (singleton-contraction(X;pth)  \mmember{}  \{X  \mvdash{}  \_:(Path\_\mSigma{}  T  (Path\_(T)p  (a)p  q)  cubical-pair(a;refl(a))
                                                                                              cubical-pair(b;pth))\})


By

---

Latex:
(Auto
  THEN  Unfold  `singleton-contraction`  0
  THEN  (Assert  refl(a)  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (a)p  q))[a]\}  BY
                          ((InstLemma  `cubical-refl\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InferEqualType
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  RWO  "csm-path-type"  0
                            THEN  Auto))
  THEN  (Assert  pth  \mmember{}  \{X  \mvdash{}  \_:((Path\_(T)p  (a)p  q))[b]\}  BY
                          (InferEqualType  THEN  Try  (Trivial)  THEN  EqCDA  THEN  RWO  "csm-path-type"  0  THEN  Auto))
  THEN  BLemma  `term-to-path-wf`
  THEN  Auto)

---

Home Index