The other talk was Christoph Benzmüller selling us on his higher-order theorem prover Leo II, which sounds pretty awesome. It pulls a bunch of tricks to reduce theorem proving problems in HOL to bits and pieces it feeds to first-order provers, and then digests the results, and then feeds back into the first-order provers, and so on. I have a meeting with him and Frank tomorrow morning to see if I can get it to do linear logic proving by pulling the same encoding tricks I did with HLF. It sounds like he already got some cool results with Deepak's authorization logic already.

I've found myself thinking recently about something

**neelk**mentioned, which is that we lambda-calculus people really ought to "already" understand something of the 2-categorical structure of adjunctions (for example between - x A and A ⇒ -) because we know that you should privilege β-

**reduction**and η-

**expansion**, this being a finer-grained notion than just adjunction, which says by dint of uniqueness of adjoint transposes that you just get

**equality**of terms that are connected βη-convertibility in any direction and indeed any zigzagging path you like.

Poking at the literature a bit, it seems the right word to look for is "biadjoint" (or occasionally "pseudoadjoint"?) but it seems that if you are smart enough to confidently talk about what biadjoints are in a published paper, you are smart enough to make everything else in your paper impenetrably advanced, so I haven't made a lot of progress understanding them.

---

ETA: But I did make this model in Sketchup, which I think is the analogue of the adjoint triangle equalities one dimension up: