Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
category object in an (∞,1)-category, groupoid object
(directed enhancement of homotopy type theory with types behaving like -categories)
In category theory, a composable pair of morphisms in a given category consists of objects of and a pair of morphisms and . The composite of this composable pair is the morphism .
A composable pair in is precisely a 2-simplex in the nerve of .
Sometimes one defines a composable pair to be a literal pair such that the target of is equal to the source of , but this violates the principle of equivalence.
The walking composable pair or (2,1)-horn category is the category which consists of three objects and two morphisms and .
The category is also called the (2,1)-horn preorder or the (2,1)-horn poset because can be shown to be a poset.
Every composable pair in a category is represented by a functor from the walking composable pair to . By definition of a category, we have an equivalence of categories between the functor category of composable pairs in and the functor category of commutative triangles in .
In dependent type theory, given a directed interval , the (2,1)-horn type representing the walking composable pair is defined as the type of pairs of elements such that or .
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, not every composable pair of morphisms has a unique composite forming a commutative triangle, so one has to distinguish between the notions.
Let be a type, and let be the directed interval in simplicial type theory. Recall that the hom-type is defined as
A composable pair of morphisms is a record consisting of
elements , , and
a morphism
and a morphism .
The type of composable pairs of morphisms is then the respective record type.
There is another definition involving the -horn type , defined from the directed interval as
A composable pair of morphisms is simply a function .
The type of composable pairs of morphisms is then the function type .
the boolean domain ; i.e. the walking pair of objects
the directed interval category ; i.e. the walking morphism
the (2,0)-horn category ; i.e. the walking cospan
the (2,1)-horn category ; i.e. the walking composable pair
the (2,2)-horn category ; i.e. the walking span
the 2-simplex category ; i.e. the walking commutative triangle
Adj; i.e. the walking adjunction
the syntactic category of a theory ; i.e. the walking -model
Emily Riehl, Mike Shulman, A type theory for synthetic ∞-categories, Higher Structures 1 1 (2017) [arxiv:1705.07442, published article]
Emily Riehl, Could -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)
Last revised on June 1, 2025 at 03:45:16. See the history of this page for a list of all contributions to it.