Homotopy Type Theory is an exciting and relatively new area of mathematics. The main resource for learning it is a Free/Open Source book with the same name: Homotopy Type Theory: Univalent Foundations of Mathematics. I’m currently reading it and I decided to publish notes that I’m taking from it. For each chapter of the original book we have a corresponding chapter with the same name containing a cheat sheet of theorems of that chapter and some extra notes.
So be prepared for lots of mathematical or grammatical mistakes. However, this is a free book, so you can help me make it better. See the How to Contribute section.
So always check that you have the latest release.
This is a libre/open source project. It is hosted on GitLab and any contribution is welcomed and highly appreciated.
[TODO] Add detailed information on how to commit to a git repository for beginners.
This book and most of its latex macros is based on the Homotopy Type Theory: Univalent Foundations of Mathematics book.
The PDF, web pages and e-books are produced with scripts around pandoc and other free software. see the GitLab page.
Except As Otherwise Noted, This Work Is Licensed Under A Creative Commons Attribution-ShareAlike 4.0 International License. To View A Copy Of This License, Visit: https://creativecommons.org/licenses/by-sa/4.0/
Code Samples Are Licensed Under The GNU General Public License v3.0. To View A Copy Of This License, Visit: https://www.gnu.org/licenses/gpl-3.0.en.html
Except As Otherwise Noted, The Content Of This Page Is Licensed Under The CC-BY-SA 4.0 License And Code Samples Are Licensed Under The GPL 3.0 License. For Details, See License.