Coherent Tietze Transformations of 1-Polygraphs in Homotopy Type Theory

A 1-polygraph $P$ consists of a 0-polygraph $\mathrm{U}P$ (the underlying 0-polygraph of $P$) together with a function $\mathrm{S}\mathrm{U}P\to 𝒰$, which to any sphere $(x,y)$ in the underlying 0-polygraph associates a type $P(x,y)$ whose elements are called the 1-generators of the 1-polygraph. In other words, 1-polygraphs correspond to type-theoretic directed graphs. A 1-polygraph is discrete when all the types $\mathrm{U}P$ and $P(x,y)$ are sets. In the following, a sphere in $\mathrm{U}P$ is called a 0-sphere of $P$.

The elements of $\mathrm{U}P$ are called 0-generators or 0-cells of $P$. We sometimes write ${\mathrm{S}}_{0}P:=\mathrm{S}\mathrm{U}P$ for the 0-spheres, as well as $P_0:=\mathrm{U}P$ and $P_1:=\mathrm{\Sigma }((x,y):{\mathrm{S}}_{0}P).P(x,y)$ for the type of 0- and 1-generators of $P$. We also write ${\partial }^{-},{\partial }^{+}:P_1\to P_0$ for the source and target functions (defined by ${\partial }^{-}:=\pi \circ \pi$ and ${\partial }^{+}:={\pi }^{\prime }\circ \pi$).

Given a 1-polygraph $P$ and a $0$-sphere $(x,y)$, we write $P^{\ast }(x,y)$ for the type of 1-cells in $P$ from $x$ to $y$. This family of types is defined inductively as the smallest one such that

• $\mathrm{■}$

  for every 0-cell $x:\mathrm{U}P$, we have a 1-cell ${\mathrm{id}}_x:P^{\ast }(x,x)$,

• $\mathrm{■}$

  for every 0-cells $x,y,z:\mathrm{U}P$, 1-generator $a:P(x,y)$ and $1$-cell $u:P^{\ast }(y,z)$, we have a 1-cell $a::u:P^{\ast }(x,z)$,

• $\mathrm{■}$

  for every 0-cells $x,y,z:\mathrm{U}P$, 1-generator $a:P(y,x)$ and $1$-cell $u:P^{\ast }(y,z)$, we have a 1-cell $a:{:}^{\prime }u:P^{\ast }(x,z)$.

Informally, cells in $P^{\ast }(x,y)$ are undirected paths from $x$ to $y$ in the graph corresponding to $P$ (where the two last cases respectively correspond to taking an arrow $a$ forward and backward). In the following, we often write $a:x\to y$ for a 1-generator $a:P(x,y)$ and $u:x\stackrel{\ast }{\to }y$ for a 1-cell $u:P^{\ast }(x,y)$.

Given two 1-cells $u:x\stackrel{\ast }{\to }y$ and $v:y\stackrel{\ast }{\to }z$, we define their composite $u\cdot v:x\stackrel{\ast }{\to }z$ by induction on $u$ by

Given a 1-cell $u:x\stackrel{\ast }{\to }y$, we define its opposite $u^{\mathrm{op}}:y\stackrel{\ast }{\to }x$ by induction on $u$ by

where $a\overline{::}u$, which corresponds to appending $a$ to $u$, is defined by

and $a{\overline{::}}^{\prime }u$, corresponding to appending $a$ backward to $u$, is defined similarly.

A sphere $s$ in a 1-polygraph $P$ consists of a $0$-sphere $(x,y)$ together with a pair of 1-cells $f,g:x\stackrel{\ast }{\to }y$. The underlying 0-sphere $(x,y)$ is noted $\mathrm{U}s$. The cell $f$ (resp. $g$) is called the source (resp. target) of $s$ and noted ${\partial }^{-}s$ (resp. ${\partial }^{+}s$), so that the sphere $s$ is the triple $(\mathrm{U}s,{\partial }^{-}s,{\partial }^{+}s)$. We write $\mathrm{S}P$ for type of spheres in a $1$-polygraph.

In the definition of 1-cell, we think of $a::-$ and $a:{:}^{\prime }-$ as respectively precomposing by the 1-cell $a$ and its inverse. However, nothing enforces that they are actually inverse operations, i.e. that we have

for any 1-generator $a$ and 1-cell $u$ of suitable types. We define the types of coherent 1-cells $P^{\sim }(x,y)$, indexed by 0-spheres $(x,y)$, as the quotient of the types of 1-cells $P^{\ast }(x,y)$ under the congruence generated by the above relations. This type is the “right” definition for the 1-cells of $P$, in the sense that it gives a description of the free groupoid generated by $P$ [9]. However, non coherent 1-cells provides representatives for those which are often simpler to work with. Namely, by definition of coherent 1-cells as a quotient of 1-cells, we have

Given a 1-polygraph $P$ its geometric realization $\overline{P}$ is the higher inductive type generated by the two constructors

More abstractly, it corresponds to the pushout on the left or to the coequalizer on the right

where the horizontal arrow $f$ sends an edge $a:x\to y$ and $0$ (resp. $1$) to $x$ (resp. $y$), which corresponds to attaching 1-cells to a 0-dimensional cell complex. The associated induction principle is the following.

By partial evaluation, the map $\gamma$ induces, for $(x,y):{\mathrm{S}}_{0}P$, a map ${\gamma }_{x,y}:P(x,y)\to \iota x=\iota y$, which extends as a map on cells ${\gamma }_{x,y}^{\ast }:P^{\ast }(x,y)\to \iota x=\iota y$ defined by induction by

Moreover, since this definition is compatible with the relations for coherent 1-cells, for every sphere $(x,y):{\mathrm{S}}_{0}P$ we have the following.

This map is an equivalence, so it provides a characterization of the paths in geometric realizations of graphs [13, KvR/1Polygraph/PathPresentation.agda]:

A map $\iota x=\iota y\to P^{\sim }(x,y)$ can be defined using the elimination principle for paths in $\overline{P}$ given in [9, Theorem 3], and both can be shown to be mutually inverse by induction. $◀$

The set presented by a 1-polygraph $P$ is the set of connected components of its geometric realization ${\Vert \overline{P}\Vert }_0$. This notion is to be understood as an analogue of a group presentation with generators and relations, but shifted down by one dimension: here, the 0-cells of $P$ are the generators of the presented set, and the 1-cells are the relations.

We now prove some technical lemmas that will be useful later on.

By [19, Theorem 7.3.12], the type ${|\iota (x)|}_0={|\iota (y)|}_0$ coincides with $\parallel \iota (x)=\iota (y){\parallel }_{-1}$. Since we are eliminating to a proposition, we can suppose given a path $p:\iota (x)=\iota (y)$ which by Theorem 5 induces a coherent cell $\tilde{p}:P^{\sim }(x,y)$, and we conclude by Section 1.1. $◀$ The following shows that we can pick a representative 0-cell in every connected component [13, has-repr]:

Any proposition being a set [19, Lemma 3.3.4], it is enough to construct a map $f:\mathrm{\Pi }(x:\overline{P}).\parallel \mathrm{\Sigma }(\widehat{x}:\mathrm{U}P).\iota (\widehat{x})=x{\parallel }_{-1}$ which can be done by using the elimination principle of $\overline{P}$ (Section 1.2). Namely, we define, for $x:\mathrm{U}P$, $f(\iota (x)):={|(x,{\mathrm{refl}}_{\iota (x)})|}_{-1}$ and, for $x,y:\mathrm{U}P$ and $a:P(x,y)$, the path associated to it by $f$ is canonically defined by the fact that we are eliminating to a proposition. $◀$

The notion of Tietze transformation generalizes to polygraphs in any dimension. In particular, for 0-polygraphs, it can be formulated as follows. An elementary Tietze transformation of 0-polygraphs consists in

(T0)

Given a 0-polygraph $P$, a type $X$ and a function $\partial :X\to P$, we consider the 0-polygraph $P{\uparrow }_0\partial :=P\bigsqcup X$.

Two 0-polygraphs are Tietze equivalent when they are related by the smallest equivalence relation identifying $P$ with $P{\uparrow }_0\partial$ for any $P$ and $\partial$.

By definition of $P{\uparrow }_0\partial$ and its geometric realization, we have a coequalizer

By computing the coequalizer partially on the left component of the coproduct, we find that $\overline{P{\uparrow }_0\partial }$ is the coequalizer of $\begin{array}{c}\text{<object type="image/svg+xml" data="dagpub-standalone-combined-2025-05-21-15-12-54-page-18.pdf2svg.svg" id="S2.SS2.SSS0.P0.SPx1.p1.m3.1.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="67" height="23" style="width: 134px; height: unset; max-width: 100\%"></object>}\end{array}$. From which we easily deduce $\overline{P{\uparrow }_0\partial }=\overline{P}$. $◀$ The transformations (T0) actually preserve, not only the presented set, but also the geometric realization. We now show that transformations (T1) are correct [13, tietze1-correct]:

By using the induction principle of geometric realization (Section 1.2), we can define a map $s:\overline{P}\to \overline{P{\uparrow }_1\partial }$ by

for $x:P_0$ and $a:x\to y$ in $P_1$. Conversely, we define a map $r:\overline{P{\uparrow }_1\partial }\to \overline{P}$ by induction by

for $x:P_0$, $a:x\to y$ in $P_1$, and $b:\partial (x,y)$ for some $(x,y):{\mathrm{S}}_{0}P$. By induction, they can be shown to form a section-retraction pair, which induces an equivalence on the 0-truncations. $◀$

Finally, we show that taking sequential colimits of Tietze transformations preserves correctness. We will see in Theorem 22 that this is not needed (in the sense that the colimiting map can always be constructed without a colimit), but it is often convenient in proofs.

Since geometric realization is a colimit, by commutation of colimits, we have ${\mathrm{colim}}_i\overline{P^i}=\overline{{\mathrm{colim}}_i{P}^i}$, and thus ${\mathrm{colim}}_i{\Vert \overline{P^i}\Vert }_0={\Vert \overline{{\mathrm{colim}}_i{P}^i}\Vert }_0$ because colimits commute to truncation [16, Corollary 7.7]. Finally, we conclude using the fact that the canonical map ${\Vert \overline{P^0}\Vert }_0\to {\Vert \overline{{\mathrm{colim}}_i{P}^i}\Vert }_0$ is an equivalence, because a colimit of equivalences is an equivalence. $◀$

We define a map $f^{\prime }$ by

where the rightmost map is the one defined in Section 1.2. By the axiom of choice, we deduce the existence of a map

satisfying the required identity. The map $\widehat{g}$ is constructed similarly. $◀$ We then show that any 1-generator in $P$ induces a 1-cell in $Q$ between the image of its endpoints.

By definition of the geometric realization, the 1-generator $a$ induces an equality $\gamma (a):\iota (x)=\iota (y)$ in $\overline{P}$, and thus, by functoriality of $f$ and $|\cdot {|}_0$, an equality

Since, by Section 2.3, we have ${|\iota (\widehat{f}(x))|}_0=f({|\iota (x)|}_0)$ (and similarly for $y$), there is an equality

and we deduce, by Section 1.2, the existence of a 1-cell $\widehat{f}(x)\stackrel{\ast }{\to }\widehat{f}(y)$ as desired. $◀$ Furthermore, the maps $\widehat{f}$ and $\widehat{g}$ are mutually inverse modulo post-composition by ${|\iota (\cdot )|}_0$.

Given $x:\mathrm{U}P$, by Section 2.3 and the fact that $f$ and $g$ are mutually inverse maps, we have ${|\iota (\widehat{g}(\widehat{f}(x)))|}_0=g({|\iota (\widehat{f}(x))|}_0)=g(f({|\iota (x)|}_0))={|\iota (x)|}_0$. $◀$ Finally, we can show the completeness theorem.

Starting from the polygraph $P$, we are going to construct step-by-step a polygraph $P^3$ that contains both $P$ and $Q$ and is Tietze-equivalent to $P$ (and thus to $Q$ by symmetry).

1. 1.

   We add the 0-generators of $Q$. We write $P^1:=P{\uparrow }_0\widehat{g}$ for the polygraph obtained from $P$ by performing a transformation (T0) with $\widehat{g}:\mathrm{U}Q\to \mathrm{U}P$. Its type of 0-generators is $\mathrm{U}P\bigsqcup \mathrm{U}Q$ and the 1-generators are those of $P$ together with one 1-generator $\widehat{g}(x)\to x$ for every $x:\mathrm{U}Q$.

2. 2.

   We add the relations from $P$ to $Q$. Given a 0-generator $x:\mathrm{U}P$, we claim that there exists a 1-cell $\widehat{f}(x)\stackrel{\ast }{\to }x$ in $P^1$. By previous step, we have a cell

   $$a:\widehat{g}(\widehat{f}(x))\to \widehat{f}(x)$$

   Moreover, by Section 2.3, we have ${|\iota (\widehat{g}(\widehat{f}(x)))|}_0={|\iota (x)|}_0$, so the type ${\Vert \widehat{g}(\widehat{f}(x))\stackrel{\ast }{\to }x\Vert }_{-1}$ is inhabited by Section 1.2, and we can suppose that we actually have a 1-cell

   $$u:\widehat{g}(\widehat{f}(x))\stackrel{\ast }{\to }x$$

   because we are eliminating to a proposition. Hence, we can define a 1-cell $w_x:\widehat{f}(x)\stackrel{\ast }{\to }x$ by $w_x:=a:{:}^{\prime }u$ for every $x:\mathrm{U}P$. Finally, we consider the function

   	$\partial :\mathrm{U}{P}^1$	$\to \mathrm{\Sigma }((x,y):{\mathrm{S}}_0{P}^1).(x\stackrel{\ast }{\to }y)$
   	$x$	$\mapsto ((\widehat{f}(x),x),w_x)$

   and define $P^2:=P^1{\uparrow }_1\partial$ by a transformation (T1’), see Section 2.1.

3. 3.

   We add the 1-generators of $Q$. Given a 1-generator $b:x\to y$ in $Q$, we have 1-generators $a:g(x)\to x$ and $c:g(y)\to y$ in $P^2$ (by the first step), and we have the 1-cell $g(a):g(x)\stackrel{\ast }{\to }g(y)$ by Section 2.3. We therefore have a 1-cell

   $$a\cdot g(b)\cdot c:x\stackrel{\ast }{\to }y$$

   in $Q$. This induces a function

   $$\partial :\mathrm{\Sigma }((x,y):{\mathrm{S}}_{0}Q).Q(x,y)\to \mathrm{\Sigma }((x,y):{\mathrm{S}}_0{P}^2).(x\stackrel{\ast }{\to }y)$$

   which, to $(x,y):{\mathrm{S}}_{0}Q$ and $a:Q(x,y)$ associates the pair consisting of $(x,y)$ (or rather its image under the canonical inclusion) and the 1-cell constructed above. Finally, we define $P^3:=P^2{\uparrow }_1\partial$ by a transformation (T1’).

In the 1-polygraph $P^3$ constructed above, the 0-generators are $\mathrm{U}{P}^3=\mathrm{U}P\bigsqcup \mathrm{U}Q$ and the 1-generators are (up to canonical inclusion): those of $P$, those of $Q$ (by the third step), $\widehat{g}(x)\to x$ for $x:\mathrm{U}Q$ (by the first step), $\widehat{f}(x)\to x$ for $x:\mathrm{U}P$ (by the second step). By exchanging the roles of $P$ and $Q$, we see that $Q$ is also Tietze-equivalent to the above 1-polygraph (up to standard isomorphisms such as commutation of coproducts). By transitivity, we conclude that $P$ and $Q$ are Tietze-equivalent. $◀$

Consider the functions ${\Vert \overline{F}\Vert }_0:{\Vert \overline{P}\Vert }_0\to {\Vert \overline{Q}\Vert }_0$ and ${\Vert \overline{G}\Vert }_0:{\Vert \overline{Q}\Vert }_0\to {\Vert \overline{P}\Vert }_0$. Given $x:{\Vert \overline{P}\Vert }_0$, our aim is to show that ${\Vert \overline{G}\Vert }_0\circ {\Vert \overline{F}\Vert }_0(x)=x$. Since this type is a proposition, and thus a set, it is enough to construct a function $\varphi :\mathrm{\Pi }(x:\overline{P}).(\parallel \overline{G}{\parallel }_0(|\overline{F}(x){|}_0)=x)$ which can be done by induction on $x$. Namely, for $x:\mathrm{U}P$, we have $\varphi (\iota x):={|\gamma ({\eta }_x^{\mathrm{op}})|}_0$ and, for $a:P(x,y)$, $\varphi (\iota a)$ is canonically given by the fact that ${\Vert \overline{P}\Vert }_0$ is a set. We can similarly show that ${\Vert \overline{F}\Vert }_0\circ {\Vert \overline{G}\Vert }_0(y)=y$ for $y:{\Vert \overline{Q}\Vert }_0$, thus allowing us to conclude. $◀$

The above proposition allows us to recover in a “constructive” way the correctness property of Tietze transformations (Theorem 13). Namely, one can show [13, preservation]:

Since functorial equivalences are closed under identities, composition and inverses, it is enough to show that any elementary Tietze transformation induces a functorial equivalence between the corresponding polygraphs.

(T0)

Given a type $X$ and a function $\partial :X\to \mathrm{U}P$, we consider the functor $F:P\to P{\uparrow }_0\partial$ which is the canonical inclusion and the functor $G:P{\uparrow }_0\partial \to P$ defined by

$G(x)$

$G(a:x\to y)$

We take ${\eta }_x:={\mathrm{id}}_x$ for $x:\mathrm{U}P$, and ${\epsilon }_y:F(Gy)\stackrel{\ast }{\to }y$ is defined as ${\mathrm{id}}_y$ for $y:\mathrm{U}P$ and as the 1-cell corresponding to the canonical 1-generator $\partial y\to y$ given by definition of (T0) for $y:X$.

(T1)

Given a function $\partial :{\mathrm{S}}_{0}P\to 𝒰$ and functions ${\partial }_{x,y}:\partial (x,y)\to (x\stackrel{\ast }{\to }y)$, we consider the functor $F:P\to P{\uparrow }_1\partial$ which is the canonical inclusion and the functor $G$, which is the identity on 0-cells and

together with ${\eta }_x$ and ${\epsilon }_y$ being both identities for $x:\mathrm{U}P$ and $y:\mathrm{U}(P{\uparrow }_1\partial )$.

$◀$ To sum up, we have introduced three notions of equivalence for 1-polygraphs: Tietze equivalence, functorial equivalence, and equivalence of presented set. The above theorems show that these three notions coincide (Theorems 13, 22, 3.3, and 3.3).