It's been a wee while

What's been happening? Foremost, I've started working towards a PhD at Strathclyde University, supervised by Conor McBride.

At the moment I am fully formalising the Simply Typed Lambda Calculus with bidirectional type checking. I've also been trying to improve the LaTeX backend for Agda, and to make writing Literate Agda papers nicer with some simple but useful Emacs functions