The Joys of a Whiteboard

I’m not going to attempt to explain much of what’s going on here, other than to say it’s a taste of things to come. I’ve spent a lot of time thinking about the duality between intuitionistic logic (IL) and co-intuitionistic logic (CIL) over the last few months, after Lucca Fraser got me hooked on it in Berlin a few years ago. I’ve also spent a lot of time thinking about its applicability to type theory, and this is the current state of my thinking regarding the relation between IL/CIL in the flavour of sequent calculus used in type theory and various logics in the flavour used in categorical model theory. There’s probably several embarrassing errors in here, but as with anything, it’s important to overcome the fear of embarrassment before you can do anything interesting!