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 proofrelevant 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.
Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.
Comments

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

François G. Dorais replied to Bob Solovay
You’re right. I don’t think the need to assemble notations and conventions here ever occurred. So this is just a placeholder that never got used.