Honestly this paper is really good. Super accessible for a DTT paper, clear and entertaining writing. No idea how I missed it until now
Conversation
looks like you were on this paper
1
2
is the proof assistant available to play with?
1
2
Did all three of the authors write together? It is some of the best writing I've read in type theory
1
1
While all three of us wrote together, I think deserves a large measure of the credit for the clarity :)
6