I used this and previous years for the logic side of things. He doesn't even mention categories, iirc. But the logic to type theory elaboration is taking a preorder\\({}^{\ast}\\) to a category\\(^{\ast\ast}\\).

\\({}^{\ast}\\) very much preorders and not posets, isomorphic objects are all over the place. In fact I think linear logic might be an equivalence relation. But sub singleton logic can't be so.. Hmm. Need to reread.

\\(^{\ast\ast}\\) Somewhat strange categories. They are for sure not "Set like" in the usual sense, that's the whole point. As the internal language of those is a normal lambda calculus. For example, in linear logic there are two pairs of meet / join, and each meet distributes with the join that's not it's dual.