---

Step * 1 of Lemma contractible-to-prop_wf


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. cA : X +⊢ Compositon(A)
4. c : {X ⊢ _:Contractible(A)}
5. ((c)p)p ∈ {X.A.(A)p ⊢ _:((Contractible(A))p)p}
6. {X.A.(A)p ⊢ _:((Contractible(A))p)p} = {X.A.(A)p ⊢ _:Contractible(((A)p)p)} ∈ 𝕌{[i' | j']}
7. ∀[x:{X.A.(A)p ⊢ _:((A)p)p}]. (contr-path(((c)p)p;x) ∈ {X.A.(A)p ⊢ _:(Path_((A)p)p contr-center(((c)p)p) x)})
8. contr-center(((c)p)p) ∈ {X.A.(A)p ⊢ _:((A)p)p}
⊢ contractible-to-prop(X;A;cA;c) ∈ {X ⊢ _:isProp(A)}
BY
{ (Unfolds ``is-prop`` 0 THEN ProveWfLemma THEN Using [`b',⌜contr-center(((c)p)p)⌝] MemCD⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  cA  :  X  +\mvdash{}  Compositon(A)
4.  c  :  \{X  \mvdash{}  \_:Contractible(A)\}
5.  ((c)p)p  \mmember{}  \{X.A.(A)p  \mvdash{}  \_:((Contractible(A))p)p\}
6.  \{X.A.(A)p  \mvdash{}  \_:((Contractible(A))p)p\}  =  \{X.A.(A)p  \mvdash{}  \_:Contractible(((A)p)p)\}
7.  \mforall{}[x:\{X.A.(A)p  \mvdash{}  \_:((A)p)p\}]
          (contr-path(((c)p)p;x)  \mmember{}  \{X.A.(A)p  \mvdash{}  \_:(Path\_((A)p)p  contr-center(((c)p)p)  x)\})
8.  contr-center(((c)p)p)  \mmember{}  \{X.A.(A)p  \mvdash{}  \_:((A)p)p\}
\mvdash{}  contractible-to-prop(X;A;cA;c)  \mmember{}  \{X  \mvdash{}  \_:isProp(A)\}


By

---

Latex:
(Unfolds  ``is-prop``  0  THEN  ProveWfLemma  THEN  Using  [`b',\mkleeneopen{}contr-center(((c)p)p)\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)

---

Home Index