- A hyperdoctrine equips a category with some kind of logic
- It's a functor
P: T^op -> C for some higher category
C, whose objects are categories whose internal logic corresponds to
- 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
- 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).