Curry’s correspondence between propositions and types was extended to predicate logic in the late 1960s by Howard (1980) and de Bruijn (1970). At around the same time Lawvere developed related ideas in categorical logic. In particular he proposed the notion of a hyperdoctrine (Lawvere 1970) as a categorical model of (typed) predicate logic. A hyperdoctrine is an indexed category \(P {:} T^{op} \rightarrow \mathbf{Cat}\), where \(T\) is a category where the objects represent types and the arrows represent terms. If \(A\) is a type then the fibre \(P(A)\) is a category of propositions depending on a variable \(x {:} A\). The arrows in this category are proofs \(Q \vdash R\) and can be thought of as proof-objects. Moreover, since we have an indexed category, for each arrow \(t\) from \(A\) to \(B\), there is a reindexing functor \(P(B) \rightarrow P(A)\) representing substitution of \(t\) for a variable \(y {:} B\). The category \(P(A)\) is assumed to be cartesian closed and conjunction and implications are modelled by products and exponentials in this category. The quantifiers \(\exists\) and \(\forall\) are modelled by the left and right adjoints of the reindexing functor. Moreover, Lawvere added further structure to hyperdoctrines to model identity propositions (as left adjoints to a diagonal functor) and a comprehension schema.