François G. Dorais

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

Originally posted on June 23, 2013, 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 on January 10, 2016, at 12:06

  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 on January 10, 2016, at 17:12

  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.

  ---