David Janin
email: janin@labri.fr

Spatio-temporal domains: an overview

come

Introduction

Research context. Program semantics is classically divided between two complementary approaches : denotational semantics and operational semantics. Denotational semantics generally refers to what the partial functions encoded by programs are : what is the relationship between (models of) their input values (or input memory state) and their output values (or output memory state). Operational semantics refers instead to when and where these values are read, transformed and eventually produced. To some extent, operational semantics defines effective models for implementing programs. It provides tools for analyzing the space and time behavior of programs therefore analyzing their complexity. On the other hand, denotational semantics provides instead methods for analyzing the (partial) correction of programs.

This suggests that semantic features can be distributed between typical operational features (time and space values) and denotational features (other data values). However, in many modern computerized systems such as, for instance, interactive music or animation systems [START_REF] Elliott | Functional reactive animation[END_REF][START_REF] Hudak | The Haskell School of Music : From signals to Symphonies[END_REF][START_REF] Archipoff | Structured reactive programming with polymorphic temporal tiles[END_REF][START_REF] Archipoff | Unified media programming: An algebraic approach[END_REF], timing or spacing information plays a crucial rôle in the definition of system's inputs and outputs. There, many data values are implicitly parameterized by some space and/or time information: think of an augmented music system taking as input the melody played by a musician dancing on a stage. How the resulting spaced-and-timed signals can be read, combined and transformed in both an efficient and a sound way is one of the central questions of numerous domain specific language proposals such as, for instance, Fran [START_REF] Elliott | Functional reactive animation[END_REF] for animation or Euterpea [START_REF] Hudak | The Haskell School of Music : From signals to Symphonies[END_REF] for music.

In all the underlying semantic models, compositionality is a key issue as it allows efficient, structure driven, development and analysis techniques. In fact, with compositionality, properties of complex systems/programs can be derived from certain combinations of the properties of their (simpler) components. As an immediate consequence, semantic models can also be studied and developed per se, adequate (domain specific) programming languages deriving a posteriori from the algebraic/combinatorial properties of these models.

Our contribution. Following such a model-driven development of programming language, we consider the possibility of lifting space or time information into typical denotational models: Scott Domains. It happens that this can be done by restricting certain constructions known in topos and fibration theory to posets. We thus provide in this paper an elementary description of these constructions and illustrate their applicability by interpreting the induced algebras in terms of typical spaced or timed programming constructs.

Detailled structure. Technically, we define spatio-temporal domain as certain discrete fibrations of posets into posets (Section 2). Simply said, elements of these domains are (partially ordered) computation histories indexed over spacetime scales. Relationships with other known semantic models are detailled in Section 3. Spatio-temporal morphisms are defined in Section 4 as monotone functions between spatio-temporal domains that uniformly act on the underlying spacetime scales. This eventually yields a fully featured category that extends to space and time the categories of posets/cpos/domains and monotone/continuous functions typically used in classical denotational semantics.

The proposed approach yields two layers of program constructs that have been long identified in Globally-Asynchronous Locally-Synchronous (GALS) system design [START_REF] Daniel | Globally-Asynchronous Locally-Synchronous Systems[END_REF][START_REF] Teehan | A survey and taxonomy of GALS design styles[END_REF]. More precisely, there appear:

(1) a synchronous layer of programming constructs available when components' inputs and outputs are located and timed on the same spacetime scale and received or produced in a synchronous way (Section 5), [START_REF] Archipoff | Structured reactive programming with polymorphic temporal tiles[END_REF] an asynchronous layer of programming constructs available when component's inputs and outputs are located and timed on possibly distinct spacetime scales (Section 6).

At the border of these two layers, when inputs and outputs are located on the same scale but without any synchronicity assumption, we show that feedback loop constructs are available for defining non trivial (least) fixpoints (Section 8), that is, infinite signals. Continuously spaced and timed posets are also studied in Section 7 where a tight relationship with various key concepts from Domain Theory is established.

It is known that fibration theory [START_REF] Streicher | Fibred categories à la Jean Bénabou. Revised notes of a course on fibred categories given at a Spring School in Munich[END_REF] is used in denotational semantics of higher-order dependently typed lambda calculus [START_REF] Jacobs | Categorical Logic and Type Theory[END_REF]. Restricting ourselves to discrete fibrations over posets yields a notion of types that weakly depends on spacetime scales (or clocks). These possibilities were already studied in language extension proposals [START_REF] Colaço | Clocks as first class abstract types[END_REF][START_REF] Colaço | Towards a higher-order synchronous data-flow language[END_REF] of the Synchronous Programming Language fam-ily [START_REF] Berry | The Esterel synchronous programming language: design, semantics, implementation[END_REF][START_REF] Benveniste | The synchronous languages twelve years later[END_REF]. Our approach provides a sound mathematical framework for the formal study of these possible extensions.

Although we aim at providing elementary descriptions of all concepts, the reader is still expected to know the (basic) definitions of a partially ordered set (poset), a category and the associated notions of (possibly continuous) functors. All other concepts are defined in the text when needed. Concrete examples defined over spaced and timed signals are detailed throughout, illustrating most concepts and their applicability to spacetime program's semantics. Some notations. A partially ordered set, or poset, is a set P equipped with a partial order relation, that is, a reflexive, symmetric and transitive binary relation. Given a poset P , we use the notation x, y ≤ z (resp. z ≤ x, y) or even X ≤ z (resp. z ≤ X) to denote the fact that both x, y ∈ P are smaller (resp. greater) than z ∈ P , or the fact that z ∈ P is an upper bound (resp. a lower bound) of the subset X ⊆ P .

The downward closure ↓ X ⊆ P of X ⊆ P is defined by ↓ X = {y ∈ P : ∃x ∈ X, y ≤ x}. By extension, for every element x ∈ P we also use the notation ↓ x = {y ∈ P : y ≤ x}. We say that X is downward closed when ↓ X = X. When it exists, its greatest lower bound (resp. least upper bound ) is denoted by X (resp. X). The poset P is a meet-semilattice when every two elements x, y ∈ P have a meet, that is, a greatest lower bound denoted by x ∧ y.

A subset X ⊆ P is directed when it is non empty and for all x, y ∈ X there is z ∈ X such that x, y ≤ z. The poset P is a (directed) complete partially ordered set, or complete poset, or even cpo, when every directed subset X ⊆ P has a least upper bound X.

A function f : P → Q between two posets is called monotone when x ≤ y implies f (x) ≤ f (y) for every x, y ∈ X. Whenever needed, the function f is extended point-wise to every subset X ⊆ P by f (X) = {f (x) ∈ Q : x ∈ X}. The function f is continuous when, for every directed subset X ⊆ P , if X is defined then f (X) = f ( X). A continuous function is necessarily monotone and, as such, maps every directed subsets to a directed subset.

In a cpo P with a least element ⊥, we know from Knaster-Tarski that every monotone function f : P → P has a least fixpoint µ(f ) = λ∈Λ f λ (⊥) with Λ any ordinal which cardinal is strictly greater than the cardinal of P . In the case f is continuous, we have µ(f ) = n∈ω f n (⊥).

Last, we shall consider various categorical concepts that are detailed when needed. We may also consider the categories Poset with partially ordered sets and monotone functions, SLattice with meet-semilattices and meet-preserving functions and Cpo with complete posets and continuous functions, as well as their restriction to posets with a least element, the resulting (full) subcategories (possibly with non strict functions) being denoted by Poset ⊥ , SLattice ⊥ and Cpo ⊥ . All these categories are known to be cartesian closed and, possibly extended with the empty set, bi-cartesian. Details about these category theoretical concepts are given in the text when needed.

Throughout this text, an arbitrary poset T may be interpreted as a spatiotemporal scale. This means that for every element u, v ∈ T , we say that u lies before v, or v lays after u, when u ≤ v, and that u lays beside v when u and v are incomparable. In other words, there is the time dimension that increases with the order, and, there is the space dimension where incomparable elements are also related.

Example 2.1 (N -distributed spacetime). As an example, let N be a set of mobile agents, each with its own clock timed over, say, the positive real line R + . As a variant of message timestamps used in distributed computing, one can define a spacetime location as any pair (S, C) with S ⊆ N a non empty set of synchronized agents and C : N → R + their shared knowledge of all clocks. This interpretation yields a partial order defined by (S , C ) < (S, C) when C ≤ C (point-wise) and C (n) < C(n) for all n ∈ S. Then it can be shown that every sub-poset of space time locations induces a canonical communication scenario between the agents that justifies the order between these locations.

More precisely, let T N be the poset of spacetime locations induced by N . We assume the following communication model between agents. There may be two-way synchronizations among a group of agent S ⊆ N when these agents are, say, in the same space location. In this case, they share all their knowledge of local clock values, taking the max of clock values of unsynchronized agents. There may also be one-way messages sent by one agent, with a copy of its own local clock value, to (any member of) a synchronized group of agents.

Then it is an easy observation that any discrete sub-poset X ⊆ T N of spacetime locations induces a canonical communication scenario define in the obvious way for two-way synchronization and as follows for one-way messages. For every spacetime location (S, C) ∈ X, for every n ∈ S, either there is (S , C ) ≤ (S, C) such that C (n) = C(n), or there is a one-way message from n to S sent from n at (local) instant C(n) and received by one/any m ∈ S at (local) instant C(m).

An example of such a communication scenario is illustrated in Figure 1 in the case of N = {1, 2, 3, 4}. The selected subset of spacetime locations is detailed on the left of the figure, with functions from N into R + represented by vectors of length four. The resulting communication scenario is detailed on the right, with two-way (resp. one-way) transversal arrows modeling two-way synchronizations (resp. one-way messages). Arrows resulting from transitivity of two-way synchronizations have been omitted. One can observe that such a model extends to arbitrary collection of posets taken as (local) time scales since local time scales are not required to be compatible in any sense.

({1, 2, 3, 4}, 0, 0, 0, 0 ) ({1, 2}, 5, 4, 0, 0 ) ({3, 4}, 0, 0, 1, 4 ) ({2, 3}, 5, 6, 3, 5 ) ({1, 2}, 8, 7, 3, 5 ) (T {1,2,3,4} ) (1) (2) (3) (4
Having said so, throughout the rest of this presentation, a spatio-temporal scale is simply referred to as a time scale and its elements are simply called instants.

Definition 2.2 (Timed poset). Let T be a time scale. A poset timed over T is a poset P equipped with a temporal projection π : P → T such that:

(IN1) if x ≤ y then π(x) ≤ π(y), i.e. the temporal projection is monotone, (IN2) for every t ≤ π(x) there is a unique element x ↓ t ∈ P such that π(x ↓ t) = t and x ↓ t ≤ x,
for all x, y ∈ P . The element x ↓ t is called the temporal cut, or simply the cut of x at instant t. This situation is depicted in [START_REF] Janin | Modeling in Event-B -System and Software Engineering[END_REF]. The cut function (x, t) → x ↓ t can be seen as sort of a (partial) action of the poset T over the poset P . Example 2.3 (Self-timed poset). Every poset T is a timed poset over itself with identity id as temporal projection.

Example 2.4 (Sub-timed poset). Let P be a poset timed over T . Let X ⊆ P be a downward closed subset of P . Let inc X : X → P be the inclusion function. Then the set X ordered as in P with π • inc X as temporal projection is also a timed poset.

Example 2.5 (Timed impulses). Let T be a time scale and E a set of event values extended into E ⊥ = E ∪ {⊥}. The set Imp(T, E) = T × E ⊥ is turned into a timed poset by equipping it with the temporal projection and partial order defined by π(u, e) = u and (t, e) ≤ (t , e ) when either (t, e) = (t , e ) or t < t and e = ⊥.

An element (t, e) ∈ Imp(T, E) with e = ⊥ is a timed impulse with value e at instant t. Observe there are no elements strictly above (or after) such an impulse and all elements strictly below (or before) bear no value as they are of the form (t , ⊥) for some t < t. Rephrased in terms of temporal cut, for every element (t, e) ∈ Imp(T, E) and instant t ≤ t, two cases are possible: either t = t and we have (t, e) ↓ t = (t, e), or t < t and we have (t, e) ↓ t = (t , ⊥).

Example 2.6 (Timed signals). With T and E as above, a timed signal is defined as a relation S ⊆ T × E that maps every instant t ∈ T to the set S(t) = {e ∈ E : (t, e) ∈ S} of event values received at instant t. Then a partial timed signal is a pair (u, S) ∈ T × P(T × E) such that for all (t, e) ∈ S we have t ≤ u.

The set Sig(T, E) of partial timed signals is turned into a timed poset by equipping it with the temporal projection defined by π(u, S) = u and the partial order relation defined by (u, S) ≤ (u , S ) when u ≤ u and S(t) = S (t) for all t ≤ u, for all (u, S), (u , S ) ∈ Sig(T, E). Following [START_REF] Matsikoudis | The fixed-point theory of strictly causal functions[END_REF], a pair (u, S) ∈ Sig(T, E) represents the observation of a timed signal until the instant u. In some sense, it is the temporal trace of some computation until that instant.

Rephrased in terms of temporal cut, for every partial signal (u, S) ∈ Sig(T, E) and instant v ≤ u = π(u, S) we have (u, S) ↓ v = (v, S ↓ v) with S ↓ v = {(t, e) ∈ S : t ≤ v}. Such a temporal cut (u, S) ↓ v models the observation of the partial signal (u, S) until instant v that lies before instant u. Definition 2.7 (Local cut). Let P be a poset timed over T . For every x ∈ P , property (IN2) induces a (total) function cut x : ↓ π(x) → P , called local cut, defined by cut x (u) = x ↓ u for every u ∈ T such that u ≤ π(x).

Remark 2.8. In the definition above and later in the text, we use the notation ↓ X ⊆ P for the downward closure of a subset X ⊆ P of a poset P defined by ↓ X = {y ∈ P : ∃x ∈ X, y ≤ x} that extends to an element x ∈ P by putting ↓ x = {y ∈ P : y ≤ x}. At first sight, this notation may clash with our chosen notation for cuts. However, for all x ∈ P and all u ≤ π(x) we have ↓(x ↓ u) = (↓ x) ↓ u as soon as we extent the (partially defined) cut point-wise. It follows that we can even write ↓ x ↓ u without any parenthesis with no ambiguity. Moreover, the downward closure can itself be seen as a cut over subsets of posets, defining for every X ⊆ P and x ∈ P the cut X ↓ x = {y ∈ X : y ≤ x}. Then we have ↓ x = P ↓ x. Lemma 2.9 (Local cut properties). Let x, y ∈ P and u, v ∈ T such that u, v ≤ π(x). Then:

(1) x ≤ y if and only if π(x) ≤ π(y) and

x = y ↓ π(x), (2) u ≤ v if and only if x ↓ u ≤ x ↓ v.
In particular, the (sub)posets ↓ x ⊆ P and ↓ π(x) ⊆ T are isomorphic posets as shown by the restriction of the cut to ↓ x and, as inverse, the temporal projection.

Proof. [START_REF] Janin | Modeling in Event-B -System and Software Engineering[END_REF]. Assume that x ≤ y. By (IN1) we have π(x) ≤ π(y) hence by (IN2), x = y ↓ π(x) since π(y ↓ π(x)) = π(x). Conversely, assume that π(x) ≤ π(y) and x = y ↓ π(x). Then, by definition of local cut, we have x ≤ y.

(2). Let u, v ≤ π(x). By (IN2) we have π(x ↓ u) = u and π(x ↓ v) = v. Assuming that u ≤ v we thus have u ≤ π(x ↓ v) hence there is y = (x ↓ v) ↓ u such that π(y) = u and y ≤ x ↓ v. But x ↓ v ≤ x hence y ≤ x and thus, by unicity (IN2), we have y

= x ↓ u therefore x ↓ u ≤ x ↓ v. Conversely, assuming that x ↓ u ≤ x ↓ v by (IN1) we have π(x ↓ u) ≤ π(x ↓ v) hence u ≤ v since, by (IN2), we have π(x ↓ u) = u and π(x ↓ v) = v.
Corollary 2.10. An element x ∈ P is minimal (resp. minimum) in P if and only if its temporal projection π(x) ∈ T is minimal (resp. minimum) in T . On the other hand, maximal elements in a timed poset can have arbitrary temporal projection as shown by timed impulse timed posets (see 2.5).

Derived notions

We review below several notions that derive from the notion of timed posets and that allow this notion to be related with other known concepts appearing in computer system modeling or programming language semantics. Temporal coherence. The following notion is inspired by Girard's notion of coherent space in linear logic [START_REF] Girard | Linear logic[END_REF]. A similar notion, even more closely related with timed domains, also appears in Winskel's notion of event structures [START_REF] Winskel | Event structures[END_REF]. Definition 3.1. Let P be a poset timed over T . Let x, y ∈ P . We say that x and y are coherent, a property denoted by x ¨y, when, for every x , y ∈ P such that x ≤ x and y ≤ y, if π(x ) = π(y ) then x = y , or, equivalently, for all u ≤ π(x), π(y), x ↓ u = y ↓ u. By extension, a subset X ⊆ P is a coherent subset when x ¨y for all x, y ∈ X. Lemma 3.2. Let x, y ∈ P . Then x ≤ y if and only if π(x) ≤ π(y) and x ¨y.

Proof. Assume that x ≤ y then we have π(x) ≤ π(x) hence x = y ↓ π(x). Let u ≤ π(x), π(y). We have x ↓ u ≤ x ≤ y hence, since ϕ(x ↓ u) = u, by (IN2), we have x ↓ u = y ↓ u. This proves that x ¨y. Conversely, assume that x ¨y and π(x) ≤ π(y). This implies that x ↓ π(x) = y ↓ π(x) hence x = y ↓ π(x) and thus x ≤ y.

In other words, coherence offers an alternative to the definition of timed poset via an order relation.

Remark 3.3. In some sense, every coherent subset X ⊆ P can be interpreted as the trace of a spatio-temporal computation that has been observed at the instants π(X). The (sub)posets X and π(X) are even isomorphic via the restriction of π to X and the downward closure ↓ X of a coherent subset is itself coherent.

Remark 3.4. The structure (P, ≤, ¨) defined for every timed poset P is a special case of an event structure [START_REF] Winskel | Event structures[END_REF], though dropping the finite history requirement. The same computational interpretations are possible. Two elements x and y in P describe concurrent computations when they are coherent and incomparable: they can both appear in the same computation trace as suggested above.

On the other hand, two incoherent elements x and y in P describe conflicting computations: they cannot appear in the same computation trace. More precisely, by the definition of coherence, when x ¨y there is u ∈ T in the past of both π(x) and π(y) such that x ↓ u = y ↓ u. This means that two distinct computations occur at the same instant (and position) u, a case that is interpreted as impossible.

Remark 3.5. Relating timed posets with event structures, one can also observe that the equivalence induced by π, defined by x ∼ π y when π(x) = π(y) for every x, y ∈ P , essentially is a symmetry2 as recently defined by Winskel in event structures [START_REF] Winskel | Events, causality and symmetry[END_REF].

This observation relates timed posets even more closely with the concepts introduced by Winskel in concurrency theory. However, the notion of timed poset is more restrictive than the notion of event structure. In a timed poset, coherence is uniformly defined via temporal projection. In an event structure, coherence is a given as part of the definition of that event structure.

Temporal distance. Timed concurrent system semantics can also be modeled by means of generalized ultrametric distance, as already developed quite in the depth by Lee, Liu et Matsikoudis [START_REF] Matsikoudis | The fixed-point theory of strictly causal functions[END_REF][START_REF] Liu | CPO semantics of timed interactive actor networks[END_REF][START_REF] Krishnaswami | Ultrametric semantics of reactive programs[END_REF]. The following definition shows that timed posets also induce such distances over their elements. Definition 3.6. Let P be a poset timed over T . Let P ↓ (T ) be the set of downward closed subsets of T ordered by reverse inclusion therefore with T itself as least element. The distance induced by π over P is the function

d : P × P → P ↓ (T ) defined by d(x, y) = {t ∈ T : t ≤ π(x), π(y), x ↓ t = y ↓ t} when x = y and by d(x, y) = T when x = y.
One can easily check that d(x, y) = ↓ d(x, y) for all x, y ∈ P hence the above definition is sound.

Lemma 3.7. The function d : P × P → P ↓ (T ) is a generalized ultrametric, that is, we have:

(1) d(x, y) = T if and only if x = y (separation), (2) d(x, y) = d(y, x) (symmetry), (3) d(x, y) ⊇ d(x, z) ∩ d(z, y) (ultra-metric inequality),
for all x, y, z ∈ P .

Proof. Properties (1) and ( 2) are immediate from the definition. Let x, y, z ∈ P and let u ∈ d(x, z) ∩ d(z, y). This implies that

x ↓ u = z ↓ u with u ≤ π(x), π(z) and z ↓ u = y ↓ u with u ≤ π(z), π(x) hence x ↓ u = y ↓ u with u ≤ π(x), π(y) that is u ∈ d(x, y).
Temporal presheaves. One last connection of timed posets with an existing notion, now complete, goes via the notion of categorical presheaves, a notion already used in concurrency theory especially by Catani, Stark and Winskel for modeling process calculi like CCS and the π-calculus [START_REF] Cattani | Presheaf models for CCS-like languages[END_REF][START_REF] Cattani | Presheaf models for the π-calculus[END_REF].

Let T be a poset. A presheaf on T is a functor F : T op → Set from the category T op , obtained from T by reversing the order relation, into the category Set of sets and functions. Then the following lemmas state that posets timed over T are isomorphic with what are known in category theory as the categories of elements of presheaves over T . This shows that timed posets and presheaves are essentially equivalent notions, an equivalence later stated as a categorical equivalence (see 4.10 below). Lemma 3.8. Let F : T op → Set be a presheaf over T . Then the set

P F = Σ t∈T F (t) = {(t, x) : t ∈ T, x ∈ F (t)},
equipped with the temporal projection defined by π(u, x) = u and the order relation defined by (u, x) ≤ (v, y) when u ≤ v and F (u ≤ v)(y) = x for all (u, x), (v, y) ∈ P F , is a timed poset, also known as the category of elements of F .

Proof. The fact P F equipped with ≤ is a poset goes as follows. Reflexivity follows from reflexivity of the order in T and the fact that F (u ≤ u) = id F (u) for all u ∈ T . Transitivity follows from the transitivity of the order in T and the fact that

F (u ≤ v) • F (v ≤ w) = F (u ≤ w) for all u, v, w ∈ T with u ≤ v ≤ w.
Anti-symmetry follows the anti-symmetry of the order in T . Indeed, whenever (u, x) ≤ (v, y) and (v, y) ≤ (u, y), by definition, we must have u ≤ v a,d v ≤ u hence u = v and thus x = id F (u) (y) hence x = y.

It remains to prove that π is a temporal projection. Let (u, x), (v, y) ∈ P F . If (u, x) ≤ (v, y), then, by definition of the order relation, we must have π

(u, x) = u ≤ v = π(v, y) which proves (IN1). Given w ≤ u = π(u, x) then there is z = F (w ≤ u)(x)
with, by definition of the order (w, z) ≤ (u, x) and if (w, z ) ≤ (u, x) then, again by definition of the order, we must have z = F (w ≤ u)(x) therefore z = z. This proves (IN2). Lemma 3.9. Let P be poset timed over T . Then the presheaf F P :

T op → Set defined by F P (t) = {x ∈ P : π(x) = t} and F P (u ≤ v)(x) = x ↓ u for all t, u, v ∈ T with u ≤ v and x ∈ F P (v)
, has an its category of elements isomorphic to P .

Proof. We first observe that whenever u ≤ v we indeed have u ≤ π(x) for all x ∈ F P (v) hence x ↓ u is well-defined. Then, proving that F P is a functor just amounts to proving that F P (u ≤ u) = id F P (u) and

F P (u ≤ v) • F P (v ≤ w) = F P (u ≤ w) for all u, v, w ∈ T such that u ≤ v ≤ w which makes no difficulty.
The stated isomorphism between P ans the category of elements of F P is also straightforward.

Timed morphisms

In this section, we define a class of timed morphisms between timed posets, called ∆-synchronous functions, as monotonic functions between timed posets that uniformly act on their underlying time scales. Somehow generalizing the approach of Colaço et al. [START_REF] Colaço | Clocks as first class abstract types[END_REF][START_REF] Colaço | Towards a higher-order synchronous data-flow language[END_REF], with timed posets interpreted as timed types, this uniformity requirement allows timed morphisms types to be defined not only as the domains and codomains of these morphisms, as in the simply-typed definition of function types, but also as the uniform transformation of time scales they induce.

∆-synchronous function. Throughout this section, let P and, resp. Q, be two posets timed over the time scales U and, resp. V . Definition 4.1 (∆-synchronous functions). A function f : P → Q together with a monotone function δ : U → V , called the temporal projection of f , is ∆-synchronous when, as depicted in ( 2):

(SD1) π(f (x)) = δ • π(x), (SD2) if x ≤ y then f (x) ≤ f (y), (SD3) f (x ↓ u) = f (x) ↓ δ(u),
for all x, y ∈ P and all u ∈ U such that u ≤ π(x). U V δ (SD1) (SD2)

P π P P P ≤ P Q π Q Q Q ≤ Q f f f (2) Remark 4.2. As soon a u ≤ π(x) then, by monotonicity of δ we have δ(u) ≤ δ • π(x) hence, by (SD1), δ(u) ≤ π(f (x)) therefore property (SD3) is sound.
Property (SD2) states that ∆-synchronous functions are poset functors. Property (SD1) formalizes the statement that they uniformly acts on the underlying time scales.

Example 4.3 (Self-synchronous). Every monotone function δ : U → V is a ∆-synchrone function between the self-timed posets U and V , with itself as temporal projection.

Lemma 4.4. Under hypothesis (SD1), properties (SD2) and (SD3) are equivalent.

Proof. Let f : P → Q be a function and let δ : U → V be a monotone function. Assume (SD1) and (SD2). Let x ∈ P and u ≤ π(x). By (IN2) we have

π(x ↓ u) = u hence π(f (x ↓ u)) = δ(u) by (SD1). By (SD2) we also have f (x ↓ u) ≤ f (x) hence, by (IN1), we have δ(u) = π(f (x ↓ u)) ≤ π(f (x)) and thus δ(u) ≤ π(f (x)). It follows, that f (x ↓ u) = f (x) ↓ δ(u) by (IN2). This proves (SD3).
Conversely, assume (SD1) and (SD3). Let x, y ∈ P such that x ≤ y. By (IN2) we have x = y ↓ π(x) hence f (x) = f (y) ↓ δ•π(x) by (SD3) and thus f (x) ≤ f (y). This proves (SD2).

On coherence preservation. It is easy to see that the ∆-synchronous image of a coherent subset bounded above is coherent. With a view towards application, this coherence preservation property is probably enough. Nevertheless, we show that without the boundedness condition this is no longer true and we provide sufficient additional conditions on time scale changes for coherence preservation.

(⊥) = ⊥, f (a) = a and f (b) = b is ∆-synchronous with temporal projection δ : U → V defined by δ(⊥) = 0, δ(a) = 1 and δ(b) = 1. Although a ¨b in U we have f (a) = a ¨b = f (b) in P . The function f does not preserve coherence.
Lemma 4.6. Assume that both U and V are meet-semilattices. Let δ : U → V be a meet-preserving function and let f : P → Q be a ∆-synchronous function with temporal projection δ. Then f is coherence preserving. Moreover, both P and Q are conditional meet-semilattice and the function f preserves conditional meet, i.e. it is stable in the sense of Berry [START_REF] Berry | Stable models of typed lambda-calculi[END_REF].

Proof. We first prove that f preserves coherence. Let x, y ∈ P such that x ¨y. We aim at proving that f (x) ¨f (y). Let v ≤ π(f (x), π(f (y)). By (SD1), both U and V are meet-semilattices and δ is meet-preserving, we have v ≤ delta(π(x) ∧ π(y)). Given u = π(x) ∧ π(y), since x ¨y we have

x ↓ u = y ↓ u hence, by (SD3), f (x) ↓ δ(u) = f (y) ↓ δ(u). It follows, since v ≤ δ(u) that we have f (x) ↓ v = f (y) ↓ v. This concludes the proof that f (x) ¨f (y).
Let x, y, z ∈ P such that x, y ≤ z. This means that x = z ↓ π(x) and y = z ↓ π(y) therefore, as routine checking shows, we have x ∧ y = z ↓ π(x) ∧ π(y). Indeed, if there is any z ≤ x, y then we have π(z

) ≤ π(x) ∧ π(y) therefore z = z ↓ π(z) ≤ z ↓ π(x) ∧ π(y).
By definition, a function is stable when it preserves pullbacks, that is, with timed posets, conditional meets. Let again x, y, z ∈ P such that x, y ≤ z. Since

x ∧ y = z ↓ π(x) ∧ π(y), by (SD3), we have f (x ∧ y) = f (z) ↓ δ(π(x) ∧ π(y)). Since δ is meet preserving, together with (SD1), this yields f (x ∧ y) = f (z) ↓ π(f (x)) ∧ π(f (y)) therefore f (x ∧ y) = f (x) ∧ f (y) since V is
also a meet-semilattice. This concludes the proof that f is stable.

Corollary 4.7. Let Coh(P ) and, resp. Coh(Q) be the set of coherent subsets of P and, resp. of Q, ordered by inclusion. Then, equipped with the point-wise extension of their temporal projection, they both are posets timed over P(U ) and P(V ) respectively. Moreover, the function f : Coh(P ) → Coh(Q) defined by extending f point-wise is ∆-synchronous, stable, and event linear in the sense of Girard [START_REF] Girard | Linear logic[END_REF], i.e. it is well-defined and we have f

(X ∩ Y ) = f (X) ∩ f (Y ) and f (X ∪ Y ) = f (X) ∪ f (X) for all X, Y ∈ Coh(X).
Remark 4.8. In example 4.5, both U and V are meet semi-lattices, but the function δ :

U → V is indeed not meet-preserving since, a ∧ b = ⊥ while δ(⊥) = 0 < 1 = δ(x) ∧ δ(b).
Synchronous functions. We restrict our attention to a smaller class of timed morphisms we call synchronous in the sense that their outputs are timed the same way as their inputs. Definition 4.9 (Synchronous function). A ∆-synchronous function f : P → Q with temporal projection δ : U → V is a synchronous function when U = V and δ = id U . In other words, f is synchronous when:

(SI1) π(f (x)) = π(x), (SI2) if x ≤ y then f (x) ≤ f (y), (SI3) f (x ↓ u) = f (x) ↓ u,
for all x ∈ P and u ∈ U such that u ≤ π(x).

Theorem 4.10. The category TPoset(T ) of posets timed over T and synchronous functions is equivalent to the category Psh(T ) of presheaves over T and natural transformations. More precisely, the functor ϕ : TPoset(T ) → Psh(T ) defined, for every timed poset P ∈ TPoset(T ), by ϕ(P ) = F P (see 3.9) and, for all synchronous function f : P → Q in TPoset(T ), by ϕ(f ) = α with α t (x) = f (x) for all t ∈ T and x ∈ F P (t), is a categorical equivalence.

Proof. A pseudo inverse functor for ϕ is the functor ψ : Psh(T ) → TPoset(T ) defined, for all presheaf F ∈ Psh(T ), by ψ(F ) = P F (see 3.8), and, for all natural transformation α : F ⇒ G in Psh(T ), by ψ(α) = f with f (t, x) = (t, α t (x)) for all (t, x) ∈ P F . This implies that the category TPoset(T ) is a Grothendieck topos. In the next section, we shall make explicit the constructions that prove it is, as a consequence, an elementary topos.

∆-synchronous vs synchronous functions. We show that every time scale change δ induces a (simple) contravariant time scale change functor in such a way that every ∆-synchronous function f with temporal projection δ uniquely (and uniformly) factorizes into a synchronous function followed by a (simple) time scale change, this functor having a (less simple) left adjoint.

Theorem 4.11 (Left Kan extension). Let δ : U → V be a monotone function. Then there are two categorical functors δ * : TPoset(V ) → TPoset(U )and δ ! : TPoset(U ) → TPoset(V ) and, for every P ∈ TPoset(U ) and Q ∈ TPoset(V ), two ∆-synchronous functions ω Q : δ * (Q) → Q and α P : P → δ ! (P ) both with temporal projection δ, such that every ∆-synchronous f : P → Q with temporal projection δ we both have:

(1) there is a unique synchronous function f * :

P → δ * (Q) such that f = ω Q •f * , (2) there is a unique synchronous function f ! : δ ! (P ) → Q such that f = f ! • α P ,
i.e. f uniquely factorizes through α P or ω Q . In particular, there is the categorical adjunction δ ! δ * . The functor δ ! is the left Kan extension operation along δ. This situation is depicted in [START_REF] Archipoff | Unified media programming: An algebraic approach[END_REF].

U V δ P Q f δ * (Q) ω Q ∃!f * δ ! (P ) α P ∃!f ! (3) Proof. The functor δ * is defined as follows. Let Q ∈ TPoset(V ). We define δ * (Q) = {(u, y) ∈ U × Q : π(y) = δ(u)} ordered point-wise with projection π(u, y) = u for all (u, y) ∈ δ * (Q). Clearly π is monotone, moreover, for every (u, y) ∈ δ * (Q) and u ≤ u we have (u, y) ↓ u = (u , y ↓ δ(u ) which proves that δ * (Q) ∈ TPoset(V ). Let h : Q → Q synchronous into some Q ∈ TPoset(V ). We define δ * (h) : δ * (Q) → DS(Q ) by δ * (h)(u, y) = (y, h(y)) for all (u, y) ∈ δ * (Q). Clearly δ * (h)
is synchronous, and δ * defined this way is indeed a functor.

Let then ω Q : δ * (Q) → Q simply defined by ω Q (u, y) = y for every (u, y) ∈ δ * (Q). By definition, we have π(y) = δ(u) for all (u, y) ∈ δ * (Q) and since ω Q is clearly monotone this proves it is ∆-synchronous.

Given ∆-synchronous f : P → Q with temporal projection δ, we define

f * : P → δ * (Q) by f * (x) = (π(x), f (x)). Given x ∈ P , by (SD1) we have (π(x), f (x)) ∈ δ * (Q) and π(f * (x)) = π(x). Given u ≤ π(x), we also have f * (x ↓ u) = (u, f (x ↓ u)) hence, by (SD2), f * (x ↓ u) = (u, f (x) ↓ δ(u)) hence f * (x ↓ u) = f * (x) ↓ u. This proves that f * is synchronous.
Last, by construction, we have f = ω Q •f * . The unicity of f * follows from the fact that, though not injective, ω Q is a mono since, when f = ω Q • g, for every x ∈ P , the value of f (x) in Q fixes the right projection of g(x) and synchronicity fixes its left projection.

The functor δ ! is defined as follows. Let P ∈ T P oset(U ). We define x ↑ v = {y ∈ P : ∃z ∈ P, v ≤ δ • π(z), z ≤ x, y} for every x ∈ P and v ∈ V . The set x ↑ v is the connected component of x above v via δ. This allows for defining δ ! (P ) = {(v, x ↑ v) ∈ V × P(P ) : v ∈ V, x ∈ P, v ≤ π(x)} ordered point-wise with reverse inclusion over P(P ) and with projection π(v, X) = v for every (v, X) ∈ δ ! (P ). We check that (v, X) ↓ w = (w, x ↑ w) for all w ≤ v and x ∈ X.

Let g : P → P be a synchronous function from into P ∈ TPoset(U ). We define δ ! (g) : δ ! (P ) → δ ! (P ) by δ ! (g)(v, X) = (v, g(x) ↑ v) for any choice of x ∈ X. If we chose another y ∈ X, then there is z ∈ P such that v ≤ δ • π(z) and z ≤ x, y. By monotony of g we thus have f (z) ≤ g(x), g(y) with π(f (z)) = π(z) since g is synchronous therefore f (y) ∈ f (x) ↑ v hence, as observed above, f (y) ↑ v = f (x) ↑ v, i.e. our definition is sound.

We easily check that δ ! (g) is synchronous and proving that δ ! defined as above is a functor makes no difficulty.

Let then α P : P → δ ! (P ) simply defined by α P (x) = (δ • π(x), x ↑ δ • π(x)) for every x ∈ P . We easily check that α P is monotone and since π(α P (x)) = δ • π(x) for all x ∈ P , it is ∆-synchronous. The fact δ ! defined as above is a functor makes no difficulties.

Given ∆-synchronous f : P → Q with temporal projection δ, we define

f ! : δ ! (P ) → Q by f ! (v, X) = f (x) ↓ v for every (v, X) ∈ δ ! (P ) and any choice of x ∈ X. We check that we indeed have v ≤ δ • π(x) hence, by (SD1), v ≤ π(f (x)).
If we chose another y ∈ X, then there is

z ∈ P such that v ≤ δ • π(z) and z ≤ x, y. This implies that f (z) ≤ f (x), f (y) hence, since v ≤ π(f (z)), we have f (z) ↓ v = f (x) ↓ v and f (z) ↓ v = f (y) ↓ v hence f (x) ↓ v = f (y) ↓ v, i.e. our definition is sound.
Given (v, X) ∈ δ ! (P ), by (SD1), we clearly have v = π(f ! (v, X)) and since f ! is obviously monotone this proves it is synchronous.

The fact f ! •α P = f follows from the definition. The unicity of f ! follows from the fact that α P , though not surjective, is an epi since every element (v, X) ∈ δ ! (P ) lays below α P (y) for some y ∈ P with X ≤ y hence f ! (v, X) is fully determined by f ! • α P (y) = f (y).

(u, Y ) ↓ u = (u , {(v, b) ∈ Y : v ≤ δ(u )})
for all (u, Y ) ∈ Sig * (δ, B) and u ≤ u. Then there is the ∆-synchronous function ω Q : Sig * (δ, B) → Sig(V, B) defined by ω Q (u, Y ) = (δ(u), Y ) for all (u, Y ) ∈ Sig * (δ, B) and, for every ∆-synchronous f : Sig(U, A) → Sig(V, B) with projection δ, the synchronous function f * : Sig(U, A) → Sig * (δ, B) defined for all (u, X) ∈ Sig(U, A) by f * (u, X) = (u, Y ) when f (u, X) = (δ(u), Y ) that uniquely factorizes f as above.

For the "upper" part, one can define over Sig(U, A) the least equivalence δ such that (u, X) δ (u , X ) whenever there is u ∈ U such that u, u ≤ u , δ(u) = δ(u ) and X ↓ u = X ↓ u. Then, one can check if (u, X) δ (u , X ) then f (u, X) = f (u , X ) for any ∆-synchronous function f with temporal projection δ. This means that Sig(U, A)/ δ can be used for defining δ ! (Q). However, in general, it does not seem that such a quotient is itself embeddable into (a sort of) a signal timed poset as done for the "lower" part above. Remark 4.13. In some sense, in the above example, the function ω Q acts as a scheduler that plans, within the time scale U , the events that will be emitted within the time scale V . Somehow dually, in the case both δ ! (Q) and α P are definable over timed signals, for instance when δ is injective, then it can be observed that function α P acts as a buffer that delays events timed on U until they are necessary for computation. More general conditions under which such an interpretation makes sense can be defined within timed signals, but we failed yet to find any general enough to be worth being detailed.

Remark 4.14. Every choice of a time scale provides a granularity at which a system behavior can be observed. The above result can thus be seen as a tool box that allows the behavior of a timed system to be analyzed at various granularity. There appear some potential links with abstraction/refinement techniques for system design [START_REF] Janin | Modeling in Event-B -System and Software Engineering[END_REF] and abstract interpretation techniques for system analysis [START_REF] Cousot | Logical abstract domains and interpretations[END_REF].

5 More on synchronous functions Theorem 4.11 shows that ∆-synchronous functions are inherently linked with synchronous functions. Theorem 4.10 ensures that the category TPoset(T ) of posets timed over T and synchronous functions is a Grothendieck topos (see 5.18) therefore an elementary topos. We review below the concrete constructions over timed posets that derive from such a result and, with a view towards system modeling, describe their fairly intuitive interpretation. Lemma 5.1 (Clock ticks). Let P be a poset timed over T . Then the temporal projection π : P → T is the unique synchronous function from P into T . In other words, the self-timed poset T is terminal in TPoset(T ).

Remark 5.2. In some sense, the time scale T , seen as a self-timed poset, can be understood as a clock. Indeed, every synchronous function c : T → P defines a timed constant which is produced, pieces after pieces, as time is passing. Observe however that the existence of such a function implies that c(T ) is a subset of P isomorphic to T . There are posets timed over T with no such a subset as shown by any strict downward closed subset of T (see 2.4). In other words, timed posets may also contain timed constants in which evolution in time may stop at some instant as if they were timed over a smaller (sub) time scale. Definition 5.3 (Synchronous product). Let P, Q be two posets timed over T . The synchronous product of P and Q is defined as the set P ⊗ Q = {(x, y) ∈ P × Q : π P (x) = π Q (y)} ordered point-wise and equipped with the temporal projection defined by π(x, y) = π(x) = π(y) for all (x, y) ∈ P ⊗ Q. Lemma 5.5. Then P ⊗ Q is a timed poset over T and, with projections p 1 : P ⊗ Q → P and p 2 : P ⊗ Q → Q, it is the categorical product of P and Q in TPoset(T ).

Proof. Given f : R → P and g : R → Q, we have to show that f ×g : R → P ⊗Q defined for all z ∈ R by f ×g(z) = (f (z), g(z)) is the unique synchronous function h : RT → P ⊗ Q through which f and g factorizes, i.e. we have f = p 1 • h and g = p 2 • h, as depicted in Figure 2.

P Q P ⊗ Q R ∀f ∀g ∃!h p1 p2 Fig. 2. Categorical product diagram.
This property is routine to check.

Remark 5.6. The interpretation of the above synchronous product shall be obvious. Thanks to the fact it is a categorical product, every pair of synchronous functions f : R → P and g : R → Q uniquely factorizes through some synchronous gluing f × g : R → P ⊗ Q of the functions f and g. Such a combinator over synchronous functions could be used is an arrow programming style [START_REF] Hughes | Programming with arrows[END_REF].

Remark 5.7 (On coproduct). One can check that the coproduct3 P ⊕ Q of two timed posets with canonical injection eventually leads to the definition of categorical coproduct of P and Q in TPoset(T ). Then the empty timed poset is the initial object in TPoset(T ). This shows that the category TPoset(T ) is bi-cartesian.

Such a coproduct can be used as a timed alternative. However, such an alternative is very likely to be solved at initialization time, before any instant in T . Indeed, as soon as T has a minimum, every coherent subset of P ⊕ Q is necessarily either the embeddings of a coherent subsets of P or the embedding of a coherent subset of Q. No mixed subset is coherent.

↓ u : P ↓ u → Q ↓ u defined by P ↓ u = {x ∈ P : π(x) ≤ u}, Q ↓ u = {y ∈ Q : π(y) ≤ u} and (f ↓ u)(x) = f (x) for all x ∈ P ↓ u.
Observe that both P ↓ u and Q ↓ u are downward closed hence (see Example 2.4) they both are posets timed over T . Moroever, since f is synchronous, property (SI1) ensures that f (x) ∈ Q ↓ u for all x ∈ P ↓ u therefore f ↓ u is a well defined synchronous function from P ↓ u into Q ↓ u. Definition 5.9 (Synchronous exponent). Let P and Q be two posets timed over T . The synchronous exponent of Q by P is defined to be the set [P → T Q] of all pairs (u, h) with u ∈ T and synchronous functions h : P ↓ u → Q ↓ u, with temporal projection defined by π(u, h) = u and partial order defined by

(u 1 , h 1 ) ≤ (u 2 , h 2 ) when u 1 ≤ u 2 and h 1 = h 2 ↓ u 1 for all (u, h), (u 1 , h 2 ), (u 2 , h 2 ) ∈ [P → T Q].
Lemma 5.10. Let P, Q, R be three posets timed over T . Then [Q → T R] is a poset timed over T . Moroever, there is also the synchronous function eval :

Q R ⊗ Q → R defined by eval ((u, h), y) = h(y) for all ((u, h), y) ∈ R Q ⊗ Q therefore with π(y) = u.
The timed poset [Q → T R] with function eval is the categorical exponent of R by Q in TPoset(T ), i.e. for all synchronous function g : P ⊗Q → R, the function g * : P → R Q defined, for all x ∈ P , by g * (x) = (π(x), λy.g(x ↓ π(y), y)) is the unique synchronous function from P into R Q such that g(x, y) = eval (g * (x), y) for all (x, y) ∈ P ⊗ Q.

Proof. The above situation is depicted in Figure 3.

P R Q ∃!g * P ⊗ Q R Q ⊗ Q R g * × id eval ∀g Fig. 3. Categorical exponent diagram.
The proof of this lemma essentially goes by first checking that both eval and g * are indeed well defined synchronous functions. In particular, when y ∈ P ↓ π(x) then we indeed have π(y) ≤ π(x) therefore eval (g * (x), y) = f (x ↓ π(y), y) is indeed well-defined. The fact that g * is the unique synchronous function such that g(x, y) = eval (g * (x), y) for all (x, y) ∈ P ⊗ Q is then routine to check.

Remark 5.11. This result states that every synchronous function f : P → Q can itself be represented by coherent subset {f ↓ u} u∈T of exponent Q P which can be transmitted and applied on-the-fly over the pieces {x ↓ u} u≤π(x) of an argument x ∈ P . Then, as soon as the instant π(x) is reached, such an on-thefly application stops since the remaining values {f ↓ u} u ≤π(x) of the functions cannot be synchronized with any further argument. This property could perhaps be used designing a timed programming language where resources are indeed freed whenever a timed (sub)computation terminates.

The following lemma comes as a complement of the construction of timed posets from downward closed subsets of timed posets (see 2.4), by characterizing subobjects 4 of the category TPoset(T ) precisely as these downward closed subsets. Lemma 5.12 (Timed subobjects). Let f : P → Q be a synchronous function. Then f (P ) = ↓ f (P ), moreover, f is injective if and only if P f (P ) as posets.

Proof. Let x ∈ P and let y ≤ f (x). This means that y = f (x) ↓ π(y). By (SI3) we thus have y = f (x ↓ π(y)) hence y ∈ f (P ).

Given then x, y ∈ P . If x ≤ y then, by (SI2), we have f (x) ≤ f (y). Conversely, assume that f (x) ≤ f (y) hence f (x) = f (y) ↓ π(f (x)). By (SI1) and monotony of π we thus have π(x) ≤ π(y). Then, (SI3) we have

f (y ↓ π(x)) = f (y) ↓ π(x) hence, by (SI1), f (y ↓ π(x)) = f (y) ↓ π(f (x)). Together, we thus have f (y ↓ π(x)) = f (x) hence x = y ↓ π(x) since f is injective and thus x ≤ y.
In the category Set, there is the powerset construction P(E) of subsets of a set E. In TPoset(T ) the analogous power object is defined below. Definition 5.13 (Synchronous power). Let P be a poset timed over T . The synchronous power of P is defined as the set Ω P = {(u, X) ∈ T × P(P ) : X = ↓ X, π(X) ≤ u} with temporal projection defined by π(u, X) = u and partial order defined by (u, X) ≤ (v, Y ) when u ≤ v and X = Y ↓ u for all (u, X), (v, Y ) ∈ Ω P .

Lemma 5.14. The synchronous power Ω P of a timed poset P is a poset timed over T and the power object of P in TPoset(P ).

Proof. We first prove that Ω T is the subobject classifier in TPoset(T ) as stated in Remark 5.17. For such a purpose, given a poset P timed over T , we easily check that the characteristic function X X : P → Ω T of a downward closed subset X ⊂ P is uniquely defined by X X (x) = (π(x), π(↓ x ∩ X)) for every x ∈ P .

Then we prove that that Ω P [P → Ω T ] which, by known result in topos theory proves that Ω P is indeed the power object of P . The expected isomorphism f :

Ω P → [P → Ω T ] is defined, for every (u, X) ∈ Ω P , by f (u, X) = (u, X X ↓ u) ∈ [P → Ω T ].
The inverse image of every pair (u, h) ∈ [P → Ω T ] is defined by f -1 (u, h) = (u, {x ∈ P ↓ u : h(x) = true(x)}) with true defined in Remark 5.17.

Example 5.15 (Timed signals). Continuing Examples 2.5 and 2.6 we have Ω Imp(T,E) ∼ = Sig(T, E). Indeed, every timed signal (u, X) ∈ Sig(T, E) is a collection of (non trivial) timed impulses arrived before or at instant u.

Remark 5.16. The above example illustrates how power objects can be interpreted in terms of parallelism: a computation trace in Ω P models arbitrarily many computation traces in P that are run synchronously. Moreover, just like subsets, two sub-traces identical at some instant are eventually merged into a single one. Alternatively, it also makes sense to interpret traces in the power object as pending nondeterministic choices much like in power domain constructions.

Remark 5.17. Following topos theory [START_REF] Barr | Category Theory for Computing Science[END_REF][START_REF] Lane | Sheaves in Geometry and Logic[END_REF], the timed domain Ω T = {(u, V ) ∈ T × P(T ) : V = ↓ V ≤ u}, with the synchronous function true : T → Ω T defined by true(t) = (t, ↓ t) for all t ∈ T is the subobject classifier in TPoset(T ). In other words, for every poset P timed over T , for every downward closed subset X ⊆ P , there is a unique synchronous function X X : P → Ω, the characteristic synchronous function of X, such that, given the synchronous inclusion inc X : X → P we have X f • inc X = true • π and this is a pullback square, i.e. for all synchronous f : Q

→ P such that X f • f = true • π we necessarily have f (Q) = X therefore f uniquely factorizes through inc X . P Q Ω T T ∀f ∃!X f π true Fig. 4. Subobject classifier pullback square.
As an immediate consequence of Theorem 4.10, or gathering the results stated in this section5 , we have: Theorem 5.18. The category TPoset(T ) is an elementary topos, i.e. it is cartesian closed, finitely complete and has all powerobjects.

6 More on ∆-synchronous functions Clearly, timed posets identities are synchronous functions and every composition of two ∆-synchronous functions is itself ∆-synchronous with temporal projection the composition of their temporal projections. It follows that every choice of a category C ⊆ Poset of time scales and time scale transformations yields the category TPoset(C) of posets timed over time scales in C and ∆-synchronous functions with temporal projections that are morphisms in C. In the most general case, one can choose for C the category Poset.

Throughout the rest of the section, we assume that the chosen time scale category C ⊆ Poset is cartesian closed with terminal poset { * } ∈ C. We also assume some time scales U and V ∈ C and some posets P and, resp., Q ∈ TPoset(C) timed over U and, resp., V . Lemma 6.1 (One instant clock). Let 1 be the one element poset { * } timed over itself. Then 1 is the terminal element in TPoset(C). Definition 6.2 (Asynchronous product). The asynchronous product of P and Q is defined as the cartesian product P × Q with temporal projection π : P × Q → U × V by π(x, y) = (π(x), π(y)), ordered point wise. Lemma 6.3. Then P × Q is a poset timed over U × V ∈ C. Both projections p 1 : P ×Q → P and p 2 :

P ×Q → Q are ∆-synchronous with temporal projection π(p 1 ) = p 1 : U × V → U in C and π(p 2 ) = p 2 : U × V → V in C.
Together, they form the categorical product of P and Q in TPoset(C). Definition 6.4 (Asynchronous exponent). The asynchronous exponent of Q by P is defined as the set Q P of ∆-synchronous function from P into Q with temporal projections in V U ∈ C just as already defined in 4.1. Lemma 6.5. Then Q P is a poset timed over V U ∈ C. The evaluation mapping eval : Q P × P → Q defined, for all f ∈ Q P and x ∈ P , by eval (f, x) = f (x) is ∆-synchronous with, thanks to (SD1), temporal projection π(eval ) = eval in C. Together, they form the exponent of Q by P in TPoset(C). Gathering all the above lemmas, we have: Theorem 6.6. The category TPoset(C) is cartesian closed whenever C is. Remark 6.7. The empty poset timed over the empty time scale is the initial object. The disjoint sum is the coproduct in TPoset(C) therefore TPoset(C) is even bi-cartesian closed whenever C is. The next theorem generalizes such a remark. Definition 6.8 (Projection of diagram functor). Let G = V, E, s, t be a graph with vertices V , edges E, source and target functions s, t : E → V . Let F : G → TPoset(C) be a diagram functor 6 . The temporal projection of F is defined to be the diagram functor H : G → C defined by, for all v ∈ V , the poset H(v) is the time scale over which F (v) is timed and, for all e ∈ E, the time scale tranformation H(e) is the temporal projection π • F (e) of the ∆-synchronous function F (e). Theorem 6.9 (Limit and colimit). A diagram functor F : G → TPoset(C) has a limit (resp. a co-limit) in Poset(C) whenever its temporal projection H : G → C has a limit (resp. a colimit) in C.

Proof. Throughout this proof, for each v ∈ V , let π v : F (v) → H(v) be the temporal projection of the poset F (v) timed over H(v).

The limit case. Assume H has a limit cone given by T ∈ C and, for each

v ∈ V , a function δ v : T → H(v) in C. By definition, we have δ t(e) = H(e) • δ s(e)
for every e ∈ E. Let then

P = t∈T {t} × v∈V π -1 v (δ v (t))
ordered point-wise with first projection as temporal projection. It is a poset timed over T . There are also the ∆-synchronous projection p v : P → F (v), one for each v ∈ V , defined by

p v (t, {x v } v∈V ) = x v for every (t, {x v } v∈V ) ∈ P with temporal projection π(p v ) = δ v .
Then it is routine to check that the subset

X = (t, {x v } v∈V ) ∈ P : ∀e ∈ E, x t(e) = F (e)(x s(e) )
is downward closed therefore a sub-timed poset of P and, equipped with the (restriction of) the projection {p v } v∈V is the limit of F .

The colimit case.

Assume that H has a colimit cone given by T ∈ C and,

for each v ∈ V , a function δ v : H(v) → T in C.
By definition, we have δ s(e) = δ t(e) • H(e) for every e ∈ E. Then we can define

P = t∈T {t} × v∈V {v} × π -1 v (δ v (t))
ordered point-wise with first projection as temporal projection. It is a poset timed over T . Moreover, there are the ∆-synchronous injection ι v : F (v) → P with temporal projection δ v defined by

ι v (x) = (δ v • π v (x), v, x)
for all x ∈ F (v) and we have P = v∈V ι v (F (v)).

Let then be the least equivalence over P such that we have

ι s(e) (x) ι t(e) (F (e)(x))
for all e ∈ E and x ∈ F (s(e)). It is routine checking that for all x, y ∈ P , if x y then π(x) = π(y) and for all t ∈ T such that t ≤ π(x) we have x ↓ t y ↓ t. It follows that P/ can be equipped with the order defined for all x, y ∈ P by [x] ≤ [y] when there is x ∈ [x] such that x ≤ y and the temporal projection defined for all x ∈ P by π([x]) = π(x).

Then P/ is a poset timed over T and, for every v ∈ V , the function j v : F (v) → P/ , defined by

j v (x) = [ι v (x)]
for all x ∈ F (v) is ∆-synchronous with temporal projection δ v . By construction, we have j s(e) = j t(e) • F (e) for every e ∈ E. Then, it is routine to check that P/ equipped with the functions {j v } v∈V form the colimit of F . As a particular case, a fixpoint equation of timed posets (or, as defined below, timed domains) has an inductive (resp. co-inductive) solution whenever the projection of this equation over time scales has an inductive (resp. co-inductive) solution.

Timed domains

Timed domains ought to be cpos timed over cpos with continuous projections and cuts. Such a definition is formalized via the notion of pre-continuous timed posets so that timed domains can precisely be defined as pre-continuous timed posets timed over cpos. Definition 7.1 (Pre-continous timed posets). Let P be a poset timed over T . We say that P is a pre-continuous timed poset when (IN3) if X is directed and π(X) is defined then so is X, for all X ⊆ P . Remark 7.2. In general, neither Imp(T, E) nor Sig(T, E) (see 2.5 and 2.6) are pre-continuous. Indeed, as soon as there is t = U with directed U ⊆ T and t ∈ U , then, in Imp(T, E), we have {(t, e) ↓ u} u∈U = {(t, ⊥) ↓ u} u∈U therefore this set as no upper bound. A remedy to this fact is proposed below.

Example 7.3 (Observable timed signals). Let < < be the relation called here way before, defined for every instant t, u ∈ T by t < < u when for every directed subset U ⊆ X such that U = u there must exists u ∈ U such that t ≤ u . Let Sig C (T, E) ⊆ Sig(T, E) be the set of timed signals (u, X) such that t < < u for all (t, e) ∈ X, i.e. every event (t, e) ∈ X is observable in the sense that it can be observed in any series of observations performed as any (directed) set of instants U such that U = u. Then, with the cut defined by (u, X) ↓ u = (u , {(t, e) ∈ X : t < < u }) for all u ≤ u, the resulting set of signals Sig C (T, E) is a pre-continuous timed poset though not, in general, a sub-timed poset of Sig(T, E). Lemma 7.4. Let P be a pre-continous timed poset timed over T . Then, for every x ∈ P the local cut cut x : ↓ π(x) → P (see 2.7) is continuous.

Proof. Let x ∈ P and let U ⊆ T , directed, such that U ≤ π(x). Assume that there is v = U . Proving the continuity of cut x amounts to proving that

x ↓ U = x ↓ v.
Since the local cut is monotone the set x ↓ U is directed with π(x ↓ U ) = U . By (IN3), there is thus y ∈ P such that (x ↓ U ) = y ≤ x. Moreover, by (IN1), we have π(y) ≤ π(x) hence, by (IN2), we have y = x ↓ π(y).

Since π(x ↓ u) = u, by monotony of the temporal projection, we have U = v ≤ π(y). Moreover, since U = v we have x ↓ U ≤ x ↓ v hence, by definition of least upper bound we have y = x ↓ π(y) ≤ x ↓ v hence π(y) ≤ v. This proves that π(y) = v hence y = x ↓ v. Remark 7.5. In general, the continuity of all local cuts in a timed poset does not imply the continuity of that timed poset as shown by the example P 1 = N timed as a timed subset of

T 1 = N = N ∪ {∞} self-timed.
Also, the continuity of a timed poset does not imply the continuity of its temporal projection, as shown by the example P 2 = N timed as a timed subset of T 2 = N ∪ {∞ } self-timed, with ∞ another upper bound of N, distinct and incomparable with ∞.

Lemma 7.6. Let P be a pre-continuous timed poset, timed over T . Assume that T is complete. Then P is complete and its temporal projection is continuous.

Proof. Let X ⊆ P directed. By monotony of the temporal projection, the set π(X) ⊆ T is directed. Since T is complete, there is v = π(X). Since P is pre-continuous, by (IN3), there is y = X. This concludes the proof that P is complete.

For every x ∈ X, we have x ≤ y therefore we have x = y ↓ π(x). Since π(X) is directed, by continuity of cut y (Lemma 7.4) we have x = y ↓ π(X) that is y = y ↓ v hence v = π(y). This concludes the proof that π is continuous. Definition 7.7 (Timed domain). A timed domain is a pre-continuous timed poset timed over a complete time scale, hence, as proved above also a complete poset with continuous local cuts and temporal projection.

Remark 7.8. As a consequence of 7.4, a timed domain P is continuous/algebraic in the sense of Scott if and only if T itself is continuous/algebraic. Indeed, it can be shown that for all x, y ∈ P , we have x < < y if and only if π(x) < < π(u). Lemma 7.9 (∆-synchronous vs continuous). Let P and Q be two timed domains. Let f : P → Q be a ∆-synchronous function with temporal projection δ : U → V . Assume that δ is continuous. Then f is continuous.

Proof. Let X ⊆ P directed and, by completness of P , let y = X. For every x ∈ X we have x ≤ y hence x = y ↓ π(x) and thus, by (SD3), f (x) = f (y) ↓ δ • π(x) with δ • π(x) ≤ π(f (y)). Since the temporal projection π, the function δ and the local cut cut f (y are all continuous this ensures that f (X) = f (y)δ • π( X). By continuity of π we have π( X) = π(y). By (SD1) we have π(f

(y)) = δ • π(y) therefore by (IN2) we have f (y)δ • π( X) = f (y) hence f (X) = f (y).
Remark 7.10. As a special case of the above lemma every synchronous function between timed domains is continuous. Theorem 7.11. Let T be a cpo. Then the category TCpo(T ) of timed domain over T and, when T has a least element, the category TCpo ⊥ (T ) of timed domain over T with least element, with, in both cases, synchronous (and continuous) functions between them, are topoi.

Proof (Sketch of ). The proof goes by rephrasing the Scott topology in terms of a Grothendieck topology J over posets in such a way that (the categories of elements of the) sheaves in Sh(T, J) are the pre-continuous timed posets timed over T . As a reminder, a subset X of a poset E is Scott closed when it is downward closed and for every directed Y ⊆ X, if Y is defined then Y ∈ X. Then, for every t ∈ T , we define J(t) to be the set of all downward closed subsets U ⊆ T such that U ≤ t, i.e. U is a sieve on t, and their Scott closure U equals ↓ t.

One can easily check that J is a Grothendieck topology (see [START_REF] Lane | Sheaves in Geometry and Logic[END_REF] p 110). Moreover, one can also check that a timed poset P ∈ TPoset(T ) is pre-continuous if and only if its associated presheaf F P : T op → Set (see 3.9) is a sheaf for J (see [START_REF] Lane | Sheaves in Geometry and Logic[END_REF] p 121). This ensures that the categorical equivalence between TPoset(T ) and Psh(T ) (see Theorem 4.10) also defines a categorical equivalence between the subcategories TCpo(T ) and Sh(T, J). It follows that TCpo(T ) is also a topos since Sh(T, J) is.

For the category TCpo ⊥ (T ) the argument is similar, though taking instead the topology J defined from J, by letting J (t) = J(t) when t > ⊥ and J (⊥) = {{⊥}, ∅}. This forces every sheaf in Sh(T, J ) to be a singleton on ⊥, and therefore its category of elements to have a least element.

Remark 7.12. The terminal object, products and exponentials in both TCpo(T ) and TCpo ⊥ (T ) are defined just in the same way as in TPoset(T ). The power object Ω P differs from TPoset(T ) by the fact that it only contains pairs of the form (u, X) ∈ T × P(P ) where X is not only downward closed but also Scott closed. This follows from the fact that in both TCpo(T ) or TCpo ⊥ (T ), subobjects correspond to Scott closed subsets of timed domains. Theorem 7.13. Both categories TCpo(Cpo) of timed domains or TCpo ⊥ (Cpo ⊥ ) of timed domains with least elements, and, in both cases, ∆-synchronous functions with continuous temporal projections (therefore themselves continuous) are cartesian closed categories.

Proof. Since Cpo and, resp. Cpo ⊥ are cartesian closed, it is routine to check that terminal objects, asynchronous products and asynchronous exponents both in TCpo(Cpo) or in TCpo ⊥ (Cpo ⊥ ) are defined just as in TPoset(Poset) (see Theorem 6.6).

Remark 7.14. Both categories above have an initial object when extended with the empty timed domain over the empty time scale. They also have coproducts: the disjoint sum in TCpo(Cpo) and the coalescent sum in TCpo ⊥ (Cpo ⊥ ). In other words, both (slightly extended) categories are bi-cartesian closed. More generally, it can be shown that Theorem 6.9 still holds when restricted to the category TCpo ⊥ (Cpo ⊥ ).

Timed fixpoints and causality

In the category TCpo ⊥ (Cpo ⊥ ) of timed domains with least elements, every ∆synchronous function has a least fixpoint. Following the footsteps of Matsikoudis and Lee [START_REF] Matsikoudis | The fixed-point theory of strictly causal functions[END_REF], we examine below the property of the induced least fixpoint operators.

Lemma 8.1. Let P ∈ TCpo ⊥ (Cpo ⊥ ) be a timed domain with least element ⊥ P timed over a complete time scale T with least element ⊥ T . Let f : P → P be a ∆-synchronous function with continuous temporal projection δ : T → T . Then both least fixpoints µ P (f ) ∈ P and µ T (δ) ∈ T are defined. Moreover, we have π • µ P (f ) = µ T (δ).

Proof. By Scott continuity, we have µ P (f ) = n∈ω f n (⊥ P ) and µ T (δ) = n∈ω δ n (⊥ T ). Moreover, by (SD1) and induction over n ∈ ω, since π(⊥ P ) = ⊥ T we easily prove that π • f n (⊥ P ) = δ n (⊥ T ) for all n ∈ ω. By continuity of π (7.6) we have π

• µ P (f ) = n∈ω δ n (⊥ T ) and thus π • µ P (f ) = µ T (δ).
Example 8.2 (Timed signals). Let T = R + be the time scale of positive reals completed with a maximum element ∞. Let f : Sig(T, E) → Sig(T, E) defined for all (u, X) ∈ Sig(T, E) by f (u, X) = (u + 2, {(0, e 0 )} ∪ {(t + 2, e) : (t, e) ∈ X}) for some fixed event value e 0 ∈ E. Then f is ∆-synchronous with temporal projection t → t + 2 with ∞ as least fixpoint. Then we have the least fixpoint µ(f ) = (∞, {(2 * n, e 0 ) : n ∈ N}). Theorem 8.3. Let P P be the exponent in TCpo ⊥ (Cpo ⊥ ) of the timed domain P by itself and let T T be the exponent of the object T by itself in Cpo ⊥ . Then the least-fixpoint mapping µ P : P P → P is a ∆-synchronous function with continuous temporal projection π(µ P ) = µ T : T T → T .

Proof. The fact µ P : P P → P is ∆-synchronous follows from the fact that µ P is monotone (SD2) and, by Lemma 8.1, we have π • µ P (f ) = µ T • π(f ) for every f ∈ P P (SD1). This means that π(µ P ) = µ T . Finally, as it is a known fact from domain theory that µ T : T T → T is continuous this proved that µ P is indeed in TCpo ⊥ (TCpo ⊥ ).

Remark 8.4. When computing the fixpoint of a function f the output of that function is sort of rewired on its input. In signal processing, there is a feedback loop. Since both inputs and outputs lie in the same timed domain, their temporal projections lie in the same time scale and can thus be compared. By default, every ∆-synchronous function is locally causal in the sense that, by monotonicity, for every n ∈ ω, with x n = f n (⊥ P ), we have x n ≤ f (x n ) and π(x n ) ≤ π(f (x n )). This suffices for Theorem 8.3 to hold. However, intuition suggests that we could require these functions to be globally causal as defined and studied below. Definition 8.5 (Global causality). Let P be a poset timed over T with least element ⊥ P ∈ P therefore also a least element ⊥ T ∈ T . Let f : P → P be a ∆-synchronous function with temporal projection δ : T → T . We say that f is globally causal when π(x) ≤ π(f (x)) for every x ∈ P . Equivalently, by (SD1), when t ≤ δ(t) for all t ∈ π(P ).

Though not needed in the general case, such a notion appears when restricting to TCpo ⊥ (SLattice ⊥ ) so that ∆-synchronous function preserves arbitrary coherence ( 4.6). Indeed, in SLattice ⊥ , the fixpoint function µ T is not in general meet-preserving hence Theorem 8.3 fails. Theorem 8.6. In the category TCpo ⊥ (CSLattice ⊥ ) of domains timed over continuous meet-semilattices and ∆-synchronous functions with meet-preserving temporal projections, the fixpoint mapping µ P : P P → P is ∆-synchronous provided we restrict ourselves to causal ∆-synchronous functions.

Proof. Applying Theorem 8.3 it suffices to prove that, restricted to (self-synchronous) meet-preserving causal functions, the least fixpoint function µT : T T → T is itself meet preserving.

For such a purpose, let δ 1 , δ 2 : T → T be two causal meet-preserving functions. Remember that δ 1 ∧ δ 2 : T → T is simply defined by (δ 1 ∧ δ 2 )(u) = δ 1 (u) ∧ δ 2 (u) for every u ∈ T . Since both δ 1 and δ 2 are causal then δ 1 ∧ δ 2 is also causal therefore the restriction to causal functions still yields a meet-semilattice.

Since δ 2 is causal, we have δ 1 ≤ δ 2 • δ 1 . But we also have id ≤ δ 2 hence, by monotony of δ 1 , we have δ 1 ≤ δ 1 • δ 2 . Rephrased in a single line we this have proved that

δ 1 ≤ δ 1 • δ 2 , δ 2 • δ 1 (4)
By symmetry, we prove similarly that ≤ δ w hence, since δ 2 is causal and n ≤ |w| 2 we have δ n 2 ≤ δ w . Applied to the above finite meet, since on of the two above cases must occur in each member, we have

δ 2 ≤ δ 1 • δ 2 , δ 2 • δ 1 (5)
δ n 1 ∧ δ n 2 ≤ (δ 1 ∧ δ 2 ) 2n
As this holds for every n ∈ N, applied to the minimal element ⊥, we thus have

n∈N δ n 1 (⊥) ∧ δ n 2 (⊥) ≤ n∈N (δ 1 ∧ δ 2 ) 2n (⊥)
Now, by continuity of the meet, we have µ(δ 1 ) ∧ µ(δ 2 ) on the left of that inequality. Moreover, since the sequence {(δ 1 ∧ δ 2 ) n (⊥)} is monotonic it has the same greatest lower bound than its even subsequence, we thus have µ(δ 1 ∧ δ 2 ) on the right of the inequality. It follows that µ(δ 1 ) ∧ µ(δ 2 ) ≤ µ(δ 1 ∧ δ 2 ).

By causality, µ(δ 1 ) ∧ µ(δ 2 ) is a fixpoint of δ 1 ∧ δ 2 and µ(δ 1 ∧ δ 2 ) is its least fixpoint hence we also have µ(δ 1 ∧ δ 2 ) ≤ µ(δ 1 ) ∧ µ(δ 2 ). It follows that µ(δ 1 ) ∧ µ(δ 2 ) = µ(δ 1 ∧ δ 2 ) which concludes the proof that µ is meet-preserving over non expanding functions. Remark 8.7. Despite such a result, global causality remains quite an ad hoc restriction. We are still in need of some additional restrictions on the notion of ∆-synchronous functions in a category TCpo ⊥ (C ⊥ ) that would guarantee their combinations to be globally causal whenever applicable. For such a purpose, adjunctions in posets could be a direction to investigate.

Conclusion

Along these pages, we have detailed a possible mathematical framework for the modeling of spatio-temporal system behaviors that extends to space and time the classical notion of cpos and continuous functions used in denotational semantics.

Bi-cartesian closed with internal fixpoint operators, and essentially all limits or co-limits that may exist in Cpo ⊥ , the category TCpo ⊥ (Cpo ⊥ ) eventually turned out to be a fairly general and fully featured category for defining and analyzing the behaviors of timed programs with both synchronous and asynchronous versions of typical categorical constructs such as sum, products or exponents, as well as, in the synchronous case, power-objects.

Technically rooted in topos and fibration theory, via the category of elements of sheaves over certain Grothendieck topologies, the resulting definitions and constructions have (mostly) been stated in elementary mathematical terms. This means that, after some more polishing and more detailed application studies, such material could even be taught to standard students in computer science and software engineering.

With a view towards concrete applications, we have not yet developed at all the potential offered by the left Kan extension theorem (see 4.11 and 4.12). When time scales are built from concrete numerical scales such a N, Q + or R + , it allows us to define sound lifting of operators over these time scales such as delays, projections, stretches, etc., into timed program constructs. This would lead to pursuing the research program initiated by Paul Hudak for an algebraic and programming theory of Polymorphic Temporal Media [START_REF] Hudak | A sound and complete axiomatization of polymorphic temporal media[END_REF] and the somehow related though earlier proposal of Functional Reactive Programming [START_REF] Elliott | Functional reactive animation[END_REF][START_REF] Elliott | Push-pull functional reactive programming[END_REF]. Links with the related ultrametric [START_REF] Krishnaswami | Higher-order functional reactive programming without spacetime leaks[END_REF] or categorical models [START_REF] Jeffrey | Functional reactive types[END_REF][START_REF] Jeltsch | An abstract categorical semantics for functional reactive programming with processes[END_REF] could be investigated.

Examples over timed signals detailed throughout suggest that timed domains also may induce some notion of timed operational semantics, probably deeply linked with the existing state based timed system modeling frameworks such as IO-timed automata theory [START_REF] Kaynar | The Theory of Timed I/O Automata[END_REF]. This surely necessitates focussing our attention on finite (or finitely representable) spaced and timed functions, a necessity that may benefit from our somewhat strong restriction to timed behaviors that uniformly act on the underlying time scales.

Fig. 1 .

 1 Fig. 1. A communication scenario.

  ) states that temporal projections are poset functors. Property (IN2) states that these functors are discrete fibrations 1 .

Example 4 . 5 .

 45 Let U = {⊥, a, b}, self-timed, with minimum element ⊥ and a and b incomparable. Let P = U ordered the same as U but timed over V = {0, 1} by π(⊥) = 0, π(a) = 1 and π(b) = 1. The function f : U → P defined by f

Example 4 . 12 (

 412 Timed signals). Continuing examples on signals (see 2.6), with P = Sig(U, A) and Q = Sig(V, B), the "lower" part of the above theorem can defined within a slight extension of the notion signals as follows. We define δ * (Q) = Sig * (δ, B) as the set of all pairs (u, Y ) ∈ U × P(V × B) such that v ≤ δ(u) for all (v, b) ∈ Y , with the cut defined by

Example 5 . 4 (

 54 Timed signals). One can check that we have Sig(T, A) ⊗ Sig(T, B) ∼ = Sig(T, A ⊕ B).

Definition 5 . 8 (

 58 Temporal cut of a synchronous function). Let f : P → Q be a synchronous function on the time scale T . Let u ∈ T . The temporal cut of f at u is the function f

1 ≤

 1 Let then A = {1, 2} seen as a two letter alphabet. Let A * be the set of finite strings over A with the empty string. Let {δ w : T → T } w∈A * be the family of function inductively defined by δ(u) = u, δ 1w = δ 1 • δ w (u) and δ 2w = δ 2 • δ w (u)for all u ∈ T and all w ∈ A * . For any string w ∈ A * , let also denote by |w| 1 the number of 1 in w and by |w| 2 the number of 2 in w.Let n ∈ N. Since both δ 1 and δ 2 are meet preserving, we observe that we have (δ 1 ∧ δ 2 ) 2n = w∈A 2n δ w Let then w ∈ A 2n . Two cases are possible. In the case |w| 2 ≤ |w| 1 , by applying |w| 2 times the inequality (4) we have δ |w|1 δ w hence, since δ 1 is causal and n ≤ |w| 1 we have δ n 1 ≤ δ w . In the symmetric case |w| 1 ≤ |w| 2 , by applying |w| 1 times the inequality (5) we have δ |w|2 2

Discrete fibrations and the related notion of categories of elements of a functor on Set are presented in[START_REF] Barr | Category Theory for Computing Science[END_REF] (Section 12.2) or in[START_REF] Lane | Sheaves in Geometry and Logic[END_REF] (Section 1.5).

Strictly speaking, for ∼π to be a symmetry, the timed poset P must be completed with sorts of "passing time" elements of the form (u, x) with x ≤ (u, x) and π(u, x) = u, defined for all x ∈ P and u ∈ T such that there is no y above x with π(y) = u.

Possibly gluing minimal elements when considering the subcategory of timed posets with a minimum elements

One can easily verify that the monomorphisms in TPoset(T ) are the injective synchronous functions. Then, as a consequence of the lemma, every injective syn-

chronous function f : Q → P is equivalent (as sub-object) with the inclusion synchronous function inc f (Q) : f (Q) → P .

additionally proving that TPoset(T ) also has all equalizers, which is easy since they are essentially defined as in Set.

We call here a diagram functor a functor from the category freely generated by a graph G. As such a functor is fully determined by its value on graph vertices and edges it can simply be seen as a graph morphism from G into (the graph of) its codomain category.

Acknowledgment

The author wishes to express his deep gratitude to Gordon Plotkin et Phil Scott for their early advice to look at the notion of presheaves, to Marek Zawadowski for his help in understanding Grothendieck topologies and sheaves, to referees for their numerous suggestions of improvement, and to Simon Archipoff, Michail Raskin and Bernard Serpette for many fruitful discussions on various aspects of this work.

Work partially supported by Inria center Bordeaux