## § 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