Spahn type category (Rev #1)

Definition

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:A\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 $A$ 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{ A\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

Reference

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

Revision on December 25, 2012 at 06:36:09 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.