Let $\mathbb{A}$ be a category.

The arrow double category $\overrightarrow{\mathbb{A}}$ is as follows: the base category is $\mathbb{A}$; a relation is a morphism of $\mathbb{A}$, and an inference is a commutative square.

We denote (vertical) processes by $\mathrm{a}$, and (horizontal) relations by $\hat{\mathrm{a}}$.

$\mathrm{(a_0a_1): \overrightarrow{\mathbb{A}} (\hat{a}^1_0, \hat{a}^1_1})$

Horizontal composition is that of squares, and horizontal units are identities.

By forming a double category, $\mathbb{A\leftarrow \overrightarrow{A}\to A}$ can act on span categories. If an object of $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ is to be a relation from an $\mathbb{A}$-type to a $\mathbb{B}$-type, then such relations should vary over processes of $\mathbb{A}$ and $\mathbb{B}$ — this is a module of arrow double categories.

A fibered category over $\mathbb{A}$ is a span category $\mathbb{A}\leftarrow \mathcal{R}\to 1$ which forms a left module of the arrow double category $\overrightarrow{\mathbb{A}}$. The action is a span functor $\odot:\mathbb{\overrightarrow{A}}\ast \mathcal{R}\to \mathcal{R}$, and coherent isomorphisms for associativity and unitality. The action, called substitution, is a matrix of functors

$$ \hat{\mathrm{a}}\odot R: \overrightarrow{\mathbb{A}}(\mathrm{A_0,A_1})\ast \mathcal{R}(\mathrm{A_1})\to \mathcal{R}(\mathrm{A_0}) $$

which is contravariant in $\mathrm{A}$. It is also known as “pullback”, and often denoted by $\mathrm{a}^\ast R$.

In string diagrams, with category 1 as white space,

the action is drawn as follows.

$\hat{\mathrm{a}}\odot R: \overrightarrow{\mathbb{A}}\ast \mathcal{R}\to \mathcal{R}$

This is an indexed category with “pull-back”.

Dually, we have the notion of indexed category with push-forward.