# Directed Homotopy in Non-Positively Curved Spaces

Eric Goubault, Samuel Mimram

► To cite this version:

Eric Goubault, Samuel Mimram. Directed Homotopy in Non-Positively Curved Spaces. Logical Methods in Computer Science, 2020, 10.23638/LMCS-16(3:4)2020. [hal-04244375](https://hal.science/hal-04244375v1)

HAL Id: hal-04244375

https://hal.science/hal-04244375v1

Submitted on 16 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
DIRECTED HOMOTOPY IN NON-POSITIVELY CURVED SPACES

ÉRIC GOUBAULT AND SAMUEL MIMRAM

LIX, École Polytechnique, 91128 Palaiseau Cedex, France

e-mail address: eric.goubault@lix.polytechnique.fr

e-mail address: samuel.mimram@lix.polytechnique.fr

ABSTRACT. A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the “geometry” of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have *non-positive curvature*, a notion that we introduce and study here for precubical sets, and can be thought of as an algebraic analogue of the well-known one for metric spaces. Using this it, as well as categorical rewriting techniques, we are then able to show that *directed and non-directed homotopy coincide* for directed paths in these precubical sets. Finally, we study the geometric realization of precubical sets in metric spaces, to show that our conditions on precubical sets actually coincide with those for metric spaces. Since the category of metric spaces is not cocomplete, we are lead to work with generalized metric spaces and study some of their properties.

1998 *ACM Subject Classification*: Mathematics of computing Algebraic topology ; Theory of computation Parallel computing models .

*Key words and phrases:* precubical set, models for concurrency, cube axiom, non-positively curved space, CAT(0) space, generalized metric space, fundamental category.
CONTENTS

<table><tr><td>1. Precubical semantics of concurrent programs</td><td>5</td></tr><tr><td>1.1. Precubical sets</td><td>5</td></tr><tr><td>1.2. Precubical semantics of concurrent programs</td><td>9</td></tr><tr><td>1.3. Non-positively curved precubical sets</td><td>12</td></tr><tr><td>1.3.1. Geometric precubical sets</td><td>12</td></tr><tr><td>1.3.2. Non-positively curved precubical sets</td><td>13</td></tr><tr><td>1.3.3. The link condition</td><td>16</td></tr><tr><td>1.3.4. 2-dimensional non-positively curved precubical sets</td><td>20</td></tr><tr><td>2. When dihomotopy coincides with homotopy</td><td>22</td></tr><tr><td>2.1. Homotopy and dihomotopy in precubical sets</td><td>22</td></tr><tr><td>2.2. A 2-categorical approach to dihomotopy in precubical sets</td><td>24</td></tr><tr><td>2.2.1. The fundamental 2-category and 2-groupoid of a precubical set</td><td>24</td></tr><tr><td>2.2.2. Rewriting homotopies as dihomotopies</td><td>29</td></tr><tr><td>2.3. Extensions</td><td>36</td></tr><tr><td>2.3.1. The free compact closed category on a unidimensional object</td><td>36</td></tr><tr><td>2.3.2. Convergence of the rewriting system</td><td>37</td></tr><tr><td>2.3.3. An axiomatization of homotopy between homotopies</td><td>37</td></tr><tr><td>3. A (geo)metric approach to the cube property</td><td>38</td></tr><tr><td>3.1. Generalized metric spaces</td><td>38</td></tr><tr><td>3.1.1. Limits and colimits</td><td>40</td></tr><tr><td>3.1.2. Symmetric metric spaces</td><td>42</td></tr><tr><td>3.1.3. The underlying topological space of a metric space</td><td>43</td></tr><tr><td>3.1.4. Directed paths</td><td>44</td></tr><tr><td>3.1.5. Geodesic and length spaces</td><td>46</td></tr><tr><td>3.2. Geometric realization of precubical sets</td><td>47</td></tr><tr><td>3.2.1. Geometric realization</td><td>47</td></tr><tr><td>3.2.2. The topology of the geometric realization</td><td>50</td></tr><tr><td>3.2.3. Cubical complexes</td><td>51</td></tr><tr><td>3.2.4. Directed geometric realization</td><td>52</td></tr><tr><td>3.3. Non-positively curved spaces</td><td>53</td></tr><tr><td>3.3.1. CAT(0) spaces</td><td>53</td></tr><tr><td>3.3.2. The Gromov link condition</td><td>54</td></tr><tr><td>4. Conclusion and future work</td><td>54</td></tr><tr><td>References</td><td>55</td></tr></table>
Deep and fruitful links have been unraveled over the recent years between concurrent programs and topological spaces. The starting point of those was the definition of the so-called “geometric semantics”, which to a concurrent program associates a space whose points correspond to states of the program, paths to executions, and homotopies between paths to equivalence of execution traces up to permutation of independent actions. To be precise, in order to take in account the orientation of time, which makes the execution of actions irreversible, one has to actually consider spaces equipped with a notion of direction, which specifies directed paths and directed homotopies. This point of view has lead to both theoretical and practical applications, which are based on the fact that the study of the geometrical features of those spaces brings us information about the possible executions of the program, without having to consider all the possible interleavings of actions of the various threads constituting the program. We refer to reader to [21], as well as the recent book about the subject [15], for more details.

All these techniques have thus been developed with the aim of using mathematical tools for computing geometric invariants in order to ease the verification of concurrent programs. However, because of the aforementioned presence of time direction, most of those tools (such as homology groups, homotopy groups, etc.) cannot directly be used in order to compute the information which is relevant from a computer scientific point of view. In this article, we focus on a particular restricted class of programs: concurrent programs using only binary mutexes as a synchronization primitive. While being constrained enough to enjoy interesting properties, this class is still realistic from a practical point of view and can be used to express many of the classical synchronization algorithms. One of the main results of this article is that, in the geometrical models associated to those programs, *homotopy coincides with directed homotopy*, thus allowing one to use all tools from ordinary homotopy theory to characterize these execution models.

*The cube property.* Apart from the general motivations stated above, the origins of this article lie in the observation that a similar property, that we call here the *cube property*, occurs in different forms in different contexts, and it turns out that there are good reasons for this to be the case. This property is namely

(1) one of the main properties satisfied by semantics in asynchronous transition systems (or precubical sets) of our class of programs, which roughly says that when the transition system contains transitions forming half of a cube then it also contains the other half:

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>
(2) the so-called Yang-Baxter axiom satisfied by symmetries in monoidal categories, which can be depicted using string diagrams as

<figure><img src="image_5.png" /></figure>

(3) the Gromov condition [26] which characterizes cubical complexes of non-positive curvature (also called NPC or CAT(0) spaces).

The correspondence between the first two will be one of the main technical tools used in order to show the coincidence between homotopy and its directed variant mentioned above. The correspondence with the third point, reveals the main characteristics of the geometry of the spaces obtained as semantics of programs: if we realize them as metric spaces, they are non-positively curved. This means that if we draw a triangle in such a space, whose sides are geodesics, it will appear to be thinner than usual. This is typically the case for hyperbolic spaces (on the left) where a triangle (also pictured in the middle) is typically thinner than an usual triangle in a flat space (on the right):

<figure><img src="image_6.png" /></figure>

*Related work.* Since the topics covered in the various sections of the article are quite distinct (but of course closely related), we have mentioned in each section the related work specific to it, and only briefly expose here transversal references. In particular, the cube property that we use for defining NPC precubical sets and characterizing precubical semantics of concurrent programs and with binary mutexes has already been used in various works, as we now briefly recall. On the one hand this condition characterizes domains arising from event structures, which were introduced by Winskel [56, 57]. In particular, an equivalence of categories between deterministic labeled event structures and generalized trace languages (which satisfy three cube properties!) is given by Sassone, Nielsen and Winskel in [50]. This line of work is quite relevant here because event structures can be thought of as “unfolded” variants of the programs we consider: in particular, our use of binary mutexes corresponds to the binary conflict relation in event structures. However, the uses of cube conditions in order to model concurrent processes dates back to Stark’s concurrent transition systems [53], to the work of Panangaden and Shanbhogue [46] (where it is linked with a stability property in domains), and to Droste [12] and Kuske [35] who showed that concurrency automata with two cube axioms correspond to dI-domains. On the other hand, this condition was used by Gromov to characterize NPC cubical complexes [26] as mentioned above. The link between the two was first explicitly made by Chepoi [8] (who noticed that event structures are in bijection with median graphs [3], which in turn are in bijection with CAT(0) cube complexes [48, 7]) and was recently rediscovered [2] (reinventing the notion of event structure under the
prosaic name “poset with inconsistent pairs”). These relationships can be summarized in the
following diagram, where the dashed arrows schematize some of our contributions.

<figure><img src="image_7.png" /></figure>

Other uses of the cube property can be found in Lévy [38] (this seems to be the first occur-
rence of the condition) and Melliès' [20, 40] study of standardization in rewriting systems,
see also [5], and Dehornoy's work on Garside monoids [10, 11] where it is used in order to
ensure that a presented category embeds in its enveloping groupoid (this is generalized to
localizations in [9]), which is closely related to the situation studied in Section 2.

*Contents of the article.* We begin by recalling the notion of precubical set (Section 1.1), as-
sociate to each program a precubical set (Section 1.2) describing its execution traces as well
as (higher) commutations between their actions, and characterize their main properties (Sec-
tion 1.3): they are geometric (Section 1.3.1), non-positively curved and satisfy in particular
the cube condition (Section 1.3.2), which can be reformulated by a condition on links (Sec-
tion 1.3.3). We then introduce the notions of homotopy and dihomotopy between paths in
precubical sets (Section 2.1) and study those in a 2-categorical context (Section 2.2.1), which
leads us to Theorem 2.30 which shows that homotopy and dihomotopy relations coincide
(Section 2.2.2). We then recall and study in detail generalized metric spaces (Section 3.1),
allowing us to realize a precubical set as a metric space (Section 3.2) which is shown in
Theorem 3.79 to be non-positively curved when obtained as the semantics of a concurrent
program (Section 3.3).

We would like to particularly thank Emmanuel Haucourt and Jean Goubault-Larrecq for many comments and discussions about the ideas developed in this article, as well as the anonymous referees for helpful suggestions.

# 1. PRECUBICAL SEMANTICS OF CONCURRENT PROGRAMS

## 1.1. Precubical sets

We first recall the definition of precubical sets which will serve as the primary algebraic
structure for defining semantics for concurrent programs. Those can be thought of as a
generalization of the notion of graph, which incorporates the information of commutation
between two actions, and more generally between *n* actions, making them quite natural to
model concurrent programs in the spirit of “true concurrency”.
**Definition 1.1.** The precubical category $\square$ is the free monoidal category containing one object 1, and two morphisms $\varepsilon^{-}, \varepsilon^{+} : 0 \to 1$, where 0 denotes the unit of the monoidal category. It can also be presented as the category whose objects are integers and morphisms are generated by morphisms $\varepsilon_{i,n}^{\epsilon} : n \to n+1$ with $\epsilon \in \{-,+\}$, $n \in \mathbb{N}$ and $0 \le i \le n$, subject to the relations

$$ \varepsilon_{i,n+1}^{\epsilon'} \varepsilon_{j,n}^{\epsilon} = \varepsilon_{j+1,n+1}^{\epsilon} \varepsilon_{i,n}^{\epsilon'} \quad (1.1) $$

whenever $i \le j$ and $\epsilon, \epsilon' \in \{-,+\}$. The category of **precubical sets** is the category $\hat{\square}$ of presheaves over this category.

A precubical set $C \in \hat{\square}$ thus consists of a family of sets $(C(n))_{n \in \mathbb{N}}$ together with maps $\partial_{i,n}^{\epsilon} : C(n+1) \to C(n)$, with $0 \le i \le n$ and $\epsilon \in \{-,+\}$, where the map $\partial_{i,n}^{\epsilon}$ is a notation for $C(\varepsilon_{i,n}^{\epsilon})$, satisfying relations which are dual to (1.1), and we sometimes simply write $\partial_{i}^{\epsilon}$ when $n$ is clear from the context. An element $c \in C(n)$ is called an $n$-cube of $C$, $\partial_{i,n}^{\epsilon}(c)$ is called a face of $c$, and given a morphism $\phi : n \to p$ in $\square$, $C(\phi)(c)$ is called an iterated face of $c$. The dimension of a precubical set $C$ is the smallest integer $d \in \mathbb{N} \cup \{\infty\}$ such that $C(n) = \emptyset$ for $n > d$. A precubical set $C$ is finite when it is finite-dimensional and each $C(n)$ is finite.

**Example 1.2.** We write $\vec{I}$ for the precubical set of dimension 1, called the standard interval,

$$ x \xrightarrow{a} y $$

with $\vec{I}(0) = \{x, y\}$, $\vec{I}(1) = \{a\}$, $\vec{I}(n) = \emptyset$ for $n \ge 2$, $\partial_{0}^{-}(a) = x$, $\partial_{0}^{+}(a) = y$.

**Example 1.3.** A simple example of a precubical set $C$ of dimension 2 is

$$ \begin{array}{c} x \xrightarrow{a} y \\ b \downarrow \alpha \downarrow \\ x \xrightarrow{a} y \end{array} $$

with $C(0) = \{x, y\}$, $C(1) = \{a, b, b'\}$ and $C(2) = \{\alpha\}$. The cells of dimension 0 are pictured as points, cells of dimension 1 as segments, and the cell of dimension 2 as a square. This precubical set can thus abstractly be thought of as a cylinder. Face maps are given by $\partial_{0}^{-}(a) = x$, $\partial_{0}^{+}(a) = y$, $\partial_{0}^{-}(\alpha) = b$, $\partial_{0}^{+}(\alpha) = b'$, $\partial_{1}^{-}(\alpha) = \partial_{1}^{+}(\alpha) = a$, etc.

We recall some operations available on precubical sets, which will be used in the following in order to define the semantics for programs. A tensor product can be defined as follows.

**Definition 1.4.** Given two precubical sets $C$ and $D$, their tensor product $C \otimes D$ is the precubical set defined by

$$ (C \otimes D)(n) = \coprod_{i+j=n} C(i) \times D(j) $$

for $n \in \mathbb{N}$, and

$$ \partial_{k,n}^{\epsilon}(C \otimes D)(c,d) = \begin{cases} (\partial_{k,n}^{\epsilon}(c), d) & \text{if } 0 \le k < i \\ (c, \partial_{k-i,n}^{\epsilon}(d)) & \text{if } i \le k < n \end{cases} $$

for $n \in \mathbb{N}$, $0 \le k < n$, $\epsilon \in \{0, 1\}$ and $(c, d) \in C(i) \times D(j) \subseteq (C \otimes D)(n)$ with $i + j = n$. This tensor equips the category $\hat{\square}$ with a monoidal structure, whose unit is the precubical set $C$ consisting of one single 0-cube.
As a presheaf category, the category of precubical sets is cocomplete, with colimits being computed pointwise [39]. In particular, we denote by $C \sqcup D$ the coproduct of two cubical sets, and given a precubical set $C$ and two 0-cubes $c, d \in C(0)$, we write $C[c = d]$ for the precubical set obtained from $C$ by identifying $c$ and $d$ (this precubical set can be obtained as the expected coequalizer). Finally, given a set $X \subseteq C(0)$ of 0-cubes of a precubical set $C$, we write $C\X$ for the *precubical subset* of $C$ consisting of $n$-cubes of $C$ which do not contain an element of $X$ as iterated face.

Given $n \in \mathbb{N}$, we write $\square_n$ for the full subcategory of $\square$ whose objects $k$ satisfy $k \le n$, and $\hat{\square}_n$ is thus the full subcategory of $\hat{\square}$ consisting of precubical sets of dimension at most $n$.

**Definition 1.5.** The presheaves in $\square_n$ are called $n$-precubical sets. The functor $\hat{\square} \to \hat{\square}_n$ induced by precomposition with the inclusion functor $\square_n \hookrightarrow \square$ is called the $n$-truncation functor.

In particular, the category $\hat{\square}_1$ is the category of graphs, and every precubical set $C$ has an underlying graph: we thus sometimes refer to the elements of $C(0)$ (resp. $C(1)$) as *vertices* (resp. *edges* or *transitions*), a *path* in a precubical set is a path in the underlying directed graph, etc. Also, a 2-cube is sometimes called a *square*.

**Definition 1.6.** We define a symmetric relation $\diamond$ on paths of length 2 as the smallest symmetric relation such that, given two paths $a \cdot b$ and $b' \cdot a'$ of length 2 constituted of edges $a, b, a'$ and $b'$, we have $a \cdot b \diamond b' \cdot a'$ whenever there exists a square $\alpha$ such that

$$a = \partial_{0,1}^{-}(\alpha)$$

$$b = \partial_{1,1}^{+}(\alpha)$$

$$b' = \partial_{1,1}^{-}(\alpha)$$

$$a' = \partial_{0,1}^{+}(\alpha)$$

or symmetrically. Graphically, we have a square $\alpha$ as on the left, which we often schematically picture as on the right

<figure><img src="image_8.png" /></figure>

In this situation, we say that the coinitial transitions $a$ and $b'$ (resp. $b'$ and $a$) are *independent*.

As for any presheaf category, there is a full and faithful embedding $Y : \square \to \hat{\square}$ given by the Yoneda functor, which is defined on objects as the set of morphisms $Ynm = \square(m, n)$. Given $n \in \mathbb{N}$, the representable precubical set $Yn$ is called the *standard $n$-cube*. It can be shown that $Yn$ is isomorphic to $\hat{I}^{\otimes n}$, the tensor product of $n$ copies of $\hat{I}$ (see Example 1.2). For instance, we have

$x$

$x \xrightarrow{f} y$

$x \xrightarrow{f} y_1$
$g \xrightarrow{\diamond} g'$
$y_2 \xrightarrow{f'} z$

$Y0$

$Y1$

$Y2$

An explicit description of standard $n$-cubes can be given as follows. We will see that it is often quite useful in order to perform computations.
**Lemma 1.7.** Given $n \in \mathbb{N}$, the cubes in $Yn$ are in bijection with strings in $\{-, 0, +\}^n$, the $k$-cubes in $Ynk$ being the strings containing the letter 0 exactly $k$ times, and given $u \in Ynk$, the face $\partial_i^-(u)$ (resp. $\partial_i^+(u)$) is obtained from $u$ by replacing the $i$-th letter 0 by $-$ (resp. $+$).

For instance, the preceding standard cubes are

<figure><img src="image_9.png" /></figure>

(here $\varepsilon$ denotes the empty word). One can notice that $Ynk = \emptyset$ for $k > n$ and there is only one element in $Ynn$ (the string $0^n$). The standard hollow $n$-cube, denoted $\partial Yn$, is the precubical set obtained from $Yn$ by removing the cell in $Ynn$. For instance,

<figure><img src="image_10.png" /></figure>

There is an obvious inclusion morphism of precubical sets $\partial Yn \to Yn$ embedding the standard hollow $n$-cube as the “border” of the standard $n$-cube. A fact that will sometimes be useful is that the faces of the standard $n$-cubes naturally index morphisms computing iterated faces of an $n$-cube: given a precubical set $C$, an $n$-cube $x \in C(n)$ and $u \in \{-, 0, +\}^n$, we write

$$ \partial^u(x) = \partial_0^{u_0} \circ \partial_1^{u_1} \circ \dots \circ \partial_{n-1}^{u_{n-1}}(x) $$

where $u_i \in \{-, 0, +\}$ is the $i$-th letter of $u$ and by convention $\partial_i^0(x) = x$.

Given a set $\mathcal{L}$ of labels, we will sometimes consider labeled variants of precubical sets.

**Definition 1.8.** A labeled precubical set $(C, \ell)$ consists of a precubical set $C$ together with a labeling function $\ell: C(1) \to \mathcal{L}$ on edges, such that we have $\ell \circ \partial_{i,1}^- = \ell \circ \partial_{i,1}^+$ for $i \in \{0, 1\}$.

Graphically, the condition on the labeling function amounts to supposing that parallel edges of a square have the same label.

**Remark 1.9.** If we suppose that the set $\mathcal{L}$ is totally ordered, we can define a precubical set $!\mathcal{L}$ such that the elements of $!\mathcal{L}(n)$ are strictly increasing sequences of $n$ elements of $\mathcal{L}$, and given $c \in !\mathcal{L}(n+1)$, $\partial_{i,n}^-(c) = \partial_{i,n}^+(c)$ is obtained by removing the $i$-th element of the sequence $c$. The category of labeled precubical sets can then alternatively be defined as the comma category $\hat{\square}/!$, see [22] for details.

We will also make some use of presimplicial sets, which are a well-known variant of precubical sets, which is based on triangles instead of squares. Formally, the category of (augmented) presimplicial sets is the presheaf category $\hat{\Delta}$, where $\Delta$ is the category whose objects are finite ordinals $[n]$ (given $n \in \mathbb{N}$, we write $[n]$ for the set $\{0, \dots, n-1\}$) and morphisms are strictly increasing functions. Given a presimplicial set $S$, the elements of $S(n)$ are called $n$-simplices, and, given $i$ with $0 \le i \le n$, we write $\partial_{i,n}: S(n+1) \to S(n)$ for the image by $S$ of the function $[n] \to [n+1]$, whose image does not contain $i$, associating to an $(n+1)$-simplex its $i$-th face.
## 1.2. Precubical semantics of concurrent programs

We now introduce an idealized concurrent programming language and provide its semantics in precubical sets. A detailed presentation of this language can be found in [15], in a variant which includes more realistic features, such as memory and manipulation of values.

We suppose fixed a set $\mathcal{A}$ of actions, containing a particular action $\text{nop} \in \mathcal{A}$ (standing for the action which has no effect), and a set $\mathcal{M}$ of mutexes. A program $p$ is an expression generated by the grammar

$$p ::= 1 \mid A \mid P_a \mid V_a \mid p \cdot p \mid p+p \mid p \| p \mid p^*$$

where $A \in \mathcal{A}$ is an arbitrary action and $a \in \mathcal{M}$ is an arbitrary mutex. The intended meaning of these constructions is the following one: 1 is the empty program, $A \in \mathcal{A}$ is an arbitrary instruction (for instance, assigning a value to a memory cell or printing a message on the screen), $p \cdot q$ is $p$ followed by $q$, $p+q$ is a (non-deterministic) choice between $p$ and $q$, $p \| q$ is the program obtained by running $p$ and $q$ in parallel, $p^*$ is the program $p$ executed an arbitrary number of times. In practice, it is desirable to forbid some actions (such as accessing memory) from running in parallel. This is generally done using mutexes which are particular kind of resources on which a program can perform two operations: a mutex $a$ can either be *locked* using the instruction $P_a$ or *released* using the instruction $V_a$. The operational semantics of a mutex is such that at most one subprogram can have locked a mutex at a time: if a subprogram tries to lock an already-locked mutex, it is frozen until the mutex is released.

The class of programs defined above is very general and thus difficult to reason about. In practice, the programs which are written are such that the state of mutexes only depends on the position in the program and not on the execution that lead to it. We will thus restrict to such programs, called *conservative*, which can be formally defined as follows.

**Definition 1.10.** The *resource consumption function* $\Delta(p) : \mathcal{M} \to \mathbb{Z}$ of a program $p$ is defined inductively by

$$
\begin{align*}
\Delta(1) &= 0 & \Delta(A) &= 0 \\
\Delta(P_a) &= -\delta_a & \Delta(V_a) &= \delta_a \\
\Delta(p \cdot q) &= \Delta(p) + \Delta(q) & \Delta(p \| q) &= \Delta(p) + \Delta(q) \\
\Delta(p+q) &= \Delta(p) & \text{if } \Delta(p) = \Delta(q) \\
\Delta(p^*) &= 0 & \text{if } \Delta(p) = 0
\end{align*}
$$

Above, 0 denotes the constant function, the sum of functions is computed pointwise, and $\delta_a : \mathcal{M} \to \mathbb{Z}$ is the function such that $\delta_a(a) = 1$ and $\delta_a(b) = 0$ for $b \neq a$. Note that, because of the side conditions in the cases for choice and loop, this function might not be defined. A program $p$ such that $\Delta(p)$ is defined is called *conservative*.

**Example 1.11.** The program $P_a \cdot (V_a \cdot P_a)^* \cdot V_a$ is conservative, as well as $P_a \| P_b$, but not the program $P_a^*$ (the number of times $a$ is taken depends on the number of loops executed) nor $P_a + P_b$ (which mutex is taken in the end depends on the chosen branch).

In the following, we will consider the following set of labels:

$$\mathcal{L} = \mathcal{A} \uplus \{P_a \mid a \in \mathcal{M}\} \uplus \{V_a \mid a \in \mathcal{M}\}$$

To any program $p$ can be inductively associated a precubical set $C_p$ labeled in $\mathcal{L}$, together with two vertices $b_p$ and $e_p$, as follows:
**Example 1.12.** The precubical sets associated to the program $(P_a \parallel P_b) + P_c$ and to the program $(P_a \cdot V_a) \parallel (P_a \cdot V_a)$ are respectively

<figure><img src="image_11.png" /></figure>

**Remark 1.13.** The transitions labeled by nop abstractly represent the evaluation of conditions (depending on which the branch of a conditional branching is chosen or a loop is stopped). If our language contained boolean expressions, they should actually be such, see [15]. Notice that these transitions cannot be contracted to a point in the semantics because it not be correct anymore: for instance the semantics of $P_a + 1$ would contain a loop.

A path $t$ of length $n$ in $C_p$, where the labels of its vertices are $l_1, l_2, \dots, l_n \in \mathcal{L}$, can be seen as a program $l_1 \cdot l_2 \dots l_n$ (i.e. a sequence of actions and operations on mutexes), and we write $\Delta(t) : \mathcal{M} \to \mathbb{Z}$ for its resource consumption. When the program is conservative, resource consumption only depends on the endpoints of paths, which explains the terminology, by analogy with the situation in physics:

**Lemma 1.14.** Given a conservative program $p$ and two paths $t$ and $u$ in $C_p$ with the same source and the same target, we have $\Delta(t) = \Delta(u)$.

It can be observed that, for any program $p$, there is a path in $C_p$ from $b_p$ to any vertex $x$. This fact and preceding lemma ensure that the following definition makes sense:

**Definition 1.15.** The resource potential $r_p : C_p(0) \to (\mathcal{M} \to \mathbb{Z})$ of a conservative program $p$ is the function which to a vertex $x \in C_p(0)$ associates $\Delta(t)$ where $t$ is any path from $b_p$ to $x$.

A vertex $x$ such that there exists $a \in \mathcal{M}$ where $r_p(x) < -1$ or $r_p(x) > 0$ is said to be forbidden: the operational semantics of mutexes enforces that such a state of the program can never be reached, because a mutex can be taken at most once and not released more than taken. The precubical semantics of a conservative program $p$ is thus obtained from $C_p$ by removing those forbidden vertices. Given a precubical set $C$ and a set $X \subseteq C(0)$ of vertices of $C$, recall that we write $C \setminus X$ for the precubical set obtained from $C$ by removing all the cubes having an element of $X$ as iterated face.

**Definition 1.16.** Given a conservative program $p$, its precubical semantics is the precubical set $\tilde{C}_p$ defined by

$$ \tilde{C}_p = C_p \setminus X \quad \text{where} \quad X = \{x \in C(0) \mid r_p(x) < -1 \lor r_p(x) > 0\} $$
**Example 1.17.** The precubical semantics of the program $(P_a \cdot V_a) \parallel (P_a \cdot V_a)$

<figure><img src="image_12.png" /></figure>

is obtained by removing then central vertex (and associated transitions) from the graph of Example 1.12.

An *execution trace* $t$ of a program $p$ is a path in $\check{C}_p$ starting from the beginning vertex $b_p$. It can be checked that those are in bijection with execution traces as they would be defined in a reasonable operational semantics [15]. Moreover, $n$-cubes of dimension 2 and higher can be used to construct a useful notion of equivalence of execution traces, called *homotopy*, as explained in Section 2.

### 1.3. Non-positively curved precubical sets

In this section, we study the general properties of precubical sets arising as semantics of programs. This will lead us to formulate a set of conditions characterizing what we call *non-positively curved precubical sets*: it will be shown in Section 3.3.2 that their geometric realizations are precisely non-positively curved precubical complexes.

#### 1.3.1. *Geometric precubical sets*

We begin by recalling the definition of “geometric” precubical sets [14]. The reason for this terminology should become apparent in Proposition 3.67: their geometric realizations are cubical complexes.

**Definition 1.18.** A precubical set $C$ is **geometric** when it satisfies the following conditions:

(1) *no self-intersection*: two distinct iterated faces of a cube in $C$ are distinct, i.e. given two morphisms $\phi, \psi : m \to n$ in $\square$, if there exists $c \in C(n)$ such that $C(\phi)(c) = C(\psi)(c)$ then $\phi = \psi$,

(2) *maximal common faces*: two cubes admitting a common face admit a maximal common face.

**Example 1.19.** Consider the following precubical sets of dimension 1

$$x \underset{b}{\overset{a}{\rightleftarrows}} y \qquad (1)$$

$$x \underset{a}{\overset{a}{\rightleftarrows}} \emptyset \qquad (2)$$

$$x \underset{b}{\overset{a}{\rightleftarrows}} y \qquad (3)$$

$$x \underset{c}{\overset{a}{\rightleftarrows}} y \quad (4)$$

(1) and (3) are not self-intersecting but fail to have maximal common faces, (2) is self-intersecting and (4) is geometric. Notice that (4) and (3) are obtained by subdividing (2). However, it is not always possible to subdivide enough a precubical set in order to obtain a geometric one [14].
**Example 1.20.** Consider the precubical set obtained from two copies of the standard square Y2 by identifying both vertices $-+$ and both vertices $+-$ in the two squares:

<figure><img src="image_13.png" /></figure>

with $a \cdot b' \diamond a' \cdot b$ and $f \cdot g' \diamond g \cdot f'$. This precubical set is not self-intersecting but does not have maximal common faces.

Interestingly, the geometricity condition can be characterized as follows on the category of elements of a precubical set (this classical notion is recalled in Section 3.2.2):

**Lemma 1.21.** A precubical set $C$ is geometric if and only if its category of elements $\mathrm{El}(C)$ is a poset such that any two elements with a common lower bound have a greatest lower bound, i.e. for every $x \in \mathrm{El}(C)$ the slice category $x/\mathrm{El}(C)$ is a meet semilattice.

*Proof*. The assumption that $C$ has no self-intersection implies that any two morphisms with the same source and the same target in $\mathrm{El}(C)$ are equal, and since the non-trivial morphisms are from a cube to a cube of strictly higher dimension, there are no non-trivial endomorphisms. The category $\mathrm{El}(C)$ is thus a poset. The condition on lower bounds is a direct reformulation of the “maximal common face” condition. $\square$

The precubical semantics of most programs is a geometric precubical set, excepting for some degenerated ones. For instance, the semantics of $1+1$ is

<figure><img src="image_14.png" /></figure>

which is not self-intersecting. Not allowing the construction $1$ to occur in programs is enough to ensure that their semantics is geometric and does not remove any expressive power to the language in practice. We will implicitly assume that this is the case in the rest of the paper. By an easy induction on the structure of programs, the following can be shown:

**Lemma 1.22.** The precubical semantics $\check{C}_p$ of a program $p$ without occurrences of $1$ is a geometric precubical set.

### 1.3.2. Non-positively curved precubical sets

In this section, we introduce the notion of non-positively curved precubical set, which will be shown to be an algebraic counterpart of the usual notion of non-positively curved space in Section 3.3.2. The conditions for being such a precubical set are easily formulated as lifting properties, which are of the following general form.

**Definition 1.23.** Given a morphism $f : D \to E$ between precubical sets, we say that a precubical set $C$ *lifts* (resp. *lifts at most once*, resp. *lifts uniquely*) the morphism $f$, when
for every morphism $h : D \to C$, there exists a morphism (resp. at most one morphism, resp. a unique morphism) $g : E \to C$ such that $h = g \circ f$.

<figure><img src="image_15.png" /></figure>

We will be mainly interested in the following lifting properties, which all more or less express the fact that, as soon as a precubical set contains a subset which could be the border of a cube, it should actually contain a cube with this border.

**Definition 1.24.** Suppose given a precubical set $C$. We say that $C$ has

(1) *no parallel edges* when it lifts at most once the canonical inclusion $\partial Y1 \hookrightarrow Y1$,

(2) the *at most one square closing property* when each of the four canonical inclusions of

<figure><img src="image_16.png" /></figure>

into

<figure><img src="image_17.png" /></figure>

i.e.

$$Y2 \setminus \{+-\} \hookrightarrow Y2$$

$$Y2 \setminus \{-+\} \hookrightarrow Y2$$

$$Y2 \setminus \{++\} \hookrightarrow Y2$$

$$Y2 \setminus \{--\} \hookrightarrow Y2$$

is lifted at most once,

(3) the *cube property* when each of four canonical inclusions of

<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /></figure>
into

<figure><img src="image_20.png" /></figure>

(we did not figure 2-cubes of $\partial Y3$ in order to keep the figure more or less readable),
i.e.

$$ Y3 \setminus \{-+-\} \hookrightarrow \partial Y3 $$

$$ Y3 \setminus \{+-+\} \hookrightarrow \partial Y3 $$

$$ Y3 \setminus \{+++\} \hookrightarrow \partial Y3 $$

$$ Y3 \setminus \{---\} \hookrightarrow \partial Y3 $$

is lifted at most once,

(4) the unique $n$-cube property (resp. at most one $n$-cube property) when it lifts uniquely (resp. at most once) the inclusion $\partial Yn \to Yn$.

**Remark 1.25.** When a precubical set satisfies the at most one square closing property, the liftings of (1.4) and (1.5) are necessarily unique.

**Remark 1.26.** Notice that, in the cube property, we require lifting four inclusions of a “half cube” into the hollow cube, but there are four more natural inclusions that we could write (there are height in total, one corresponding to each vertex of the cube). However, those are superfluous, because the cube has non-trivial automorphisms. For instance, the lifting of the inclusion of

<figure><img src="image_21.png" /></figure>

into $\partial Y3$ can be deduced from the lifting of the inclusion corresponding to the left of (1.4).

By definition of the condition of being geometric (Definition 1.18), we have the following.

**Lemma 1.27.** A geometric precubical set $C$ lifts at most once the embedding $\partial Yn \to Yn$ for any $n \ge 1$. In particular, it has no parallel edges. Moreover, $C$ satisfies the at most one square filling property.

We introduce the following terminology, whose meaning should be explained in Section 3.3.2.

**Definition 1.28.** A precubical set which

(1) is geometric,

(2) satisfies the cube property,

(3) and satisfies the unique $n$-cube property for $n \ge 3$,

is said to be **non-positively curved** (or **NPC** for short).

**Proposition 1.29.** The precubical semantics of a program is non-positively curved.
*Proof.* We have already seen in Lemma 1.22 that the cubical semantics of a non-degenerated program is geometric. We show the other properties. Given a program *p*, it is easy to show by induction on *p* that the precubical set *C*<sub>*p*</sub> is non-positively curved (essentially, one has to check that the properties (2) and (3) are preserved by gluing along vertices and taking tensor product). The precubical semantics is defined as Ĉ<sub>*p*</sub> = *C*<sub>*p*</sub> \ *X* where *X* is the set of forbidden vertices. Clearly, the unique *n*-cube property, with *n* ≥ 3, is still satisfied for Ĉ<sub>*p*</sub>. However, the cube property requires a little more care. Write *L* (resp. *R*) for the precubical set on the left (resp. right) of (1.4). Notice that the hollow 3-cube ∂*Y*3 can be obtained by gluing *L* and *R* along their “border” (i.e. by identifying the vertices and edges with the same names in both precubical sets). Suppose given a morphism *L* → Ĉ<sub>*p*</sub>: we are going to show that it can be extended as a morphism ∂*Y*3 → Ĉ<sub>*p*</sub>. By abuse of notation, we identify *L* with its image in Ĉ<sub>*p*</sub> and simply say that Ĉ<sub>*p*</sub> “contains” *L*. Since *C*<sub>*p*</sub> satisfies the cube property, it also contains *R*. Thus, in Ĉ<sub>*p*</sub>, *L* can be completed as a hollow 3-cube unless the vertex −−− is forbidden. We write *A*, *B* and *C* for the actions respectively labeling the edges of the form 0*ε*ε', *ε*0*ε'* and *ε*ε'0, with *ε*, *ε'* ∈ {−, +}: *L* and *R* in *C*<sub>*p*</sub> are respectively labeled as

<figure><img src="image_22.png" /></figure>

Suppose that $--$ is forbidden. Since none of the vertices in $L$ is forbidden, there exists a resource $a$ such that either $r_p(--)(a) = 1$ and $B$ is $V_a$, or $r_p(--) = -2$ and $B$ is $P_a$. Suppose that we are in the first case (the other case is similar), i.e. $B = V_a$. Notice that we have $r_p(---) = 0$. Necessarily, we have $A = P_a$ (otherwise $r_p(++-) = r_p(--) = 1$ and the vertex $++$ would be forbidden) and $C = P_a$ (otherwise $--$ would be forbidden). But in this case, we have $r_p(++) = -2$ and therefore $--$ would be forbidden, contradicting the hypothesis that $\check{C}_p$ contains $L$. All other cases can be handled by similar reasoning. $\square$

**Remark 1.30.** The precubical semantics of the program $A+B$ is

<figure><img src="image_23.png" /></figure>

showing that the 2-cube property is not generally satisfied for cubical semantics of programs.

### 1.3.3. *The link condition*

The Gromov condition for characterizing NPC cubical complexes, which is recalled in Section 3.3.2, is generally expressed in terms of a “flagness” condition on the “link” of vertices in the complex. We extend here the definition of link to precubical sets and show that a similar characterization of NPC can be formulated in terms of those links.

**Definition 1.31.** Given a precubical set *C*, the **link** of *C*, denoted *link*(*C*), is the (augmented) presimplicial set whose *n*-simplices are pairs $(u, y)$ with $u \in \{-, +\}^n$ and $y \in C(n)$.
Given $i$ with $i \in [n]$, the $i$-th simplicial face of such an $n$-simplex $(u, y)$ is given by

$$ \partial_i(u, y) = (u', \partial_i^{u_i}(y)) $$

where $u'$ is the word $u$ with the $i$-th letter removed. Given a vertex $x \in C(0)$, the link of $x$, denoted $link(x)$, is the presimplicial subset of $link(C)$ whose simplices are those having $(\varepsilon, x)$ as iterated 0-face.

Note that, by definition, the link of a vertex has only one 0-simplex, and as such can be seen as a non-augmented presimplicial set, shifting dimensions by -1. This will implicitly be used in the following in order to draw pictures.

**Example 1.32.** Consider the precubical set $C$ on the left. The link of the vertex $x$ is shown on the right:

<figure><img src="image_24.png" /></figure>

The link of a vertex $x$ is constituted of the cubes having $x$ as iterated face. Its simplices can be represented as follows.

**Definition 1.33.** Given $u \in \{-, +\}^n$, we write $\Lambda^u$ for the precubical subset of $\partial Yn$ whose cubes $v \in \{-, 0, +\}^n$ are those having at least one letter in common with $u$ (i.e. there exists $i$, with $0 \le i < n$, such that $v_i = u_i$).

**Remark 1.34.** The precubical set $\Lambda^u$ can alternatively defined from $\partial Yn$ by removing all cubes having the vertex $\bar{u}$ as iterated face, where $\bar{u} = \bar{u}_0...\bar{u}_{n-1}$ with $\bar{=} = +$ and $\bar{=} = -$.

**Example 1.35.** The precubical sets (1.3) are respectively $\Lambda^{-+}$, $\Lambda^{+-}$, $\Lambda^{--}$ and $\Lambda^{++}$. Those of (1.4) are respectively $\Lambda^{+-+}$ and $\Lambda^{-+-}$, and similarly for (1.5), see also Remark 1.36.

**Remark 1.36.** By definition, given $u \in \{-, +\}^n$, there is a canonical inclusion $\Lambda^u \hookrightarrow \partial Yn$ and thus a canonical inclusion $\Lambda^u \hookrightarrow Yn$ by post-composing with the canonical inclusion $\partial Yn \hookrightarrow Yn$. By Remark 1.26, the cube property is precisely the lifting property wrt all possible such inclusions in the case $n = 3$. In particular, the two precubical sets of (1.4) are respectively $\Lambda^{+-+}$ and $\Lambda^{-+-}$, and those of (1.5) are respectively $\Lambda^{---}$ and $\Lambda^{+++}$.

Geometric precubical sets which are non-positively curved can be characterized by a lifting condition on the links. We write $Z : \triangle \to \hat{\triangle}$ for the Yoneda embedding of the presimplicial category into presimplicial sets (the notation $Y$ is reserved for the Yoneda embedding $Y : \square \to \hat{\square}$). Given $n \in \triangle$, the representable $Zn$ is called the *standard $n$-simplex*. As in the case of precubical sets, it can be explicitly described as the presimplicial set whose $k$-simplices are the sets $\{j_0, ..., j_{k-1}\} \subseteq [n]$ such that $j_0 < j_1 < ... < j_{k-1}$ and, given $i$ with $0 \le i < k$ the $i$-th face of such a simplex is given by removing the element $j_i$. We thus have $Znk = \emptyset$ for $k > n$ and $Znn$ is reduced to one element (the simplex $[n]$). The *standard hollow $n$-simplex* $\partial Zn$ is the presimplicial set obtained from $Zn$ by removing the top-dimensional simplex in $Zn$, and there is a canonical inclusion $\partial Zn \hookrightarrow Zn$.
**Definition 1.37.** A presimplicial $S \in \hat{\Delta}$ set is **flag** if, for every integer $n \ge 3$ and morphism $f : \partial Zn \to S$, there exists a unique morphism $g : Zn \to S$ making the diagram

<figure><img src="image_25.png" /></figure>

commute, where the vertical arrow is the standard inclusion.

As previously, we sometimes say that a flag presimplicial set lifts uniquely the inclusions $\partial Zn \hookrightarrow Zn$. In Theorem 1.42, we characterize NPC precubical sets in terms of their links, and this will follow from the following lemmas.

**Lemma 1.38.** Suppose given a precubical set $C$ and a vertex $x \in C(0)$.

- There is a bijection between presimplicial morphisms $\phi : Zn \to \text{link}(x)$ and pairs $(u, \psi)$ with $u \in \{-, +\}^n$ and $\psi : Y(n) \to C$ a precubical morphism such that $\psi(u) = x$.

- Similarly, there is a bijection between presimplicial morphisms $\phi : \partial Zn \to \text{link}(x)$ and all precubical morphisms of the form $\psi : \Lambda^u \to C$, for some $u \in \{-, +\}^n$, such that $\psi(u) = x$.

*Proof.* The first bijection follows easily from the Yoneda lemma: morphisms $\phi : Zn \to \text{link}(x)$ are in bijection with $n$-simplices in $\text{link}(x)$, i.e. pairs $(u, y)$ with $u \in \{-, +\}^n$ and $y \in C(n)$ such that $\partial^u(y) = x$, which are in turn in bijection with pairs $(u, \psi)$ with $u \in \{-, +\}^n$ and $\psi : Y(n) \to C$ such that $\psi(u) = x$. The second bijection is a slight variant of the first one. $\square$

**Remark 1.39.** It can moreover be checked that these bijections are compatible with restriction to the border, what we will generally leave implicit in the following. This means that given a presimplicial morphism $\phi : Zn \to \text{link}(x)$ corresponding to a precubical morphism $\psi : Y(n) \to C$ by the first bijection, the presimplicial morphism $\partial Zn \hookrightarrow Zn \xrightarrow{\phi} \text{link}(x)$ corresponds to the precubical morphism $\partial Y(n) \hookrightarrow Y(n) \xrightarrow{\psi} C$ by the second bijection.

The following lemma shows that NPC precubical sets, always satisfy a higher-dimensional generalization of the cube property.

**Lemma 1.40.** Suppose given an NPC precubical set $C$. Given $n \in \mathbb{N}$ with $n \ge 3$ and $u \in \{-, +\}^n$, $C$ lifts uniquely the canonical embedding $\Lambda^u \hookrightarrow Yn$.

*Proof.* Given $u \in \{-, +\}^n$ and $k$ with $0 \le k \le n$, we write $\Lambda_k^u$ for the subcomplex of $Yn$ whose cubes are the strings $v = \{-, 0, +\}^n$ which either have one letter in common with $u$ (i.e. $v_i = u_i$ for some $i \in [n]$) or have at most $k$ occurrences of the letter “0”. In particular, we have $\Lambda_0^u = \Lambda^u$, $\Lambda_{n-1}^u = \partial Yn$ and $\Lambda_n^u = Yn$. We show that $C$ lifts uniquely the embedding $\Lambda^u \hookrightarrow \Lambda_2^u$, and the embeddings $\Lambda_k^u \hookrightarrow \Lambda_{k+1}^u$ for $2 \le k < n$, from which we can conclude. In order to illustrate our proof, we suppose that $u = -n$ (other cases can be obtained by symmetry) and that $n = 5$ (but the arguments go through similarly in the general case).

Case $k = 0$. Suppose fixed a morphism $\phi : \Lambda^u \to C$. Given any triple of indices $0 \le i_0 < i_1 < i_2 < n$, there is an embedding $\lambda_{i_0, i_1, i_2} : \Lambda^{---} \hookrightarrow \Lambda^u$, sending a $k$-cube $v_0 v_1 v_2$ to the $k$-cube

$$w = +^{i_0} v_0 + (i_1 - i_0 - 1) v_1 + (i_2 - i_1 - i_0 - 2) v_2 + (n - 3 - i_2)$$
i.e. $w$ is obtained by inserting $v_0$, $v_1$ and $v_2$ at positions $i_0$, $i_1$ and $i_2$ respectively in the word constituted of $n-3$ letters “+”:

$$w_i = \begin{cases} v_{i_p} & \text{if } i = i_p \text{ for some } p \in \{0, 1, 2\} \\ + & \text{otherwise} \end{cases}$$

For instance, with $n=5$, we have $\lambda_{1,2,4}(v_0v_1v_2) = +v_0v_1+v_2$ and the image of $\lambda_{1,2,4}$ is shown on the left

<figure><img src="image_26.png" /></figure>

<figure><img src="image_27.png" /></figure>

By the cube property, the morphism $\Lambda^{---} \hookrightarrow \Lambda^u \xrightarrow{\phi} C$ extends to a morphism $\partial Y(n) \to C$ (i.e. in the case of $\lambda_{1,2,4}$, $C$ also contains the other half-cube shown on the right above) and into $Y^3$ by the unique 3-cube property. By the at most one square closing property (which holds by Lemma 1.27), the image of the image of the vertex $+^{n+1}$ thus defined does not depend on the indices $i_0, i_1, i_2$. For instance, the embeddings $\lambda_{1,2,4}$ and $\lambda_{0,2,3}$ can both be completed and both define an image for the vertex $++++$: the one defined by $\lambda_{1,2,4}$ is the same as the one defined by $\lambda_{1,2,3}$ (the completions share the face $+00+$), which in turn is the same as the one defined by $\lambda_{0,2,3}$ (the completions share the face $++00$). Similarly, the 1- and 2-cubes defined by multiples embeddings do not depend on the choice of the embedding. Therefore, the precubical complex $C$ lifts the embedding $\Lambda^u \hookrightarrow \Lambda_2^u$. Finally, by the at most one square closing property again, the lifting is unique.

Suppose given $k$ with $2 \le k < n$ and a morphism $\phi: \Lambda_k^u \to C$. For any $(k+1)$-uple of indices $0 \le i_0 < \dots < i_k < n$, there is an embedding $\lambda_{i_0, \dots, i_k}: \partial Y(k+1) \hookrightarrow \Lambda_k^u$ sending a cube $v \in \{-, 0, +\}^{k+1}$ to the cube $w \in \{-, 0, +\}^n$ defined by

$$w_i = \begin{cases} v_{i_p} & \text{if } i = i_p \text{ for some } p \in [k+1] \\ + & \text{otherwise} \end{cases}$$

By the unique $(k+1)$-cube property, the morphism $\partial Y(k+1) \hookrightarrow \Lambda_k^u \xrightarrow{\phi} C$ extends uniquely to a morphism $Y(k+1) \to C$. The precubical set $\Lambda_{k+1}^u$ can be obtained from $\Lambda_k^u$ by properly adding $(k+1)$-cubes: more precisely, one can easily check that $\Lambda_{k+1}^u$ is the colimit of the diagram of precubical sets

<figure><img src="image_28.png" /></figure>

where the $I_j$ range over subsets of cardinal $k+1$ of $[n]$. Therefore, by universal property of the colimit, the morphism $\phi$ extends uniquely to a morphism $\Lambda_{k+1}^u \to C$. $\square$
Notice that previous lemma also shows that the canonical embedding $\Lambda^u \hookrightarrow \partial Yn$ is lifted uniquely. When the precubical set is only supposed to be geometric, the lifting does not generally exists, but the proof can easily be adapted in order to show that it is necessarily unique (the particular case with $n=3$ was already noticed in Remark 1.25):

**Lemma 1.41.** Suppose given a geometric precubical set $C$. Given $n \in \mathbb{N}$ with $n \ge 3$ and $u \in \{-, +\}^n$, $C$ lifts at most once the canonical embedding $\Lambda^u \hookrightarrow \partial Yn$.

**Theorem 1.42.** A geometric precubical set $C$ is non-positively curved if and only if for every vertex $x \in C(0)$, the presimplicial set link$(x)$ is flag.

*Proof.* We first show the left-to-right implication and suppose that $C$ is non-positively curved. We show that for every vertex $x$ of $C$ the presimplicial set link$(x)$ lifts the inclusion $\partial Zn \hookrightarrow Zn$. Suppose fixed a presimplicial morphism $\partial Zn \to \text{link}(x)$. By Lemma 1.38, this amounts to fix a precubical morphism $\phi : \Lambda^u \to C$, for some $u \in \{-, +\}^n$, such that $\phi(u) = x$. By Lemma 1.40, this morphism extends uniquely to a morphism $\psi : Y(n) \to C$, satisfying $\psi(u) = x$, which corresponds by Lemma 1.38 to a morphism $Zn \to \text{link}(x)$.

We now show the right-to-left implication and suppose that link$(x)$ is flag for every vertex $x$ of $C$. We first show that $C$ satisfies the cube property. Suppose given $u \in \{-, +\}^3$ and a precubical morphism $\phi : \Lambda^u \to C$, by Remark 1.36 we want to show that it extends to a morphism $Y3 \to C$ (the uniqueness is granted by Remark 1.25). We write $x = \phi(u)$. By Lemma 1.38, the precubical morphism $\phi : \Lambda^u \to C$ corresponds to a presimplicial morphism $\partial Z2 \to \text{link}(x)$, which can be uniquely completed into a presimplicial morphism $Z2 \to \text{link}(x)$ since the link is flag, which corresponds to a morphism $Y3 \to C$ by Lemma 1.38, and therefore to a morphism $\partial Y3 \to C$ by precomposition with the inclusion $\partial Y3 \hookrightarrow Y3$. We now show that $C$ satisfies the unique $(n)$-cube property for $n \ge 2$. Suppose given a morphism $\phi : \partial Y(n) \to C$ and write $x = \phi(u)$ for some vertex $u$ of $\partial Y(n)$. By Lemma 1.38, the precubical morphism $\Lambda^u \hookrightarrow \partial Y(n) \xrightarrow{\phi} C$ corresponds to a presimplicial morphism $\partial Zn \to \text{link}(x)$, which extends to a presimplicial morphism $Zn \to \text{link}(x)$ because the link is flag, which in turn corresponds to a morphism $\psi : Y(n) \to C$ by Lemma 1.38. By Remark 1.39, we have that the morphisms $\Lambda^u \hookrightarrow \partial Y(n) \xrightarrow{\phi} C$ and $\Lambda^u \hookrightarrow Y(n) \xrightarrow{\psi} C$ coincide, therefore the morphisms $\phi$ and $\partial Y(n) \hookrightarrow Y(n) \xrightarrow{\psi} C$ also coincide by Lemma 1.41. Finally, the lifting is necessarily unique by Lemma 1.27. $\square$

### 1.3.4. 2-dimensional non-positively curved precubical sets

Interestingly, a precubical set $C$ satisfying the unique $n$-cube property, for every $n \ge 3$, is characterized by its underlying 2-precubical set $C_2$ (i.e. its image under the 2-truncation functor $\Box \to \Box_2$, see Definition 1.5). Higher-dimensional cubes can be recovered by a “completion” process: the 3-cubes can be recovered from $C_2$ by adding a 3-cube whenever $C_2$ contains the border of a cube (i.e. for every morphism $\partial Y3 \to C_2$), then the 4-cubes can be obtained by adding a 4-cube whenever the precubical set contains the border of a 4-cube, etc. More precisely, by general results about presheaf categories, we have

**Proposition 1.43.** The 2-truncation functor $\Box \to \Box_2$ admits a right adjoint $\Box_2 \to \Box$, and this adjunction restricts to an equivalence of categories between the category $\Box_2$ and the full subcategory of $\Box$ whose objects are precubical sets satisfying the unique $n$-cube property for every $n \ge 3$.
The image of a 2-precubical set under the right adjoint will be called its completion. All the constructions preformed here preserve the above equivalence. For instance, we could easily define a “2-precubical semantics” by adapting the definitions of Section 1.2 in order to associate a 2-precubical set to every program in the obvious way. It could then easily be shown that the completion of the 2-precubical semantics is isomorphic to the precubical semantics.

For this reason, we will mostly restrict, without loss of generality, to the underlying 2-precubical sets in the rest of the article. In this setting, the property of being geometric can be also reformulated by lifting properties, i.e. there is a reciprocal to Lemma 1.27.

**Definition 1.44.** Suppose given a 2-precubical set $C$.

- We say that a precubical set $C$ has no looping edge when there is no edge $x \in C(1)$ with the same source and target (i.e. $\partial^{-}(x) = \partial^{+}(x)$).

- We say that it has no folded square when for all squares $x \in C(2)$ we have $\partial^{--}(x) \neq \partial^{++}(x)$ and $\partial^{-+}(x) \neq \partial^{+-}(x)$.

- We say that is has no pinned squares when for all squares $x, y \in C(2)$, either
  $- \partial^{--}(x) = \partial^{--}(y)$ and $\partial^{++}(x) = \partial^{++}(y)$, or
  $- \partial^{+-}(x) = \partial^{+-}(y)$ and $\partial^{-+}(x) = \partial^{-+}(y)$
implies $x = y$.

A typical example of pinned square is given in Example 1.20.

**Lemma 1.45.** A 2-precubical set $C$ is geometric if and only if it has

(1) no looping edge,

(2) no folded square,

(3) no parallel edges,

(4) no pinned squares,

(5) and the at most one square closing property.

*Proof.* Suppose given a 2-precubical set $C$ satisfying the five above conditions. The first condition says precisely that $C$ has no self-intersecting edge. We now show that it has no self-intersecting square. Suppose given square $x \in C(2)$. Suppose that $x$ has two 0-faces which are equal: $\partial^{\epsilon_0 \epsilon_1}(x) = \partial^{\epsilon'_0 \epsilon'_1}(x)$. The case $\epsilon_0 \neq \epsilon'_0$ and $\epsilon_1 \neq \epsilon'_1$ is excluded because $C$ has no folded square. Therefore we can suppose $\epsilon_0 = \epsilon'_0$ (the case $\epsilon_1 = \epsilon'_1$ is similar). If $\epsilon_1 \neq \epsilon'_1$ then the edge $y = \partial^{\epsilon_0}(x)$ is looping, which is forbidden, therefore $\epsilon_1 = \epsilon'_1$ and the faces are not distinct. Suppose that $x$ has two 1-faces which are equal: $\partial_i^{\epsilon}(x) = \partial_i^{\epsilon'}(x)$. If $i = i'$ then $\epsilon = \epsilon'$, otherwise the edges $\partial_{1-i}^{-}(x)$ and $\partial_{1-i}^{+}(x)$ would both be looping. Suppose that $i \neq i'$, then it can easily be checked that this common face is a looping edge. The fact that $C$ satisfies the other conditions required for being geometric can be checked by case analysis in a similar way, and the converse implication is simple to check. $\square$

To sum up, in the rest of the paper, by a non-positively curved precubical set, we can thus mean the following:

**Definition 1.46.** A non-positively curved precubical set is a 2-precubical set which satisfies

(1) the five conditions of Lemma 1.45

(2) the cube property.
## 2. WHEN DIHOMOTOPY COINCIDES WITH HOMOTOPY

### 2.1. Homotopy and dihomotopy in precubical sets

As exposed in the introduction, one of the main contributions of this article is to show that homotopy coincides with its directed variant for paths in NPC precubical sets. We begin by formally introducing these equivalences on paths, which can be thought of as algebraic variants of the classical notion of homotopy between paths in algebraic topology. Since we will need to consider both directed and non-directed paths in precubical sets C, we will consistently use the following terminology in the remainder of the article. A *directed path* (or *dipath*) is a path in the underlying directed graph of C (i.e. what we have been simply calling a “path” up to now), and a *path* is a path in the underlying non-directed graph C (i.e. a sequence of composable transitions which might contain transitions taken backwards, that we call *reversed* transitions). We sometimes write $s : x \to y$ to indicate that $s$ is a path with $x$ as source and $y$ as target, and $id_x : x \to x$ for the empty path on $x$. The *length* $\|s\|$ of a path $s$ is the number of (possibly reversed) edges occurring in it. The concatenation of two paths $s : x \to y$ and $t : y \to z$ is written $s \cdot t : x \to z$, and the reversal of a path $s : x \to y$ is written $\bar{s} : y \to x$. By an edge (or a transition) $a : x \to y$, we will always denote a dipath of length one, and write $\bar{a} : y \to x$ for the corresponding reversed transition, unless we explicitly state that it can be possibly reversed, in which case we denote a path of length one.

We conservatively extend the definition relation $\diamond$ (Definition 1.6) from dipaths to paths: given a precubical set C, this relation is now defined as the smallest symmetric relation on paths of length 2 such that

$$ a \cdot b \diamond b' \cdot a' \qquad \bar{b} \cdot \bar{a} \diamond \bar{a}' \cdot \bar{b}' \qquad \bar{a} \cdot b' \diamond b \cdot \bar{a}' \qquad \bar{b}' \cdot a \diamond a' \cdot \bar{b} \qquad (2.1) $$

whenever there is a square

<figure><img src="image_29.png" /></figure>

in C.

**Definition 2.1.** Given a precubical set C, the **dihomotopy** relation $\sim$ on paths is the smallest congruence wrt concatenation containing $\diamond$. A *dihomotopy step* is a dihomotopy between two paths using only one of the four above relations (2.1) in context. The **homo-** **topy** relation $\sim$ on paths is the smallest congruence containing $\sim$ and such that for every edge $a : x \to y$ we have

$$ a \cdot \bar{a} \sim \mathrm{id}_x \qquad \bar{a} \cdot a \sim \mathrm{id}_y \qquad (2.3) $$

A *homotopy step* is a homotopy reduced to one of the six relations (2.1) and (2.3) in context.

For geometric precubical sets, the notion of (di)homotopy coincides with the usual topological one through the geometric realization, see Section 2.3.3 and [14].

By definition of the axioms defining dihomotopy, we have the following properties.

**Lemma 2.2.** *Two dihomotopic paths have the same length.*
**Lemma 2.3.** *A path which is dihomotopic to a dipath is necessarily a dipath.*

These notions allow us to introduce variants of the well-known construction of fundamental
groupoid in algebraic topology.

**Definition 2.4.** Given a precubical set $C$, its **fundamental groupoid** $\Pi_1(C)$ is the category whose objects are vertices and morphisms are paths up to homotopy, and its **fundamental category** $\bar{\Pi}_1(C)$ is the category whose objects are vertices and morphisms are dipaths up to dihomotopy.

Since the relations (2.3) are precisely those required for every transition $a$ to admit $\bar{a}$ as
inverse, it is not hard to show that

**Lemma 2.5.** *Given a precubical set *C*, the category *Π*₁(*C*) is the free groupoid over the category *Π*₁(*C*).*

By definition, two dipaths which are dihomotopic are homotopic. The main goal of
Section 2.2 is to show that for precubical sets satisfying the cube property, the converse is
true and both relations thus coincide (Theorem 2.29).

**Example 2.6.** Consider the standard hollow cube $\partial Y_3$ without the “bottom” face $0-0$, first considered in [13]:

<figure><img src="image_30.png" /></figure>

The two external paths $-0 \cdot 0-+$ and $0--+0$ are homotopic (as detailed in Example 2.15),
but not dihomotopic (each of those two paths is dihomotopic only to itself). Notice that
this precubical set does not satisfy the cube property.

We will also see in Section 3 that our algebraic conditions for NPC precubical sets are
closely related to those characterizing non-positively curved metric spaces in the traditional
sense. Those spaces are locally geodesic: in our context, a counterpart of this notion can be
defined as follows.

**Definition 2.7.** A path $s$ is locally geodesic if it is not dihomotopic to a path of the form $s' \cdot a \cdot \bar{a} \cdot s''$ or $s' \cdot \bar{a} \cdot a \cdot s''$. It is geodesic if every path homotopic to it has a greater or equal length.

By Lemma 2.3, since the dihomotopy class of a dipath contains only dipaths, the situation
of previous definition can never occur:

**Lemma 2.8.** Every dipath is locally geodesic.

Clearly, a geodesic path is locally geodesic, but the reciprocal is not generally true.

**Example 2.9.** Consider again the hollow cube without bottom face introduced in Example 2.6. The “loop around the hole”, i.e. the path $-0 \cdot 0-+ \cdot +-0 \cdot \overline{0}-$, is locally geodesic. However it is not geodesic, since it is homotopic to the identity path on the vertex $---$, which is strictly shorter.
## 2.2. A 2-categorical approach to dihomotopy in precubical sets

In this section, we reuse and extend the rewriting techniques developed by Lafont [36] for presenting monoidal categories, and the subsequent developments in the second author's PhD thesis [41, 42], in order to show one of the main results of this article: homotopy and dihomotopy relations coincide for directed paths in NPC precubical sets (Theorem 2.29). This will be done by rewriting homotopies between paths into a canonical form, which is always a dihomotopy when the two paths are directed.

### 2.2.1. *The fundamental 2-category and 2-groupoid of a precubical set*

In the following, we suppose fixed a 2-precubical set $C$ which satisfies:

(1) the at most one square closing property,

(2) the cube property,

(3) for any square $\bar{a} \cdot a' \diamond b \cdot \bar{b}'$ as in (2.2), we have $a = a'$ if and only if $b = b'$.

In particular any NPC precubical set (see Definition 1.46) satisfies those conditions, which is our main object of interest here, but the results of this section hold in this more general context. To such a precubical set, we can canonically associate two distinct 2-categories respectively defined as follows, which are 2-dimensional refinements of the categories introduced in Definition 2.4. The precise way in which those are generalizations is given in Lemma 2.18.

In classical algebraic topology, the fundamental groupoid $\Pi_1(X)$ of a topological space is constructed as the category with, as objects, the points of $X$, and as morphisms, the 1-tracks, or paths modulo homotopy. A direct generalization is that of the fundamental bicategory, where points are still 0-cells, paths are 1-cells and 2-tracks or homotopies relative end points modulo higher homotopies are 2-cells [29]. Composition in dimension 2, i.e. vertical composition is associative and even groupoidal (every 2-cell has an inverse), but composition in dimension 1 is a little less well-behaved: composition is only associative up to some 2-cells. Hence the natural structure of weak 2-category, or bicategory. In dimension one also, the fundamental bicategory has all its 1-cells being invertible (up to coherent 2-cells again), hence is a bigroupoid. For Hausdorff spaces, it is possible to construct directly a fundamental 2-groupoid (hence a strict version) [28], which is biequivalent to the fundamental bigroupoid. We follow an equivalent approach here, in defining a fundamental 2-category and fundamental 2-groupoid, but based on a combinatorial structure, instead of a topological structure.

**Definition 2.10.** The fundamental 2-category $\vec{\Pi}_2(C)$ associated to $C$ is the 2-category whose

- 0-cells are the vertices of $C$,

- 1-cells are generated by (non-reversed) edges of $C$: 1-cells are dipaths in $C$ and composition is given by concatenation,

- 2-cells are freely generated by

$$ \gamma_{b',a'}^{a,b} : a \cdot b \Rightarrow b' \cdot a' $$

whenever $a, b, a', b'$ are transitions such that $a \cdot b \diamond b' \cdot a'$, and quotiented by the smallest congruence (wrt both compositions) such that

$$ (\gamma_{c'',b''}^{b',c'} \circ \mathrm{id}_{a''}) \circ (\mathrm{id}_{a'} \cdot \gamma_{c',a''}^{a',c}) \circ (\gamma_{b',a'}^{a,b} \cdot \mathrm{id}_c) = (\mathrm{id}_{c''} \cdot \gamma_{b'',a''}^{a''',b'''}) \circ (\gamma_{c'',a''}^{a,c'''} \cdot \mathrm{id}_{b'''}) \circ (\mathrm{id}_a \cdot \gamma_{c'',b''}^{b,c}) $$
$$ \gamma_{a,b}^{b',a'} \circ \gamma_{b',a'}^{a,b} = \mathrm{id}_{a,b} \qquad (2.4) $$

for transitions such that all the involved morphisms are defined. Graphically,

<figure><img src="image_31.png" /></figure>

The horizontal composition will be denoted as concatenation (·), in sequential order, whereas the vertical composition will be denoted as usual (◦), in categorical order, thus following the usual convention for monoidal categories.

**Remark 2.11.** In the 2-category $\vec{\Pi}_2(C)$, if $\gamma_{b',a'}^{a,b}$ is defined, then the transitions $a'$ and $b'$ are uniquely determined from $a$ and $b$ because $C$ satisfies the at most one square closing property. Moreover, if $\gamma_{b',a'}^{a,b}$ is defined then $\gamma_{a,b}^{a',b'}$ is also defined, and is an inverse for $\gamma_{b',a'}^{a,b}$ by (2.4): in fact, the 2-category is a category enriched in groupoids.

**Lemma 2.12.** Two dipaths $f, g: x \to y$ in $C$ are dihomotopic if and only if there exists a 2-cell $\alpha: f \Rightarrow g$ in $\vec{\Pi}_2(C)$.

**Definition 2.13.** The fundamental 2-groupoid $\Pi_2(C)$ associated to $C$ is the 2-category whose

- 0-cells are the vertices of $C$,

- 1-cells are generated by edges of $C$ or their reverse: 1-cells are paths in $C$ and composition is given by concatenation,

- 2-cells are freely generated by

$$ \gamma_{b',a'}^{a,b} : a \cdot b \Rightarrow b' \cdot a' $$

whenever $a, b, a', b'$ are possibly reversed transitions such that $a \cdot b \diamond b' \cdot a'$, and

$$ \eta_a : \mathrm{id}_x \Rightarrow a \cdot \bar{a} $$

$$ \varepsilon_a : \bar{a} \cdot a \Rightarrow \mathrm{id}_y $$

whenever $a: x \to y$ is a possibly reversed transition, and quotiented by the smallest congruence (wrt both compositions) such that

$$ (\gamma_{c'',b''}^{b',c'} \circ \mathrm{id}_{a''}) \circ (\mathrm{id}_{a'} \cdot \gamma_{c'',a''}^{a',c}) \circ (\gamma_{b',a'}^{a,b} \cdot \mathrm{id}_c) = (\mathrm{id}_{c''} \cdot \gamma_{b'',a''}^{a''',b'''}) \circ (\gamma_{c'',a''}^{a,c'''} \cdot \mathrm{id}_{b'''}) \circ (\mathrm{id}_a \cdot \gamma_{c''',b'''}^{b,c}) \qquad (2.5) $$

$$ \gamma_{a,b}^{b',a'} \circ \gamma_{b',a'}^{a,b} = \mathrm{id}_{a,b} \qquad (2.6) $$

$$ (\mathrm{id}_a \cdot \varepsilon_a) \circ (\eta_a \cdot \mathrm{id}_a) = \mathrm{id}_a \qquad (2.7) $$

$$ (\varepsilon_a \cdot \mathrm{id}_{\bar{a}}) \circ (\mathrm{id}_{\bar{a}} \cdot \eta_a) = \mathrm{id}_{\bar{a}} \qquad (2.8) $$
$$ \varepsilon_{\bar{a}} \circ \eta_a = \mathrm{id}_{\mathrm{id}} \qquad (2.9) $$

$$ \gamma_{\overline{a'}, a'}^{a, \bar{a}} \circ \eta_a = \eta_{a'} \qquad (2.10) $$

$$ \varepsilon_{a'} \circ \gamma_{\overline{a'}, a'}^{a, \bar{a}} = \varepsilon_{\bar{a}} \qquad (2.11) $$

$$ (\gamma_{b,a'}^{a,b'} \cdot \mathrm{id}_{\overline{a'}}) \cdot (\mathrm{id}_a \cdot \gamma_{b',a'}^{\bar{a},b}) \circ (\eta_a \cdot \mathrm{id}_b) = \mathrm{id}_b \cdot \eta_{a'} \qquad (2.12) $$

$$ (\mathrm{id}_{a'} \cdot \gamma_{\overline{a'}, b}^{b', \bar{a}}) \circ (\gamma_{a', b'}^{b, a} \cdot \mathrm{id}_{\overline{a}}) \circ (\mathrm{id}_b \cdot \eta_a) = \eta_{a'} \cdot \mathrm{id}_b \qquad (2.13) $$

$$ (\varepsilon_{a'} \cdot \mathrm{id}_b) \circ (\mathrm{id}_{\overline{a'}} \cdot \gamma_{a', b}^{b', a}) \circ (\gamma^{b, \bar{a}} \cdot \mathrm{id}_a) = \mathrm{id}_b \cdot \varepsilon_a \qquad (2.14) $$

$$ (\mathrm{id}_b \cdot \varepsilon_{a'}) \circ (\gamma_{b,a'}^{\bar{a},b'} \cdot \mathrm{id}_{a'}) \circ (\mathrm{id}_{\bar{a}} \cdot \gamma_{b',a'}^{a,b}) = \varepsilon_a \cdot \mathrm{id}_b \qquad (2.15) $$

for possibly reversed transitions $a, a', a'', b, b', b'', c, c', c''$ such that all the involved morphisms are defined.

In string diagrammatic notation, the generators are drawn as

<figure><img src="image_32.png" /></figure>

or often simply as

<figure><img src="image_33.png" /></figure>

and the relations of Definition 2.13 can be pictured as

<figure><img src="image_34.png" /></figure>
$$ \begin{array}{ccc} \bar{a} & = & a \\ \swastika[3]_{a} \quad \bar{a} \quad \swastika[3]_{a} \end{array} $$

$$ a \circled{=} \bar{a} $$

$$ a \quad \bar{a} \quad = \quad \begin{array}{c} \swastika[3] \\ \bar{a}' \quad a' \end{array} $$

$$ \begin{array}{ccc} a & b & a \\ \swastika[3]_{a} & b' & a' \end{array} = \begin{array}{ccc} b & & a' \\ b & & a' \end{array} $$

$$ \begin{array}{ccc} b & a & a' \\ \swastika[3]_{b'} & a' & a' \end{array} = \begin{array}{ccc} b & & a' \\ b & & a' \end{array} $$

$$ \begin{array}{ccc} \bar{a} & = & a \\ \swastika[3]_{\bar{a}} \quad \bar{a} \quad \swastika[3]_{\bar{a}} \end{array} $$

$$ \begin{array}{ccc} a & \bar{a} & a' \\ \swastika[3]_{a'} & a' & a' \end{array} = \begin{array}{ccc} a & \bar{a} & a' \\ \swastika[3]_{a'} & a' & a' \end{array} $$

$$ \begin{array}{ccc} a & b & a' \\ \swastika[3]_{a} & b' & a' \end{array} = \begin{array}{ccc} a' & & a' \\ a' & & a' \end{array} $$

$$ \begin{array}{ccc} \bar{a} & a & b \\ \swastika[3]_{\bar{a}} & b' & a' \end{array} = \begin{array}{ccc} \bar{a} & a & b \\ \swastika[3]_{\bar{a}} & a' & b' \end{array} $$

By definition of the generating 2-cells, we have that

**Lemma 2.14.** Two paths $f, g: x \to y$ in $C$ are homotopic if and only if there exists a 2-cell $\alpha: f \Rightarrow g$ in $\Pi_2(C)$.

**Example 2.15.** In the hollow cube without bottom $C$ of Example 2.6, the fact that the two paths $f = --0 \cdot 0-+$ and $g = 0-- \cdot +-0$ are homotopic is witnessed by the following 2-cell
$\phi : f \Rightarrow g$ in $\Pi_2(C)$ (drawn from left to right instead of top to bottom for space constraints):

<figure><img src="image_35.png" /></figure>

Of course, this precubical set does not satisfy our assumptions, but we could still define a fundamental 2-category, excepting that some members of the equations may not be defined. We allow ourselves to consider it in this example only, for illustrative purposes.

**Proposition 2.16.** The following relations are derivable for 2-cells in $\Pi_2(C)$:

$$ (\gamma_{a,b'}^{b,a'} \cdot \mathrm{id}_{\overline{a'}}) \circ (\mathrm{id}_b \cdot \eta_{a'}) = (\mathrm{id}_a \cdot \gamma_{b',\overline{a'}}^{\overline{a},b}) \circ (\eta_a \cdot \mathrm{id}_b) \quad (2.16) $$

$$ (\mathrm{id}_{b'} \cdot \varepsilon_{a'}) \circ (\gamma_{b',a'}^{\overline{a},b} \cdot \mathrm{id}_{a'}) = (\varepsilon_a \cdot \mathrm{id}_{b'}) \circ (\mathrm{id}_{\overline{a}} \cdot \gamma_{a,b'}^{b,a'} ) \quad (2.17) $$

$$ (\varepsilon_{a'} \cdot \mathrm{id}_a) \circ (\mathrm{id}_{\overline{a'}} \cdot \gamma_{a',a}^{a',a}) \circ (\eta_{\overline{a'}} \cdot \mathrm{id}_a) = \mathrm{id}_a \quad (2.18) $$

(when the involved morphisms are defined). Graphically,

<figure><img src="image_36.png" /></figure>

*Proof.* We provide graphical derivations for the first and third relations:

<figure><img src="image_37.png" /></figure>

It can easily be checked that the intermediate morphisms are always defined when the first and last one are. For instance, the equational derivation of the first relation is

$$ (\gamma_{a,b'}^{b,a'} \cdot \mathrm{id}_{\overline{a'}}) \circ (\mathrm{id}_b \cdot \eta_{a'}) = (\mathrm{id}_a \cdot \gamma_{b',\overline{a'}}^{\overline{a},b}) \circ (\mathrm{id}_a \cdot \gamma_{\overline{a},b}^{b',\overline{a}'}) \circ (\gamma_{a,b'}^{b,a'} \cdot \mathrm{id}_{\overline{a'}}) \circ (\mathrm{id}_b \cdot \eta_{a'}) = (\mathrm{id}_a \cdot \gamma_{b',\overline{a'}}^{\overline{a},b}) \circ (\eta_a \cdot \mathrm{id}_b) $$
Since $\gamma_{a,b'}^{b,a'}$ is supposed to be defined, we have $b \cdot a' \diamond a \cdot b'$ in $C$ and therefore the morphisms $\gamma_{\bar{a},b}^{b',\bar{a}'}$ and $\gamma_{b',a'}^{\bar{a},b}$ are also defined. The relation (2.17) is similar to (2.16). $\square$

**Remark 2.17.** The generators (for 0-, 1- and 2-cells) of $\tilde{\Pi}_2(C)$ are a subset of the generators of $\Pi_2(C)$ and similarly for relations. There is thus a canonical functor $\tilde{\Pi}_2(C) \to \Pi_2(C)$ exhibiting a quotient of $\tilde{\Pi}_2(C)$ as a subcategory of $\Pi_2(C)$. In the following we study some of the properties of this functor.

The interest of those 2-categories is that they respectively contain “more information” than the fundamental category and groupoid, in the following sense. Given a 2-category $C$, we write $\tilde{C}$ for the category with the 0-cells of $C$ as objects, and morphisms are the 1-cells of $C$ quotiented by the smallest equivalence relation identifying two 1-cells between which there exists a 2-cell.

**Lemma 2.18.** We have $\tilde{\Pi}_1(C) \cong \tilde{\Pi}_2(C)$ and $\Pi_1(C) \cong \tilde{\Pi}_2(C)$.

### 2.2.2. Rewriting homotopies as dihomotopies

By definition, the 2-cells of $\Pi_2(C)$ are equivalence classes of 2-cells in the free 2-category generated by the 2-cells $\gamma_{b',a'}^{a,b}$, $\eta_a$ and $\varepsilon_a$, quotiented by the equivalence relation $\equiv$ generated by the relations. An element of such an equivalence class is called a *formal 2-cell*. We say that a formal 2-cell $\phi$ *rewrites* to a 2-cell $\psi$, which we write $\phi \Rightarrow \psi$, when $\psi$ can be obtained from $\phi$ by iteratively replacing the left member of a relation in some context by the right member of the relation in the same context, where the relation is one of the eleven relations of Definition 2.13 or the three relations of Proposition 2.16. For instance the formal 2-cell on the left rewrites to the formal 2-cell on the right using the relation (2.6):

<figure><img src="image_38.png" /></figure>

More formally, we can introduce a 3-category with the above free 2-category as underlying 2-category, and 3-cells generated by the relations oriented from left to right, and we would have $\phi \Rightarrow \psi$ precisely when there exists a 3-cell from $\phi$ to $\psi$ in this 3-category. The interested reader can find a more detailed presentation of this construction in [43]. Notice that if $\phi$ and $\psi$ are two formal 2-cells such that $\phi \Rightarrow \psi$ then $\phi$ and $\psi$ are in the same equivalence class, moreover the following lemma ensures that rewriting a formal 2-cell will always produce a (well-defined) formal 2-cell:

**Lemma 2.19.** In Definition 2.13 and Proposition 2.16, if the left member of a relation is well-defined then the right member is also well-defined.

*Proof.* We show that when the left member of a relation is well-defined then the right member is also well-defined. The property is verified for (2.5) because $C$ is supposed to satisfy the cube property, and the right members of other relations of Definition 2.13 are always well-defined. For (2.16), if the left-member is well-defined then $\gamma_{a,b}^{b,a'}$ is, i.e. $b \cdot a' \diamond a \cdot b'$ in $C$, and therefore $\gamma_{b',a'}^{\bar{a},b}$ is well-defined. The case of (2.17) is similar, and the right-member of (2.18) is always defined. $\square$
We call a *slice* a formal 2-cell $\phi$ of the form $\phi = \mathrm{id}_f \cdot \alpha \cdot \mathrm{id}_g$ where $f, g$ are 1-cells and $\alpha$ is a generating 2-cell. A slice is thus a 2-cell constituted of a unique generator in identity context:

<figure><img src="image_39.png" /></figure>

Using the laws of 2-categories it is easy to show the following lemma, which will enable us to reason by induction on formal 2-cells:

**Lemma 2.20.** Any formal 2-cell $\phi$ can be expressed as a composite of slices: there exists slices $\phi_1, \dots, \phi_n$ such that $\phi = \phi_n \circ \dots \circ \phi_1$. Moreover, any two such decompositions have the same number of slices.

**Definition 2.21.** The number $n$ of slices in the decomposition of a formal 2-cell $\phi$ is called its length and is denoted $\|\phi\|$.

We first generalize the notation for the 2-cells $\gamma_{b',a'}^{a,b}$ as follows:

**Definition 2.22.** Given transitions $a, a'$ and 1-cells $f, f'$, we write $\gamma_{f',a'}^{a,f} : a \cdot f \Rightarrow f' \cdot a'$ for the 2-cell defined by induction on the length of $f$ by

– if $a : x \to y$ then

$$ \gamma_{\mathrm{id}_{x}, a}^{a, \mathrm{id}_{y}} = \mathrm{id}_{a} $$

– given transitions $a, b, a', b'$ such that $a \cdot b \diamond b' \cdot a'$, we have

$$ \gamma_{b' \cdot f', a''}^{a, b \cdot f} = (\gamma_{b'a'}^{a, b} \cdot \mathrm{id}_f) \circ (\mathrm{id}_{b'} \cdot \gamma_{f', a''}^{a', f}) $$

whenever $\gamma_{f',a''}^{a',f}$ is defined.

Graphically, we have

<figure><img src="image_40.png" /></figure>

As explained in the beginning of the section, we are going to show that every formal 2-cell can be rewritten into one of a particular form, called a canonical form. For those, we will be able to show that they are actually homotopies when the source and target are directed paths (Lemma 2.28) and conclude.

**Definition 2.23.** A formal 2-cell $\phi$ is a *canonical form* when it is of the form $\mathrm{id}_{\mathrm{id}_x}$ for some 0-cell $x$, what we write $Z_x$, or there exists a canonical form $\psi$ such that $\phi$ is of one of the four following forms:

$$ G_{f',a'}^{a,f,g} \psi = (\gamma_{f',a'}^{a,f} \cdot \mathrm{id}_g) \circ (\mathrm{id}_a \cdot \psi) $$

$$ H_{g',a'}^{f,a,g,h} \psi = (\mathrm{id}_{f \cdot a} \cdot \gamma_{g',a'}^{\bar{a},g} \cdot \mathrm{id}_h) \circ (\mathrm{id}_f \cdot \eta_a \cdot \mathrm{id}_{g \cdot h}) \circ \psi $$

$$ E^{a,f} \psi = (\varepsilon_a \cdot \mathrm{id}_f) \circ (\mathrm{id}_{\bar{a}} \cdot \psi) $$
for some transitions $a, a'$ and morphisms $f, f', g, g', h$. Graphically,

$Z_x =$

<figure><img src="image_41.png" /></figure>

<figure><img src="image_42.png" /></figure>

<figure><img src="image_43.png" /></figure>

The operations $G$, $H$ and $E$ on 2-cells are called *operators*. Notice that the operator $E^{a,f}$ transforms a 2-cell $\psi : f \Rightarrow \bar{a} \cdot g$ into a 2-cell $E^{a,f}\psi : a \cdot f \Rightarrow g$. Similarly, the “type” for other operators is

$$ G_{f',a'}^{a,f,g} : h \Rightarrow f \cdot g \rightsquigarrow a \cdot h \Rightarrow f' \cdot a' \cdot g $$

$$ H_{g',a'}^{f,a,g,h} : i \Rightarrow f \cdot g \cdot h \rightsquigarrow i \Rightarrow f \cdot a \cdot g' \cdot \bar{a}' \cdot h $$

$$ E^{a,f} : g \Rightarrow \bar{a} \cdot f \rightsquigarrow a \cdot g \Rightarrow f $$

We sometimes use the notation $I^{a,f}$ for the operator $G_{id,a,f}^{a,id,f}$:

$$ I^{a,f} \psi = G_{id,a,f}^{a,id,f} \psi = \mathrm{id}_a \cdot \psi = \left| \begin{array}{c|c} a & g \\ \hline a & f \end{array} \right. $$

and simply write $I^a$ when $f$ is clear from the context.

**Proposition 2.24.** Every formal 2-cell $\phi$ rewrites to a canonical form.

*Proof.* By induction on the length of $\phi$. If $\|\phi\| = 0$, then $\phi = \mathrm{id}_f = I^{a_1} \cdots I^{a_n} Z$ for some 1-cell $f = a_1 \cdots a_n$ and we conclude. Otherwise $\|\phi\| = n+1$, and by Lemma 2.20, $\phi$ admits a decomposition as $\phi = \sigma \circ \psi$ with $\|\psi\| = n$ and $\sigma$ is a slice, i.e. $\sigma = \mathrm{id}_f \cdot \alpha \cdot \mathrm{id}_g$ for some generating 2-cell $\alpha$ and 1-cells $f$ and $g$. By induction hypothesis, $\psi$ is equal to a canonical form, and we conclude by examining all the possible forms for the canonical form $\psi$ and the slice $\sigma$.

- Suppose that $\alpha = \eta_a$. Then $\phi = (\mathrm{id}_f \cdot \eta_a \cdot \mathrm{id}_g) \circ \psi = H_{id,a}^{f,a,id,g} \psi$.

- Suppose that $\alpha = \varepsilon_b$. We proceed by induction on $\psi$.
– Suppose that $\psi = G_{f',a'}^{a,f'',g'}\psi'$:

<figure><img src="image_44.png" /></figure>

Depending on $f$ and $g$, the following cases are possible.

– If $f' = f'_1 \cdot \bar{b} \cdot b \cdot f'_2$, $f = f'_1$ and $g = f'_2 \cdot a' \cdot g'$,

<figure><img src="image_45.png" /></figure>

where $\psi''$ is a canonical form obtained by induction.

– If $f' = f'_1 \cdot \overline{a'}$, $b = a'$, $f = f'_1$ and $g = g'$,

<figure><img src="image_46.png" /></figure>

where $\psi''$ is a canonical form obtained by induction.

– If $g' = \overline{a'} \cdot g'_2$, $b = \overline{a'}$, $f = f'$, $g = g'_2$,

<figure><img src="image_47.png" /></figure>

where $\psi''$ is a canonical form obtained by induction.

– If $g' = g'_1 \cdot \bar{b} \cdot b \cdot g'_2$

<figure><img src="image_48.png" /></figure>

where $\psi''$ is a canonical form obtained by induction.

– The cases where $\psi = H_{g',a'}^{f,a,g,h}\psi'$ and $\psi = E^{a,f}\psi'$ can be handled similarly by case analysis.

– The case where $\alpha = \gamma_{b',a'}^{a,b}$ can be handled similarly by case analysis.

<figure><img src="image_49.png" /></figure>
A canonical form is not, in general, a normal form. The following lemma shows that a canonical form of the form XEHY (where X and Y are composites of operators and we omit indices) can always be rewritten to a canonical form of the form XGY of XHEY, and XGHY to XHGY. By severely abusing notations, this can be summarized as

$EH \Rightarrow G \text{ or } HE$

$GH \Rightarrow HG$

From these relations, it is easy to show that if a canonical form contains a *H* (i.e. is of the form XHY) then it can be rewritten to one which contains a *H* in first position (i.e. of the form HX) and if it contains an *E* (i.e. is of the form XEY) then it can be rewritten to one of the form XEY where *Y* does not contain an *H*. This will be used in Lemma 2.28.

**Lemma 2.25.** *The following rewriting relations can be shown:*

(1) for every morphism $\phi : i \to g \cdot h$,

<figure><img src="image_50.png" /></figure>

(2) for every morphism $\phi : i \to b \cdot f \cdot g \cdot h$,

<figure><img src="image_51.png" /></figure>

(3) for every morphism $\phi : i \to f_1 \cdot f_2 \cdot g \cdot h$,

$$
G_{f_1, b'}^{b, f_1, f_2 \cdot a' \cdot g' \cdot a' \cdot h} H_{g', a'}^{f_1 \cdot f_2, a, g, h} \phi \Rightarrow H_{g', a'}^{f'_1 \cdot b' \cdot f_2, a, g, h} G_{f_1, b'}^{b, f_1, f_2 \cdot g \cdot h} \phi
$$
<figure><img src="image_52.png" /></figure>

(4) for every morphism $\phi : i \Rightarrow f \cdot g_1 \cdot g_2 \cdot h$

<figure><img src="image_53.png" /></figure>

(5) for every morphism $\phi : i \Rightarrow f \cdot g \cdot h_1 \cdot h_2$

<figure><img src="image_54.png" /></figure>

(in the last two cases the omitted indices can be inferred from the figure).

*Proof.* (1) is a direct application of relation (2.8), (2) and (3) are equalities (they follow from the exchange law in 2-categories), (4) and (5) can be shown by applying suitable sequence of rewriting, which can easily be guessed from the figures. $\square$
In the following, we sometimes omit the superscript and subscript indices of operators for simplicity. We say that a 1-cell $f$ contains a reversed transition when it can be written in the form $f = f_1 \cdot \bar{a} \cdot f_2$ where $\bar{a}$ is a reversed transition: a path $f$ is a dipath when it does not contain a reversed transition. Two possibly reversed transitions $a$ and $a'$ are said to have the same direction if they are both non-reversed or both reversed.

**Lemma 2.26.** In a 2-cell of the form $\gamma_{b',a'}^{a,b}$, the transitions $a$ and $a'$ (resp. $b$ and $b'$) have the same direction. In a 2-cell of the form $\gamma_{f',a'}^{a,f}$, the transitions $a$ and $a'$ have the same direction, and $f$ contains a reversed transition if and only if $f'$ does.

*Proof.* The first point is immediate by definition of $\gamma_{b',a'}^{a,b}$. This can easily be used to show the result on $\gamma_{f',a'}^{a,f}$ by induction on its definition (Definition 2.22). $\square$

**Lemma 2.27.** The source and target of a formal 2-cell in canonical form satisfy the following properties.

(1) A formal 2-cell of the form $H\phi$ necessarily contains a reversed transition in its target.

(2) $Z$ contains no reversed transition in its source or its target.

(3) $G\phi$ contains a reversed transition in its target if and only if either it contains a reversed transition in its source or $\phi$ contains a reversed transition in its target.

(4) A formal 2-cell of the form $EX$ where $EX$ consists of operators within $\{Z, E, G\}$ necessarily contains a reversed transition in its source.

*Proof.* The properties can be shown as follows.

(1) The target of a formal 2-cell $H_{a',g'}^{f,a,g,h}$ is $f \cdot a \cdot g' \cdot \bar{a}' \cdot h$ and thus contains a reversed transition since it contains both $a$ and $\bar{a}'$, and $a$ and $a'$ have the same direction (this follows easily from Lemma 2.26).

(2) The source (resp. target) of $Z$ is an empty path.

(3) Consider $G_{f',a'}^{a,f,g}\phi : a \cdot h \Rightarrow f' \cdot a' \cdot g$ with $\phi : h \Rightarrow f \cdot g$, where $G_{f',a'}^{a,f,g}\phi = (\gamma_{f',a'}^{a,f} \cdot \mathrm{id}_g) \circ (\mathrm{id}_a \cdot \phi)$. If the transition $a'$ is reversed then $a$ is also reversed and we conclude. Otherwise, either $f'$ or $g$ contains a reversed transition. If it the case for $g$ then $\phi$ contains a reversed transition in its target. Otherwise $f'$ contains a reversed transition and thus also $f$ by previous lemma. The converse implication is similar.

(4) It is enough to show the property in the case where $X$ is of the form $X = GG...GZ$ because if $EX$ contains a reversed transition in its source then so does $EX'EX$. Consider $E^{a,f}\phi : \bar{a} \cdot g \Rightarrow f$ with $\phi : g \to a \cdot f$, if $a$ not reversed then $E^{a,f}\phi$ contains the reversed transition $\bar{a}$ in its source. Otherwise $\phi$ contains a reversed transition in its target and is of the form $GG...GZ$. By an easy induction, using the two previous cases, it thus contains a reversed transition in its source. The converse implication is similar. $\square$

**Lemma 2.28.** Suppose given a formal 2-cell $\phi : f \Rightarrow g$ whose source $f$ and target $g$ are dipaths (i.e. do not contain reversed transitions). Then $\phi$ rewrites to a formal 2-cell which is a composite of generators not involving generators of the form $\eta_a$ and $\varepsilon_a$.

*Proof.* By Proposition 2.24, $\phi$ rewrites to a canonical form. This canonical form corresponds to a formal 2-cell involving a generator of the form $\eta_a$ if and only if it contains an operator $H$. By Lemma 2.25, up to more rewriting, if the canonical form contains an operator $H$ we can always suppose that there is one placed at leftmost position. This situation is impossible because a morphism of the form $H\psi$ necessarily contains a reversed transition in its target
by Lemma 2.27. Similarly, the formal 2-cell involves a generator $\epsilon_a$ if and only if its canonical form contains an operator $E$. Up to rewriting more, we can always suppose that the canonical form is of the form $YEX$ where $X$ consists of operators not involving $H$. By Lemma 2.27, it thus contains a reversed transition in its source, contradicting the hypothesis. $\square$

**Theorem 2.29.** *Two dipaths in $C$ are homotopic if and only if they are dihomotopic.*

*Proof.* We show the left-to-right implication, the converse being obvious. Suppose that $f$ and $g$ are two homotopic dipaths. By Lemma 2.14, this means that there exists a 2-cell $\phi : f \Rightarrow g$ in $\Pi_2(C)$. This 2-cell $\phi$ is, by definition, an equivalence class of formal 2-cells under the relations defining fundamental 2-groupoids. Choose an arbitrary formal 2-cell $\psi$ in this equivalence class. By Lemma 2.28, $\psi$ rewrite to a formal 2-cell $\psi'$, which is still in the equivalence class $\phi$ by definition of rewriting, and does not involve generators $\eta$ or $\epsilon$. Therefore, the 2-cell $\phi$ is in the image of the canonical functor $\vec{\Pi}_2(C) \to \Pi_2(C)$ (see Remark 2.17), and there exists a dihomotopy from $f$ to $g$ by Lemma 2.12. $\square$

This can be formulated more categorically as follows.

**Theorem 2.30.** *The quotient functor $\vec{\Pi}_1(C) \to \Pi_1(C)$ is full and faithful.*

On a related note, a characterization of the embeddability of small categories into their groupoid completion is given in [31], and variants of the above theorem have also been investigated in more geometric contexts, see the references given in Section 3.2.4.

## 2.3. Extensions

In this section, we briefly comment on a few topics and extensions related to the preceding approach. We omit proofs, they should be detailed in subsequent works.

### 2.3.1. *The free compact closed category on a unidimensional object*

Given an NPC precubical set $C$, we have seen (Lemma 2.14) that homotopy corresponds to the existence of a 2-cell in $\Pi_2(C)$ and therefore the relations we put on 2-cells in the definition of $\Pi_2(C)$ do not really matter as long as they are well-defined (Lemma 2.19) and allow us to rewrite a homotopy between dipaths to a dihomotopy (Theorem 2.29). In this section, we advocate that our axioms are not completely arbitrary by showing that our construction encompasses the free compact closed category on a unidimensional object as a particular case.

We study here the particular case of the 2-category $C = \Pi_2(C)$ where $C$ is the precubical set with one vertex $x$, one edge $a : x \to x$ and one square $a \cdot a \diamond a \cdot a$:

<figure><img src="image_55.png" /></figure>

This will illustrate that our axioms for the category $\vec{\Pi}_2(C)$ constitute a variant of the well-known notion of compact-closed category. Since the 2-category $C$ has only one 0-cell, we can consider it as a monoidal category, with “.” as tensor product. It can be noticed that the
monoidal category $\mathcal{C}$ is symmetric (the symmetry being generated by $\gamma_{a,a}^{a,a} : a \cdot a \to a \cdot a$), and compact closed (with $\bar{a}$ being dual to $a$):

**Definition 2.31.** A symmetric monoidal category $(\mathcal{C}, \cdot, I)$ is *compact closed* when for every object $A \in \mathcal{C}$, there exists an object $A^* \in \mathcal{C}$, called the *dual* of $A$, together with two morphisms

$$ \eta_A : I \to A \cdot A^* \quad \text{and} \quad \varepsilon_A : A^* \cdot A \to A $$

such that

$$ (\mathrm{id}_A \cdot \varepsilon_A) \circ (\eta_A \cdot \mathrm{id}_A) = \mathrm{id}_A \qquad (\varepsilon_A \cdot \mathrm{id}_{A^*}) \circ (\mathrm{id}_{A^*} \cdot \eta_A) = \mathrm{id}_{A^*} $$

An object $A \in \mathcal{C}$ in such a category is *unidimensional* when $\varepsilon_A \circ \gamma_{A,A^*} \circ \eta_A = \mathrm{id}_I$.

**Example 2.32.** Consider the symmetric monoidal category **FDVect** of finite-dimensional vector spaces over a fixed field $\mathbb{k}$, equipped with the usual tensor product $\otimes$, the unit $I$ being $\mathbb{k}$ equipped with its canonical $\mathbb{k}$-vector space structure. This category is compact closed, the dual of a vector space $A$ being the space $A^*$ of linear functionals on $A$. Notice that given a linear map $f : A \to B$, the morphism $\mathrm{Tr}(f) : I \to I$ defined by $\mathrm{Tr}(f) = \varepsilon_{A^*} \circ (f \otimes \mathrm{id}_{A^*}) \circ \eta_A$ is the linear map $x \mapsto \mathrm{tr}(f)x$ where $\mathrm{tr}(f) \in \mathbb{k}$ is the trace of $f$ in the usual sense. In particular, given a space $A$, we have $\mathrm{tr}(\mathrm{id}_A) = \dim(A)$ and $\mathrm{Tr}(\mathrm{id}_A) = \mathrm{id}_I$ precisely when $A$ is of dimension 1 (we suppose that $\mathbb{k}$ is of null characteristic).

A converse to the preceding remark can be shown, and precisely formulated as follows. The proof of this result is not entirely obvious, and can be obtained as a variant of [32, 47].

**Proposition 2.33.** *The category $\mathcal{C}$ is the free compact closed category containing a unidimensional object.*

### 2.3.2. Convergence of the rewriting system

We conjecture that this rewriting system is convergent, i.e. both terminating and confluent. We believe that Guiraud's techniques based on derivations [27] can be used in order to show the termination of the rewriting system. Confluence is quite tedious to check. Because of the "Yang-Baxter" rule (2.5) there is an infinite number of critical pairs as discovered by Lafont [36]. We could still be able to handle those families of critical pairs (as done by Lafont), however this requires beforehand to establish the existence of canonical forms as we did in previous section: it would therefore require strictly more work than done here. As a byproduct of this result, we expect to be able to show that in $\Pi_2(\mathcal{C})$ (and therefore also in $\vec{\Pi}_2(\mathcal{C})$ by Theorem 2.30) there is at most one homotopy between any two paths (of course, when $\mathcal{C}$ satisfies the cube property and other hypothesis).

### 2.3.3. An axiomatization of homotopy between homotopies

As explained in detail in next section, one can interpret a precubical set $\mathcal{C}$ as a directed space $\upharpoonright \mathcal{C} \upharpoonright$ by taking its geometric realization (see Definition 3.72). It has been shown by Fajstrup [14] that two paths in $\mathcal{C}$ are dihomotopic (resp. homotopic) in $\mathcal{C}$ if and only if the corresponding paths in $\upharpoonright \mathcal{C} \upharpoonright$ are dihomotopic (resp. homotopic) in the geometric sense, i.e. our algebraic notion of (di)homotopy corresponds to the geometric one. We conjecture that this result extends one dimension higher, i.e. that two formal 2-cells in $\Pi_2(\mathcal{C})$ (resp. $\vec{\Pi}_2(\mathcal{C})$) are equal (i.e. in the same equivalence class modulo the relations) if and only if
the corresponding homotopies (resp. dihomotopies) in $\mathbb{1}C\mathbb{1}$ are homotopic, thus bringing a
geometric justification for our axiomatic definition of $\Pi_2(C)$ and $\bar{\Pi}_2(C)$.

3. A (GEO)METRIC APPROACH TO THE CUBE PROPERTY

The cube condition which is at the heart of the developments in previous sections is quite
reminiscent of Gromov’s condition for characterizing non-positively curved cubical com-
plexes [26]. In order to make the connection precise, one has to associate to every precubical
set a geodesic metric space (which is a cubical complex). Such a construction could be per-
formed abstractly as a geometric realization in the category of metric spaces if this category
were cocomplete... which is not the case. This leads us to investigate a generalization of the
notion of metric spaces (called *generalized metric spaces* [24] or *Lawvere metric spaces* [37]
or *hemi-metric spaces* [23]) which form a cocomplete category. Interestingly, these spaces
also allow one to encode a notion of “time direction” in the metric, as first noticed by Gran-
dis [25, 24], thus enabling one to formulate a metric semantics for concurrent programs,
which is not only able to encode the direction of time but also the duration of the elapsed
time during an execution. The use of non-positive curvature has been used by Ghrist in
order to study configuration spaces and cubical complexes [18, 17, 16].

In Section 3.1, we recall the definition of generalized metric spaces as well as associated
basic definitions and properties: the properties of the resulting category, the symmetric
variant of generalized metric spaces (which can be thought of as being “undirected”), the
topology induced by a metric, and the various notions of paths. In Section 3.2, we define
the realization of a precubical set as a metric space and show that the underlying topology
of the realization induced by the metric is the expected one: this means that considering
the metric bring more (as opposed to different) information compared to the usual case.
Finally, in Section 3.3, we recall the original definition of space with non-positive curvature,
and show that our definition corresponds with this one, through geometric realization.

The two main results are those in the end of Sections 3.2 and 3.3 (compatibility of the
metric with usual topology and correspondence of our axioms with the usual ones). We
do not claim much originality in this section, but we did our best to collect in a concise
way results which are disseminated in the literature or, worse, considered as folklore. The
reason why we have presented this here is to explain the inspiration for our axiomatics on
precubical sets, but none of the results in this paper depend on the geometric interpretation
of those axioms.

**3.1. Generalized metric spaces**

Recall that a *metric space* $(X, d)$ consists of a set $X$ equipped with a metric $d: X \times X \to [0, \infty)$,
i.e. a function such that, given $x, y, z \in X$, we have

(1) point equality: $d(x, x) = 0$

(2) triangle inequality: $d(x, z) \le d(x, y) + d(y, z)$

(3) finite distances: $d(x, y) < \infty$

(4) separation: $d(x, y) = d(y, x) = 0$ implies $x = y$

(5) symmetry: $d(x, y) = d(y, x)$

Generalized metric space are defined similarly, but only keeping the two first conditions:
**Definition 3.1.** A generalized metric space $(X, d)$ consists of a set $X$ equipped with a function $d: X \times X \to [0, \infty]$, called generalized *metric* or *distance*, such that, given $x, y, z \in X$, we have

$$ (1) \quad \text{point equality: } d(x, x) = 0 $$

$$ (2) \quad \text{triangle inequality: } d(x, z) \le d(x, y) + d(y, z) $$

A morphism $f: (X, d_X) \to (Y, d_Y)$ between two such spaces is a function $f: X \to Y$ which is *nonexpansive* (does not increase distance): for every $x, y \in X$, $d_Y(f(x), f(y)) \le d_X(x, y)$. We write **GMet** for the *category of generalized metric spaces* and their morphisms.

By a *space* we will always mean an object in this category, unless we explicitly state that the space is “non-generalized”. It was observed by Lawvere [37] that it can alternatively be defined as the category of categories and functors enriched over the posetal category $\mathcal{V} = [0, \infty]$ (with an arrow $x \to y$ whenever $x \ge y$) equipped with the monoidal structure induced by addition. Our main interest in considering this category instead of the full subcategory of (usual) metric spaces is double. Firstly, removing conditions (3) and (4) makes the category much more well-behaved (the category of generalized metric spaces has small colimits, which is not the case for metric spaces). Of course, we generally work with separated $(T_0)$ spaces and we will have to show that colimits we obtain from such spaces are still separated. Secondly, removing condition (5) allows us to encode a notion of direction of the space: intuitively, a point $x$ is really “before” a point $y$ whenever the distance $d(x, y)$ is finite and $d(y, x) = \infty$.

**Example 3.2.** Given $a, b \in \mathbb{R}$, we write $[a, b]$ for the interval equipped with the usual metric given by $d(x, y) = |y - x|$. We write $\overrightarrow{[a, b]}$ for the same interval metrized by

$$ d(x, y) = \begin{cases} y - x & \text{if } y \ge x \\ \infty & \text{if } y < x \end{cases} $$

In particular, we often write $I$ (resp. $\vec{I}$) instead of $[0, 1]$ (resp. $\overrightarrow{[0, 1]}$) for the (*directed*) *standard interval*. Similarly, we write $\mathbb{R}$ (resp. $\vec{\mathbb{R}}$) for the (*directed*) *real line*, which is also sometimes called the *Sorgenfrey line* [52, 23].

**Example 3.3.** The *directed unit circle* $\vec{\mathbb{S}}^1$ is the set of complex points of the form $e^{i2\pi\theta}$, with $\theta \in \mathbb{R}$, equipped with the distance $d(x, y) = \angle\{\rho - \theta \mid x = e^{i2\pi\theta}, y = e^{i2\pi\rho}, \rho \ge \theta\}$.

**Definition 3.4.** An *isometry* $f: X \to Y$ is a distance-preserving morphism, i.e. satisfies $d_Y(f(x), f(x')) = d_X(x, x')$ for every $x, x' \in X$.

**Remark 3.5.** Isomorphisms in **GMet** are isometries.

**Lemma 3.6.** Suppose given an isometry $f: X \to Y$. For every $x, y \in X$, we have $f(x) = f(y)$ implies $d(x, y) = 0 = d(y, x)$. In particular, when $X$ separated $f$ is injective, and we write $f^{-1}(y)$ for the unique antecedent of $y \in Y$ under $f$.

We write $d_0$ for the constant distance equal to 0 and $d_\infty$ for the distance such that $d(x, x) = 0$ and $d(x, y) = \infty$ for $x \ne y$.
### 3.1.1. Limits and colimits

We now show that the category of generalized metric spaces has all limits and colimits and describe how to explicitly construct those. These are also studied in [24, 23].

**Proposition 3.7.** The category **GMet** is complete and cocomplete. Moreover, the forgetful functor **GMet** $\to$ **Set** admits both a left and a right adjoint and thus preserves limits and colimits.

*Proof.* Since the category $\mathcal{V}$ is complete and cocomplete, with products (resp. coproducts) being given by supremum (resp. infimum), by general results about enriched categories [4], the category **GMet** = $\mathcal{V}$-Cat has small limits and colimits. The left (resp. right) adjoint to the forgetful functor **GMet** $\to$ **Set** is the functor which to a set $X$ associates the generalized metric space $(X, d_0)$ (resp. $(X, d_\infty)$). The underlying set of a limit of metric spaces is thus the limit of the underlying sets and similarly for colimits. $\square$

Limits and colimits can be constructed explicitly as follows. It is well-known that it is enough to construct all (co)products and (co)equalizers to construct all (co)limits.

**Lemma 3.8.** Given a family $(X_i, d_i)_{i \in I}$ of metric spaces, its product (resp. coproduct) is the set $\coprod_{i \in I} X_i$ (resp. $\prod_{i \in I} X_i$), respectively equipped with the distances

$$d_{\coprod X_i}((x_i), (y_i)) = \bigvee_{i \in I} d_i(x_i, y_i) \qquad d_{\prod X_i}(x, y) = \begin{cases} d_i(x, y) & \text{if } x, y \in x_i \\ \infty & \text{otherwise} \end{cases}$$

**Lemma 3.9.** Given a pair of morphisms $f, g : (X, d_X) \to (Y, d_Y)$, their equalizer is the equalizer set $Z = \{x \in X \mid f(x) = g(x)\}$ equipped with the restriction of $d_X$ as distance.

**Lemma 3.10.** Given a pair of morphisms $f, g : (X, d_X) \to (Y, d_Y)$, the coequalizer of $f$ and $g$ is the set $Y/\approx$, where $\approx$ is the smallest equivalence relation such that $y \approx y'$ whenever there exists $x \in X$ with $y = f(x)$ and $y' = g(x)$, equipped with the following distance. Given two points $x, y \in Y$, a "chain" from $x$ to $y$ is a sequence of points $x_1, y_1, x_2, y_2, \dots, x_n, y_n \in Y$ such that $x = x_1, y_i \approx x_{i+1}$, and $y_n = y$. The length of such a chain $u$ is defined to be $l(u) = \sum_{i=1}^n d(x_i, y_i)$. The distance between two points $x, y \in Y/\approx$ is the infimum of the lengths of chains from a representative of $x$ to a representative of $y$ (in fact, it does not depend on the choice of representatives for $x$ and $y$).

**Remark 3.11.** With the notations of previous lemma, given $x, y \in Y$, the sequence $x, y$ is a chain from $x$ to $y$ and thus $d_{Y/\approx}(x, y) \le d_Y(x, y)$.

**Example 3.12.** The directed circle (see Example 3.3) can be constructed from $\overrightarrow{[0, 1]}$ as a colimit, by identifying the points 0 and 1.

**Example 3.13.** Consider the spaces $(I_n, d_n)$ indexed by $n \in \mathbb{N}$ with $I_n = [0, 1]$ and distance $d_n(x, y) = |y - x|/n$. The colimit $I_\omega = \coprod_{n \in \mathbb{N}} /\approx$ where $\approx$ identifies points 0, resp. 1, in various $I_n$ is the colimit of the sets equipped with the distance $d_\omega$ such that given $x \in I_n$ and $y \in I_m$,

$$d_\omega(x, y) = \begin{cases} 0 & \text{if } x, y \in \{0, 1\} \\ |y - x|/n & \text{if } n = m \\ (x/n + y/m) \vee ((1-x)/n + (1-y)/m) & \text{otherwise} \end{cases}$$
In particular, we have $d_\omega(0, 1) = 0$, which shows that coequalizers of separated spaces are not necessarily separated. Notice that, in the space $I_\omega$, if we “cut in the middle” all the intervals we obtain two “star-shaped” spaces which are both separated. The space $I_\omega$ can then be obtained as a pushout of the two spaces (over the discrete space with $\mathbb{N}$ as points), showing that separated spaces are not either closed under pushouts.

**Remark 3.14.** Since the category **GMet** is cocomplete, we can easily mimic the definitions of Section 1.2 in order to associate a generalized metric space to each program. We do not detail this here, because we will be able to reuse the precubical semantics and realize it as a space, see Section 3.2, instead of starting all over again. In particular, an action in this semantics will typically be realized as a directed unit interval $\vec{I}$ (see Example 3.2): this corresponds to the intuition that executing an action is a directed process and takes « one unit of time » (but of course, other duration choices could be made depending on the nature of the actions, as illustrated in next remark). Moreover, parallel composition is naturally interpreted as product of metric spaces: the time taken to execute two programs in parallel is the maximum of both execution times.

**Remark 3.15.** In order to illustrate why removing the separation axiom makes sense in this context, consider the action **nop**, which is instantaneously executed and does nothing. This particular action is most naturally modeled as $(I, d)$, with $d(x, y) = 0$ for $x \le y$ and $d(y, x) = \infty$ otherwise (but other actions are still modeled as $\vec{I}$). For instance, the geometric semantics of a program of the form $A^*$, where $A$ is some action, would be a space of the form

<figure><img src="image_56.png" /></figure>

In this space, we have $d(x, y) = 0$ and $d(y, x) = 1$; it is thus neither separated nor symmetric. Similarly, $nop^*$ provides an example of a non-trivial space (non-contractible in particular) equipped with the constant null distance $d_0$.

Because our spaces are not supposed to be separated, it will sometimes be useful to consider the following kind of quotient.

**Definition 3.16.** Given a space $X$, an equivalence relation $\approx$ on $X$ is called *instantaneous* when $x \approx y$ implies $d(x, y) = 0$ for every $x, y \in X$.

**Lemma 3.17.** Given a space $X$ and a instantaneous equivalence relation $\approx$, the quotient morphism $X \to X/\approx$ is an isometry.

*Proof.* The quotient space $X/\approx$ can be computed as the coequalizer of $\approx \rightrightarrows X$, where the two arrows are the projections of the relation $\approx \subseteq X \times X$. Given $x, y \in X$ and a chain $x_0, y_0, \dots, x_n, y_n$ with $x_0 = x, y_n = y$, by the triangle inequality we have

$$ \begin{aligned} d_X(x, y) &\le d(x_0, y_0) + d(y_0, x_1) + \dots + d(y_{n-1}, x_n) + d(x_n, y_n) \\ &= d(x_0, y_0) + d(x_1, y_1) + \dots + d(x_{n-1}, y_{n-1}) + d(x_n, y_n) \end{aligned} $$

and therefore $d_X(x, y) \le d_{X/\approx}(x, y)$. Conversely, since $x, y$ is a chain, we have that $d_{X/\approx}(x, y) \le d_X(x, y)$. $\square$
In particular, given a generalized metric space $X$, the free separated space can be constructed as $X/\approx$, where $\approx$ is the smallest equivalence relation such that $d(x, y) = 0$ or $d(y, x) = 0$ implies $x \approx y$, for $x, y \in X$. The quotient map will be an isometry when the relation $\approx$ is instantaneous, i.e. when $d(x, y) = 0$ implies $d(y, x) = 0$. The colimits of non-generalized metric spaces usually considered in literature can be obtained from those described here by freely separating the resulting colimits.

### 3.1.2. Symmetric metric spaces

The category of spaces which are symmetric forms an interesting subcategory, in which most of the usual properties of (non-generalized) metric spaces are still valid. They are sometimes also called pseudo-metric spaces in the literature [55, 1, 33].

**Definition 3.18.** We write **SGMet** for the full subcategory of **GMet** whose object are symmetric generalized metric spaces, i.e. spaces $(X, d)$ such that $d(x, y) = d(y, x)$ for every $x, y \in X$.

The constructions of Proposition 3.7 are easily checked to preserve the symmetry of spaces:

**Lemma 3.19.** The category **SGMet** is complete and cocomplete.

**Remark 3.20.** Notice that given a symmetric space $(X, d)$ and $x, x', y, y' \in X$, we have

$$|d(x', y') - d(x, y)| \le |d(x', y') - d(x, y')| + |d(x, y') - d(x, y)| \le d(x, x') \lor d(y, y')$$
the last step using the well-known “reverse triangle inequality”. The distance $d$ can thus be seen as a morphism $d: X \times X \to [0, \infty)$ in **SGMet**.

Any generalized metric space can canonically be symmetrized in two ways as follows.

**Proposition 3.21.** The forgetful functor **SGMet** $\to$ **GMet** admits a left adjoint sending a space $(X, d)$ to the symmetric space $(X, \bar{d})$ where the metric $\bar{d}$ is called the symmetric metric generated by $d$ and is defined by

$$\bar{d}(x, y) = \bigwedge_{x=x_0, x_1, \dots, x_{2n}, x_{2n+1}=y} \sum_{i=0}^{n} d(x_{i+1}, x_i) + d(x_{i+1}, x_{i+2})$$

It also admits a right adjoint sending $(X, d)$ to the space $(X, d^\vee)$ where $d^\vee(x, y) = d(x, y) \lor d(y, x)$. The forgetful functor thus preserves limits and colimits.

**Example 3.22.** For instance, consider the directed plane $\mathbb{R}^2$, whose distance is given by $d((x_1, x_2), (y_1, y_2)) = d_{\mathbb{R}}(x_1, y_1) \lor d_{\mathbb{R}}(x_2, y_2)$, and $d_{\mathbb{R}}$ is described in Example 3.2. The left and right adjoint of the proposition respectively equip $\mathbb{R}^2$ with the distances $\bar{d}$ and $d^\vee$ such that

$$\bar{d}((x_1, x_2), (y_1, y_2)) = \begin{cases} |y_1 - x_1| \lor |y_2 - x_2| & \text{if } (y_1 - x_1)(y_2 - x_2) \ge 0 \\ |y_1 - x_1| + |y_2 - x_2| & \text{if } (y_1 - x_1)(y_2 - x_2) \le 0 \end{cases}$$

and

$$d^\vee((x_1, x_2), (y_1, y_2)) = \begin{cases} |y_1 - x_1| \lor |y_2 - x_2| & \text{if } (y_1 - x_1)(y_2 - x_2) \ge 0 \\ \infty & \text{if } (y_1 - x_1)(y_2 - x_2) \le 0 \end{cases}$$
**Remark 3.23.** For every points $x$ and $y$ in a generalized metric space $(X, d)$, we have $d(x, y) \ge \bar{d}(x, y)$ (as witnessed by the unit of the monad on **GMet** induced by the adjunction). Moreover, if $d$ is a symmetric metric then $\bar{d} = d$ (the comonad on **SGMet** induced by the adjunction is the identity comonad).

**Remark 3.24.** We say a self-dual category $\mathcal{C}$ is a category equipped with an isomorphism $\mathcal{C} \cong \mathcal{C}^{\text{op}}$ which is the identity on objects. The above construction for the left adjoint functor is a particular case of the construction of the free self-dual $\mathcal{V}$-category on a $\mathcal{V}$-category, and a variant of the more well-known construction of the enveloping $\mathcal{V}$-groupoid of a $\mathcal{V}$-category.

### 3.1.3. The underlying topological space of a metric space

We are now interested in equipping our spaces with a topology, i.e. in constructing a decent functor **GMet** $\to$ **Top** (in particular, we want directed paths, see Definition 3.32, to be continuous). In the case of symmetric spaces, a satisfactory answer is provided by the usual functor **SGMet** $\to$ **Top** sending a symmetric space $(X, d)$ to the topological space $X$ equipped with the metric topology, which is generated by open balls

$$B^{\epsilon}(x) = \{y \in X \mid d(x, y) < \epsilon\}$$

for $x \in X$ and $\epsilon > 0$. Since the maps in **GMet** are nonexpansive, it can be easily checked that they are continuous wrt to the metric topology and the functor is well-defined. For (general) generalized metric spaces, the situation is however not so clear. Before presenting our answer, we would first like to explain why other “intuitive” options are not satisfactory. Given a space $(X, d)$ and $x \in X$, one can construct past and future open balls of radius $\epsilon > 0$, which are respectively defined by

$$B_{-}^{\epsilon}(x) = \{y \in X \mid d(y, x) < \epsilon\}$$

$$B_{+}^{\epsilon}(x) = \{y \in X \mid d(x, y) < \epsilon\}$$

Considering the topology generated by future open balls is intuitive, but leads to a topology which is too fine: for instance, the map $f: \vec{I} \to \vec{I}$ such that $f(t) = 0$ if $t < 0.5$ and $f(t) = 1$ otherwise would be continuous wrt this topology. Another option could also consider the topology generated by sets of the form $B_{-}^{\epsilon}(x) \cup B_{+}^{\epsilon}(x)$. However, an easy computation shows that in $\mathbb{R}^2$, the resulting topology is the discrete one. Namely, a generating open set is drawn on the left below (continuous lines mean that the border is included and dotted ones that the border is excluded). In the middle right, an open set is shown (it is obtained by intersecting two generating open sets as drawn on the middle left). Finally, by intersecting two such open sets, we can obtain an open set reduced to a point, as shown on the right.

<figure><img src="image_57.png" /></figure>

We hope to have convinced the reader that the canonical way of assigning a topological space to a generalized metric space is the following

**Definition 3.25.** We define the forgetful functor **GMet** $\to$ **Top** as the composite functor **GMet** $\to$ **SGMet** $\to$ **Top**, where the first functor **GMet** $\to$ **SGMet** is the left adjoint to
the forgetful functor constructed in Proposition 3.21 and the second functor **SGMet** $\to$ **Top**
is the forgetful functor described at the beginning of this section.

**Remark 3.26.** Example 3.22 illustrates why the left adjoint (and not the right adjoint) is suitable here.

In the following, when we implicitly see a generalized metric space $(X, d)$ as a topolog-
ical space, it will always be in this way, i.e. with topology generated by the open balls
$B^\epsilon(x) = \{y \in X \mid \bar{d}(x, y) < \epsilon\}$. Morphisms of spaces being nonexpansive functions, the
following can easily be shown:

**Lemma 3.27.** A morphism $f : X \to Y$ of generalized metric spaces is continuous. In particular, by Remark 3.20, given a space $(X, d)$, the distance $\bar{d} : X \times X \to X$ is continuous.

**Remark 3.28.** Notice the distance is not necessarily continuous wrt to the induced topology.
For instance, in $\mathbb{R}^2$ (see the figure on the left),

<figure><img src="image_58.png" /></figure>

when $y$ “moves” vertically to $y'$, the value of $d(x, y)$ suddenly “jumps” from a finite value to $\infty$. Similarly in $\mathbb{S}^1$ (figure on the right), when $y$ moves to $y'$, the value of $d(x, y)$ jumps from 0 to $2\pi$.

**Proposition 3.29.** *The functor **G**Met $\to$ **Top** preserves finite limits and small coproducts.*

*Proof.* It can be directly checked that the functor preserves binary products, equalizers, and small coproducts, as described in Section 3.1.1, see also [23]. □

**Remark 3.30.** The functor does not preserve coequalizers. Namely, if we consider the colimit of Example 3.13, the colimit as topological spaces has points 0 and 1 separated in $I_\omega$, whereas $d_\omega(0, 1) = 0$ and thus the points are not separated in the topological space associated to the colimit of generalized metric spaces.

**Remark 3.31.** The functor does not preserve infinite products. Namely, given a family $(X_i)$ of generalized metric spaces, the underlying topology of the generalized metric space $\prod_i X_i$ is the box topology, which is finer than the product topology.

3.1.4. *Directed paths*

In this section, we define the notion of directed path in a generalized metric space.

**Definition 3.32.** A *path* in a space *X* is a continuous function *γ* : *I* → *X*. Notice that *γ* is not required to be nonexpansive, i.e. it is a path in the underlying topological space. The point *x* = *γ*(0) (resp. *y* = *γ*(1)) is called the *source* (resp. *target*) of the path. We often write *γ* : *x* → *y* to indicate that *γ* is a path from *x* to *y*. The *length* ||*γ*|| of a path *γ* is defined by

$$
\|\gamma\| = \bigvee_{n \in \mathbb{N}} \bigvee_{0 = t_0 < t_1 < \dots < t_n = 1} \sum_i d(\gamma(t_i), \gamma(t_{i+1}))
$$

A path $\gamma$ is called *directed* (or a *dipath*, or a *rectifiable* path) when its length is finite.
**Example 3.33.** In the directed circle $\tilde{S}^1$ (see Example 3.3), directed paths are those which are “turning counter-clockwise”, i.e. maps of the form $t \mapsto e^{i\theta(t)}$ where $\theta: I \to [0, 2\pi]$ is increasing modulo $2\pi$.

**Remark 3.34.** By the triangle inequality, we always have $\|\gamma\| \ge d(\gamma(0), \gamma(1))$ for an arbitrary path $\gamma$.

**Remark 3.35.** By Lemma 3.27, given a path $\gamma: I \to X$ and a morphism $f: X \to Y$, the morphism $f \circ \gamma: I \to Y$ is also a path. Since $f$ is nonexpansive, the path $f \circ \gamma$ is directed when $\gamma$ is: morphisms preserve the direction of paths.

**Remark 3.36.** Since a (non-generalized) metric space is symmetric, it does not contain any information about a “direction of time” and it is thus natural to expect that every path is directed in this case. However, this is not the case because it is well known that, in general, a path is not necessarily rectifiable (for instance the well-known topologist’s sine curve in $\mathbb{R}^2$ defined by $\gamma(0) = 0$ and $\gamma(t) = t \sin(1/t)$ for $0 < t \le 1$). The definition of directed path given in Definition 3.32 is thus not completely satisfactory yet, and we leave the investigation of a more general notion for future works; we expect that in the case of geometric semantics of concurrent programs, the current and the right notions of directed paths coincide. Notice that many simple generalizations of the notion of directedness that one could think of in order to overcome this problem do not work. For instance, one could declare that a path $\gamma$ is directed if we have $d(\gamma(t_1), \gamma(t_2)) < \infty$, for every $t_1, t_2 \in I$ with $t_1 < t_2$. However, with this definition, every path of the directed unit circle (see Example 3.3) would be directed.

Of course, the usual notions of homotopy and dihomotopy directly extend to our setting:

**Definition 3.37.** A homotopy between two paths $\gamma, \rho: I \to X$ is a continuous function $h: I \times I \to X$ such that $h(0, -) = \gamma$ and $h(1, -) = \rho$. Such a homotopy is a dihomotopy when $h(t, -)$ is a directed path for every $t \in I$.

Intuitively, a morphism $[0, a] \to X$ is the same as a rectifiable path in $X$. However, because the maps take distance in account (they are nonexpansive), this is only true up to an expected equivalence relation on paths: if $a$ is too small, there is no possible parametrisation of the path. A partial reparametrization is a continuous non-decreasing map $\theta: I \to I$ and a reparametrization is a surjective partial reparametrization. A trace is an equivalence class of paths under the relation identifying two paths $f$ and $g$ whenever there exists a reparametrization $\theta$ such that $g = f \circ \theta$. It can easily be shown that length is well-defined on traces and a trace is rectifiable when its length is finite. The following proposition shows that in every trace containing a rectifiable path, there is a canonical one which corresponds to a morphism in $\mathcal{G}\mathit{Met}$. Its proof is a direct generalization of the one in the classical case [6, Prop. I.1.20]. Given $t, t' \in \mathbb{R}$ with $t < t'$, we write $\iota_{[t,t')}: I \to [t, t']$ for the function such that $\iota_{[t,t')}(u) = t + (t' - t)u$.

**Lemma 3.38.** Suppose that $(X, d)$ is a separated space and $\gamma: I \to X$ a directed path of length $a = \|\gamma\|$. The function $\lambda: I \to [0, a]$ such that $\lambda(t) = \|\gamma \circ \iota_{[0,t]}\|$ is well-defined, continuous and non-decreasing, and there exists a unique morphism $\tilde{\gamma}: [0, a] \to X$ such that $\tilde{\gamma} \circ \lambda = \gamma$ and $\|\tilde{\gamma} \circ \iota_{[0,t]}\| = t$ for every $t \in [0, a]$.

**Remark 3.39.** In order to see why we need the separation hypothesis, consider a path in a space $X$ equipped with the constant distance $d_0$ equal to 0. Any path in $X$ has length 0 and the lemma is clearly wrong.
As a direct corollary of previous lemma, we have:

**Proposition 3.40.** Given a separated space $X$, rectifiable traces are in bijection with maps $[0, a] \to X$ sending distance to length, with $a \ge 0$.

Finally, we briefly mention here that we can recover traditional notions of directed spaces from generalized metric spaces. The notion of d-space has emerged as the “standard” model for topological spaces equipped with a notion of time direction [24]. It consists in a space together with the specification of which paths are to be considered as directed.

**Definition 3.41.** A d-space $(X, dX)$ consists of a topological space $X$ together with a set $dX \subseteq X^1$ of paths in $X$, whose elements are called d-paths, which contains all constant paths and is closed under concatenation and reparametrization. We write **dTop** for the category of d-spaces with continuous functions preserving d-paths as morphisms.

**Proposition 3.42.** *The operation which to a metric space associates its underlying topological space together with the set of directed paths defines a functor $\mathbf{GMet} \to \mathbf{dTop}$.*

A metric space is *acyclic* when every path $f: x \to x$ with the same source and target is constant. To such a space, we can associate the following.

**Definition 3.43.** A pospace $(X, \leq)$ consists of a topological space $X$ equipped with a partial order $\leq$. We write **POSpace** for the category of pospace and non-decreasing continuous maps.

**Remark 3.44.** Some authors impose additional restrictions on pospaces such as the fact that $\leq$ is a closed subset of $X \times X$, or at least that the limit of an increasing sequence of points is its supremum.

**Proposition 3.45.** *The operation which to a metric space $(X, d)$ associates its underlying topological space $X$, equipped with the partial order $\leq$ such that $x \leq y$ if and only if $d(x, y) < \infty$ for every $x, y \in X$, extends to a functor from the category of acyclic generalized metric spaces to the category of pospaces.*

### 3.1.5. Geodesic and length spaces

In this section, we briefly turn our attention to length spaces, since all geodesic spaces are such, and the CAT(0) condition we are interested in is formulated on such spaces, by considering the “size” of triangles whose sides are geodesics.

**Definition 3.46.** Given a space $(X, d)$, the intrinsic metric $d_I$ is defined by

$$d_I(x, y) = \bigwedge_{\gamma: x \to y} \|\gamma\|$$

A space equipped with its intrinsic metric is called a *length space*.

**Example 3.47.** Consider the circle $S^1 = \{e^{i2\pi\theta} \mid \theta \in \mathbb{R}\} \subseteq \mathbb{C}$ equipped with the distance induced by the euclidian distance on $\mathbb{C}$, i.e. $d(x + iy, x' + iy') = \sqrt{(x' - x)^2 + (y' - y)^2}$. This space is not a length space. The associated intrinsic metric is

$$d_I(e^{i\theta}, e^{i\rho}) = \bigwedge \{\rho' - \theta', \theta' - \rho' \mid \theta' = \theta, \rho' = \rho \mod 2\pi\}$$
**Definition 3.48.** A directed path $\gamma : I \to X$ is a geodesic when for every $t < t'$ in $I$ we have $d(\gamma(t), \gamma(t')) = \lambda(t' - t)$ with $\lambda = d(\gamma(0), \gamma(1))$. A space is geodesic (resp. uniquely geodesic) when between any two points at finite distance there exists a geodesic (resp. a unique geodesic).

**Remark 3.49.** Every geodesic space is a length space, but the converse is not true in general (for instance, the Hopf-Rinow theorem [30] provides sufficient conditions on spaces so that a length space satisfying those conditions is geodesic).

**Example 3.50.** The space $\mathbb{R}^2$ equipped with the euclidian distance is geodesic. The subspace $\mathbb{R}^2 \setminus \{(0,0)\}$ is a length space but is not geodesic since there is no path of length $2 = d(x, y)$ from $x = (0, -1)$ to $y = (0, 1)$ (however, there exists a path of length $2 + \varepsilon$ from $x$ to $y$ for arbitrarily small $\varepsilon > 0$).

In the case of a geodesic space, Proposition 3.40 can be reformulated as follows.

**Proposition 3.51.** Given a separated space $X$, geodesic paths are in bijection with isometries $\overrightarrow{[0, a]} \to X$, with $a \ge 0$.

**Lemma 3.52.** The subcategory of length spaces is closed under colimits.

*Proof.* See [6, Lem. I.5.20]. It can be checked directly that the property of being a length space is preserved under taking coproducts and coequalizers. $\square$

## 3.2. Geometric realization of precubical sets

We now consider two ways of associating a generalized metric space to a precubical set, and study the properties of the resulting space. Since here we are mainly concerned about precubical sets arising as the cubical semantics of concurrent programs, we study mainly finite geometric precubical sets, but try to provide more general hypothesis when these generalizations are easy to make. Part of the current section is a reformulation – and generalization – in the categorical language of properties studied in the framework of polyhedral complexes [6]. The two main results of this section are that metric and topological geometric realization provide comparable constructions (Theorem 3.65) and that realization of NPC precubical sets are CAT(0) cubical complexes (Theorem 3.79).

### 3.2.1. Geometric realization

Recall from Example 3.2 that we write $I = [0, 1]$ for the *standard interval*, and we write $I^n$ for the *standard (topological) n-cube* obtained as the product of $n$ copies of $I$. We write $\delta^- = 0$ and $\delta^+ = 1$. Given $i$ with $0 \le i < n$, and $\epsilon = -$ (resp. $\epsilon = +$), the set of points in $I^n$ whose $i$-th coordinate is $\delta^\epsilon$ is isomorphic to $I^{n-1}$ and called the $i$-th back (resp. front) face of the cube. Now, consider the functor $I : \square \to \mathbf{GMet}$ such that the image of an object $n \in \square$ is $I^n$, and the images of morphisms $\varepsilon_{i,n}^\epsilon$ are the morphisms $I(\varepsilon_{i,n}^\epsilon) : I^n \to I^{n+1}$ such that

$$I(\varepsilon_{i,n}^{\epsilon})(x_0, \dots, x_{n-1}) = (x_0, \dots, x_{i-1}, \delta^{\epsilon}, x_i, \dots, x_n)$$

i.e. they are the inclusions of the faces of a cube into the cube. A topological space can be obtained from a precubical set $C$ by taking a topological $n$-cube for each element of $C(n)$ an gluing them according to faces.
**Definition 3.53.** The geometric realization functor $|-|: \hat{\square} \to \mathbf{GMet}$ is the functor obtained as the left Kan extension of $I: \square \to \mathbf{GMet}$ along the Yoneda embedding $y: \square \to \hat{\square}$. More explicitly, given a cubical set $C$, its geometric realization is the space

$$|C| = \left( \bigsqcup_{n \in \mathbb{N}} I^n \times C_n \right) / \approx$$

where $\approx$ is the smallest equivalence relation such that $(x, c) \approx (y, d)$ whenever $d = \partial_{i,n}^{\epsilon}(c)$ for some indices $\epsilon, i, n$ and $I(\epsilon_{i,n}^{\epsilon})(y) = x$.

**Remark 3.54.** One can define similarly a functor $I: \square \to \mathbf{Top}$ (by post-composing previous functor with the forgetful functor $\mathbf{GMet} \to \mathbf{Top}$), which induces, by left Kan extension along the Yoneda embedding $y: \square \to \hat{\square}$, a **topological geometric realization** functor $|-|: \hat{\square} \to \mathbf{Top}$. Unless we add the adjective “topological”, “geometric realization” will always be meant in generalized metric spaces.

By Proposition 3.21, the forgetful functor $\mathbf{SGMet} \to \mathbf{GMet}$ preserves colimits, and therefore geometric realization commutes with it. And similarly, it commutes with the symmetrization functor $\mathbf{GMet} \to \mathbf{SGMet}$, which is a left adjoint. In the following, we will mainly focus on symmetric spaces for simplicity.

For every $n$-cube $c \in C(n)$ there is a canonical morphism of metric spaces $\iota_c: I^n \to |C|$ such that the image of $x \in I^n$ is the equivalence class of $(x, c)$. Formally, these morphisms can be obtained as the cocone arrows of the colimit defining the geometric realization. They allow one to see the cube $I^n$ as a “subspace” of $|C|$. Notice that there is no a priori reason why these morphisms should be isometries; we will however see below that, they are isometries “locally”. We say a cube $c$ contains a point $x \in |C|$ when $x$ is in the image of $\iota_c$. When the precubical set $C$ has no self-intersection (in particular when $C$ is geometric) the function $\iota_c$ is injective, and we write $\iota_c^{-1}$ for its partial inverse. In this case, following [6, Def. 7.8], given a point $x \in |C|$ and an $n$-cube $c \in C(n)$ such that $x$ occurs in the image of $\iota_c$, we write

$$\varepsilon(x, c) = \bigwedge \{d_{I^n}(\iota_c^{-1}(x), K) \mid K \text{ is a face of } I^n \text{ not containing } x\}$$

with, by convention, $\varepsilon(x, c) = \infty$ when $c$ is a 0-cube (above, the distance between $\iota_c^{-1}(x)$ and $K$ is taken to be the infimum of distances between $\iota_c^{-1}(x)$ and some point of $K$). We then define

$$\varepsilon(x) = \bigwedge \{\varepsilon(x, c) \mid n \in \mathbb{N} \text{ and } c \in C(n) \text{ is such that } x \text{ belongs to the image of } \iota_c\}$$

It is easy to show that $\varepsilon(x) > 0$ for any point $x \in |C|$, see [6, 7.33]. This constant, called the *escape distance* from $x$, intuitively reflects the fact that a path (or a chain) starting from $x$ and going outside a simplex containing $x$ will at least be of length $\varepsilon(x)$. Otherwise said, the distance from $x$ to a point $y$ “near $x$” (i.e. at distance less than $\varepsilon(x)$) will be the same whether we consider the distance within the face or in the whole complex:

**Lemma 3.55.** Suppose given a precubical set $C$ with no self-intersection, and a point $y$ such that $d_{|C|}(x, y) < \varepsilon(x)$. Then any cube $c$ which contains $y$ also contains $x$ and we have $d_{|C|}(x, y) = d_{I^n}(\iota_c^{-1}(x), \iota_c^{-1}(y))$.

*Proof.* See [6, Lem. 7.9]. Fix a “chain” $u = x_0, x_1, x_2, \dots, x_n$ in $|C|$ from $x = x_0$ to $y = x_n$, i.e. a sequence of points such that $x_i$ and $x_{i+1}$ both belong to $\iota_{c_i}$ for some given cube $c_i \in C(n_i)$ (to be precise, the $c_i$ are part of the data defining the chain). Its length is by
definition $l(u) = \sum_i d_{I^{n_i}}(\iota_{c_i}^{-1}(x_i), \iota_{c_i}^{-1}(x_{i+1}))$ and the distance $d_{|C|}(x, y)$ is the infimum of lengths of such chains. The points $x_1$ and $x_2$ belong to the image of $\iota_{c_1}$. If we suppose moreover that $l(u) < \varepsilon(x)$ then $x$ also belongs to $\iota_{c_1}$, and by the triangle inequality the chain $u' = x_0, x_2, x_3, \dots, x_n$ has smaller length. We can conclude by a simple induction. $\square$

**Lemma 3.56.** Given a precubical set $C$ with no self-intersection, its geometric realization $|C|$ is separated.

*Proof.* This is a corollary of Lemma 3.55, since the spaces $I^n$ are separated. $\square$

<figure><img src="image_59.png" /></figure>

**Lemma 3.57.** The geometric realization of a precubical set is a length space.

*Proof.* The spaces $I^n$ are length spaces and, by Lemma 3.52, length spaces are closed under colimits. $\square$

<figure><img src="image_60.png" /></figure>

**Lemma 3.58.** The geometric realization of a finite dimensional precubical set $C$ is a complete space.

*Proof.* The ideas is as follows, see [6, Thm. 7.13], of which this proof is a variant, for details. Given a Cauchy sequence $(x_n)$ in $|C|$, we show that it contains a convergent subsequence. The points $x_i$ belong to the image of $\iota_{c_i}$ for some $n_i$-cell $c_i \in C(n_i)$. Up to taking a subsequence, we can suppose that all the $n_i$ are equal and we write $n$ for the corresponding integer: the points $c_i$ are the images $\iota_{c_i}(x_i)$ for some points $x_i \in I^n$. Up to taking a further subsequence, we can suppose that the sequence $(x_i)$ converges to a point $x_\infty$. Now, noting that the $\iota_{c_i}$ are nonexpansive, using an argument based on $\varepsilon(x_\infty)$ as in the proof of Lemma 3.52, one can show that the $c_i$ are all equal to some $c_\infty$ for $i$ big enough, and conclude that the subsequence converges to $\iota_{c_\infty}(x_\infty)$ in $|C|$. $\square$

<figure><img src="image_61.png" /></figure>

We have seen in Lemma 3.55 that the geometric realization of a precubical set is locally isometric to a space $I^n$. The proof used here does not really depend on the choice of the functor $I: \square \to \mathbf{GMet}$ used to specify the realization of representable precubical sets, and would extend to other choices. We however conjecture that, with this specific choice, this property is more “global” in the sense that the canonical inclusions of standard cubes in the realizations are in fact isometries. The intuition behind this is that within a cube any two points are at distance at most one, and that a non-trivial chain going outside a cube has to cross another cube and will thus be of length more than one.

**Conjecture 3.59.** Given a finite dimensional geometric precubical set $C$, $n \in \mathbb{N}$ and $c \in C(n)$ the morphism $\iota_c: I^n \to |C|$ is an isometry.

**Remark 3.60.** Notice that the above conjecture is not true if the precubical set is not supposed to be geometric. For instance, consider the following precubical set $C$:

$$ \begin{array}{c} c \\ \searrow \\ c' \end{array} $$

The morphism $\iota_c: I^1 \to |C|$ is clearly not an isometry. Moreover, the property strongly depends on the functor $I: \square \to \mathbf{GMet}$ we used. For instance, suppose that we had defined the geometric realization using the functor $I$ such that $I(n)$ is the set $I^n$ equipped with the euclidian metric (instead of the product metric), and consider the following precubical
set C :

<figure><img src="image_62.png" /></figure>

In the square, we have $d_{I2}(y_1, y_2) = \sqrt{2}$ but in the realization we have $d_{|C|}(y_1, y_2) = 1$. The above precubical set is not geometric, but it can easily be turned into a geometric one: instead of having one edge $h$, consider a sequence of two edges $h_1 \cdot h_2$ (whose length is 2), and instead of gluing it along the diagonal of a square, glue it along the diagonal of an hypercube of dimension 5, so that the length of the diagonal is $\sqrt{5} > 2$.

### 3.2.2. The topology of the geometric realization

In previous section, we have introduced two possible geometric realizations: in metric spaces and in topological spaces. We now show that the two agree for the precubical sets of interest here. Notice that, by Remark 3.30, we have no hope to show this using very general arguments since the forgetful functor **SGMet** $\rightarrow \mathbf{Top}$ does not preserve colimits (nor even finite ones). Consider a symmetric generalized metric space $(X, d)$. We write $U : \mathbf{SGMet} \rightarrow \mathbf{Top}$ for the forgetful functor described in Section 3.1.3.

**Lemma 3.61.** *Given an equivalence relation $R$ on $X$, the underlying sets of $(UX)/R$ and $U(X/R)$ are the same and the identity function $f : (UX)/R \rightarrow U(X/R)$ is continuous.*

*Proof.* The underlying sets of both $(UX)/R$ and $U(X/R)$ are the same because the forgetful functors **Top** $\rightarrow$ **Set** and **SGMet** $\rightarrow$ **Set** both admit a right adjoint (see Proposition 3.7). Suppose given $V$ open in $U(X/R)$: for every $x \in V$ there exists $\varepsilon > 0$ such that $B_{X/R}^{\varepsilon}(x) \subseteq V$. Thus, for every $x \in f^{-1}(V)$, there exists $\varepsilon > 0$ such that $f^{-1}(B_{X/R}^{\varepsilon}(f(x))) \subseteq f^{-1}(V)$. Given $x \in X$, we have $B_X^{\varepsilon}(x) \subseteq B_{X/R}^{\varepsilon}(x)$ by Remark 3.11. Therefore, for every $x \in X$ such that $x \in \pi^{-1}(V)$, there exists $\varepsilon > 0$ such that $B_X^{\varepsilon}(x) \subseteq \pi^{-1}(V)$, from which we can conclude that $\pi^{-1}(V)$ is open. $\square$

The following lemma is well-known [49, Thm. 4.17]:

**Lemma 3.62.** *A continuous bijection $f : X \rightarrow Y$ between topological spaces such that $X$ is compact and $Y$ is separated is an homeomorphism.*

*Proof.* Given a closed set $U$ of $X$, $U$ is compact since $X$ is, therefore $f(U)$ is also compact, and therefore $f(U)$ is closed since $Y$ is separated. Therefore $(f^{-1})^{-1}(U) = f(U)$ is closed and $f^{-1}$ is continuous since the preimage of a closed set is closed. $\square$

**Proposition 3.63.** *The geometric realization of finite geometric precubical sets commutes with the forgetful functor **SGMet** $\rightarrow$ **Top**.*

*Proof.* Given a finite geometric precubical set $C$, the colimit defining its geometric realization can be computed as a quotient of the space $X = \coprod_{n \in \mathbb{N}} \coprod_{x \in C(n)} I(n)$, by a relation that we denote $R$. The space $UX$ is compact, as a finite coproduct of compact spaces (the functor $U$ commutes with coproducts, see Proposition 3.29), and thus the space $(UX)/R$ is compact too, as a quotient of a compact space. Since $C$ is geometric, and thus without self-intersection, its geometric realization $U(X/R)$ is separated by Lemma 3.56. Finally, the
identity function $(UX)/R \to U(X/R)$ is continuous by Lemma 3.61 and thus an homeomorphism by Lemma 3.62. □

Since the topology of a space is determined locally, previous proposition can be generalized to the case of precubical sets which are only locally finite:

**Definition 3.64.** A precubical set is locally finite if for every vertex $x$, only finitely many cubes have $x$ as iterated vertex.

**Theorem 3.65.** The geometric realization of locally finite geometric precubical sets commutes with the forgetful functor **SGMet** → **Top**.

*Proof.* Suppose given a locally finite geometric precubical set $C$ and a point $x \in |C|$. We write $c$ for the carrier of $x$, i.e. the cube in $C$ of lowest dimension which contains $x$. Consider the precubical set $C_c$ defined as the smallest precubical subset of $C$ which contains all the cubes having $c$ as iterated face (the star of $c$): its cubes are faces of maximal cubes with $c$ as iterated face. Since $C$ is supposed to be both locally finite and geometric, the precubical set $C_c$ is easily shown to be finite and we can apply Proposition 3.63. By Lemma 3.55, a neighborhood of $x$ in the geometric realization of $C$ is isometric to a neighborhood of $x$ in the geometric realization of $C_c$ (because the lemma shows that the distance is the distance of standard cubes). Therefore, locally around $x$, the metric topology is the colimit topology. □

### 3.2.3. Cubical complexes

Geometric precubical sets give rise to cubical complexes, in the following sense.

**Definition 3.66.** A cubical complex $K$ is a topological space of the form

$$K = \left( \bigsqcup_{\lambda \in \Lambda} I^{n_{\lambda}} \right) / \approx$$

where $\Lambda$ is a set, $(n_\lambda)_{\lambda \in \Lambda}$ is a family of integers, and $\approx$ is an equivalence relation, such that, writing $p_\lambda : I^{n_\lambda} \to K$ for the restriction of the quotient map $\bigsqcup_{\lambda \in \Lambda} I^{n_\lambda} \to K$, we have

(1) for every $\lambda \in \Lambda$, the map $p_\lambda$ is injective,

(2) given $\lambda, \mu \in \Lambda$, if $p_\lambda(I^{n_\lambda}) \cap p_\mu(I^{n_\mu}) \neq \emptyset$ then there is an isometry from a face $J_\lambda$ of $I^{n_\lambda}$ to a face $J_\mu$ of $I^{n_\mu}$ such that $p_\lambda(x) = p_\mu(y)$ if and only if $y = h_{\lambda,\mu}(x)$.

A directed cubical complex is defined similarly, as a d-space of the form $K = (\bigsqcup_{\lambda \in \Lambda} I^{n_\lambda}) / \approx$.

**Proposition 3.67.** The geometric realization of a geometric precubical set is a cubical complex.

Moreover, the metric of the geometric realization of a geometric precubical set is precisely the intrinsic metric (as defined in [6, Sect. I.7.33]).

**Remark 3.68.** Notice that the geometric realization of precubical complexes of Example 1.19 which are not geometric are not precubical complexes.

**Remark 3.69.** The converse of the above lemma is not true. For instance, one can construct a Möbius strip as a complex, and it cannot be obtained as the geometric realization of a geometric precubical set because there is a “mismatch of direction” of the edges. One can actually show that directed geometric realizations of geometric precubical sets are precisely directed cubical complexes.
Finally, we mention the following useful fact, whose proof can be found in [6, 7.33].

**Lemma 3.70.** *A finite dimensional precubical complex is geodesic.*

To sum up the above properties shown on geometric realizations of geometric precubical sets, we have:

**Proposition 3.71.** *Finite dimensional precubical complexes are complete geodesic length spaces.*

### 3.2.4. Directed geometric realization

Interestingly, all the above properties can easily be checked to hold for a variant of the geometric realization which is really “directed”, and makes much more sense from a concurrency point of view. In Definition 3.53 of geometric realization, we can replace the functor $I: \Box \to \mathbf{G}\mathbf{Met}$ sending $n$ to $I^n$ by the functor $\vec{I}: \Box \to \mathbf{G}\mathbf{Met}$ which send $n$ to $\vec{I}^n$ and thus obtain a variant of the notion of geometric realization where not every path is directed.

**Definition 3.72.** The directed geometric realization $\mathbb{1}C$ of a precubical complex is the functor obtained as the left Kan extension of $\vec{I}: \Box \to \mathbf{G}\mathbf{Met}$ along the Yoneda embedding $y: \Box \to \hat{\Box}$.

**Proposition 3.73.** *The directed geometric realization of a finite dimensional geometric precubical set is a complete geodesic length space.*

Given a precubical set $C$, we can consider its directed geometric realization $\mathbb{1}C$. A vertex in $C$ can be seen as a morphism $Y0 \to C$ (where $Y$ denotes the Yoneda functor, see Section 1.1) and thus induces, by functoriality of the realization, a point $\mathbb{1}x$ of $\mathbb{1}C$, which is given by the image of the morphism $\mathbb{1}Y0 \to \mathbb{1}C$. Similarly, a path (resp. dipath) $f$ in $C$ induces a path (resp. dipath) $\mathbb{1}f$ in $\mathbb{1}C$. It is easy to show that given two dipaths $f, g: x \to y$ in $C$, if they are homotopic (resp. dihomotopic) then the dipaths $\mathbb{1}f$ and $\mathbb{1}g$ are also homotopic (resp. dihomotopic). A converse property was shown by Fajstrup for locally finite precubical sets [14] (more exactly, this result was formulated for geometric realization of precubical sets as d-spaces, but the proof adapts straightforwardly to the case of generalized metric spaces).

**Proposition 3.74.** *Given $C$ geometric and locally finite, a geometric and locally finite precubical set, the homotopy (resp. dihomotopy) classes of dipaths from $x$ to $y$ in $C$ are in bijection with homotopy (resp. dihomotopy) classes of dipaths from $\mathbb{1}x$ to $\mathbb{1}y$ in $\mathbb{1}C$.*

From the previous proposition and Theorem 2.29, one can deduce that, for dipaths between any two points which are realizations of vertices of $C$, homotopy coincides with dihomotopy in $\mathbb{1}C$. Variants of this properties have been shown in the literature: in the case of geometric semantics of “simple” programs with mutexes [15], in the case of NPC cube complexes [16] (see also next section). A similar observation has been made for spaces which are hypercontinuous lattices equipped with their Lawson topology, such that their underlying space has connected CW type [34]. In that case also, increasing paths that are homotopic are in fact dihomotopic.
### 3.3. Non-positively curved spaces

#### 3.3.1. CAT(0) spaces

We now recall the notion of non-positively curved space (also called CAT(0) space), with the aim of showing that this notion is a topological counterpart of the notion introduced for precubical sets (Definition 1.28). We chose not to define this earlier in the paper in order to emphasize that this is only an inspiration for our axiomatics on precubical sets, but the geometric interpretation is not needed in order to work with non-positively curved precubical sets (excepting, maybe, to forge intuitions).

This notion generalizes hyperbolic geometry by formalizing the observation that, in a non-positively curved space, triangles with geodesic sides appear to be thinner than in usual, flat, spaces. Its importance is due to the numerous applications this notion has allowed. We only mention basic notions here, and refer the reader to standard texts for a more detailed presentation of the subject [26, 6, 19]. In the rest of this section, for simplicity, we only consider symmetric generalized metric spaces, since the topology of a space does not depend on its direction. Interesting possible generalizations in the directed case are mentioned in Section 4.

**Definition 3.75.** A geodesic triangle $\Delta(x, y, z)$ in a geodesic metric space $X$ consists of three points $x, y, z$ and three geodesics joining any pair of two. A comparison triangle for a geodesic triangle $\Delta(x, y, z)$ consists of an isometry $\bar{\Delta} : \Delta(x, y, z) \to \mathbb{R}^2$ whose image is a geodesic triangle $\bar{\Delta}(\bar{x}, \bar{y}, \bar{z})$, where $\mathbb{R}^2$ is equipped with the usual euclidian distance $d_{\mathbb{R}^2}$.

We now recall the definition of non-positively curved space based on the comparison axiom of Cartan, Alexandrof and Topogonov. This is the origin of the name CAT(0), where the 0 refers to the fact that strictly positive or negative curvature can also be defined in a similar way, but we will refrain from introducing those in full generality here (see below).

**Definition 3.76.** A geodesic triangle $\Delta(x, y, z)$ is CAT(0) when there exists a comparison triangle $\bar{\Delta}(\bar{x}, \bar{y}, \bar{z})$ such that for any two points $p, q \in \Delta(x, y, z)$, we have $d(p, q) \le d_{\mathbb{R}^2}(\bar{p}, \bar{q})$. A geodesic metric space is CAT(0) when every geodesic triangle is CAT(0), and locally CAT(0) or non-positively curved (NPC) when every point admits a neighborhood which is CAT(0).

These spaces enjoy many nice properties such as being (locally) uniquely geodesic and contractible. We refer the reader to [6] for more details about those.

Other notions of curvature can be defined if we consider other “model spaces” instead of $\mathbb{R}^2$ in which we take our comparison triangles. This amounts, in Definitions 3.75 and 3.76, to consider geodesic triangles $\bar{\Delta} : \Delta(x, y, z) \to M_k$ where $M_k$ is called a model space. For $k=0$, we have $M_k = \mathbb{R}^2$ and we recover the above definitions; for $k > 0$, $M_k$ is a 2-sphere (the smaller $k$ is, the bigger its radius is); for $k > 0$, $M_k$ is a hyperbolic space. Compared to usual model spaces $M_0$, triangles in model spaces $M_k$ are fatter when $k > 0$ and slimmer when $k < 0$, this getting more accentuated when $|k|$ becomes large. In particular, for $k=1$, we consider the standard 2-sphere $\mathbb{S}^2$ equipped with the distance $d$ such that $d(x, y) \in [0, \pi]$ is defined by $\cos(d(x, y)) = \langle x, y \rangle$. A space is CAT(1) when for every triangle $\Delta(x, y, z)$ whose diameter is less than $2\pi$, there exists a comparison triangle $\bar{\Delta}(\bar{x}, \bar{y}, \bar{z})$ in $\mathbb{S}^2$, such that we have $d(p, q) \le d_{\mathbb{S}^2}(\bar{p}, \bar{q})$ for every points $p, q \in \Delta(x, y, z)$.
### 3.3.2. *The Gromov link condition*

In this section we recall the characterization given by Gromov [26] of CAT(0) cubical complexes, see also [6, II.5.4] and [6, II.5.20]. We first introduce some necessary definitions.

**Definition 3.77** ([6, Section 7.14]). Given a geodesic metric space $X$ and a point $x \in X$, the link $\text{link}_X(x)$ of $x$ in $X$ is the set of geodesics $\gamma : [0, a] \to X$ such that $\gamma(0) = x$, equipped with the compact-open topology, quotiented by the relation identifying two paths which coincide on an interval of the for $[0, \varepsilon]$ for some $\varepsilon > 0$, i.e. the “directions” from $x$ pointing into $X$. This space can be metrized using the angle between two such directions.

This notion of link can be formally related to the one introduced for precubical sets in Definition 1.31 by observing that the former is a geometric realization of the latter (where the standard $n$-simplex is realized as a spherical simplex with edges of length $\pi/2$).

**Definition 3.78.** An abstract simplicial complex is flag if whenever the complex contains the 1-skeleton of a simplex, it also contains the simplex: given vertices $x_1, \dots, x_k$ such that $\{x_i, x_j\}$ are simplices for every indices $i, j$, the set $\{x_1, \dots, x_k\}$ is also a simplex.

Again, this notion corresponds to the one of Definition 1.37 through the geometric realization.

Finally, we can explain in which way our conditions for non-positively curved precubical sets (Definition 1.28) correspond to the traditional geometric one.

**Theorem 3.79.** Given a finite dimensional geometric precubical set $C$, the following are equivalent:

(i) $|C|$ is non-positively curved

(ii) in $|C|$ the link of every point is CAT(1)

(iii) in $|C|$ the link of every vertex is a flag complex

(iv) in $C$ the link of every vertex is a flag complex

(v) $C$ satisfies the cube condition

Moreover, the following are equivalent:

(i') $|C|$ is CAT(0)

(ii') $|C|$ is uniquely geodesic

(iii') $|C|$ is non-positively curved and simply connected

(iv') $C$ satisfies the cube condition and is simply connected

*Proof.* First, notice that because $C$ is supposed to be finite dimensional, its realization is geodesic by Proposition 3.71. The equivalence between (i), (ii) and (iii) is due to Gromov [26], see also [6, Thm. 5.20]. The equivalence between (iii) and (iv) is immediate and the equivalence between (iv) and (v) was shown in Theorem 1.42. The equivalence between (i'), (ii') and (iii') is due to Gromov [6, Thm. 5.5]. The equivalence between (iii') and (iv') follows from the equivalence between (i) and (v). $\square$

## 4. CONCLUSION AND FUTURE WORK

We showed in this article that numerous concepts from different fields of mathematics and computer science are closely related, non-positively curved spaces and rewriting systems with the cube property in particular, etc. These are important observations since, in many ways, non-positively curved spaces are “simpler” to work with than general spaces: topological
invariants are much simpler, e.g. the homology and homotopy groups have no torsion, and their universal covering space are contractible [6].

There are many possible extensions to this work. First, in the case of a non-positively curved precubical set, as used in the geometric semantics of programs in Section 1.1, we believe that the coreflexion of the adjunction between (some form of labeled) precubical sets and (labeled) prime event structures of [22] is directly linked to the universal dicovering in the sense of [15]. This would enlighten the relationship between these two models, in case we are dealing with concurrent programs with mutual exclusion primitives.

Our original idea was that for non-positively curved spaces $X$, dihomotopy of dipaths can be characterized by the first relative homology group $H_1(X, A)$ where $A$ is the subspace of $X$ formed of the initial and final points of the dipaths we are considering. By the work of Steiner [54], we know that the homotopy 2-categories, for some particular loop-free spaces, are in one-to-one correspondence with some particular augmented directed complexes, and that homotopic dipaths would map onto homologous elements of the corresponding chain complex. In the case of non-positively curved spaces, this implies that dihomotopic dipaths would be mapped onto homologous elements of the underlying chain complex, in a not too distant manner, by Hurewicz theorem, i.e. up to abelianization. Unfortunately, it seems that we need to further shrink down the class of spaces so that dihomotopy of dipaths can be fully characterized by this first relative homology group, and there are probably subtle combinatorial properties to be discovered.

We also expect to extend the results of this article to programs with resources of arbitrary capacity, where we still have some control of the homotopy type of the spaces generated by the semantics of such programs. This is, after all, part of an endeavor to better understand the geometries that can appear in the study of rewriting, concurrent and distributed systems, where other primitives (test-and-set and all read-modify-write statements) will generate different types of geometries. The relationship between metrics and (di-)homotopies, unravelled in this paper, may also pave the way to considering timed concurrent models, studied up to deformation (and amenable to state-space reduction techniques [15]). This has actually already been used in a different context, in robotics, by Ghrist and collaborators, to design efficient algorithms, see e.g. [16].

## REFERENCES

[1] G. E. Albert. A note on quasi-metric spaces. *Bulletin of the American Mathematical Society*, 47(6):479-482, 1941.

[2] F. Ardila, M. Owen, and S. Sullivant. Geodesics in CAT(0) cubical complexes. *Advances in Applied Mathematics*, 48(1):142-163, 2012.

[3] J.-P. Barthélemy and J. Constantin. Median graphs, parallelism and posets. *Discrete mathematics*, 111(1):49-63, 1993.

[4] R. Betti, A. Carboni, R. Street, and R. Walters. Variation through enrichment. *Journal of Pure and Applied Algebra*, 29(2):109-127, 1983.

[5] M. Bezem, J. Klop, R. de Vrijer, and Terese. *Term Rewriting Systems*. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[6] M. R. Bridson and A. Haefliger. *Metric spaces of non-positive curvature*, volume 319. Springer, 2009.

[7] V. Chepoi. Graphs of some CAT(0) complexes. *Advances in Applied Mathematics*, 24(2):125-179, 2000.

[8] V. Chepoi. Nice labeling problem for event structures: a counterexample. *SIAM Journal on Computing*, 41(4):715-727, 2012.

[9] F. Clerc and S. Mimram. Presenting a category modulo a rewriting system. In *LIPIcs-Leibniz International Proceedings in Informatics*, volume 36. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015.

[10] P. Dehornoy. On completeness of word reversing. *Discrete Mathematics*, 225(1):93-119, 2000.
[11] P. Dehornoy, F. Digne, E. Godelle, D. Krammer, and J. Michel. Foundations of garside theory. *arXiv preprint arXiv:1309.0796*, 2013.

[12] M. Droste. A kleene theorem for recognizable languages over concurrency monoids. In *Automata, Languages and Programming*, pages 388–399. Springer, 1994.

[13] U. Fahrenberg. Directed homology. *Electr. Notes Theor. Comput. Sci.*, 100:111–125, 2004.

[14] L. Fajstrup. Dipaths and dihomotopies in a cubical complex. *Advances in Applied Mathematics*, 35(2):188–206, 2005.

[15] L. Fajstrup, É. Goubault, E. Haucourt, S. Mimram, and M. Raussen. *Directed Algebraic Topology and Concurrency*. SpringerBriefs in Mathematical Methods. Springer International Publishing, 2016. Book to appear.

[16] R. Ghrist and S. M. LaValle. Nonpositive curvature and pareto-optimal coordination of robots. *SIAM Journal of Control and Optimization*, 45(5):1697–1713, 2006.

[17] R. Ghrist and V. Peterson. A Geometric Approach to Dipath Classification on Process Graphs. Unpublished.

[18] R. Ghrist and V. Peterson. The geometry and topology of reconfiguration. *Advances in Applied Mathematics*, 38(3):302–323, 2007.

[19] É. Ghys, P. de La Harpe, et al. *Sur les groupes hyperboliques d'apres Mikhael Gromov*, volume 83. Birkhäuser Basel, 1990.

[20] G. Gonthier, J.-J. Lévy, and P.-A. Melliès. An abstract standardisation theorem. In *Logic in Computer Science, 1992. LICS'92., Proceedings of the Seventh Annual IEEE Symposium on*, pages 72–81. IEEE, 1992.

[21] E. Goubault. Geometry and concurrency: a user's guide. *Mathematical structures in computer science*, 10(04):411–425, 2000.

[22] E. Goubault and S. Mimram. Formal relationships between geometrical and classical models for concurrency. *Electronic Notes in Theoretical Computer Science*, 283:77–109, 2012.

[23] J. Goubault-Larrecq. *Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology*, volume 22. Cambridge University Press, 2013.

[24] M. Grandis. Directed algebraic topology: Models of non-reversible worlds. *AMC*, 10:12, 2009.

[25] M. Grandis et al. The fundamental weighted category of a weighted space: From directed to weighted algebraic topology. *Homology, Homotopy and Applications*, 9(1):221–256, 2007.

[26] M. Gromov. *Hyperbolic groups*. Springer, 1987.

[27] Y. Guiraud. Termination orders for three-dimensional rewriting. *Journal of Pure and Applied Algebra*, 207(2):341–371, 2006.

[28] K. Hardie, K. Kamps, and R. Kieboom. A homotopy 2-groupoid of a hausdorff space. *Applied Categorical Structures*, 8(1-2):209–234, 2000.

[29] K. Hardie, K. Kamps, and R. Kieboom. A homotopy bigroupoid of a topological space. *Applied Categorical Structures*, 9(3):311–327, 2001.

[30] H. Hopf and W. Rinow. Über den begriff der vollständigen differentialgeometrischen fläche. *Commentarii Mathematici Helvetici*, 3(1):209–225, 1931.

[31] P. T. Johnstone. On embedding categories in groupoids. In *Mathematical Proceedings of the Cambridge Philosophical Society*, volume 145, pages 273–294. Cambridge University Press, 2008.

[32] G. M. Kelly and M. L. Laplaza. Coherence for compact closed categories. *Journal of Pure and Applied Algebra*, 19:193–213, 1980.

[33] J. Kelly. Bitopological spaces. *Proceedings of the London Mathematical Society*, 3(1):71–89, 1963.

[34] S. Krishnan. Criteria for homotopic maps to be so along monotone homotopies. *Electron. Notes Theor. Comput. Sci.*, 230:141–148, Mar. 2009.

[35] D. Kuske. Nondeterministic automata with concurrency relations and domains. In *Trees in Algebra and Programming—CAAP'94*, pages 202–217. Springer, 1994.

[36] Y. Lafont. Towards an algebraic theory of boolean circuits. *Journal of Pure and Applied Algebra*, 184(2):257–310, 2003.

[37] F. W. Lawvere. Metric spaces, generalized logic, and closed categories. *Rendiconti del seminario matematico e fisico di Milano*, 43(1):135–166, 1973.

[38] J.-J. Lévy. *Réductions correctes et optimales dans le lambda-calcul*. PhD thesis, Université Paris 7, 1978.

[39] S. Mac Lane. *Categories for the working mathematician*, volume 5. Springer, 1998.
[40] P.-A. Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In *Rewriting techniques and applications*, pages 24–50. Springer, 2002.

[41] S. Mimram. *Sémantique des jeux asynchrones et réécriture 2-dimensionnelle*. PhD thesis, PPS, CNRS – Université Paris Diderot, 2008.

[42] S. Mimram. The structure of first-order causality. *Mathematical Structures in Computer Science*, 21(01):65–110, 2011.

[43] S. Mimram. Towards 3-Dimensional Rewriting Theory. *Logical Methods in Computer Science*, 10(1):1–47, 2014.

[44] M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part I. *Theoretical Computer Science*, 13(1):85–108, 1981.

[45] M. Nielsen, V. Sassone, and G. Winskel. *Relationships between models of concurrency*. Springer, 1994.

[46] P. Panangaden, V. Shanbhogue, and E. W. Stark. *Stability and sequentiality in dataflow networks*. Springer, 1990.

[47] A. Preller and J. Lambek. Free compact 2-categories. *Mathematical Structures in Computer Science*, 17(02):309–340, 2007.

[48] M. Roller. Poc sets, median algebras and group actions. An extended study of Dunwoody's construction and Sageev's theorem. *Southampton Preprint Archive*, 1998.

[49] W. Rudin. *Principles of mathematical analysis*, volume 3. McGraw-Hill New York, 1964.

[50] V. Sassone, M. Nielsen, and G. Winskel. Deterministic behavioural models for concurrency. In *Mathematical Foundations of Computer Science 1993*, pages 682–692. Springer, 1993.

[51] V. Sassone, M. Nielsen, and G. Winskel. Models for concurrency: Towards a classification. *Theoretical Computer Science*, 170(1):297–348, 1996.

[52] R. Sorgenfrey. On the topological product of paracompact spaces. *Bulletin of the American Mathematical Society*, 53(6):631–632, 1947.

[53] E. W. Stark. Concurrent transition systems. *Theoretical Computer Science*, 64(3):221–269, 1989.

[54] R. Steiner. Omega-categories and chain complexes. *Homology, Homotopy and Applications*, 6(1):175–200, 2004.

[55] W. Wilson. On quasi-metric spaces. *American Journal of Mathematics*, 53(3):675–684, 1931.

[56] G. Winskel. *Events in computation*. PhD thesis, University of Edinburgh, 1980.

[57] G. Winskel and M. Nielsen. Models for concurrency. *DAIMI Report Series*, 22(463), 1993.