nLab walking commutative triangle

Definition

Definition

The walking commutative triangle or triangle category or 2-simplex category is the category $\Delta^2$ which consists of three objects $0, 1, 2 \in \Delta^2$ and three morphisms $h_{01}:\mathrm{hom}_{\Delta^2}(0, 1)$, $h_{02}:\mathrm{hom}_{\Delta^2}(0, 2)$, $h_{12}:\mathrm{hom}_{\Delta^2}(1, 2)$, such that $h_{02} = h_{12} \circ h_{01}$.

$\Delta^2$ is also called the 2-simplex poset or triangle poset because $\Delta^2$ is a thin category and thus a poset.

Every commutative triangle in a category $C$ is represented by a functor $F:\Delta^2 \to C$ from the walking commutative triangle 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 simplicial type theory

In simplicial type theory, given a directed interval $\mathbb{I}$, the 2-simplex type representing the walking commutative triangle is defined as the type of pairs of elements of $\mathbb{I}$ such that $i \leq j$

$$\Delta^2 \coloneqq \sum_{i:\mathbb{I}} \sum_{j:\mathbb{I}} i \leq j$$

Properties

The walking commutative triangle is equivalent to the endofunctor category $I^I$ of the walking morphism $I$ to itself.

Related concepts

• 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

• triangle, 2-simplex

• commutative triangle

References

The phrase “walking commutative triangle” appears in:

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

The phrase “2-simplex” appears in

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

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, The Yoneda embedding in simplicial type theory (arXiv:2501.13229)