HoTT Math Series

I am planning to do a series of posts where I attempt to do math in Homotopy Type Theory (HoTT). The plan is to do some relatively simple proof-relevant mathematics at an informal level. The topics will all be undergraduate level so the mathematics won’t be hard to follow. I’m hoping to keep the series brief so each post will only be an appetizer and not a full course dinner. Enjoy!

This preamble will serve to accumulate a table of contents and various conventions and notations that come up along the way. The only prerequisites (or rather corequisites) are the first two chapters of the (free) Homotopy Type Theory book. Further prerequisites and reverences to later topics in the book will always be indicated where they occur.


  1. Elementary group theory
  2. More on equational logic
  3. Unit group of a ring
  4. Local rings and fields
 

2 thoughts on “HoTT Math Series

  1. You refer to various conventions and notations as appearing in this preamble. BUT, I see no such conventions and notations here. What gives?

Leave a Reply

Your email address will not be published. Required fields are marked *