Guides In this part of the wiki, you will find everything you need to write good code. List of relevant reading about Univalent mathematics / HoTT / topics related to the library Nlab Dan Grayson's introduction to univalent foundations? The HoTT book The paper about Displayed Categories