type category (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

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}:\mathrm{AX}\u22c9A\to X$$~~ 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 $\mathrm{AY}$~~ 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$.

$$\begin{array}{ccc}\mathrm{AY}\u22c9{f}^{*}A& \stackrel{f\u22c9A}{\to}& X\u22c9A\\ {\downarrow}^{{p}_{{f}^{*}A}}& & {\downarrow}^{{p}_{\mathrm{aA}}}\\ Y& \stackrel{f}{\to}X\end{array}$$ \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$

- 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