Some research themes that make me tick, a quick and incomplete thread:
Conversation
In type theory, there's always a choice whether to make something internal or external. When we take something and make it internal to a type theory---like univalence---we usually learn a lot about it and refine it. I like to take those internal things and pull them back out.
2
6
Lots of type theorists like developing the type theory but then don't like building automation and tooling. I like to take the gunk the type theorists don't like to do and build awesome automation and tooling around beautiful type theory, like ornaments and transport.
2
11
