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}$.

Definition

The walking commutative triangle $\Delta^2$ is defined in Cisinski, Cnossen, Nguyen & Walde as the functor category $I^I$ from the walking morphism $I$ to itself. In this definition, the objects $0, 2 \in \Delta^2$ is given by the identity morphisms on the two objects $0, 1 \in I$ and the object $1 \in \Delta^2$ the unique morphism from $0$ to $1$ in $I$, and the morphisms of $\Delta^2$ can be constructed as three face map functors from $I$ to $\Delta^2$: the first which takes $0 \in I$ to $0 \in \Delta^2$ and $1 \in I$ to $1 \in \Delta^2$; the second which takes $0 \in I$ to $0 \in \Delta^2$ and $1 \in I$ to $2 \in \Delta^2$; and the third which takes $0 \in I$ to $1 \in \Delta^2$ and $1 \in I$ to $2 \in \Delta^2$.

$\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$$

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

• 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

• triangle, 2-simplex

• commutative triangle

References

The phrase “walking commutative triangle” is defined in Definition 1.5.12 of:

• Denis-Charles Cisinski, Bastiaan Cnossen, Hoang Kim Nguyen, Tashi Walde, section 1.5.1 of: Synthetic Category Theory, 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)