type category

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

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

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

$p_A:X \ltimes A \to X$

called the *projection morphism* of $A$.

(3) For each morphism $f:Y\to X$ in $C$, an operation assigning to each $X$-indexed type $A$, a $Y$ indexed type $f^* A$ called the pullback of $A$ along $X$, together with a morphism $f\ltimes A:Y\ltimes f^* A\to X\ltimes A$ making the following a pullback square in the category $C$.

$\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=A$

$id_X\ltimes A=id_{X\ltimes A}$

$g^*(f^* A)=(f\circ g)^* 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.