---

Step * of Lemma singleton-contraction_wf2

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[a:{X ⊢ _:T}]. ∀[s:{X ⊢ _:Singleton(a)}].
  (singleton-contraction(X;s.2) ∈ {X ⊢ _:(Path_Singleton(a) singleton-center(X;a) s)})
BY
{ (Auto
   THEN Assert ⌜singleton-contraction(X;s.2) ∈ {X ⊢ _:(Path_Singleton(a) singleton-center(X;a) cubical-pair(s.1;s.2))}⌝⋅
   ) }

1
.....assertion..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. a : {X ⊢ _:T}
4. s : {X ⊢ _:Singleton(a)}
⊢ singleton-contraction(X;s.2) ∈ {X ⊢ _:(Path_Singleton(a) singleton-center(X;a) cubical-pair(s.1;s.2))}

2
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. a : {X ⊢ _:T}
4. s : {X ⊢ _:Singleton(a)}
5. singleton-contraction(X;s.2) ∈ {X ⊢ _:(Path_Singleton(a) singleton-center(X;a) cubical-pair(s.1;s.2))}
⊢ singleton-contraction(X;s.2) ∈ {X ⊢ _:(Path_Singleton(a) singleton-center(X;a) s)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:T\}].  \mforall{}[s:\{X  \mvdash{}  \_:Singleton(a)\}].
    (singleton-contraction(X;s.2)  \mmember{}  \{X  \mvdash{}  \_:(Path\_Singleton(a)  singleton-center(X;a)  s)\})


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}singleton-contraction(X;s.2)  \mmember{}  \{X  \mvdash{}  \_:(Path\_Singleton(a)  singleton-center(X;a)
                                                                                                                    cubical-pair(s.1;s.2))\}\mkleeneclose{}\mcdot{}
  )

---

Home Index