+-- {: .num_defn} ###### 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](www.cl.cam.ac.uk/techreports/UCAM-CL-TR-367.ps.gz), chapter 6.3