# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMay 8th 2012
• (edited May 8th 2012)

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.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMay 9th 2012

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