---

Step * 1 of Lemma contractible-iff-inhabited-prop


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. {X ⊢ _:isProp(A)} ⇒ {X ⊢ _:A} ⇒ {X ⊢ _:Contractible(A)}
4. cA : X +⊢ Compositon(A)
5. c : {X ⊢ _:Contractible(A)}
⊢ {X ⊢ _:isProp(A)}
BY
{ (UseWitness ⌜contractible-to-prop(X;A;cA;c)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  \{X  \mvdash{}  \_:isProp(A)\}  {}\mRightarrow{}  \{X  \mvdash{}  \_:A\}  {}\mRightarrow{}  \{X  \mvdash{}  \_:Contractible(A)\}
4.  cA  :  X  +\mvdash{}  Compositon(A)
5.  c  :  \{X  \mvdash{}  \_:Contractible(A)\}
\mvdash{}  \{X  \mvdash{}  \_:isProp(A)\}


By

---

Latex:
(UseWitness  \mkleeneopen{}contractible-to-prop(X;A;cA;c)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index