---

Step * of Lemma contractible-to-prop_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[cA:X +⊢ Compositon(A)]. ∀[c:{X ⊢ _:Contractible(A)}].
  (contractible-to-prop(X;A;cA;c) ∈ {X ⊢ _:isProp(A)})
BY
{ (Intros
   THEN Unhide
   THEN ((Assert ((c)p)p ∈ {X.A.(A)p ⊢ _:((Contractible(A))p)p} BY
                Auto)
         THEN (Assert {X.A.(A)p ⊢ _:((Contractible(A))p)p} = {X.A.(A)p ⊢ _:Contractible(((A)p)p)} ∈ 𝕌{[i' | j']} BY
                     (EqCDA
                      THEN (InstLemmaIJ `csm-contractible-type` [⌜X⌝;⌜A⌝;⌜X.A⌝;⌜p⌝]⋅ THENA Auto)
                      THEN ApFunToHypEquands `Z' ⌜(Z)p⌝ {X.A.(A)p ⊢ _} (-1)⋅
                      THEN Auto
                      THEN InstLemmaIJ `csm-contractible-type` [⌜X.A⌝;⌜(A)p⌝;⌜X.A.(A)p⌝;⌜p⌝]⋅
                      THEN Auto))
         )
   THEN (InstLemmaIJ `contr-path_wf` [⌜X.A.(A)p⌝;⌜((A)p)p⌝;⌜((c)p)p⌝]⋅ THENA Auto)
   THEN (InstLemmaIJ `contr-center_wf` [⌜X.A.(A)p⌝;⌜((A)p)p⌝;⌜((c)p)p⌝]⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[cA:X  +\mvdash{}  Compositon(A)].  \mforall{}[c:\{X  \mvdash{}  \_:Contractible(A)\}].
    (contractible-to-prop(X;A;cA;c)  \mmember{}  \{X  \mvdash{}  \_:isProp(A)\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  ((Assert  ((c)p)p  \mmember{}  \{X.A.(A)p  \mvdash{}  \_:((Contractible(A))p)p\}  BY
                            Auto)
              THEN  (Assert  \{X.A.(A)p  \mvdash{}  \_:((Contractible(A))p)p\}  =  \{X.A.(A)p  \mvdash{}  \_:Contractible(((A)p)p)\}  BY
                                      (EqCDA
                                        THEN  (InstLemmaIJ  `csm-contractible-type`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}(Z)p\mkleeneclose{}  \{X.A.(A)p  \mvdash{}  \_\}  (-1)\mcdot{}
                                        THEN  Auto
                                        THEN  InstLemmaIJ  `csm-contractible-type`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}X.A.(A)p\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
                                        THEN  Auto))
              )
  THEN  (InstLemmaIJ  `contr-path\_wf`  [\mkleeneopen{}X.A.(A)p\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((c)p)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemmaIJ  `contr-center\_wf`  [\mkleeneopen{}X.A.(A)p\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((c)p)p\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index