Displayed category theory MOC

Displayed category

A displayed category over a category consists of¹ #m/def/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
• composition and identities are induced from those of and in the straightforward way, and similarly for the axioms.

This is naturally equipped with a forgetful functor

#state/develop | #lang/en | #SemBr