Hi @Matthew, in [#57](https://forum.azimuthproject.org/discussion/comment/17071/#Comment_17071) you translate "right adjoints preserve meets" as if saying "preserve the meet operation", but Proposition 1.84 goes beyond, saying that they preserve even the meet of an arbitrary set of elements (not just two). That code starts to take shape, wish I knew some Haskell.