How much do you know about type theory? If you know type theory then the gist of HoTT can be summarized as follows: HoTT is a dependent type theory where you

How much do you know about type theory? If you know type theory then the gist of HoTT can be summarized as follows: HoTT is a dependent type theory where you have a user defined equality for each user defined type (this is what HITs, higher inductive types, are). This is a generalization of quotient types and lets you do things like integers modulo k by defining that an integer n mod k == (n+k) mod k. It also has a better equality for functions (two functions are equal if they return the same result for each input), and types (two types are equal if there is a bijection between them).