A couple of entries are requesting a link for “singleton contractibility”

(e.g. *function extensionality*, *identity type* and *higher observational type theory*).

It seems weird to leave such a basic notion undefined in these entries. Since I am assuming that it is meant to point to the notion of *singleton induction* discussed in this entry here, I have now made “singleton contractibility” redirect to here.

(If it should go elsewhere, remove the redirect and create the necessary entry!)

]]>meant uniqueness quantifier instead of universal quantifier

Anonymous

]]>adding link to universal quantifier

Anonymous

]]>and pointer to:

- Univalent Foundations Project, §3.11 in:
*Homotopy Type Theory – Univalent Foundations of Mathematics*(2013) [web, pdf]

added pointer to what I guess is the original document with the notion of contractible types:

- Vladimir Voevodsky, p. 8. 10 of:
*Univalent Foundations Project*(2010) [pdf]

adding natural deduction syntax rules for isContr

Anonymous

]]>added third definition of contractible type, and replaced depreciated Markdown notation for definitions/theorems/propositions/proofs with LaTeX notation.

Anonymous

]]>adding examples of contractible types

Anonymous

]]>Excellent, thank you. I corrected some $\dashv$s to $\vdash$s.

]]>I have worked a bit on *contractible type*. Apart from beautifying it a bit (or so I hope I did) I have added in the section *Categorical semantics* a fair bit of pedestrian detail on how to see that a term of $isContr(A)$ is indeed a contraction right homotopy, and vice versa.