Yoneda

[emilyriehl]

Here are updates which reflect the current state of the Yoneda repository.

Most significantly:

• new HoTT proofs on contractibility of based path spaces, equivalences between contractible types, contractible maps and equivalences, and families of equivalences, with supporting path algebra etc; these files are now in md format

• an application to homotopies in Segal types

The organization of the HoTT files is suboptimal as is the naming of defined terms. Suggestions are very welcome.

[fizruk]

This is great, thanks! I have some ideas regarding the file structure and naming, but this looks good for now.