|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-proposition, mere proposition|
|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|
More specifically, the syntactic category of a type theory is naturally equipped with a class of maps called “display maps” which come from its type dependencies, while models for such a theory can be studied in any other category equipped with a suitable class of maps called “display maps.” By the usual adjunction, such models are then equivalent to functors out of the syntactic category which preserve the relevant structure, including the display maps.
Since the most common dependent type theories include dependent product types, and any display map in a category that represents semantics for such a theory must be exponentiable, the term display map is sometimes used to mean any exponentiable morphism.
The category with displays is called well rooted if it has a terminal object and all the morphisms to are display maps.
Often (which simplifies matters) is closed under composition:
which preserves display maps and their pullbacks.
This appears as (Taylor, def. 8.3.2).
Examples of categories with displays, def. 1, include
One extreme: any locally cartesian category with the class of all morphisms. (This is well rooted —if has a terminal object— and closed under composition.)
Another extreme: any category with the empty class of no morphisms.
Modifying (2) for an extreme case closed under composition: any category with the class of isomorphisms.
A category equipped with a singleton pretopology. (This is closed under composition.)
See also Taylor, example 8.3.6.
Section 8.3 in