Displayed category theory MOC

Displayed category

A displayed category over a category consists of[^2017] cat

• for each object , a collection of objects over ;
• for each morphism , and , a set of morphisms from to over , denoted or ;
• for each object and , a morphism ;
• for all morphisms and and objects , , and , a composition function

where these data satisfy

• and for any ;
• for appropriately typed .

In the quintessential examples, we think of an object over as a structure on , and a morphism as a witness that is structure-preserving. Thus displayed categories are naturally used in a paradigm with propositions as types. This motivates the total category as the category of structures and structure morphisms, defined as follows:

• an object is a pair consisting of an object and an object over , so that
• a morphism is a pair where and , so that

\left( \int {\cat C} \cat D \right)((a,x),(b,y)) = \sum{f \in \cat C(a,b)} \cat D_{f}(x,y)

\begin{align*} \pi_{1}^{\cat D} : \int_{\cat C} \cat D \to \cat C. \end{align*}