§ Hyperdoctrine

• A hyperdoctrine equips a category with some kind of logic L.
• It's a functor P: T^op -> C for some higher category C, whose objects are categories whose internal logic corresponds to L.
• In the classical case, L is propositional logic, and C is the 2-category of posets. We send A ∈ T to the poset of subobjects Sub_T(A).
• We ask that for every morphism f: A -> B, the morphism P(f) has left and right adjoints.
• These left and right adjoints mimic existential / universal quantifiers.
• If we have maps between cartesian closed categories, then the functor f* obeys frobenius reciprocity if it preserves exponentials: f*(a^b) ~iso~ f*(a)^f*(b).
• https://ncatlab.org/nlab/show/Mitchell-B%C3%A9nabou+language