Showing changes from revision #13 to #14: Added | Removed | Changed

Contents

Idea

Two morphisms in a category $C$ (or just edges in a directed graph) are parallel if they have the same source and target. Equivalently a pair of parallel morphisms in $C$ consists of an object $x$, and object $y$, and two morphisms $f, g: x \to y$.

This may be extended to a family of any number of morphisms, but the morphisms are always compared pairwise to see if they are parallel. Degenerate cases: a family of one parallel morphism is simply a morphism; a family of zero parallel morphisms is simply a pair of objects.

The walking parallel pair

The above considerations can be formalized in the following definition.

\begin{definition} The walking parallel pair category $P$ has two objects, 0 and 1, and two nonidentity arrows, $f,g\colon 0\to 1$. \end{definition}

Now functors $P\to C$ are precisely pairs of parallel morphisms.

Limits and colimits

The limit of a pair (or family) or morphisms is called their equalizer; the colimit is their coequalizer. (Of course, these do not always exist.)

Related concepts

• fork

• walking structure

  • walking pair of objectsthe boolean domain $2 \coloneqq \partial \Delta^1$; i.e. the walking pair of objects

  • walking morphismthe directed interval category $I \coloneqq \Delta^1$; i.e. the walking morphism

  • walking parallel pairthe (2,0)-horn category $\Lambda_0^2$; i.e. the walking cospan

  • walking commutative trianglethe (2,1)-horn category $\Lambda_1^2$; i.e. the walking composable pair

  • walking isomorphismthe (2,2)-horn category $\Lambda_2^2$; i.e. the walking span

  • walking equivalencethe 2-simplex category $\Delta^2$; i.e. the walking commutative triangle

  • the walking parallel pair

  • the walking isomorphism

  • Adj; i.e. the walking adjunction

  • the walking equivalence

  • the walking adjoint equivalence

  • the walking 2-isomorphism with trivial boundary

  • the syntactic category of a theory $T$; i.e. the walking $T$-model

• In dependent type theory, many higher inductive types can be considered to be walking structures:

  • the unit type is the walking element

  • the boolean type is the walking pair of elements

  • the interval type is the walking identification

  • one definition of the circle type is the walking self-identification

  • another definition of the circle type is the walking parallel pair of identifications.

  • the suspension type of a type $I$ is the walking parallel $I$-indexed family of identifications.

  • the natural numbers type is the walking sequence

  • the integers type is the walking bi-infinite sequence

  • the walking bridge

  • the directed interval type is the walking morphism in the sense of element of a hom type

shapes of free diagrams and the names of their limits/colimits

free diagram	limit/colimit
empty diagram	terminal object/initial object
discrete diagram	product/coproduct
parallel morphisms	equalizer/coequalizer
span/cospan	pullback,fiber product/pushout
tower/cotower	sequential limit/sequential colimit