nLab composable pair

Definition

In category theory, a composable pair of morphisms in a given category $C$ consists of objects $X,Y,Z$ of $C$ and a pair of morphisms $f\colon X \to Y$ and $g\colon Y \to Z$. The composite of this composable pair is the morphism $g \circ f\colon X \to Z$.

A composable pair in $C$ is precisely a 2-simplex in the nerve of $C$.

Sometimes one defines a composable pair to be a literal pair $(f,g)$ such that the target of $f$ is equal to the source of $g$, but this violates the principle of equivalence.

The walking composable pair

The walking composable pair or (2,1)-horn category is the category $\Lambda_1^2$ which consists of three objects $0, 1, 2 \in \Lambda_1^2$ and two morphisms $h_{01}:\mathrm{hom}_{\Lambda_1^2}(0, 1)$ and $h_{12}:\mathrm{hom}_{\Lambda_1^2}(1, 2)$.

The category $\Lambda_1^2$ is also called the (2,1)-horn preorder or the (2,1)-horn poset because $\Lambda_1^2$ can be shown to be a poset.

Every composable pair in a category $C$ is represented by a functor $F:\Lambda_1^2 \to C$ from the walking composable pair to $C$. By definition of a category, we have an equivalence of categories between the functor category $C^\Lambda_1^2$ of composable pairs in $C$ and the functor category $C^\Delta^2$ of commutative triangles in $C$.

In dependent type theory, given a directed interval $\mathbb{I}$, the (2,1)-horn type representing the walking composable pair is defined as the type of pairs of elements $i, j:\mathbb{I}$ such that $i = 1$ or $j = 0$.

$$\Lambda_1^2 \coloneqq \sum_{i:\mathbb{I}} \sum_{j:\mathbb{I}} (i = 1) \vee (j = 0)$$

Unlike the case for the other horns representing the walking span and the walking cospan, the walking composable pair is only a category if there is an axiom stating that every type is a Segal type.

In simplicial type theory

In simplicial type theory, not every composable pair of morphisms has a unique composite forming a commutative triangle, so one has to distinguish between the notions.

Let $A$ be a type, and let $\mathbb{I}$ be the directed interval in simplicial type theory. Recall that the hom-type is defined as

$$\mathrm{hom}_A(x, y) \coloneqq \sum_{f:\mathbb{I} \to A} (f(0) = x) \times (f(1) = y)$$

A composable pair of morphisms is a record consisting of

• elements $x:A$, $y:A$, and $z:A$

• a morphism $f:\mathrm{hom}_A(x, y)$

• and a morphism $g:\mathrm{hom}_A(y, z)$.

The type of composable pairs of morphisms is then the respective record type.

There is another definition involving the $(2,1)$-horn type $\Lambda^2_1$, defined from the directed interval as

$$\Lambda^2_1 \coloneqq \sum_{i:\mathbb{I}} \sum_{j:\mathbb{I}} (i = 0) \vee (j = 1)$$

A composable pair of morphisms is simply a function $f:\Lambda^2_1 \to A$.

The type of composable pairs of morphisms is then the function type $\Lambda^2_1 \to A$.

Related concepts

• horn

• hom set, hom type

• composite

• commutative triangle

• unique composite

• span, cospan

• Segal type

• walking structure

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

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

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

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

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

  • the 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

References

• Emily Riehl, Mike Shulman, A type theory for synthetic ∞-categories, Higher Structures 1 1 (2017) [arxiv:1705.07442, published article]

• Emily Riehl, Could $\infty$-category theory be taught to undergraduates?, Notices of the AMS (May 2023) [published pdf, arxiv:2302.07855]

• Denis-Charles Cisinski, Bastiaan Cnossen, Hoang Kim Nguyen, Tashi Walde, section 1.6 of: Formalization of Higher Categories, work in progress (pdf)