# Spahn type category (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

###### 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 p_A:X A\to \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 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{ A\ltimes Y\ltimes f^* A&\stackrel{f\ltimes A}{\to}&X\ltimes A \\ \downarrow^{p_{f^* A}}&&\downarrow^{p_a} 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 12, 2014 at 12:05:58 by kirelagin. See the history of this page for a list of all contributions to it.