Spahn type category

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: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

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