|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
(where is the subcategory of the category of Heyting algebras containing only those morphisms with left and right adjoints) such that the following Beck-Chevalley condition is satisfied: for every object , the left adjoints to for the projections comprise a natural transformation from to , and so do the right adjoints. This expresses the Beck-Chevalley condition for pullback squares of the form
An element of is often called a predicate over (with respect to the hyperdoctrine).
For any first-order hyperdoctrine, an equality predicate can be defined for each type as
where for any morphism in , we use to denote the left adjoint of , and denotes the top element in a Heyting algebra . However, to get good properties for equality, we need to assume a little more. A first-order hyperdoctrine with equality is a first-order hyperdoctrine such that the Beck-Chevalley condition is also satisfied for pullback diagrams of the form
This says ; this equation is also known as a Frobenius law. By taking right adjoints, a similar equation holds for in place of , where .
With this, we have enough structure to interpret multi-sorted first-order intuitionistic logic with equality, taking the objects of to be sorts and its morphisms to be terms, to assign to each sort the Lindenbaum algebra? of predicates upon that sort and to each term the operation of substitution of that term into predicates, and the left and right adjoints to upon projections to provide existential and universal quantification, respectively, with the existence of the further adjoints providing the ability to interpret equality, and the Beck-Chevalley condition ensuring that quantification commutes appropriately with substitution (just as the propositional connectives do).
There are, of course, many variants on this, corresponding straightforwardly to modifications of the kind of logic one wishes to represent. For instance, to represent specifically classical logic, one should use Boolean algebras instead of Heyting algebras. To represent first-order logic without equality, one should no longer require left and right adjoints to every morphism in the range of , but rather only those given by the natural transformations yielding the quantifiers (i.e., only requiring adjoints to substitution along projections). Various higher-order constructs can be added by adding new ways of forming objects in (e.g., adding cartesian closedness). Etc.
One can even extend this into the realm not just of provability, but furthermore of proof theory, by taking the objects in the codomain of to be categories rather than mere preorders (e.g., by using bicartesian closed categories rather than Heyting algebras); in this case, the objects in a category would still represent predicates on the sort , but the morphisms in would represent proofs (rather than mere provability) of entailments between these predicates, with the possibility that not all such proofs would be equal.