nLab display map



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels






In type theory, a display map [Taylor 1983-7, §4.3.2] is a morphism p:BAp\colon B\to A in a category which represents a dependent type under categorical semantics of dependent type theory.

That is, BB represents (interprets) a type dependent on a variable of type AA, usually written syntactically as x:AB(x):Typex\colon A \vdash B(x)\colon Type. The intended intuition is that B(x)B(x) is the fiber of the map pp over x:Ax\colon A.

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.

Sometimes all maps are display maps. This happens particularly in extensional type theory, such as versions of the internal logic of categories that include dependent types.

In the context of homotopy type theory display maps are fibrations, for instance in a type-theoretic model category.



For 𝒞\mathcal{C} a category, a class DMor(𝒞)D \subset Mor(\mathcal{C}) of morphisms of 𝒞\mathcal{C} is called a class of displays if

  • All pullbacks of elements of DD exist and belong to DD.

It follows automatically that the full subcategory on DD of the arrow category Arr(𝒞)\Arr(\mathcal{C}) is replete; in other words, the property of 𝒞\mathcal{C}-morphisms given by membership in DD respects the principle of equivalence.


The category with displays is called well rooted if it has a terminal object 11 and all the morphisms to 11 are display maps.

It follows that binary products exist and their projections are display maps.


Often (which simplifies matters) DD is closed under composition:

  1. Every identity morphism (and hence every isomorphism) belongs to DD.

  2. The composite of a composable pair of elements of DD belongs to DD.


An interpretation or model of a category with class of displays (𝒞,D)(\mathcal{C}, D) in another category with displays (𝒞,D)(\mathcal{C}', D') is a functor

S:𝒞𝒞 S\colon \mathcal{C} \to \mathcal{C}'

which preserves display maps and their pullbacks.

This appears as (Taylor 1999, def. 8.3.2).



Examples of categories with displays, def. , include

  1. One extreme: any locally cartesian category 𝒞\mathcal{C} with the class of all morphisms. (This is well rooted —if 𝒞\mathcal{C} has a terminal object— and closed under composition.)

  2. Another extreme: any category with the empty class of no morphisms.

  3. Modifying (2) for an extreme case closed under composition: any category with the class of isomorphisms.

  4. Modifying (2) for an extreme well-rooted case: A category 𝒞\mathcal{C} with finite products and DD the class of product projections X×AXX \times A \to X. (This is also closed under composition.)

  5. A locally cartesian category 𝒞\mathcal{C} (such as a topos) equipped with its class of monomorphisms. (This is closed under composition.)

  6. A category equipped with a singleton pretopology. (This is closed under composition.)

  7. (…)

See also Taylor 1999, Exp. 8.3.6.


The notion is due to

Last revised on October 2, 2023 at 15:08:44. See the history of this page for a list of all contributions to it.