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
P	—	Fibration	Hyperdoctrine
f*	—	Reindex	Substitution
∃_f	—	Left adjoint	Existential
∀_f	—	Right adjoint	Universal
⊣	U+22A3	Adjoint	Adjunction

Metatheory. Sound and complete for predicate logic. Generalizes to dependent types. Internal language. Doctrinal approach.

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

Limitations. Abstract framework. Category theory required. Strictness issues. Specialized audience.