I have recently been deeply involved in homotopy type theory. I am also interested in (higher) category theory and its applications to the rest of mathematics, particularly homotopy theory. I also tend to be a partisan of higher-categorical structures other than -categories (such as double categories, multicategories, proarrow equipments, F-categories, and so on), which sometimes seem to get neglected.
For my own reference: some pages that I was once planning to do some work on: * theory * lax 2-adjunction * structured (infinity,1)-topos and classifying topos * generalized multicategory, virtual double category, virtual equipment * functoriality of codiscrete cofibrations, * create a separate page two-sided fibration, also work on fibration in a 2-category * categories over computads at monadicity theorem. * copy some stuff over from my personal web * write descent object
And here’s how to make a barred arrow , since I always forget:
And here’s the esh (see here):