Hyperdoctrines

Origin. Lawvere (1969), who called the general pattern a doctrine. Categorical semantics for predicate logic. Indexed categories for substitution. Adjoints for quantifiers. Foundation for categorical logic.

Models. Base category of contexts. Fibers: propositions/types over context. Substitution: reindexing functors. Quantifiers: adjoints to substitution.

Formalism.

Hyperdoctrine: Functor P: C^op → Cat C: base category (contexts) P(Γ): fiber category (propositions/types over Γ)

Reindexing: f: Δ → Γ in C gives f*: P(Γ) → P(Δ) Substitution functor.

Beck-Chevalley: For pullback squares, reindexing commutes with quantifiers.

Existential quantifier: ∃_f: P(Δ) → P(Γ) left adjoint to f* ∃_f ⊣ f*

Universal quantifier: ∀_f: P(Δ) → P(Γ) right adjoint to f* f* ⊣ ∀_f

Frobenius reciprocity: ∃_f(A ∧ f*B) ≅ ∃_f(A) ∧ B Quantifier distributes.

First-order hyperdoctrine: Fibers are Heyting algebras. Quantifiers are adjoints. Equality via diagonal.

Higher-order: Fibers are CCCs. Power objects for higher-order quantification. Elementary toposes as the higher doctrine.

Examples: Subsets: P(X) = Sub(X) Predicates: P(Γ) = [Γ, Ω] Realizability: P(Γ) = assemblies

Symbols.

Symbol	Unicode	Name	Meaning
⊣	U+22A3	Adjoint	∃_f ⊣ f* ⊣ ∀_f, the quantifiers as adjoints
∃	U+2203	Exists	Left adjoint to substitution
∀	U+2200	For all	Right adjoint to substitution
∧	U+2227	Conjunction	Meet in the fibre; the ∧ of Frobenius reciprocity
≅	U+2245	Isomorphism	The Frobenius isomorphism in the fibre
→	U+2192	Arrow	A morphism of contexts, or a functor
Γ	U+0393	Gamma	A context, an object of the base category
Δ	U+0394	Delta	A second context, source of a substitution
Ω	U+03A9	Subobject classifier	Predicates as maps into it, P(Γ) = [Γ, Ω]
P	—	Hyperdoctrine	The indexed category C^op → Cat
C	—	Base category	Contexts and substitutions
Cat	—	Category of categories	Target of the indexing functor
^op	—	Opposite	Contravariance of substitution
f*	—	Reindexing	Substitution functor P(Γ) → P(Δ)
∃_f	—	Left adjoint	Existential quantification along f
∀_f	—	Right adjoint	Universal quantification along f
Sub(X)	—	Subobject lattice	The canonical example of a fibre

Metatheory. Lawvere's "Adjointness in Foundations" (1969) and "Equality in Hyperdoctrines and the Comprehension Schema as an Adjoint Functor" (1970) established the identifications the subject rests on: existential and universal quantification are the left and right adjoints to substitution, equality is the left adjoint to reindexing along the diagonal, and comprehension is itself an adjoint. Intuitionistic first-order logic is sound and complete for first-order hyperdoctrines, the syntactic hyperdoctrine of a theory — contexts as base, provable-entailment preorders of formulas as fibres — furnishing the generic model, so completeness is a Lindenbaum–Tarski construction carried out fibrewise. The two side conditions are not decorative: Beck–Chevalley is exactly the commutation of quantifiers with substitution, and Frobenius reciprocity exactly the interaction of ∃ with ∧, and each is needed for soundness of the corresponding rule. In a topos the subobject hyperdoctrine satisfies both automatically. The tripos-to-topos construction of Hyland, Johnstone and Pitts (1980) shows a hyperdoctrine over Set with a generic predicate generates a topos; the effective topos arises this way from the realizability tripos.

Applies to. Categorical logic. Type theory semantics. Topos theory. Proof theory. Algebraic logic.

Limitations. Posetal fibres record provability and discard proofs: two derivations of the same sequent are identified, so no proof-theoretic content survives, and recovering it requires genuinely Cat-valued fibres, at which point the coherence problems of pseudofunctoriality appear. Beck–Chevalley and Frobenius reciprocity have to be imposed as axioms — they do not follow from the adjunctions — and dropping either makes the interpretation unsound for the quantifier rules. The definition asks for a strict functor C^op → Cat, but the motivating examples, Sub(X) among them, are only pseudofunctorial, so a splitting must be chosen. A hyperdoctrine has no context extension: fibres sit over contexts without types over contexts feeding back into the base, which is why dependent type theory needs comprehension categories instead. Classical logic requires Boolean fibres as a further assumption, and the tripos-to-topos construction is not an equivalence.