---

Step * of Lemma is-prop-contractible

No Annotations
∀X:j⊢. ∀A:{X ⊢ _}.  ({X ⊢ _:isProp(A)} ⇒ {X ⊢ _:A} ⇒ {X ⊢ _:Contractible(A)})
BY
{ (Intros THEN All (Unfolds ``is-prop contractible-type``) THEN FLemma `cubical-pi-implies-sigma` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.    (\{X  \mvdash{}  \_:isProp(A)\}  {}\mRightarrow{}  \{X  \mvdash{}  \_:A\}  {}\mRightarrow{}  \{X  \mvdash{}  \_:Contractible(A)\})


By

---

Latex:
(Intros
  THEN  All  (Unfolds  ``is-prop  contractible-type``)
  THEN  FLemma  `cubical-pi-implies-sigma`  [-1;-2]
  THEN  Auto)

---

Home Index