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