A Generalized Algebraic Theory of Directed Equality

"See below for a desciption of the contents of the thesis, at four different levels of assumed background knowledge: 'Basic' (no assumed familiarity with type theory and category theory), 'Intermediate' (some familiarity), 'Advanced' (significant assumed familiarity), and 'Expert'."

This is a brilliant idea and very well executed. I almost did not click the link because I would put myself into the 'Intermediate' (some familiarity) bucket and most blog posts are either too basic or too advanced for me. Glad I clicked.