“What are we thinking when we present a type theory?” by Peter LeFanu Lumsdaine: youtube.com/watch?v=kQe0kn
I found the clarification of some of the hidden rules you have in your head when reading type theories really interesting and worthwhile!
Conversation
Also found the observation that the order in which the rules for dependent pairs and dependent functions are defined shouldn't really matter (44:56) interesting too. Links in with some of the graph/module stuff I've been pondering recently…