type category


A type category is defined to be a category satisfying the following conditions:

(1) For each object XCX\in C there is a collection Type C(X)Type_C(X) whose elements are called XX-indexed types in CC.

(2) For each object XCX\in C operations assigning to each XX-indexed type AA an object XAX \ltimes A called the total object of AA, together with a morphism

p A:XAXp_A:X \ltimes A \to X

called the projection morphism of AA.

(3) For each morphism f:YXf:Y\to X in CC, an operation assigning to each XX-indexed type AA, a YY indexed type f *Af^* A called the pullback of AA along XX, together with a morphism fA:Yf *AXAf\ltimes A:Y\ltimes f^* A\to X\ltimes A making the following a pullback square in the category CC.

Yf *A fA XA p f *A p A Y fX\array{ Y\ltimes f^* A&\stackrel{f\ltimes A}{\to}&X\ltimes A \\ \downarrow^{p_{f^* A}}&&\downarrow^{p_A} \\ Y&\stackrel{f}{\to} X }

In addition the following strictness conditions will be imposed

id X *A=Aid^*_X A=A
id XA=id XAid_X\ltimes A=id_{X\ltimes A}
g *(f *A)=(fg) *Ag^*(f^* A)=(f\circ g)^* A
(fA)(gf *A)=(fg)A(f\ltimes A)\circ (g\ltimes f^* A)=(f\circ g)\ltimes A


  • Pitts, Andrew M. Categorical logic. Handbook of logic in computer science, Vol. 5, 39–128, Handb. Log. Comput. Sci., 5, Oxford Univ. Press, New York, 2000. pdf, chapter 6.3

Last revised on December 12, 2014 at 12:05:58. See the history of this page for a list of all contributions to it.