A new blog
Posted by Mike Shulman
Readers may have noticed that I haven’t been very active here for a while. That isn’t because I haven’t felt the “blogging urge”, but because I felt that the things I want to blog about right now wouldn’t be very interesting to much of the n-Category Cafe audience: they’re mostly fairly technical details about implementing proof assistants (because that’s what I’m mostly working on right now).
Accordingly, I’ve started a new blog! It’s at https://gwaithimirdain.github.io/blog/. (Gwaith-i-Mírdain is the github organization for development of Narya, the experimental proof assistant for Higher Observational Type Theory – and now Multimodal Type Theory as well – that I’ve been spending most of my time on, and will primarily be blogging about.) And I already wrote three posts (mostly about implementing multimodal type theory, with several survey questions for the reader), so you can check it out right now and see whether it’s likely to be your cup of tea.
Never fear, I’ll still come back here when I have more category-theoretic things to write about.
Posted at June 2, 2026 7:34 PM UTC
Re: A new blog
Is Gwaith-i-Mírdain a name from Tolkien?
(Sorry for such an irrelevant comment, but I can’t help wondering.)
A lot of my blogging urges don’t seem to fit into the n-Cafe either. Sometimes I decide to try anyway—but my latest post, which was on analysis, garnered no comments, so I decided it wasn’t worthwhile.