Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
Excellent, thank you. I corrected some $\dashv$s to $\vdash$s.
added pointer to what I guess is the original document with the notion of contractible types:
and pointer to:
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!)
1 to 10 of 10