Spahn type category (changes)

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

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 X ⋉ A \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 $A Y$ 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{matrix} A Y ⋉ f^{*} A & \overset{f ⋉ A}{\to} & X ⋉ A \\ ↓^{p_{f^{*} A}} & ↓^{p_{a A}} \\ Y & \overset{f}{\to} X \end{matrix}

\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

Last revised on December 12, 2014 at 12:05:58. See the history of this page for a list of all contributions to it.