IT University of Copenhagen, Denmark and<EMAIL_ADDRESS>IT University of Copenhagen, Denmark and
<EMAIL_ADDRESS>Rasmus Ejlers Møgelberg
and Maaike Annebet Zwart [100]Theory of Computation $\rightarrow$ Semantics
and Reasoning $\rightarrow$ Program semantics; Theory of computation
$\rightarrow$ Semantics and reasoning $\rightarrow$ Program constructs
$\rightarrow$ Type structures

###### Acknowledgements.

This work was funded by the Independent Research Fund Denmark grant number
2032-00134B.

# What monads can and cannot do
with a bit of extra time

Rasmus Ejlers Møgelberg  Maaike Annebet Zwart

###### Abstract

The delay monad provides a way to introduce general recursion in type theory.
To write programs that use a wide range of computational effects directly in
type theory, we need to combine the delay monad with the monads of these
effects. Here we present a first systematic study of such combinations.

We study both the coinductive delay monad and its guarded recursive cousin,
giving concrete examples of combining these with well-known computational
effects. We also provide general theorems stating which algebraic effects
distribute over the delay monad, and which do not. Lastly, we salvage some of
the impossible cases by considering distributive laws up to weak bisimilarity.

###### keywords:

Delay Monad, Monad Compositions, Distributive Laws, Guarded Recursion, Type
Theory

##  1 Introduction

Martin Löf type theory [29] is a language that can be understood both as a
logic and a programming language. For the logical interpretation it is crucial
that all programs terminate. Still, one would like to reason about programming
languages with general recursion, or even write general recursive programs
inside type theory. One solution to this problem is to encapsulate recursion
in a monad, such as the delay monad $D$. This monad maps an object $X$ to the
coinductive solution to $DX\cong X+DX$. The right inclusion into the sum of
the above isomorphism introduces a computation step, and infinitely many steps
correspond to divergence. Capretta [8] showed how $D$ introduces general
recursion via an iteration operator of type $(X\to D(X+Y))\to X\to DY$. For
this reason, $D$ has been used to model recursion in type theory [14, 41, 4],
and in particular forms part of the basis of interaction trees [42].

The delay monad has a guarded recursive variant defined using Nakano’s [33]
fixed point modality $\triangleright$. Data of type $\triangleright X$ should
be thought of as data of type $X$ available only one time step from now. This
modal operator has a unit $\operatorname{next}:X\to\triangleright X$
transporting data to the future, and a fixed point operator
$\mathsf{fix}:(\triangleright X\to X)\to X$ mapping productive definitions to
their fixed points satisfying
$\mathsf{fix}(f)=f(\operatorname{next}(\mathsf{fix}(f)))$. Guarded recursion
can be modelled in the topos of trees [7] – the category
$\mathsf{Set}^{{{\omega}^{\mathrm{op}}}}$ of presheaves on the ordered natural
numbers – by defining $(\triangleright X)(0)=1$ and $(\triangleright
X)(n+1)=X(n)$. The guarded delay monad $D^{\mathsf{g}}$ is defined as the free
monad on $\triangleright$, i.e., the inductive (and provably also coinductive)
solution to $D^{\mathsf{g}}X\cong X+\triangleright(D^{\mathsf{g}}X)$.

The two delay monads can be formally related by moving to a multiclock variant
of guarded recursion, in which the modal operator $\triangleright$ is indexed
by a clock variable $\kappa$, which can be universally quantified. Then by
defining the guarded delay monad ${D^{\kappa}}X$ to be the unique solution to
${D^{\kappa}}X\cong X+\triangleright^{\kappa}({D^{\kappa}}X)$, the coinductive
variant can be encoded [2] as
$DX\mathbin{\overset{\textsf{def}}{=}}\forall\kappa.{D^{\kappa}}X$. In this
paper we will work informally in Clocked Cubical Type Theory (CCTT) [5], a
type theory in which such encodings of coinductive types can be formalised and
proven correct.

Unlike the coinductive variant, the guarded delay monad has a fixed point
operator of type
$((X\to{D^{\kappa}}Y)\to(X\to{D^{\kappa}}Y))\to(X\to{D^{\kappa}}Y)$, defined
using $\mathsf{fix}$. For the coinductive delay monad, fixed points only exist
for continuous maps, but in the guarded case, continuity is a consequence of a
causality property enforced in types using $\triangleright$. As a consequence,
higher order functional programming languages with recursion can be embedded
in type theories like CCTT by interpreting function spaces as Kleisli
exponentials for ${D^{\kappa}}$. For example, Paviotti et al. [36] showed how
to model the simply typed lambda calculus with fixed point terms (PCF), and
proved adequacy of the model, all in a type theory with guarded recursion.
These results have since been extended to languages with recursive types [31]
and (using an impredicative universe) languages with higher-order store [38].
This suggests that the guarded delay monad can be used for programming and
reasoning about programs using a wide range of advanced computational effects
directly in type theory. However, a mathematical theory describing the
interaction of the delay monads with other monads is still lacking, even for
basic computational effects.

###  1.1 Combining the delay monad with other effects

In this paper, we present a first systematic study of monads combining delay
with other effects. We first show how to combine the delay monad with standard
monads known from computational effects: exceptions, reader, global state and
the selection monad. Most of these follow standard combinations of effects and
non-termination known from domain theory, but, the algebraic status of these
combinations is simpler than in the domain theoretic case: Whereas the latter
can be understood as free monads for order-enriched algebraic theories [20],
the combinations with the guarded recursive delay monad are simply free models
of theories in the standard sense, with the caveat that the arity of the step
operation is non-standard.

The rest of the paper is concerned with distributive laws of the form $TD\to
DT$, where $T$ is any monad and $D$ is the delay monad in any of the two forms
mentioned above. Such a distributive law distributes the operations of $T$
over steps, and equips the composite $DT$ with a monad structure that
describes computations whose other effects are only visible upon termination.
This is the natural monad for example in the case of writing to state, when
considering non-determinism and observing must-termination, or for computing
data contained in data structures such as trees or lists.

There are two natural ways of distributing an $n$-ary operation
$\operatorname{op}$ over computation steps: The first is to execute each of
the $n$ input computations in sequence until they have all terminated, the
second is to execute the $n$ inputs in parallel, delaying terminated
computations until all inputs have terminated. We show that sequential
execution yields a distributive law for algebraic monads (monads generated by
algebraic theories) where all equations are balanced, i.e., the number of
occurrences of each variable on either side is the same. Trees, lists, and
multisets are examples of such monads.

The requirement of balanced equations is indeed necessary. This was observed
already by Møgelberg and Vezzosi [32] who showed that for the finite powerset
monad, sequential distribution of steps over the union operator was not well
defined, and parallel distribution did not yield a distributive law due to
miscounting of steps. Here we strengthen this result to show that no
distributive law is possible for the finite powerset monad over the
coinductive delay monad. At first sight it might seem that the culprit in this
case is the idempotency axiom. However, we show that in some cases it is
possible to distribute idempotent operations over the coinductive delay monad,
but not over the guarded one (we show this just for commutative operations).

Finally, we show that if one is willing to work up to weak bisimilarity, i.e.,
equating elements of the delay monad that only differ by a finite number of
computation steps, then one can construct a distributive law $TD\to DT$ for
any monad $T$ generated by an algebraic theory with no drop equations
(equations where a variable appears on one side, but not the other). To make
this precise, we formulate this result as a distributive law of monads on a
category of setoids.

#### Agda formalisation

Some of the results presented in this paper have been formalised in Agda using
Vezzosi’s Guarded Cubical library111https://github.com/agda/guarded. The code
can be found at https://tinyurl.com/WMCDAgda.

##  2 Monads and algebraic theories

In this background section we briefly remind the reader of algebraic theories
and free model monads for an algebraic theory. We mention different classes of
equations that play a role in our analysis of monad compositions, and we
discuss distributive laws for composing monads.

######  Definition 2.1 (Algebraic Theory).

An algebraic theory $A$ consists of a signature $\Sigma_{A}$ and a set of
equations $E_{A}$. The signature is a set of operation symbols with arities
given by natural numbers. The signature $\Sigma_{A}$ together with a set of
variables $X$ inductively defines the set of $A$-terms: Every variable $x:X$
is a term, and for each operation symbol $\operatorname{op}$ in $\Sigma_{A}$,
if $\operatorname{op}$ has arity $n$ and $t_{1},\ldots,t_{n}$ are terms, then
$\operatorname{op}(t_{1},\ldots,t_{n})$ is a term. The set of equations
contains pairs of terms $(s,t)$ in a finite variable context which are to be
considered equal, often written as $s=t$. These pairs then define an
equivalence relation on terms via equational logic.

######  Example 2.2 (Monoids).

The algebraic theory of monoids has a signature consisting of a constant $c$
and a binary operation $*$, satisfying the left and right unital equations:
$\forall x:X.\,c*x=x$ and $\forall x:X.\,x*c=x$, and associativity: $\forall
x,y,z:X.\,(x*y)*z=x*(y*z)$. Commutative monoids also include the commutativity
equation: $\forall x,y:X.\,x*y=y*x$.

######  Definition 2.3 (Category of models).

A model of an algebraic theory $(\Sigma_{A},E_{A})$ is a set $X$ together with
an interpretation ${\operatorname{op}}_{X}:X^{n}\rightarrow X$ of each $n$-ary
operation $\operatorname{op}$ in $\Sigma_{A}$, such that ${s}_{X}={t}_{X}$ for
each equation $s=t$ in $E_{A}$. Here ${s}_{X}$ is the interpretation of $s$
defined inductively using the interpretation of operations.

A homomorphism between two models $(X,{(-)}_{X})$ and $(Y,{(-)}_{Y})$ is a
morphism $h:X\rightarrow Y$ such that
$h({\operatorname{op}}_{X}(x_{1},\ldots,x_{n}))={\operatorname{op}}_{Y}(h(x_{1}),\ldots,h(x_{n}))$
for each $n$-ary operation $\operatorname{op}$ in $\Sigma_{A}$ and
$x_{1},\ldots,x_{n}:X$. The models of an algebraic theory and homomorphisms
between them form a category called the _category of algebras_ of the
algebraic theory, denoted $A$-alg.

The free model of an algebraic theory $A$ with variables in a set $X$ consists
of the set of equivalence classes of $A$-terms in context $X$. The functor
$F:\mathbf{Set}\rightarrow A$-alg sending each set $X$ to the free model of
$A$ on $X$ is left adjoint to the forgetful functor sending each $A$-model to
its underlying set. This adjunction induces a monad on $\mathbf{Set}$, called
the _free model monad_ of the algebraic theory [24, 23, 25]. The category of
algebras of $A$ is isomorphic to the Eilenberg-Moore category of this monad.
If a monad $T$ is isomorphic to the free model monad of an algebraic theory,
then we say that $T$ _is presented_ by that algebraic theory.

######  Example 2.4 (Boom Hierarchy monads [30]).

The binary tree monad, the list monad, the multiset monad and the powerset
monad are the free model monads of respectively the theories of:

  * •

Magmas, the theory consisting of a constant and a binary operation satisfying
the left and right unit equations.

  * •

Monoids, which are magmas satisfying the associativity equation.

  * •

Commutative monoids.

  * •

Idempotent commutative monoids, which are also known as semilattices.

The equations of an algebraic theory determine much of the behaviour of its
free model monad. For example, linear equations result in monads that always
compose with commutative monads [26, 34]. In this paper, we built upon the
ideas of Gautam [16] and Parlant et al [35], and distinguish the following
classes of equations:

######  Definition 2.5.

Write $\operatorname{var}(t)$ for the set of variables that appear in a term
$t$. We say that an equation $s=t$ is:

Linear

if $\operatorname{var}(s)=\operatorname{var}(t)$ and each variable in these
sets appears exactly once in both $s$ and $t$. Example: $x*y=y*x$.

Balanced

if $\operatorname{var}(s)=\operatorname{var}(t)$ and each variable in these
sets appears equally many times in $s$ and $t$. Example:
$(x*y)*(y*z)=(y*y)*(x*z)$.

Dup

if there is an $x:\operatorname{var}(s)\cup\operatorname{var}(t)$, such that
$x$ appears $\geq 2$ times in $s$ and/or $t$. Example: the balanced equation
above, as well as $x*x=x*x*x$ and $x\wedge(x\vee y)=x$.

Drop

if $\operatorname{var}(s)\neq\operatorname{var}(t)$. Example: $x\wedge(x\vee
y)=x$.

######  Remark 2.6.

Notice that these types of equations are not mutually exclusive. An equation
can for instance be both dup and drop, such as the absorption equation
$x\wedge(x\vee y)=x$.

###  2.1 Distributive laws

One way of composing two monads is via a _distributive law_ describing the
interaction between the two monads [6].

######  Definition 2.7 (Distributive Law).

Given monads $\langle S,\eta^{S},\mu^{S}\rangle$ and $\langle
T,\eta^{T},\mu^{T}\rangle$, a distributive law distributing $S$ over $T$ is a
natural transformation $\zeta:ST\rightarrow TS$ satisfying the following
axioms:

$\displaystyle\zeta\circ\eta^{S}T$ $\displaystyle=T\eta^{S}$
$\displaystyle\zeta\circ S\eta^{T}$ $\displaystyle=\eta^{T}S$ (unit axioms)
$\displaystyle\zeta\circ\mu^{S}T$ $\displaystyle=T\mu^{S}\circ\zeta S\circ
S\zeta$ $\displaystyle\zeta\circ S\mu^{T}$ $\displaystyle=\mu^{T}S\circ
T\zeta\circ\zeta T$ (multiplication axioms)

######  Example 2.8 (Lists and Multisets).

Distributive laws are named after the well-known distributivity of
multiplication over addition: $a*(b+c)=(a*b)+(a*c)$. Many distributive laws
follow the same distribution pattern. For example, the list monad distributes
over the multiset monad in this way: $\zeta[\Lbag a\Rbag,\Lbag
b,c\Rbag]=\Lbag[a,b],[a,c]\Rbag$. However, this is by no means the only way a
distributive law can function.

######  Theorem 2.9 (Beck [6]).

Let $\mathcal{C}$ be a category, and $\langle S,\eta^{S},\mu^{S}\rangle$ and
$\langle T,\eta^{T},\mu^{T}\rangle$ two monads on $\mathcal{C}$. If
$\zeta:ST\rightarrow TS$ is a distributive law, then the functor $TS$ carries
a monad structure with unit $\eta^{T}\eta^{S}$ and multiplication
$\mu^{T}\mu^{S}\circ T\zeta S$.

We frequently use the following equivalence in our proofs:

######  Theorem 2.10 (Beck [6]).

Given two monads $\langle S,\eta^{S},\mu^{S}\rangle$ and $\langle
T,\eta^{T},\mu^{T}\rangle$ on a category $\mathcal{C}$, there is a bijective
correspondence between distributive laws of type $ST\rightarrow TS$, and
liftings of $T$ to the Eilenberg-Moore category $\mathcal{C}^{S}$ of $S$.

Here, a lifting of $T$ to $\mathcal{C}^{S}$ is an assignment mapping
$S$-algebra structures on a set $X$ to $S$-algebra structures on $TX$ such
that $\eta^{T}$ and $\mu^{T}$ are $S$-algebra homomorphisms.

##  3 Guarded recursion and the delay monad

In this paper we work informally in Clocked Cubical Type Theory (CCTT) [5]. At
present, this is the only known theory combining the features we need:
Multiclocked guarded recursion and quotient types (to express free monads).
Here we remind the reader of the basic principles of CCTT, but we refer to
Kristensen et al. [5] for the full details, including a denotational semantics
for CCTT.

###  3.1 Algebraic theories in Cubical Type Theory

CCTT is an extension of Cubical Type Theory (CTT) [12], which in turn is a
version of Homotopy Type Theory (HoTT) [39] that gives computational content
to the univalence axiom. In CTT, the identity type of Martin-Löf type theory
is replaced by a path type, which we shall write infix as $t=_{A}u$, often
omitting the type $A$ of $t$ and $u$. We will work informally with $=$, using
its standard properties such as function extensionality.

A type $A$ is a _homotopy proposition_ (or hprop) in HoTT and CTT, if any two
elements of $A$ are equal, and an _hset_ if $x=_{A}y$ is an hprop for all
$x,y:A$. Assuming a universe of small types, one can encode universes
$\mathsf{hProp}$ and $\mathsf{hSet}$ of homotopy sets and propositions in the
standard way. The benefit of working with hsets is that there is no higher
structure to consider. In particular, the collection of hsets and maps between
these forms a category in the sense of HoTT [39], and so basic category
theoretic notions such as functors and monads on hsets can be formulated in
the standard way.

The notion of algebraic theory can also be read directly in CTT this way.
Moreover, the free monads on algebraic theories can be defined using higher
inductive types (HITs). These are types given inductively by constructors for
terms as well as for equalities. For example, the format for HITs used in CCTT
[5] (adapted from Cavallo and Harper [9]) is expressive enough222Full details
are in the appendix..

We write type equivalence as $A\simeq B$. For hsets this just means that there
are maps $f:A\to B$ and $g:B\to A$ that are inverses of each other, as
expressed in CTT using path equality.

###  3.2 Multi-clocked guarded recursion

* Γ ⊢_ Γ, κ: clock ⊢_ * κ: clock∈Γ Γ, α: κ ⊢_ * Γ, TimeLess(Γ’) ⊢_ t: ▷ (α : κ) . A
Γ,β:κ,Γ’ ⊢_ Γ,β: κ,Γ’ ⊢_ t [β] : A[β/α] * Γ,α:κ ⊢_ t: A Γ ⊢_ λ(α : κ). t: ▷
(α : κ) . A * Γ,κ: clock ⊢_ t: A Γ ⊢_ Λκ. t: ∀κ. A * Γ ⊢_ t: ∀κ. A
Γ ⊢_ κ’: clock Γ ⊢_ t [κ’]: A [κ’/κ] * Γ ⊢_ t: ▷^κA →A Γ ⊢_ dfix^κ t: ▷^κA * Γ
⊢_ t: ▷^κA →A Γ ⊢_ pfix^κ t: ▷ (α : κ) .(dfix^κt) [α] =_A t(dfix^κt)

Figure 1: Selected typing rules for Clocked Cubical Type Theory [5]. The
telescope ${\mathsf{TimeLess}(\Gamma^{\prime})}$ is composed of the timeless
assumptions in $\Gamma$, i.e. interval variables and faces (as in Cubical Type
Theory) as well as clock variables.

CCTT extends CTT with multi-clock guarded recursion. The central component in
this is a modal type operator $\triangleright$ indexed by clocks $\kappa$,
used to classify data that is delayed by one time step on clock $\kappa$. The
most important typing rules of CCTT are collected in Figure 1. Clocks are
introduced as special assumptions $\kappa:\mathsf{clock}$ in a context, and
can be abstracted and applied to terms of the type $\forall\kappa.A$ which
behaves much like a $\Pi$-type for clocks. Like function extensionality,
extensionality for $\forall\kappa.A$ also holds in CCTT.

The rules for $\triangleright$ also resemble those of $\Pi$-types:
Introduction is by abstracting special assumptions $\alpha:\kappa$ called
_ticks_ on the clock $\kappa$. Since ticks can appear in terms, the modal type
${\triangleright}\,(\alpha\\!:\\!\kappa).A$ binds $\alpha$ in $A$, just like a
$\Pi$-type binds a variable. We write $\triangleright^{\kappa}A$ for
${\triangleright}\,(\alpha\\!:\\!\kappa).A$ when $\alpha$ does not appear in
$A$. The introduction rule for $\triangleright$ can be read as stating that if
$t$ has type $A$ after the tick $\alpha$, then
$\lambda(\alpha\\!:\\!\kappa).t$ has type
${\triangleright}\,(\alpha\\!:\\!\kappa).A$ now.

The modality $\triangleright$ is eliminated by applying a term to a tick. Note
that the term $t$ applied to the tick $\beta$ cannot already contain $\beta$
freely. This restriction prevents $t$ from being applied twice to the same
tick, which would construct terms of type
$\triangleright^{\kappa}\triangleright^{\kappa}A\to\triangleright^{\kappa}A$,
collapsing two steps into one. Moreover, $t$ cannot contain any variables nor
other ticks occurring in the context after $\beta$, only _timeless_
assumptions, i.e., clocks, interval assumptions and faces. One application of
timeless assumptions is to type the extensionality principle for
$\triangleright$:

$(t=_{{\triangleright}\,(\alpha:\kappa).A}u)\simeq{\triangleright}\,(\alpha\\!:\\!\kappa).(t\,[\alpha]=_{A}u\,[\alpha]).$
(1)

For all explicit applications of terms to ticks in this paper, the term will
not use timeless assumptions. The usual $\eta$ and $\beta$ laws hold for tick
abstraction and application.

The use of ticks for programming with $\triangleright$ implies that
$\triangleright$ is an applicative functor, and can even be given a dependent
applicative action of type

$\Pi(f:\triangleright^{\kappa}(\Pi(X:A).B(x)).\Pi(y:\triangleright^{\kappa}A).{\triangleright}\,(\alpha\\!:\\!\kappa).B(y\,[\alpha]).$

Ticks are named in CCTT for reasons of normalisation [3], but are essentially
identical. This is expressed in type theory as the _tick irrelevance
principle_ :

$\mathsf{tirr}^{\kappa}:\Pi(x:\triangleright^{\kappa}A).\,{\triangleright}\,(\alpha\\!:\\!\kappa).\,{\triangleright}\,(\beta\\!:\\!\kappa).(x\,[\alpha]=_{A}x\,[\beta]).$
(2)

The term $\mathsf{tirr}^{\kappa}$ is defined in CCTT using special combinators
on ticks, allowing for computational content to $\mathsf{tirr}^{\kappa}$. This
means that the rule for tick application is more general than the one given in
Figure 1. However, we will not need this further generality for anything apart
from $\mathsf{tirr}^{\kappa}$, which we use directly.

Finally, CCTT has a fixed point operator $\mathsf{dfix}$ which unfolds up to
path equality as witnessed by $\mathsf{pfix}$. Using these, one can define
$\mathsf{fix}^{\kappa}:(\triangleright^{\kappa}A\to A)\to A$ as
$\mathsf{fix}^{\kappa}(t)=t(\mathsf{dfix}^{\kappa}t)$ and prove
$\mathsf{fix}^{\kappa}(t)=t(\operatorname{next}^{\kappa}(\mathsf{fix}^{\kappa}(t)))$
where
$\operatorname{next}^{\kappa}\mathbin{\overset{\textsf{def}}{=}}(\lambda(x:A).\lambda(\alpha\\!:\\!\kappa).x):A\to\triangleright^{\kappa}A$.
Note that this uses that also variables appearing before a tick in a context
can be introduced. This is not the case in all Fitch-style modal type theories
[11, 17].

###  3.3 Guarded recursive types

A guarded recursive type is a recursive type in which the recursive
occurrences of the type are all guarded by a $\triangleright$. These can be
encoded up to equivalence of types using fixed points of maps on the universe.
Our primary example is the guarded recursive delay monad ${D^{\kappa}}$
defined to map an $X$ to the recursive type

$\displaystyle{D^{\kappa}}X\simeq X+\triangleright^{\kappa}({D^{\kappa}}X).$

We write $\operatorname{now}:X\to{D^{\kappa}}X$ and for the two maps given by
inclusion and the equivalence above.

Since $\triangleright^{\kappa}$ preserves the property of being an hset, one
can prove by guarded recursion that ${D^{\kappa}}X$ is an hset whenever $X$
is. ${D^{\kappa}}$ can be seen as a free construction in the following sense.

######  Definition 3.2.

A _delay algebra_ on the clock $\kappa$ is an hset $X$ together with a map
$\triangleright^{\kappa}X\to X$.

Given an hset $X$, the hset ${D^{\kappa}}X$ carries a delay algebra structure.
It is the free delay algebra in the sense that given any other delay algebra
$(Y,\xi)$, and a map $f:X\to Y$, there is a unique homomorphism
$\overline{f}:{D^{\kappa}}X\to Y$ extending $f$ along $\operatorname{now}$,
defined by the clause

$\displaystyle\overline{f}($
$\displaystyle=\xi(\lambda(\alpha\\!:\\!\kappa).\overline{f}(x\,[\alpha])).$
(3)

This is a recursive definition that can be encoded as a fixed point of a map
$h:\triangleright^{\kappa}({D^{\kappa}}X\to Y)\to({D^{\kappa}}X\to Y)$ defined
using the clause $h(g)($. In this paper we use the simpler notation of
Equation (3) for such definitions rather than the explicit use of
$\mathsf{fix}^{\kappa}$.

We sketch the proof that $\overline{f}$ is the unique homomorphism extending
$f$, to illustrate the use of $\mathsf{fix}^{\kappa}$ for proofs. Suppose $g$
is another such extension. To use guarded recursion, assume that
$\triangleright^{\kappa}(g=\overline{f})$. We show that $g($. Since $g$ is a
homomorphism: $g($. So by extensionality for $\triangleright$ (1) it suffices
to show that
${\triangleright}\,(\alpha\\!:\\!\kappa).{(g(x\,[\alpha])=\overline{f}(x\,[\alpha]))}$,
which follows from the guarded recursion hypothesis.

Tick irrelevance implies that ${D^{\kappa}}$ is a commutative monad in the
sense of Kock [22].

###  3.4 Encoding coinductive types

Coinductive types can be encoded using a combination of guarded recursive
types and quantification over clocks. This was first observed by Atkey and
McBride [2]. We recall the following special case of a more general theorem
for this in CCTT [5]. First a definition.

######  Definition 3.7.

A functor $F:\mathsf{hSet}\to\mathsf{hSet}$ _commutes with clock
quantification_ , if the canonical map
$F(\forall\kappa.(X\,[\kappa]))\to\forall\kappa.F(X\,[\kappa])$ is an
equivalence for all $X:\forall\kappa.\mathsf{hSet}$. An hset $X$ is _clock
irrelevant_ if the constant functor to $X$ commutes with clock quantification,
i.e. if the canonical map $X\to\forall\kappa.X$ is an equivalence.

Note that functors commuting with clock quantification map clock irrelevant
types to clock irrelevant types.

######  Theorem 3.8 ([5]).

Let $F$ be an endofunctor on the category of hsets commuting with clock
quantification, and let $\nu^{\kappa}F$ be the guarded recursive type
satisfying $F(\triangleright^{\kappa}(\nu^{\kappa}F))\simeq\nu^{\kappa}F$,
then $\nu F\mathbin{\overset{\textsf{def}}{=}}\forall\kappa.\nu^{\kappa}F$
carries a final coalgebra structure for $F$.

In order to apply Theorem 3.8, of course, one needs a large collection of
functors $F$ commuting with clock quantification. Fortunately, the collection
of such functors is closed under almost all type constructors, including
finite sum and product, $\Pi$ and $\Sigma$ types, $\triangleright$,
$\forall\kappa$, and guarded recursive types [5, Lemma 4.2]. Clock irrelevant
types are likewise closed under the same type constructors, and path equality.
The only exception to clock irrelevance is the universe type.

For example, if $X$ is clock irrelevant, then $F(Y)=X+Y$ commutes with clock
quantification, and so
$DX\mathbin{\overset{\textsf{def}}{=}}\forall\kappa.{D^{\kappa}}X$ is the
coinductive solution to $DX\simeq X+DX$.

CCTT moreover has a principle of _induction under clocks_ allowing one to
prove that many HITs are clock irrelevant, including the empty type, booleans
and natural numbers. Moreover, one can prove the following.

######  Proposition 3.9.

Let $A=(\Sigma_{A},E_{A})$ be an equational theory such that $\Sigma_{A}$ and
$E_{A}$ are clock irrelevant. Then the free model monad $T$ commutes with
clock quantification. In particular, $T(X)$ is clock irrelevant for all clock
irrelevant $X$.

The collection of clock irrelevant propositions can be shown to be closed
under standard logical connectives. Alternatively, one can assume a global
clock constant $\kappa_{0}$, which then can be used to prove that all
propositions are clock irrelevant.

######  Convention 3.10.

In the remainder of this paper, the word _set_ will refer to a clock-
irrelevant hset, and the word _proposition_ will refer to clock-irrelevant
homotopy propositions. We will write $\mathsf{Set}$ and $\mathsf{Prop}$ for
the universes of these. Similarly, whenever we mention functors these are
assumed to commute with clock quantification.

##  4 Specific combinations with delay

In this section we look at some specific examples of monads, and see how they
combine with the delay monads. In particular, we will look at the exception,
reader, state, and selection monads. Intuitively, these monads model (parts
of) the process: read input - compute - do something with the output. For
instance, the state monad reads a state, then both updates the current state
and gives an output. Combining the state monad with the delay monads allows us
to model the fact that the computation in between reading the input and giving
the output takes time, and might not terminate.

The examples we give follow the same pattern as the adaptation of these monads
to domain theory: we insert a delay monad where one would use lifting in the
domain theoretic case. However, we also show that the algebraic status of
these monads is much simpler in the guarded recursive case than in the domain
theoretic one: they can simply be understood as being generated by algebraic
theories where one operation () has a non-standard arity. In the domain
theoretic case, the algebraic description is in terms of enriched Lawvere
theories [20]. We give no algebraic description of the combinations with the
coinductive delay monads, because this does not by itself have an algebraic
description.

First note that for combinations with delay via a distributive law, it is
enough to find a distributive law for the guarded recursive version
${D^{\kappa}}$.

######  Lemma 4.2.

Let $T$ be a monad. A distributive law
$\zeta_{X}:\forall\kappa.T({D^{\kappa}}(X))\to{D^{\kappa}}(T(X))$ for the
guarded delay monad induces a distributive law $TD\to DT$ for the coinductive
delay monad. Similarly, if $T^{\kappa}$ is a family of monads indexed by
$\kappa$ then $T(X)=\forall\kappa.T^{\kappa}(X)$ carries a monad structure.

######  Proof 4.3.

The distributive law can be constructed as the composite

$T(\forall\kappa.{D^{\kappa}}(X))\to(\forall\kappa.T({D^{\kappa}}(X)))\to\forall\kappa.{D^{\kappa}}(T(X)),$

where $\kappa$ is fresh for $T$ and $X$. For the second statement define the
multiplication as the composite
$\forall\kappa.T^{\kappa}(\forall\kappa.T^{\kappa}(X))\to(\forall\kappa.T^{\kappa}(T^{\kappa}(X)))\to\forall\kappa.T^{\kappa}(X)$.

#### Exceptions

The first monad we consider is the exception monad. For a set of exceptions
$E$, the exception monad is given by the functor $(-+E)$, with obvious unit
and multiplication. The exception monad is the free model monad of the
algebraic theory consisting of a signature with a constant $e$ for each
exception in $E$, and no equations.

It is well known that the exception monad distributes over any monad, and
therefore we have a distributive law
$\zeta:({D^{\kappa}}(-)+E)\rightarrow{D^{\kappa}}(-+E)$. The resulting
composite monad ${D^{\kappa}}(-+E)$ is the free model monad of the theory
consisting of constants $e:E$ and a -operator forming a delay algebra, with no
additional equations.

#### Reading

The reader monad $(-)^{R}$ is presented by the algebraic theory consisting of
a single operation $\operatorname{lookup}:X^{R}\rightarrow X$, satisfying the
equations

$\displaystyle\forall x:X.\,$ $\displaystyle\operatorname{lookup}(\lambda
r.x)=x$ $\displaystyle\forall g:(X^{R})^{R}.\,$
$\displaystyle\operatorname{lookup}(\operatorname{lookup}\circ
g)=\operatorname{lookup}(\lambda s.g\,s\,s).$

To combine the reader monad with the delay monad, we define a distributive law
${D^{\kappa}}R\rightarrow R{D^{\kappa}}$ by the clauses
$\zeta(\operatorname{now}f)=\lambda r.\operatorname{now}(fr)$ and $\zeta($,
where $f:X^{R}$ and $d:\triangleright^{\kappa}(X^{R})$. The resulting
composite monad $R{D^{\kappa}}$ is the free model monad of the theory
consisting of $\operatorname{lookup}$ and satisfying the above equations for
$\operatorname{lookup}$ and

$\displaystyle\forall d:\triangleright^{\kappa}(X^{R}).\,$
$\displaystyle=\operatorname{lookup}(\lambda r.$ (4)

#### Global state

Plotkin and Power [37] show that the global state monad $(S\times-)^{S}$ can
be described algebraically by two operations:
$\operatorname{lookup}:\,X^{S}\rightarrow X$ and
$\operatorname{update}:\,X\rightarrow X^{S}$, satisfying four interaction
diagrams. They call the category of such algebras _GS-algebras_.

The natural combination of global state and ${D^{\kappa}}$ is
$({D^{\kappa}}(S\times-))^{S}$ describing computations whose steps occur
between reading the initial state and writing back the updated state. To
describe this monad algebraically define a GSD-algebra to be a GS-algebra
which also carries a delay algebra structure satisfying (4) and

$\displaystyle\forall x:\triangleright^{\kappa}X.\,\lambda
s.\operatorname{update}($ $\displaystyle=\lambda s.$

Diagrammatically:

${\triangleright^{\kappa}(X^{S})}$${(\triangleright^{\kappa}X)^{S}}$${X^{S}}$${\triangleright^{\kappa}X}$${\triangleright^{\kappa}(X^{S})}$${(\triangleright^{\kappa}X)^{S}}$${\triangleright^{\kappa}X}$${X}$${X}$${X^{S}}$$\scriptstyle{\triangleright^{\kappa}(\operatorname{lookup})}$$\scriptstyle{\operatorname{lookup}}$$\scriptstyle{\triangleright^{\kappa}(\operatorname{update})}$$\scriptstyle{\operatorname{update}}$

######  Theorem 4.16.

The monad $({D^{\kappa}}(S\times-))^{S}$ is the free model monad of the theory
of GSD-algebras.

Note that also $(D(S\times-))^{S}$ is a monad by Lemma 4.2, since the
assumption of $S$ being clock irrelevant implies
$(D(S\times-))^{S}\simeq\forall\kappa.(({D^{\kappa}}(S\times-))^{S})$.

#### Selecting

The selection monad $\mathcal{J}X=(X\rightarrow S)\rightarrow X$ takes a
function $X\rightarrow S$, and selects an input $x:X$ to return [15]. This
could, for example, be an input for which the function attains an optimal
value. It is a monad similar to the reader monad, with a more advanced input.
It is also a close companion to the continuation monad $(X\rightarrow
S)\rightarrow S$, and it has many applications in for example game theory and
functional programming [18].

The selection monad combines with the delay monad via a distributive law of
type ${D^{\kappa}}\mathcal{J}\rightarrow\mathcal{J}{D^{\kappa}}$. Intuitively,
it first gathers all the data from the function $X\rightarrow S$, and then
computes which element from $X$ to select. This computation takes time and
might not terminate. We assume that the initial input is readily available,
even though the resulting type of the monad composition is
$({D^{\kappa}}X\rightarrow S)\rightarrow{D^{\kappa}}X$. This fact is reflected
in the definition of the distributive law below.

The distributive law is similar to the distributive law for the delay monad
over the reader monad, and is given by:

$\displaystyle\zeta($ $\displaystyle=\lambda g.$

where $f:(X\rightarrow S)\rightarrow X$ and
$d:\triangleright^{\kappa}({D^{\kappa}}((X\rightarrow S)\rightarrow X))$. As a
result, both $\mathcal{J}{D^{\kappa}}$ and $\mathcal{J}D$ can be equipped with
monad structures.

#### Free combinations with delay

The sum of two monads $T$ and $S$ is a monad $T\oplus S$ whose algebras are
objects $X$ with algebra structures for both $T$ and $S$ [19]. In terms of
algebraic theories, the sum can be understood as combining two theories with
no equations between them. The sum of ${D^{\kappa}}$ with any other monad
always exists [19, Theorem 4]:

######  Corollary 4.19.

Let $T$ be a monad, and define $T\oplus{D^{\kappa}}$ as the guarded recursive
type:

$(T\oplus{D^{\kappa}})X\simeq
T(X+\triangleright^{\kappa}((T\oplus{D^{\kappa}})X)).$

Then $(T\oplus{D^{\kappa}})(X)$ is the carrier of the free $T$-algebra and
delay-algebra structure.

The monad mapping $X$ to $\forall\kappa.(T\oplus{D^{\kappa}})(X)$ includes the
coinductive delay monad and $T$, but we have not been able to prove a general
universal property for this. We believe that it is not the sum of the two.

##  5 Parallel and sequential distribution of operations

We now consider distributive laws of type $TD\rightarrow DT$, where $D$ is one
of the delay monads and $T$ is any presentable monad. Such laws equip the
composite $DT$ with a monad structure, which is the natural one in particular
for monads describing data structures, such as those in the Boom hierarchy.

We again focus on distributive laws involving the guarded version of the delay
monad, invoking Lemma 4.2. Intuitively, such a distributive law pulls all the
steps out of the algebraic structure of $T$: it turns a $T$-structure with
delayed elements into a delayed $T$-structure. There are two obvious
candidates for such a lifting: _parallel_ and _sequential_ computation. We
define both of these on operations using guarded recursion. A lifting of terms
then follows inductively from lifting each operation in the signature of the
presentation of $T$.

######  Definition 5.1 (Parallel lifting of operators).

Let $A$ be an algebraic theory, and let $X$ be an $A$-model. Define, for each
n-ary operation $\operatorname{op}$ in $A$, a lifting
${\operatorname{op}}^{par}_{{D^{\kappa}}X}:({D^{\kappa}}X)^{n}\to{D^{\kappa}}X$
by:

$\displaystyle{\operatorname{op}}^{par}_{{D^{\kappa}}X}(\operatorname{now}x_{1},\dots,\operatorname{now}x_{n})$
$\displaystyle=\operatorname{now}({\operatorname{op}}_{X}(x_{1},\dots,x_{n}))$
$\displaystyle{\operatorname{op}}^{par}_{{D^{\kappa}}X}(x_{1},\dots,x_{n})$
$\displaystyle=$

where the second clause only applies if one of the $x_{i}$ is of the form and

$x_{i}^{\prime}=\begin{cases}x_{i}&\text{ if
}x_{i}=\operatorname{now}(x_{i}^{\prime\prime})\\\
x_{i}^{\prime\prime}\,[\alpha]&\text{ if
}x_{i}=\step(x_{i}^{\prime\prime})\end{cases}$

######  Definition 5.5 (Sequential lifting of operators).

Let $A$ be an algebraic theory, and let $X$ be an $A$-model. Define, for each
n-ary operation $\operatorname{op}$ in $A$, a lifting
${\operatorname{op}}^{seq}_{{D^{\kappa}}X}:({D^{\kappa}}X)^{n}\to{D^{\kappa}}X$
by:

$\displaystyle{\operatorname{op}}^{seq}_{{D^{\kappa}}X}(\operatorname{now}x_{1},\dots,\operatorname{now}x_{n})$
$\displaystyle=\operatorname{now}({\operatorname{op}}_{X}(x_{1},\dots,x_{n}))$
$\displaystyle{\operatorname{op}}^{seq}_{{D^{\kappa}}X}(\operatorname{now}x_{1},\dots,$
$\displaystyle=$

where, in the second clause, the $i$th argument is the first not of the form
$\operatorname{now}(x_{k}^{\prime})$.

In general, for an $n$-ary operation $\operatorname{op}$, parallel lifting
evaluates all arguments of the form in parallel, and sequential lifting
evaluates them one by one from the left. Parallel lifting of an operator
therefore terminates in as many steps as the maximum required for each of its
inputs to terminate, while sequential lifting terminates in the sum of the
number of steps required for each input.

The evaluation order of arguments in the case of sequential lifting is
inessential, which can be proved using guarded recursion and tick irrelevance.

######  Lemma 5.9.

Let $A$ be an algebraic theory, and let $\operatorname{op}$ be an $n$-ary
operation in $A$. Then

$\displaystyle{\operatorname{op}}^{seq}_{{D^{\kappa}}X}(x_{1},\ldots,\,$

###  5.1 Preservation of equations

Parallel lifting preserves all non-drop equations, whereas sequential lifting
only preserves balanced equations. We prove this in the two following
propositions. We write ${s}^{par}_{{D^{\kappa}}X}$ for the interpretation of a
term $s$ on ${D^{\kappa}}X$ defined by induction of $s$ using the parallel
lifting of operations, and likewise ${s}^{seq}_{{D^{\kappa}}X}$ for the
interpretation defined using sequential lifting of operations.

######  Proposition 5.12 (Parallel preserves non-drop).

Let $A=(\Sigma_{A},E_{A}$) be an algebraic theory, $X$ an $A$-model, and $s=t$
a non-drop equation that is valid in $A$. Then also
${s}^{par}_{{D^{\kappa}}X}={t}^{par}_{{D^{\kappa}}X}$.

The restriction to non-drop equations is necessary, because divergence in a
dropped variable leads to divergence on one side of the equation, but not on
the other.

Møgelberg and Vezzosi [32] observed that parallel lifting does not define a
distributive law in the case of the finite powerset monad. Their proof uses
idempotency, but in fact parallel lifting does not define a monad even just in
the presence of a single binary operation.

######  Theorem 5.13.

Let $T$ be an algebraic monad with a binary operation $\operatorname{op}$.
Then the natural transformation $\zeta:TD\rightarrow DT$ induced by parallel
lifting does not define a distributive law, because it fails the second
multiplication axiom.

######  Proof 5.14.

The counter example is the same as used by Møgelberg and Vezzosi:

$\displaystyle{\operatorname{op}}^{par}_{DDX}(\mu^{D}(\operatorname{now}($
$\displaystyle=$
$\displaystyle\mu^{D}({\operatorname{op}}^{par}_{DDX}(\operatorname{now}($
$\displaystyle=$

Note that we used the coinductive version of the delay monad in the above
theorem. By Lemma 4.2, this implies the same result for the guarded recursive
version.

######  Proposition 5.22 (Sequential preserves balanced).

Let $A$ be an algebraic theory, and $s,t$ be two $A$-terms such that $s=t$ is
a balanced equation that is valid in $A$. Then also
${s}^{seq}_{{D^{\kappa}}X}={t}^{seq}_{{D^{\kappa}}X}$.

Balance is necessary. For example, if $t$ and $s$ are terms in a single
variable which occurs twice in $t$ and once in $s$, then
${t}^{seq}_{{D^{\kappa}}X}($ takes at least two steps, but
${s}^{seq}_{{D^{\kappa}}X}($ might take only one. Building on Proposition
5.22, one can prove the following.

######  Theorem 5.25.

Let $T$ be the free model monad of algebraic theory
$\mathbb{T}=(\Sigma_{\mathbb{T}},E_{\mathbb{T}})$, such that $E_{\mathbb{T}}$
only contains _balanced_ equations. Then sequential lifting defines a
distributive law $T{D^{\kappa}}\rightarrow{D^{\kappa}}T$.

Combining this with Lemma 4.2 we obtain a distributive law $TD\to DT$ for all
$T$ as in Theorem 5.25.

######  Remark 5.26.

Since ${D^{\kappa}}$ is a commutative monad, we already know from Manes and
Mulry [26] and Parlant [34] that there is a distributive law in the case where
$\mathbb{T}$ only has _linear_ equations. We can extend this linearity
requirement here to allow duplications of variables, as long as there are
equally many duplicates on either side of each equation.

######  Example 5.27.

The sequential distributive law successfully combines the delay monad with the
binary tree monad, the list monad, and the multiset monad, resulting in the
monads ${D^{\kappa}}B$, ${D^{\kappa}}L$, and ${D^{\kappa}}M$, respectively.

##  6 Idempotent equations

This section studies distributive laws $TD\rightarrow DT$ for $T$ an algebraic
monad with an idempotent binary operation “$\operatorname{op}$”. Since
idempotency is not a balanced equation, as remarked after Proposition 5.22,
sequential distribution does not respect it, and so neither parallel nor
sequential distribution define distributive laws in this case. Idempotency
turns out to be a tricky equation: We first show an example of such a theory
$T$ where no distributive law $TD\rightarrow DT$ is possible, then a theory
where it is, and finally we show that no distributive law of type
$T{D^{\kappa}}\rightarrow{D^{\kappa}}T$ is possible. First observe the
following.

######  Lemma 6.1.

Let $T$ be an algebraic monad with an idempotent binary operation
$\operatorname{op}$ and let $\zeta:TD\rightarrow DT$ be a distributive law.
There exist binary $T$-operations $\operatorname{op_{1}}$ and
$\operatorname{op^{\prime}}$ such that for any $T$-model $X$, the lifting of
$\operatorname{op}$ to $DX$ satisfies $\operatorname{op}($ and either 1)
$\operatorname{op}($ and $\operatorname{op^{\prime}}(x,$ or 2)
$\operatorname{op}($ and $\operatorname{op^{\prime}}(x,$.

######  Proof 6.11 (Proof (Sketch)).

We just sketch the proof of existence of $\operatorname{op_{1}}$. Consider the
naturality diagram for the unique map $!:2\to 1$ from the $2$-element set
$\\{\mathsf{tt},\mathsf{ff}\\}$ to the singleton set $\\{\star\\}$.

${D(T(2))\times D(T(2))}$${D(T(2))}$${D(T(1))\times
D(T(1))}$${D(T(1))}$$\scriptstyle{\operatorname{op}}$$\scriptstyle{D(T(!))\times
D(T(!))}$$\scriptstyle{D(T(!))}$$\scriptstyle{\operatorname{op}}$

By idempotency, the lower composition maps $($ to . Therefore it must be the
case that $\operatorname{op}($ is for some $\operatorname{op_{1}}$.

######  Proposition 6.18.

There is no distributive law ${\mathsf{P}_{\mathsf{f}}}D\to
D{\mathsf{P}_{\mathsf{f}}}$ for ${\mathsf{P}_{\mathsf{f}}}$ the finite
powerset functor.

######  Proof 6.19 (Proof Sketch).

There are only four possible cases for $\operatorname{op_{1}}(x,y)$ and
$\operatorname{op^{\prime}}(x,y)$: $\emptyset,\\{x\\},\\{y\\}$ and
$\\{x,y\\}$. An easy analysis rules out the first three. Lemma 6.1 then
implies that $\\{$. This leads to a contradiction as follows

######  Example 6.29.

Let $A$ be the algebraic theory with one idempotent binary operation $*$ and
one unary operator $!$, with no further equations. Let $T$ be the monad
generated by $A$. There is a distributive law $\zeta:TD\to DT$ given by the
following clauses

$\displaystyle!($ $\displaystyle=x$ $\displaystyle=$ $\displaystyle x*$
$\displaystyle=$

Note in particular, that . This example can be extended to $*$ associative, if
the equation $!(x*y)=(!x)*(!y)$ is added.

######  Theorem 6.40 (No-Go theorem).

Let $T$ be a monad with a binary algebraic operation that is commutative and
idempotent. Then there is no distributive law of type
$T{D^{\kappa}}\rightarrow{D^{\kappa}}T$.

##  7 Semi-Go Theorem: up to weak bisimilarity

In the proof of Theorem 6.40 the failure of existence of distributive laws
comes down to a miscounting of steps. This section shows that this is indeed
all that fails, and that parallel lifting defines a distributive law _up to
weak bisimilarity_ for algebraic monads with no drop equations. Weak
bisimilarity is a relation on the coinductive delay monad, which relates
computations that only differ by a finite number of steps. To make this
precise, we work in a category of setoids. The objects are pairs $(X,R)$,
where $R$ is an equivalence relation on $X$, and morphisms are equivalence
classes of maps $f$ between the underlying sets respecting the relations. Two
such maps are equivalent if their values on equal input are related by the
equivalence relation on the target type.

We first define a lifting of the coinductive delay monad $D$ to the category
of setoids. We do this via a similar relation (taken from Møgelberg and
Paviotti [31]) defined for the guarded delay monad, because that allows us to
reason using guarded recursion. We write $\delta^{\kappa}$ for .

######  Definition 7.2 ([31]).

Let $X,Y$ be sets, and suppose $R:X\to Y\to\mathsf{Prop}$ is a relation.
Define weak bisimilarity up to $R$, written
$\sim_{R}^{\kappa}\,:{D^{\kappa}}X\to{D^{\kappa}}Y\to\mathsf{Prop}$, by:

$\displaystyle\operatorname{now}(x)\sim_{R}^{\kappa}\,y\leavevmode\nobreak\
\mathbin{\overset{\textsf{def}}{=}}\;$
$\displaystyle\exists(n:\mathbb{N},y^{\prime}:Y).y=(\delta^{\kappa})^{n}(\operatorname{now}(y^{\prime}))\text{and
}R(x,y^{\prime}),$ $\displaystyle
x\sim_{R}^{\kappa}\,\operatorname{now}(y)\leavevmode\nobreak\
\mathbin{\overset{\textsf{def}}{=}}\;$
$\displaystyle\exists(n:\mathbb{N},x^{\prime}:X).x=(\delta^{\kappa})^{n}(\operatorname{now}(x^{\prime}))\text{and
}R(x^{\prime},y),$
$\displaystyle{\triangleright}\,(\alpha\\!:\\!\kappa).(x\,[\alpha]\sim_{R}^{\kappa}\,y\,[\alpha]).$

Note that the two first cases both apply for
$\operatorname{now}(x)\sim_{R}^{\kappa}\,\operatorname{now}(y)$, but that they
are equivalent in that case. If $R$ is symmetric and reflexive, then the same
properties hold for $\sim_{R}^{\kappa}\,$, but transitivity is not preserved.
In fact, if $\sim_{=}^{\kappa}\,$ were transitive, then one could prove that
it is the total relation, which is not the case.

######  Definition 7.5.

Let $R:X\to Y\to\mathsf{Prop}$ be a relation. Define $\sim_{R}\,:DX\to
DY\to\mathsf{Prop}$ as

$\displaystyle
x\sim_{R}\,y\mathbin{\overset{\textsf{def}}{=}}\forall\kappa.x\,[\kappa]\sim_{R}^{\kappa}\,y\,[\kappa].$

The above definition is an encoding (using guarded recursion) of the standard
coinductive definition of weak bisimilarity. We note the following, which was
also observed by Chapman et al [10].

######  Proposition 7.6.

The mapping $D_{\mathsf{sd}}(X,R)=(DX,\sim_{R}\,)$ defines a monad on the
category of setoids.

In fact, the multiplication for ${D^{\kappa}}$ preserves the guarded recursive
definition of weak bisimilarity.

Similarly, any algebraic monad $T$ can be lifted to the category of setoids by
defining $T(R)$ to be the smallest equivalence relation relating an
equivalence class $[t(x_{1},\dots,x_{n})]$ to $[t(y_{1},\dots,y_{n})]$ if
$R(x_{i},y_{i})$ for all $i$. We write $T_{\mathsf{sd}}$ for this.

Recall that by Proposition 5.12, if $T$ is an algebraic monad given by a
theory with no drop equations, then parallel lifting defines a natural
transformation $TD\to DT$ on the category of sets. We show that this map lifts
to a distributive law on the category of setoids.

######  Theorem 7.7.

Let $T$ be the free model monad of algebraic theory
$\mathbb{T}=(\Sigma_{\mathbb{T}},E_{\mathbb{T}})$, such that $E_{\mathbb{T}}$
contains no drop equations. Then parallel lifting defines a distributive law
of monads $T_{\mathsf{sd}}D_{\mathsf{sd}}\to D_{\mathsf{sd}}T_{\mathsf{sd}}$.

######  Remark 7.8.

The free monad on an algebraic theory could alternatively be expressed on the
category of setoids by taking the set to be the free monad just on operations,
introducing the equations of the theory into the equivalence relation. In the
presence of the axiom of choice this generates a monad equivalent to
$T_{\mathsf{sd}}$, and we expect that the proof above can be adapted to that
choice as well.

##  8 Related work

Møgelberg and Vezzosi [32] study two combinations of the guarded delay monad
${D^{\kappa}}$ with the finite powerset monad ${\mathsf{P}_{\mathsf{f}}}$
expressed as a HIT in CCTT. They use these to show that applicative simulation
is a congruence for the untyped lambda calculus with finite non-determinism
using denotational techniques. One combination is the sum
${\mathsf{P}_{\mathsf{f}}}\oplus{D^{\kappa}}$, which is used for the case of
may-convergence, and the other is the composite
${D^{\kappa}}{\mathsf{P}_{\mathsf{f}}}$ equipped with the parallel lifting,
which is used for must-convergence. They observe that only the former is a
monad. In this paper, we not only provide a more general study of such
combinations, but also suggest a way to remedy the situation in the latter
case by considering weak bisimilarity.

Weak bisimilarity for the coinductive delay monad was first defined by
Capretta [8]. Møgelberg and Paviotti [31] show that their embedding of FPC in
guarded dependent type theory respects weak bisimilarity and use that to prove
an adequacy theorem up to weak bisimilarity.

Chapman et al. [10] observe that quotienting the coinductive delay monad by
weak bisimilarity appears to not yield a monad unless countable choice is
assumed. Altenkirch et al. [1] propose a solution to this problem by
constructing the quotient and the weak bisimilarity relation simultaneously,
as a higher inductive-inductive type. Chapman et al. themselves suggest a
different solution, constructing the quotient as the free $\omega$-cpo using
an ordinary HIT. These quotients have not (to the best of our knowledge) been
studied in combination with other effects.

Interaction trees [42] are essentially monads of the form
$\forall\kappa.(T\oplus{D^{\kappa}})(-)$ for $T$ an algebraic monad generated
by operations with no equations. Much work has gone into building libraries
for working with these up to weak bisimilarity in Coq, and these allow for
interaction trees to be used for program verification. To our knowledge,
versions of interaction trees with equations between terms have not been
considered.

As mentioned in the introduction, the guarded recursive delay monad has two
benefits over the coinductive one: Firstly, it has a fixed point operator of
the type (rather than an iteration operator), which means that it allows for
embedding languages with recursion directly in type theory. In the coinductive
case, one must either use some encoding of recursion using the iteration
operator, or prove that all constructions used are continuous. We believe this
is a considerable burden for higher order functions. The second advantage is
that guarded recursion allows for also advanced notions of state to be
encoded, as shown recently by Sterling et al. [38]. Neither the interaction
trees nor the quotiented delay monads appear to have these benefits.

### Related work on monad compositions

The field of monad compositions in general has attracted quite a bit of
attention lately. After Plotkin proved that there is no distributive law
combining probability and non-determinism [40], Klin and Salamanca [21]
studied impossible distributions of the powerset monad over itself, while
Zwart and Marsden provided a general study on what makes distributive laws
fail [43]. Meanwhile, the initial study of monad compositions by Manes and
Mulry [26, 27] was continued by Parlant et al [13, 34, 35]. In both the
positive and the negative theorems on distributive laws in these papers,
certain classes of equations were identified as causes for making or breaking
the monad composition. Idempotence, duplication, and dropping variables came
out as especially noteworthy types of equations, which the findings in this
paper confirm.

Our study of the delay monad provides an interesting extension on the previous
works, because of its non-standard algebraic structure given by delay
algebras, and the fact that the delay monad is neither affine nor relevant,
which are the main properties studied by Parlant et al.

##  9 Conclusion and future work

We have studied how both the guarded recursive and the coinductive version of
the delay monad combine with other monads. After studying some specific
examples and free combinations, we looked more generally at possible
distributive laws of $T{D^{\kappa}}\rightarrow{D^{\kappa}}T$. We found two
natural candidates for such distributive laws, induced by _parallel_ and
_sequential_ lifting of operations on $T$. We showed that:

  * •

Sequential lifting provides a distributive law for monads presented by
theories with balanced equations.

  * •

There is no distributive law possible for monads with a binary operation that
is commutative and idempotent over ${D^{\kappa}}$, but this does not rule out
a distributive law of such monads over $D$.

  * •

Parallel lifting does not define a distributive law, but it does define one
_up to weak bisimilarity_ , for monads presented by theories with non-drop
equations.

It is unfortunate that weak bisimilarity requires working with setoids, but
this is due to the quotient of $D$ up to weak bisimilarity not being a monad
[10]. It is not clear how to adapt the solutions to this problem mentioned
above [10, 1] to the guarded recursive setting.

This paper only considers the case of finite arity operations (except for
state, which can be of any arity). Distributive laws for countable arity
operations such as countable non-deterministic choice are more difficult. In
those cases sequential lifting seems an unnatural choice, not only because it
does not interact well with idempotency, but also because it introduces
divergence even in the cases where there is an upper limit to the number of
steps taken by the arguments. Extending our parallel lifting operation to the
countable case requires deciding whether all the countably many input
operations are values, which is not possible in type theory.

The results presented in this paper are formulated and proven in CCTT. It is
natural to ask whether the results proven for the coinductive delay monad $D$
also hold for $D$ considered as a monad on the category $\mathsf{Set}$ of
sets. For some of the results proven in this paper (Proposition 6.18 and
Example 6.29) both the statements and proofs can be read in $\mathsf{Set}$.
These results can therefore easily be seen to hold in this setting. In many
other cases, our constructions use guarded recursion (e.g. the definitions of
parallel and sequential lifting of operators). To lift these results to
$\mathsf{Set}$, one would need to redo the constructions and argue for their
productivity. However, we believe that using guarded recursion is the natural
way to work with coinductive types and proofs. Another approach could
therefore be to use guarded recursion as a language to reason about
$\mathsf{Set}$. This should be possible because the universe used to model
clock irrelevant types in the extensional model of Clocked Type Theory [28]
classifies a category equivalent to $\mathsf{Set}$. We leave this as a
direction for future research.

## References

  * [1] Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus.  Partiality, revisited.  In International Conference on Foundations of Software Science and Computation Structures, pages 534–549. Springer, 2017.
  * [2] Robert Atkey and Conor McBride.  Productive coprogramming with guarded recursion.  ACM SIGPLAN Notices, 48(9):197–208, 2013.
  * [3] Patrick Bahr., Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg.  The clocks are ticking: No more delays!  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12. IEEE, 2017.
  * [4] Patrick Bahr and Graham Hutton.  Monadic compiler calculation (functional pearl).  Proc. ACM Program. Lang., 6(ICFP), August 2022.  doi:10.1145/3547624.
  * [5] Magnus Baunsgaard Kristensen, Rasmus Ejlers Mogelberg, and Andrea Vezzosi.  Greatest hits: Higher inductive types in coinductive definitions via induction under clocks.  In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1–13, 2022.
  * [6] Jon Beck.  Distributive laws.  In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119–140. Springer Berlin Heidelberg, 1969.
  * [7] Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring.  First steps in synthetic guarded domain theory: step-indexing in the topos of trees.  Logical Methods in Computer Science, 8(4), 2012.
  * [8] Venanzio Capretta.  General recursion via coinductive types.  Logical Methods in Computer Science, 1, 2005.
  * [9] Evan Cavallo and Robert Harper.  Higher inductive types in cubical computational type theory.  Proceedings of the ACM on Programming Languages, 3(POPL):1–27, 2019\.
  * [10] James Chapman, Tarmo Uustalu, and Niccolò Veltri.  Quotienting the delay monad by weak bisimilarity.  Mathematical Structures in Computer Science, 29(1):67–92, 2019\.
  * [11] Ranald Clouston.  Fitch-style modal lambda calculi.  In International Conference on Foundations of Software Science and Computation Structures, pages 258–275. Springer, 2018.
  * [12] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.  Cubical type theory: A constructive interpretation of the univalence axiom.  In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018\.
  * [13] Fredrik Dahlqvist, Louis Parlant, and Alexandra Silva.  Layer by layer - combining monads.  In Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings, pages 153–172, 2018.  doi:10.1007/978-3-030-02508-3\\_9.
  * [14] Nils Anders Danielsson.  Operational semantics using the partiality monad.  SIGPLAN Not., 47(9):127–138, sep 2012.  doi:10.1145/2398856.2364546.
  * [15] Martín Escardó and Paulo Oliva.  Selection functions, bar recursion and backward induction.  Mathematical Structures in Computer Science, 20(2):127–168, 2010\.  doi:10.1017/S0960129509990351.
  * [16] ND Gautam.  The validity of equations of complex algebras.  Archiv für mathematische Logik und Grundlagenforschung, 3(3):117–124, 1957.
  * [17] Daniel Gratzer, GA Kavvos, Andreas Nuyts, and Lars Birkedal.  Multimodal dependent type theory.  In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 492–506, 2020.
  * [18] Jules Hedges.  Monad transformers for backtracking search.  In Paul Levy and Neel Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, Grenoble, France, 12 April 2014, volume 153 of Electronic Proceedings in Theoretical Computer Science, pages 31–50. Open Publishing Association, 2014\.  doi:10.4204/EPTCS.153.3.
  * [19] Martin Hyland, Gordon Plotkin, and John Power.  Combining effects: Sum and tensor.  Theoretical Computer Science, 357(1):70–99, 2006.  doi:10.1016/j.tcs.2006.03.013.
  * [20] Martin Hyland and John Power.  Discrete lawvere theories and computational effects.  Theoretical Computer Science, 366(1-2):144–162, 2006.
  * [21] Bartek Klin and Julian Salamanca.  Iterated covariant powerset is not a monad.  In Proceedings 34th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, 2018.
  * [22] Anders Kock.  Monads on symmetric monoidal closed categories.  Archiv der Mathematik, 21(1):1–10, 1970.
  * [23] F. William Lawvere.  Functorial semantics of algebraic theories.  Proceedings of the National Academy of Sciences of the United States of America, 50(5):869–872, 1963.
  * [24] Fred EJ Linton.  Some aspects of equational categories.  In Proceedings of the Conference on Categorical Algebra, pages 84–94. Springer, 1966.
  * [25] Ernie Manes.  Algebraic theories, volume 26.  Springer, 1976.
  * [26] Ernie Manes and Philip Mulry.  Monad compositions I: general constructions and recursive distributive laws.  Theory and Applications of Categories, 18:172–208, 04 2007.
  * [27] Ernie Manes and Philip Mulry.  Monad compositions II: Kleisli strength.  Mathematical Structures in Computer Science, 18(3):613–643, 2008\.  doi:10.1017/S0960129508006695.
  * [28] Bassel Mannaa, Rasmus Ejlers Møgelberg, and Niccolò Veltri.  Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory.  Logical Methods in Computer Science, 16, 2020.
  * [29] Per Martin-Löf.  Intuitionistic Type Theory.  Bibliopolis, Napoli, 1984.
  * [30] Lambert Meertens.  Algorithmics, towards programming as a mathematical activity.  In J.W. De Bakker, M. Hazewinkel, and J.K. Lenstra, editors, Mathematics and Computer Science: Proceedings of the CWI Symposium, November 1983, CWI monographs, pages 289–334. North-Holland, 1986.
  * [31] Rasmus E Møgelberg and Marco Paviotti.  Denotational semantics of recursive types in synthetic guarded domain theory.  Mathematical Structures in Computer Science, 29(3):465–510, 2019\.
  * [32] Rasmus Ejlers Møgelberg and Andrea Vezzosi.  Two guarded recursive powerdomains for applicative simulation.  In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 200–217, 2021.  doi:10.4204/EPTCS.351.13.
  * [33] Hiroshi Nakano.  A modality for recursion.  In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science, pages 255–266. IEEE, 2000.
  * [34] Louis Parlant.  Monad Composition via Preservation of Algebras.  PhD thesis, UCL (University College London), 2020.
  * [35] Louis Parlant, Jurriaan Rot, Alexandra Silva, and Bas Westerbaan.  Preservation of equations by monoidal monads.  In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020.
  * [36] Marco Paviotti, Rasmus Ejlers Møgelberg, and Lars Birkedal.  A model of PCF in guarded type theory.  Electronic Notes in Theoretical Computer Science, 319:333–349, 2015\.
  * [37] Gordon Plotkin and John Power.  Notions of computation determine monads.  In International Conference on Foundations of Software Science and Computation Structures, pages 342–356. Springer, 2002.
  * [38] Jonathan Sterling, Daniel Gratzer, and Lars Birkedal.  Denotational semantics of general store and polymorphism.  Unpublished manuscript, July 2022.
  * [39] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [40] Daniele Varacca and Glynn Winskel.  Distributing probability over non-determinism.  Mathematical Structures in Computer Science, 16(1):87–113, 2006\.
  * [41] Niccolò Veltri and Niels F. W. Voorneveld.  Inductive and coinductive predicate liftings for effectful programs.  In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 260–277, 2021.  doi:10.4204/EPTCS.351.16.
  * [42] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic.  Interaction trees: Representing recursive and impure programs in Coq.  Proc. ACM Program. Lang., 4(POPL), dec 2019.  doi:10.1145/3371119.
  * [43] Maaike Zwart and Dan Marsden.  No-go theorems for distributive laws.  In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS), pages 1–13, 2019.  doi:10.1109/LICS.2019.8785707.

##  Appendix A Appendix of proofs

Please find the following proofs and clarifications in this appendix:

  * •

Appendix B shows:

    * –

How to encode the notion of algebraic theory in CCTT.

    * –

How to construct free functors at HITS.

    * –

A proof of Proposition 3.9, which claimed that the free model monad of
algebraic theory commutes with clock quantification if the signature and
equations of the algebraic theory are clock irrelevant.

  * •

Appendix C contains:

    * –

References to agda files where we proved all claims made in Section 4:
_Specific combinations with delay_.

    * –

A written proof sketch of Theorem 4.16, which claimed that the monad
$({D^{\kappa}}(S\times-))^{S}$ is the free model monad of the theory of GSD-
algebras.

  * •

Appendix D contains the omitted proofs of Section 5: _Parallel and sequential
distribution of operations_.

  * •

Appendix E contains the omitted proofs of Section 6: _No-Go Theorem for
idempotent equations_.

  * •

Appendix F contains the omitted proof details of Section 7: _Semi-Go Theorem:
up to weak bisimilarity_.

##  Appendix B Encoding algebraic theories in CCTT

The type of algebraic theories can be defined as an element of a large
universe written informally as follows.

######  Definition B.1.

An algebraic theory comprises

  * •

A signature type indexed by arities $\Sigma:\mathbb{N}\to\mathsf{Set}$

  * •

A type of equations indexed by the number of free variables
$\mathsf{E}:\mathbb{N}\to\mathsf{Set}$

  * •

Two maps giving the left hand side and right hand side of an equation
respectively

$\displaystyle\mathsf{lhs},\mathsf{rhs}$
$\displaystyle:(n:\mathbb{N})\to\mathsf{E}(n)\to\mathsf{Tm}(n)$

Where $\mathsf{Tm}(n)$ is the set of terms in context $\overline{n}$, the type
of numbers $0,\dots,n-1$. Both of these can be defined in the standard type
theoretic way. Recall that $\mathsf{Set}$ is the universe of small clock-
irrelevant hsets. Both $\mathsf{Tm}(n)$ and $\overline{n}$ are clock
irrelevant because $\Sigma(n)$ is [5, Theorem 5.3].

The free monad on an algebraic signature
$A=(\Sigma,\mathsf{ar},\mathsf{E},\mathsf{lhs},\mathsf{rhs})$ is defined to
map $X:\mathsf{Set}$ to a higher inductive type. The natural definition for
this would be to have a constructor for each operation in $\Sigma$ and a path
for each element of $\mathsf{E}$, plus constructors and paths to set-truncate
$T(X)$. However, this would require recursion in the boundary condition of the
equalities to interpret the terms given by $\mathsf{lhs}$ and $\mathsf{rhs}$,
and this is not allowed in the rule format for HITs in CCTT. Instead we use a
constructor for each term of the theory and add equations to enforce
flattening of terms, as expressed in the following definition which follows
the format of HITs in CCTT [5].

######  Definition B.2.

The free monad given by the signature $A$ applied to $X:\mathsf{Set}$ is the
HIT $T(X)$ given by the following constructors

$\displaystyle\mathsf{var}$ $\displaystyle:X\to T(X)$
$\displaystyle\mathsf{tm}$
$\displaystyle:(n:\mathbb{N})\to(\tau:\mathsf{Tm}(n))\to(\overline{n}\to
T(X))\to T(X)$ $\displaystyle\mathsf{flt}$
$\displaystyle:(n,m:\mathbb{N})\to(\sigma:\Sigma(n))\to(\tau:\overline{n}\to\mathsf{Tm}(m))\to(m\to
T(X))\to\mathbb{I}\to T(X)$ $\displaystyle\mathsf{eq}$
$\displaystyle:(n:\mathbb{N})\to(e:\mathsf{E}(n))\to(\overline{n}\to
T(X))\to\mathbb{I}\to T(X)$

These satisfy the following boundary conditions (writing $\equiv$ for
judgemental equality)

$\displaystyle\mathsf{flt}\,n\,m\,\sigma\,\tau\,\rho\,0$
$\displaystyle\equiv\mathsf{tm}\,m\,(\sigma[\tau])\,\rho$
$\displaystyle\mathsf{flt}\,n\,m\,\sigma\,\tau\,\rho\,1$
$\displaystyle\equiv\mathsf{tm}\,n\,\sigma\,(\lambda
k:\overline{n}.\mathsf{tm}\,m\,(\tau\,k)\,\rho)$
$\displaystyle\mathsf{eq}\,n\,e\,\rho\,0$
$\displaystyle\equiv\mathsf{tm}\,n\,(\mathsf{lhs}\,n\,e)\,\rho$
$\displaystyle\mathsf{eq}\,n\,e\,\rho\,1$
$\displaystyle\equiv\mathsf{tm}\,n\,(\mathsf{rhs}\,n\,e)\,\rho$

where $\sigma[\tau]$ is the result of substituting the elements of $\tau$ for
the free variables of $\sigma$. To these should be added standard constructors
and equalities for set truncation [5], which we omit.

###  B.1 The free monad commutes with clock quantification

Hypotheses

A type

$\Gamma,x:\forall\kappa.T(X\,[\kappa])\vdash B(x)\,\operatorname{type}$

Terms

$\displaystyle\Gamma,x:\forall\kappa.(X\,[\kappa])$ $\displaystyle\vdash
u_{\mathsf{var}}:B(\lambda\kappa.\mathsf{var}(x\,[\kappa]))$
$\displaystyle\Gamma,n:\forall\kappa.\mathbb{N},\tau:\forall\kappa.\mathsf{Tm}(n\,[\kappa]),$
$\displaystyle\rho:\forall\kappa.(\overline{n\,[\kappa]}\to T(X\,[\kappa])),$
$\displaystyle\rho^{\prime}:(k:\forall\kappa.\overline{n\,[\kappa]})\to
B(\lambda\kappa.\rho\,[\kappa](k\,[\kappa])))$ $\displaystyle\vdash
u_{\mathsf{tm}}:B(\lambda\kappa.\mathsf{tm}(n\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa]))$
$\displaystyle\Gamma,n,m:\forall\kappa.\mathbb{N},\sigma:\forall\kappa.\Sigma(n\,[\kappa]),$
$\displaystyle\tau:\forall\kappa.(\overline{n\,[\kappa]}\to\mathsf{Tm}(m\,[\kappa])),$
$\displaystyle\rho:\forall\kappa.(m\,[\kappa]\to T(X\,[\kappa])),$
$\displaystyle\rho^{\prime}:(k:\forall\kappa.m\,[\kappa])\to
B(\lambda\kappa.\rho\,[\kappa](k\,[\kappa])),i:\mathbb{I}$
$\displaystyle\vdash
u_{\mathsf{flt}}:B(\lambda\kappa.\mathsf{flt}(n\,[\kappa])(m\,[\kappa])(\sigma\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa])\,i)$
$\displaystyle\Gamma,n:\forall\kappa.\mathbb{N},e:\forall\kappa.\mathsf{E}(n\,[\kappa]),$
$\displaystyle\rho:\forall\kappa.(\overline{n\,[\kappa]}\to T(X\,[\kappa])),$
$\displaystyle\rho^{\prime}:(k:\forall\kappa.\overline{n\,[\kappa]})\to
B(\lambda\kappa.\rho\,[\kappa](k\,[\kappa])))),i:\mathbb{I}$
$\displaystyle\vdash
u_{\mathsf{eq}}:B(\lambda\kappa.\mathsf{eq}(n\,[\kappa])(e\,[\kappa])(\rho\,[\kappa])\,i)$

Satisfying

$\displaystyle u_{\mathsf{flt}}(n,\sigma,m,\tau,\rho,\rho^{\prime},0)$
$\displaystyle\equiv
u_{\mathsf{tm}}(\lambda\kappa.(m\,[\kappa]),\lambda\kappa.(\sigma\,[\kappa])[\tau\,[\kappa]],\rho,\rho^{\prime})$
$\displaystyle u_{\mathsf{flt}}(n,\sigma,m,\tau,\rho,\rho^{\prime},1)$
$\displaystyle\equiv u_{\mathsf{tm}}(n,\sigma,\lambda\kappa.\lambda
k.\mathsf{tm}\,(m\,[\kappa])\,(\tau\,[\kappa]\,k)\,(\rho\,[\kappa]),\lambda
k.u_{\mathsf{tm}}((m\,[\kappa]),\lambda\kappa.\tau\,[\kappa](k\,[\kappa]),\rho,\rho^{\prime})$
$\displaystyle u_{\mathsf{eq}}(n,e,\rho,\rho^{\prime},0)$ $\displaystyle\equiv
u_{\mathsf{tm}}(n,(\lambda\kappa.\mathsf{lhs}(e\,[\kappa])),\rho,\rho^{\prime})$
$\displaystyle u_{\mathsf{eq}}(n,e,\rho,\rho^{\prime},1)$ $\displaystyle\equiv
u_{\mathsf{tm}}(n,(\lambda\kappa.\mathsf{rhs}(e\,[\kappa])),\rho,\rho^{\prime})$

Conclusion

A section

$\Gamma,x:\forall\kappa.T(X\,[\kappa])\vdash t(x):B(x)$

Satisfying

$\displaystyle t(\lambda\kappa.\mathsf{var}(x\,[\kappa]))$
$\displaystyle\equiv u_{\mathsf{var}}(x)$ $\displaystyle
t(\lambda\kappa.\mathsf{tm}(n\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa]))$
$\displaystyle\equiv u_{\mathsf{tm}}(n,\tau,\rho,\lambda
k.t(\lambda\kappa.\rho\,[\kappa]\,(k\,[\kappa])))$ $\displaystyle
t(\lambda\kappa.\mathsf{flt}(n\,[\kappa])(m\,[\kappa])(\sigma\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa])\,i))$
$\displaystyle\equiv u_{\mathsf{flt}}(n,m,\sigma,\tau,\rho,\lambda
k.t(\lambda\kappa.\rho\,[\kappa](k\,[\kappa])),i)$ $\displaystyle
t(\lambda\kappa.\mathsf{eq}(n\,[\kappa])(e\,[\kappa])(\rho\,[\kappa])\,i)$
$\displaystyle\equiv u_{\mathsf{eq}}(n,e,\rho,\lambda
k.t(\lambda\kappa.\rho\,[\kappa](k\,[\kappa])),i)$

Figure 2: The principle of induction under clocks for $T(X)$. We omit the
hypotheses concerning set truncation, which are standard [5]. We assume given
an algebraic signature and an $X:\forall\kappa.\mathsf{Set}$ both in context
$\Gamma$. Note that the equalities are judgemental (denoted $\equiv$)

We now prove Theorem 3.9. For this we need the principle of induction under
clocks [5] which in the case of $T(X)$ specialises to the principle described
in Figure 2.

First recall that the canonical map
$f:T(\forall\kappa.X\,[\kappa])\to\forall\kappa.T(X\,[\kappa])$ defined using
functoriality of $T$ satisfies the clauses

$\displaystyle f(\mathsf{var}\,x)$
$\displaystyle=\lambda\kappa.\mathsf{var}(x\,[\kappa])$ $\displaystyle
f(\mathsf{tm}\,n\,\tau\,\rho)$
$\displaystyle=\lambda\kappa.(\mathsf{tm}\,n\,\tau\,(\lambda
k.f(\rho(k))\,[\kappa]))$ $\displaystyle
f(\mathsf{flt}\,n\,m\,\sigma\,\tau\,\rho\,i)$
$\displaystyle=\lambda\kappa.(\mathsf{flt}\,n\,m\,\sigma\,\tau\,(\lambda
k.f(\rho(k))\,[\kappa])\,i)$ $\displaystyle f(\mathsf{eq}\,n\,e\,\rho\,i)$
$\displaystyle=\lambda\kappa.(\mathsf{eq}\,n\,e\,(\lambda
k.f(\rho(k))\,[\kappa])\,i)$

(omitting the clauses for set truncation, which are standard [5]). The inverse
to $f$ can be constructed using the principle of induction under clocks. We
write the definition using clauses as follows

$\displaystyle g(\lambda\kappa.\mathsf{var}(x\,[\kappa]))$
$\displaystyle\equiv\mathsf{var}(x)$ $\displaystyle
g(\lambda\kappa.\mathsf{tm}(n\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa]))$
$\displaystyle\equiv\mathsf{tm}(n\,[\kappa_{0}],\tau\,[\kappa_{0}],\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k))$ $\displaystyle
g(\lambda\kappa.\mathsf{flt}(n\,[\kappa])(m\,[\kappa])(\sigma\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa])\,i))$
$\displaystyle\equiv\mathsf{flt}(n\,[\kappa_{0}],m\,[\kappa_{0}],\sigma\,[\kappa_{0}],\tau\,[\kappa_{0}],\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k),i)$ $\displaystyle
g(\lambda\kappa.\mathsf{eq}(n\,[\kappa])(e\,[\kappa])(\rho\,[\kappa])\,i)$
$\displaystyle\equiv\mathsf{eq}(n\,[\kappa_{0}],e\,[\kappa_{0}],\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k),i)$

Here $\kappa_{0}$ is the clock constant, which we will assume. In the cases of
the recursive calls, $k$ will have type $\overline{n\,[\kappa_{0}]}$ and
$\rho\,[\kappa]$ expects an input of type $\overline{n\,[\kappa]}$. These
types are equivalent, since $\mathbb{N}$ is clock-irrelevant. We leave this
equivalence implicit.

We must show that $g$ satisfies the boundary condition, which we just do in a
single case. The rest are similar.

$\displaystyle
g(\lambda\kappa.\mathsf{eq}(n\,[\kappa])(e\,[\kappa])(\rho\,[\kappa])\,0)$
$\displaystyle\equiv\mathsf{eq}(n\,[\kappa_{0}],e\,[\kappa_{0}],\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k),0)$
$\displaystyle\equiv\mathsf{tm}(n\,[\kappa_{0}],\mathsf{lhs}(e\,[\kappa_{0}]),\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k))$ $\displaystyle\equiv
g(\lambda\kappa.\mathsf{tm}(n\,[\kappa])(\mathsf{lhs}(e\,[\kappa]))(\rho\,[\kappa]))$

Again, we omit the standard cases of constructors and boundary cases for set
truncation [5].

It is easy to show that $g\circ f$ is the identity by induction. For example,

$\displaystyle g(f(\mathsf{tm}\,n\,\tau\,\rho))$ $\displaystyle\equiv
g(\lambda\kappa.(\mathsf{tm}\,n\,\tau\,(\lambda k.f(\rho(k))\,[\kappa])))$
$\displaystyle\equiv
g(\lambda\kappa.(\mathsf{tm}\,n\,\tau\,((\lambda\kappa^{\prime}.\lambda
k.f(\rho(k))\,[\kappa^{\prime}])\,[\kappa])))$
$\displaystyle\equiv\mathsf{tm}(n,\tau,\lambda
k.g(\lambda\kappa.f(\rho(k))\,[\kappa]))$
$\displaystyle\equiv\mathsf{tm}(n,\tau,\lambda k.g(f(\rho(k))))$
$\displaystyle\equiv\mathsf{tm}(n,\tau,\rho)$

using induction in the last equality.

Proving $f\circ g$ the identity requires another use of induction under
clocks. We just show one case.

$\displaystyle f(g$
$\displaystyle(\lambda\kappa.\mathsf{tm}(n\,[\kappa])(\tau\,[\kappa])(\rho\,[\kappa])))$
$\displaystyle\equiv f(\mathsf{tm}(n\,[\kappa_{0}],\tau\,[\kappa_{0}],\lambda
k.g(\lambda\kappa.\rho\,[\kappa]\,k)))$
$\displaystyle\equiv\lambda\kappa.\mathsf{tm}(n\,[\kappa_{0}],\tau\,[\kappa_{0}],\lambda
k.f(g(\lambda\kappa^{\prime}.\rho\,[\kappa^{\prime}]\,k))\,[\kappa])$
$\displaystyle=\lambda\kappa.\mathsf{tm}(n\,[\kappa_{0}],\tau\,[\kappa_{0}],\lambda
k.(\lambda\kappa^{\prime}.\rho\,[\kappa^{\prime}]\,k)\,[\kappa])$
$\displaystyle\equiv\lambda\kappa.\mathsf{tm}(n\,[\kappa],\tau\,[\kappa],\rho\,[\kappa])$

using the induction hypothesis and, in the last step, clock irrelevance of
$\mathbb{N}$ and $\mathsf{Tm}{(n\,[\kappa])}$.

We must show that this definition satisfies the boundary conditions. Since the
target type is a path type of $\forall\kappa.T(X\,[\kappa])$, which is an
hset, these conditions hold up to path equality. To force them to hold up to
judgemental equality, we can change the term using a composition, similarly to
the proof of Theorem 5.3 of [5].

##  Appendix C Proofs of Section 4

All claims about combinations of ${D^{\kappa}}$ with the reader monad, state
monad, and selection monad have been machine checked in Agda. The code can be
found in the following files in the supplementary material at
https://tinyurl.com/WMCDAgda:

  * •

The file “combinations-of-delay-and-reader.agda” contains proofs of the facts
that the natural transformation $\zeta:{D^{\kappa}}R\rightarrow R{D^{\kappa}}$
given by

$\displaystyle\zeta(\operatorname{now}f)$ $\displaystyle=\lambda
r.\operatorname{now}(fr)$ $\displaystyle\zeta($ $\displaystyle=\lambda r.$

where $f:X^{R}$ and $d:\triangleright^{\kappa}(X^{R})$, satisfies the
distributive law axioms, and that the resulting monad is indeed the free model
monad of the theory consisting of $\operatorname{lookup}$ and satisfying the
equations:

$\displaystyle\forall x:X.\,$ $\displaystyle\operatorname{lookup}(\lambda
r.x)=x$ $\displaystyle\forall g:(X^{R})^{R}.\,$
$\displaystyle\operatorname{lookup}(\operatorname{lookup}\circ
g)=\operatorname{lookup}(\lambda s.g\,s\,s)$ $\displaystyle\forall
d:\triangleright^{\kappa}(X^{R}).\,$

  * •

The file “combinations-of-delay-and-state.agda” contains proofs that functor
$({D^{\kappa}}(S\times-))^{S}$ has a monad structure, and that this monad is
the free model monad of the theory of GSD-algebras. That is, it contains a
proof of Theorem 4.16.

  * •

The file “combinations-of-delay-and-selection.agda” proves that the natural
transformation $\zeta:{D^{\kappa}}R\rightarrow R{D^{\kappa}}$ given by

$\displaystyle\zeta(\operatorname{now}f)$ $\displaystyle=\lambda
g.\operatorname{now}(f(\lambda x.g(\operatorname{now}x)))$
$\displaystyle\zeta($ $\displaystyle=\lambda g.$

where $f:(X\rightarrow S)\rightarrow X$ and
$d:\triangleright^{\kappa}({D^{\kappa}}((X\rightarrow S)\rightarrow X))$,
satisfies the distributive law axioms.

All code needs Agda version 2.6.3 to run, as it includes Vezzosi’s Guarded
Cubical library333https://github.com/agda/guarded.

In addition, we provide a proof sketch of Theorem 4.16 for those who prefer
paper proofs to Agda code.

######  Proof C.8 (Proof of Theorem 4.16).

We show that $({D^{\kappa}}(S\times-))^{S}$ maps a set $X$ to the carrier set
of the free, that is initial, GSD-algebra.

First note that $({D^{\kappa}}(S\times X))^{S}$ carries a GSD-algebra
structure defined as follows:

$\displaystyle\forall x:(({D^{\kappa}}(S\times X))^{S})^{S},s:S.\,$
$\displaystyle\operatorname{lookup_{DS}}\,x\,s=x\,s\,s$ $\displaystyle\forall
x:({D^{\kappa}}(S\times X))^{S}.\,$
$\displaystyle\operatorname{update_{DS}}\,x=\lambda s.\lambda t.x\,s$
$\displaystyle\forall x:\triangleright^{\kappa}(({D^{\kappa}}(S\times
X))^{S}).\,$ $\displaystyle\operatorname{step_{DS}}\,x=\lambda s.$

We show that $({D^{\kappa}}(S\times-))^{S}$ is the initial GSD-algebra, by
constructing a map $h$ from $({D^{\kappa}}(S\times-))^{S}$ to the initial GSD
algebra $I$, such that $h$ followed by $!$ is the identity, where
$!:I\rightarrow({D^{\kappa}}(S\times-))^{S}$ is the unique map from $I$ to
$({D^{\kappa}}(S\times-))^{S}$. First define
$h^{\prime}:{D^{\kappa}}(S\times-)\rightarrow I$ as:

$\displaystyle h^{\prime}(\operatorname{now}(s,x))=\;$
$\displaystyle\operatorname{update}xs$ $\displaystyle h^{\prime}($

then for all $x:({D^{\kappa}}(S\times X))^{S}$, define $h(x)$ as:

$h(x)=\operatorname{lookup}(\lambda s.h^{\prime}(x\,s)).$

Then: $(!\circ h)x=x$, which can be shown by guarded recursion.

All required properties for $({D^{\kappa}}(S\times-))^{S}$ to be the initial
GSD-algebra then follow from chasing the following diagram:

${X}$${({D^{\kappa}}(S\times-))^{S}}$${I}$${Y}$$\scriptstyle{f}$$\scriptstyle{h}$$\scriptstyle{\overline{f}}$$\scriptstyle{!}$$\scriptstyle{!}$

where $f$ is a given map from $X$ into a GSD-algebra $Y$, and
$\overline{f}=(!\circ h)$ is the unique extension
$({D^{\kappa}}(S\times-))^{S}\rightarrow Y$ of $f$.

######  Proof C.12 (Proof of Theorem 4.19).

Notice that $(T\oplus{D^{\kappa}})(X)$ carries a free $T$-algebra structure,
and a delay algebra structure defined by , where $\eta$ is the unit for $T$.
Given another set $Y$ with both a $T$-algebra structure and a delay algebra
structure, and a map $f:X\to Y$, the unique extension of $f$ to
$\overline{f}:T\oplus{D^{\kappa}}X\to Y$ is defined by guarded recursion, by
first defining $g:X+\triangleright^{\kappa}((T\oplus{D^{\kappa}})X)\to Y$,
then lifting using the monad structure on $T$.

##  Appendix D Proofs of Section 5

######  Proof D.1 (Proof of Lemma 5.9).

For readability, we prove this just in the case of $n=2$ and $i=2$, naming the
variables $x$ and $y$. If $x=\operatorname{now}x^{\prime}$, then the equation
holds by definition of ${\operatorname{op}}^{seq}_{{D^{\kappa}}X}$. If $x=$,
then:

$\displaystyle{\operatorname{op}}^{seq}_{{D^{\kappa}}X}(x,$ $\displaystyle=\;$
$\displaystyle=\;$ $\displaystyle=\;$ $\displaystyle=\;$

using guarded recursion and tick irrelevance.

######  Proof D.13 (Proof of Proposition 5.12).

Let $n$ be the number of free variables of $s$ and $t$ (by the non-drop
assumption $s$ and $t$ have the same free variables). Then
${s}^{par}_{{D^{\kappa}}X},{t}^{par}_{{D^{\kappa}}X}:({D^{\kappa}}X)^{n}\to{D^{\kappa}}X$,
and an easy induction shows that these both satisfy the parallel lifting
equations of Definition 5.1. Suppose now that at least one of the arguments
$x_{1},\dots,x_{n}$ is a step and write

$x_{i}^{\prime}=\begin{cases}x_{i}&\text{ if
}x_{i}=\operatorname{now}(x_{i}^{\prime\prime})\\\
x_{i}^{\prime\prime}\,[\alpha]&\text{ if
}x_{i}=\step(x_{i}^{\prime\prime})\end{cases}$

Then

$\displaystyle{s}^{par}_{{D^{\kappa}}X}(x_{1},\dots,x_{n})$ $\displaystyle=$
$\displaystyle=$ $\displaystyle={t}^{par}_{{D^{\kappa}}X}(x_{1},\dots,x_{n})$

by guarded recursion. The case where all $x_{i}$ are of the form
$\operatorname{now}(x_{i}^{\prime})$ is easy.

######  Proof D.17 (Proof of Proposition 5.22).

Suppose $s$ and $t$ both have $n$ free variables. Then:

$\displaystyle{s}^{seq}_{{D^{\kappa}}X}(\operatorname{now}(x_{1}),\dots,\operatorname{now}(x_{n})))$
$\displaystyle=\operatorname{now}({s}_{X}(x_{1},\dots,x_{n}))$
$\displaystyle=\operatorname{now}({t}_{X}(x_{1},\dots,x_{n}))$
$\displaystyle={s}^{seq}_{{D^{\kappa}}X}(\operatorname{now}(x_{1}),\dots,\operatorname{now}(x_{n}))).$

Suppose one of the inputs steps, say $x_{i}=$, and that $x_{i}$ occurs $k$
times in both $s$ and $t$. Then an easy induction using Lemma 5.9 and tick
irrelevance shows that

$\displaystyle{s}^{seq}_{{D^{\kappa}}X}(x_{1},\dots,$ $\displaystyle=$

where $\delta^{\kappa}=$, and likewise for
${t}^{seq}_{{D^{\kappa}}X}(x_{1},\dots,$. The result now follows from guarded
recursion.

######  Proof D.23 (Proof of Theorem 5.25).

We use the fact that a distributive law of the given type is equivalent to a
lifting of the monad ${D^{\kappa}}$ to the Eilenberg-Moore category of $T$,
see Theorem 2.10.

By Proposition 5.22, sequential lifting defines a lifting of $T$-algebra
structures on $X$ to $T$-algebra structures on ${D^{\kappa}}X$. It therefore
suffices to show that $\eta^{{D^{\kappa}}}$ and $\mu^{{D^{\kappa}}}$ are
homomorphisms of $T$-algebras. We just show this for $\mu^{{D^{\kappa}}}$, and
only in the case where one of the input steps, say $x_{i}=$. Then, using Lemma
5.9:

$\displaystyle\mu({\operatorname{op}}^{seq}_{{D^{\kappa}}{D^{\kappa}}X}(x_{1},\ldots,$
$\displaystyle=\mu($ $\displaystyle=$ $\displaystyle=$
$\displaystyle={\operatorname{op}}^{seq}_{{D^{\kappa}}X}((\mu
x_{1}),\ldots,(\mu x_{i}),\ldots,(\mu x_{n})).$

Using guarded recursion in the third equality.

##  Appendix E Omitted proofs Section 6

######  Proof E.1 (Proof of Lemma 6.1).

To see that there exists a $T$-operation $\operatorname{op_{1}}$ satisfying

$\operatorname{op}($ (5)

consider the naturality diagram for the unique map $!:2\to 1$.

${D(T(2))\times D(T(2))}$${D(T(2))}$${D(T(1))\times
D(T(1))}$${D(T(1))}$$\scriptstyle{\operatorname{op}}$$\scriptstyle{D(T(!))\times
D(T(!))}$$\scriptstyle{D(T(!))}$$\scriptstyle{\operatorname{op}}$

Let $\eta^{T}$ be the unit of $T$, and write $\mathsf{tt},\mathsf{ff}$ for the
two elements of $2$, and $\star$ for the unique element of $1$. Then chasing
the element $($ along the down, then right path yields:

$\displaystyle\operatorname{op}(D(T(!))\times D(T(!))\,($
$\displaystyle=\operatorname{op}($
$\displaystyle=\;\;\left\\{\;\operatorname{op}\text{ is
idempotent}\;\right\\}$

So then by following the right, then down path:

$\displaystyle\operatorname{op}($ (6)

for some element $\operatorname{op_{1}}(\mathsf{tt},\mathsf{ff})$ in $T(2)$
satisfying
$T(!)(\operatorname{op_{1}}(\mathsf{tt},\mathsf{ff}))=\eta^{T}(\star)$. Such
an element corresponds to an operation $T\times T\to T$, for which we shall
also write $\operatorname{op_{1}}$. We can then extend Equation 6 to conclude
that for any algebra $X$ for $T$, and for any $x,y:X$:

$\operatorname{op}($ (7)

by using the following naturality diagram, where we take $f:2\rightarrow X$
such that $f(\mathsf{tt})=x$ and $f(\mathsf{ff})=y$.

${D(T(2))\times D(T(2))}$${D(T(2))}$${D(T(X))\times
D(T(X))}$${D(T(X))}$$\scriptstyle{\operatorname{op}}$$\scriptstyle{D(T(f))\times
D(T(f))}$$\scriptstyle{D(T(f))}$$\scriptstyle{\operatorname{op}}$

Note that $\operatorname{op_{1}}$ on the right hand side of (7) should be
interpreted in $X$ using the algebra structure.

To conclude (5), we use that the multiplication $\mu^{D}$ for $D$ is a
homomorphism. From this, we get that for any $x,y:DX$:

$\displaystyle\mu^{D}(\operatorname{op}($
$\displaystyle=\operatorname{op}(\mu($

The left hand side of this equation rewrites to:

$\displaystyle\mu(\operatorname{op}($ $\displaystyle=\mu($ $\displaystyle=$

and the right hand side to:

$\displaystyle\operatorname{op}(\mu($ $\displaystyle=\operatorname{op}($

which, indeed, proves Equation 5.

Next, we want to show that there exists a $T$-operation
$\operatorname{op^{\prime}}$ such that either

$\displaystyle\operatorname{op}($ $\displaystyle=$
$\displaystyle\operatorname{op^{\prime}}(x,$
$\displaystyle=\operatorname{op_{1}}(x,y),$

or

$\displaystyle\operatorname{op}($
$\displaystyle=\operatorname{op^{\prime}}(x,y)$
$\displaystyle\operatorname{op^{\prime}}(x,$ $\displaystyle=$

To see this, define for any $T$-algebra $X$ and any $x,y:DX$, an operation
$\operatorname{op^{\prime\prime}}:DX\times DX\to DX$ by:

$\operatorname{op^{\prime\prime}}(x,y)=\operatorname{op}($

We then have:

$\displaystyle\operatorname{op^{\prime\prime}}(x,$
$\displaystyle=\operatorname{op}($

So it follows that either $\operatorname{op^{\prime\prime}}(x,y)=$ for some
operation $\operatorname{op^{\prime}}$ on $T$ such that:

$\operatorname{op^{\prime}}(x,$

or $\operatorname{op^{\prime\prime}}(x,y)=\operatorname{op^{\prime}}(x,y)$ for
some operation $\operatorname{op^{\prime}}$ on $T$ such that:

$\operatorname{op^{\prime}}(x,$

######  Proof E.45 (Proof of Proposition 6.18).

From Lemma 6.1 we know that there exists a
${\mathsf{P}_{\mathsf{f}}}$-operation $\operatorname{op_{1}}$ such that $\\{$,
and a ${\mathsf{P}_{\mathsf{f}}}$-operation $\operatorname{op^{\prime}}$ such
that either:

$\displaystyle\\{$ $\displaystyle=$
$\displaystyle\operatorname{op^{\prime}}(x,$
$\displaystyle=\operatorname{op_{1}}(x,y),$ (8)

or

$\displaystyle\\{$ $\displaystyle=\operatorname{op^{\prime}}(x,y)$
$\displaystyle\operatorname{op^{\prime}}(x,$ $\displaystyle=$ (9)

There are four possibilities for $\operatorname{op_{1}}(x,y)$:
$\emptyset,\\{x\\},\\{y\\}$ and $\\{x,y\\}$ (this can be proved by HIT-
induction on $\operatorname{op_{1}}(x,y)$). We show that the first three of
these lead to contradictions. From the naturality diagram

${D(T(X))\times D(T(X))}$${D(T(X))}$${D(T(1))\times
D(T(1))}$${D(T(1))}$$\scriptstyle{\operatorname{op}}$$\scriptstyle{D(T(!))\times
D(T(!))}$$\scriptstyle{D(T(!))}$$\scriptstyle{\operatorname{op}}$

we concluded that in particular: $D({\mathsf{P}_{\mathsf{f}}}(!))($. Because
$D({\mathsf{P}_{\mathsf{f}}}(!))($, $\operatorname{op_{1}}(x,y)=\emptyset$ is
not possible.

If $\operatorname{op_{1}}(x,y)=\\{x\\}$ then:

$\\{$

But, by naturality applied to the swap operation:

$\\{$

So by symmetry of sets:

which implies $x=y$, which is a contradiction. The same reasoning applies in
the case where $\operatorname{op_{1}}(x,y)=\\{y\\}$. Therefore we must have
$\operatorname{op_{1}}(x,y)=\\{x,y\\}$.

Next we look at the possible values for $\operatorname{op^{\prime}}(x,y)$.
Again, there are four possibilies: $\emptyset,\\{x\\},\\{y\\}$ and
$\\{x,y\\}$.

If $\operatorname{op^{\prime}}(x,y)=\emptyset$, then
$\operatorname{op^{\prime}}(\operatorname{now}x,$, contradicting both (8) and
(9).

If $\operatorname{op^{\prime}}(x,y)=\\{x\\}$, then
$\operatorname{op^{\prime}}(\operatorname{now}x,$, again contradicting
equations (8) and (9).

If $\operatorname{op^{\prime}}(x,y)=\\{y\\}$, then
$\operatorname{op^{\prime}}(\operatorname{now}x,$, again contradicting
equations (8) and (9).

So we conclude that $\operatorname{op^{\prime}}(x,y)=\\{x,y\\}$. From this we
now prove

$\\{$

In the case of (8), this is the first equation of (8), in the case of (9),
this is proved as follows

$\\{$

Finally the contradiction can be obtained as follows:

######  Proof E.88 (Details of Example 6.29).

Let $A$ be the algebraic theory with one idempotent binary operation $*$ and
one unary operator $!$, with no further equations. Let $T$ be the monad
generated by $A$. To define the distributive law $\zeta:TD\to DT$ it suffices
to give a lifting of the monad $D$ to the category of $T$-algebras. We first
define a $T$-algebra structure on $DX$, for $X$ a $T$-algebra, then check that
$D$ preserves $T$-algebra homomorphisms, and finally we show that the unit and
the multiplication of $D$ are $T$-algebra homomorphisms.

Let $X$ be a $T$-algebra. Define $!:DX\to DX$ by:

$\displaystyle!(\operatorname{now}(x))$ $\displaystyle=\operatorname{now}(!x)$
$\displaystyle!($ $\displaystyle=x.$

Define $*:DX\times DX\to DX$ as:

$x*y=\Lambda\kappa.x*^{\kappa}y,$

where $*^{\kappa}:DX\times DX\to{D^{\kappa}}X$ is defined by guarded recursion
as:

$\displaystyle(\operatorname{now}(x))*^{\kappa}(\operatorname{now}(y))$
$\displaystyle=\operatorname{now}^{\kappa}(x*y)$
$\displaystyle(\operatorname{now}(x))*^{\kappa}($ $\displaystyle=$
$\displaystyle($ $\displaystyle=$ $\displaystyle($ $\displaystyle=$

To show that this defines a $T$-algebra on $DX$, we need to prove that $*$ is
idempotent. For this it suffices to prove that

$\forall x:DX.\>x*^{\kappa}x=x\,[\kappa]$

which we prove by guarded recursion as follows:

If $x$ is of the form $\operatorname{now}(x^{\prime})$, then:

$\displaystyle(\operatorname{now}(x^{\prime}))*^{\kappa}(\operatorname{now}(x^{\prime}))$
$\displaystyle=\operatorname{now}^{\kappa}(x^{\prime}*x^{\prime})$
$\displaystyle=\operatorname{now}^{\kappa}(x^{\prime})$
$\displaystyle=x\,[\kappa],$

where we used idempotency of $*:X\times X\rightarrow X$ in the second
equality.

If $x$ is of the form , then:

$\displaystyle=$ $\displaystyle=$ $\displaystyle=$

where we applied guarded recursion in the second equality.

It is clear that if $f:X\to Y$ is a $T$-algebra homomorphism, then so is $Df$.

Finally, we must show that the unit ($\operatorname{now}$) and the
multiplication $\mu$ of $D$ are homomorphisms. In the case of
$\operatorname{now}$, this is clear from definitions. For $\mu$, we first show
that $\mu(!x)=!\mu(x)$ by cases, for $x:DDX$.

If $x$ is of the form $\operatorname{now}x^{\prime}$, then:

$\displaystyle\mu!(\operatorname{now}x^{\prime})$
$\displaystyle=\mu\operatorname{now}(!x^{\prime})$ $\displaystyle=!x^{\prime}$
$\displaystyle=!\mu(\operatorname{now}(x^{\prime})).$

If $x$ is of the form , then:

$\displaystyle\mu(!$ $\displaystyle=\mu(y)$ $\displaystyle=!$
$\displaystyle=!\mu($

Finally, to show that $\mu$ commutes with $*$ we prove that
$\mu^{\kappa}(x*^{\kappa}y)=\mu(x)*^{\kappa}\mu(y)$ by guarded recursion, and
case analysis for $x,y:DDX$.

If $x$ is of form $\operatorname{now}x^{\prime}$ and $y$ is of form
$\operatorname{now}y^{\prime}$, with $x^{\prime},y^{\prime}:DX$, then:

$\displaystyle\mu^{\kappa}((\operatorname{now}x^{\prime})*^{\kappa}(\operatorname{now}y^{\prime}))$
$\displaystyle=\mu^{\kappa}(\operatorname{now}^{\kappa}(x^{\prime}*^{\kappa}y^{\prime}))$
$\displaystyle=(x*^{\kappa}y)$
$\displaystyle=(\mu(\operatorname{now}x^{\prime}))*^{\kappa}(\mu(\operatorname{now}y^{\prime})).$

If $x$ is of form $\operatorname{now}x^{\prime}$ and $y$ is of form , with
$x^{\prime}:DX,y^{\prime}:DDX$, then we distinguish two cases:
$x^{\prime}=\operatorname{now}x^{\prime\prime}$ with $x^{\prime\prime}:X$ and
$x^{\prime}=$ with $x^{\prime\prime}:DX$. We first consider the case where
$x^{\prime}=\operatorname{now}x^{\prime\prime}$.

$\displaystyle\mu^{\kappa}((\operatorname{now}(\operatorname{now}x^{\prime\prime}))*^{\kappa}($
$\displaystyle=\mu^{\kappa}($ $\displaystyle=$
$\displaystyle=\;\;\left\\{\;\text{Guarded recursion}\;\right\\}$
$\displaystyle=\;\;\left\\{\;!\text{ commutes with }\mu\;\right\\}$
$\displaystyle=$
$\displaystyle=(\operatorname{now}x^{\prime\prime})*^{\kappa}($
$\displaystyle=(\mu(\operatorname{now}(\operatorname{now}x^{\prime\prime})))*^{\kappa}(\mu($

We then consider the case where $x^{\prime}=$.

$\displaystyle\mu^{\kappa}((\operatorname{now}($ $\displaystyle=\mu^{\kappa}($
$\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=\;\;\left\\{\;!\text{ commutes with
}\mu\;\right\\}$ $\displaystyle=$ $\displaystyle=$ $\displaystyle=($
$\displaystyle=(\mu(\operatorname{now}($

The case where $x$ is of form and $y$ is of form
$\operatorname{now}y^{\prime}$, with $x^{\prime}:DDX,y^{\prime}:DX$ is
symmetric.

Finally, if $x$ is of form and $y$ is of form , with
$x^{\prime},y^{\prime}:DDX$, then:

$\displaystyle\mu^{\kappa}(($ $\displaystyle=\mu^{\kappa}($ $\displaystyle=$
$\displaystyle=\;\;\left\\{\;\text{Guarded recursion}\;\right\\}$
$\displaystyle=($ $\displaystyle=(\mu($

This finishes the proof of the first statement of the example.

For the second statement suppose we further add the equation for associativity
of $*$, and the equation $!(x*y)=(!x)*(!y)$ to the theory $A$. We must show
that also the constructed $*$ and $!$ on $DX$ satisfy these equations.

We start by showing associativity for $*$. We prove this by showing

$\forall x,y,z:DX.\>((x*y)*^{\kappa}z)=(x*^{\kappa}(y*z)),$

which is by definition:

$\forall
x,y,z:DX.\>((\Lambda\kappa.(x*^{\kappa}y))*^{\kappa}z)=(x*^{\kappa}(\Lambda\kappa.(y*^{\kappa}z))).$

We prove this by guarded recursion as follows:

If
$x=\operatorname{now}x^{\prime},y=\operatorname{now}y^{\prime},z=\operatorname{now}z^{\prime}$
for $x^{\prime},y^{\prime},z^{\prime}:X$, then:

$\displaystyle((\operatorname{now}x^{\prime})*(\operatorname{now}y^{\prime}))*^{\kappa}(\operatorname{now}z^{\prime})$
$\displaystyle=(\operatorname{now}(x^{\prime}*y^{\prime}))*^{\kappa}(\operatorname{now}z^{\prime})$
$\displaystyle=\operatorname{now}^{\kappa}((x^{\prime}*y^{\prime})*z^{\prime})$
$\displaystyle=\;\;\left\\{\;\text{Associativity of }*\;\right\\}$
$\displaystyle\quad\operatorname{now}^{\kappa}(x^{\prime}*(y^{\prime}*z^{\prime}))$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\operatorname{now}(y^{\prime}*z^{\prime}))$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}((\operatorname{now}y^{\prime})*(\operatorname{now}z^{\prime}))$

If $x=\operatorname{now}x^{\prime},y=\operatorname{now}y^{\prime},z=$ for
$x^{\prime},y^{\prime}:X,z^{\prime}:DX$, then:

$\displaystyle(\Lambda\kappa.((\operatorname{now}x^{\prime})*^{\kappa}(\operatorname{now}y^{\prime})))*^{\kappa}($
$\displaystyle=(\Lambda\kappa.(\operatorname{now}^{\kappa}(x^{\prime}*y^{\prime})))*^{\kappa}($
$\displaystyle=\operatorname{now}(x^{\prime}*y^{\prime})*^{\kappa}($
$\displaystyle=$ $\displaystyle=$ $\displaystyle=$ $\displaystyle=$
$\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}($
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\Lambda\kappa.$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\Lambda\kappa.$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\Lambda\kappa.(\operatorname{now}y^{\prime})*^{\kappa}($

The case where $x=$ is similar.

If $x=\operatorname{now}x^{\prime},y=$ for
$x^{\prime},z^{\prime}:X,y^{\prime}:DX$, then:

$\displaystyle(\Lambda\kappa.((\operatorname{now}x^{\prime})*^{\kappa}($
$\displaystyle=(\Lambda\kappa.$ $\displaystyle=($ $\displaystyle=$
$\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}($
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\Lambda\kappa.$
$\displaystyle=(\operatorname{now}x^{\prime})*^{\kappa}(\Lambda\kappa.($

If $x=$ for $x^{\prime},y^{\prime}:DX,z^{\prime}:X$, then:

$\displaystyle(\Lambda\kappa.(($ $\displaystyle=(\Lambda\kappa.($
$\displaystyle=($ $\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=($ $\displaystyle=($ $\displaystyle=($

The case where $x=\operatorname{now}x^{\prime},y=$ is similar.

If $x=$ $x^{\prime},z^{\prime}:DX,y^{\prime}:X$, then:

$\displaystyle(\Lambda\kappa.(($ $\displaystyle=(\Lambda\kappa.($
$\displaystyle=($ $\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=($ $\displaystyle=($ $\displaystyle=($

Finally, if $x=$, then:

$\displaystyle(\Lambda\kappa.(($ $\displaystyle=(\Lambda\kappa.($
$\displaystyle=($ $\displaystyle=$ $\displaystyle=\;\;\left\\{\;\text{Guarded
recursion}\;\right\\}$ $\displaystyle=\quad$ $\displaystyle=(($
$\displaystyle=(($ $\displaystyle=(($

This shows that $*:DX\times DX\rightarrow DX$ is associative.

The last thing to show is that $!(x*y)=(!x)*(!y)$, for $x,y:DX$. We show this
by case analysis:

If $x=\operatorname{now}x^{\prime}$ and $y=\operatorname{now}y^{\prime}$,
then:

$\displaystyle!((\operatorname{now}x^{\prime})*(\operatorname{now}y^{\prime}))$
$\displaystyle=!(\operatorname{now}(x^{\prime}*y^{\prime}))$
$\displaystyle=\operatorname{now}(!(x^{\prime}*y^{\prime}))$
$\displaystyle=\operatorname{now}((!x^{\prime})*(!y^{\prime}))$
$\displaystyle=(!(\operatorname{now}x^{\prime}))*(!(\operatorname{now}y^{\prime})),$

where we have used that $\operatorname{now}$ is a $T$-algebra homomorphism.

If $x=\operatorname{now}x^{\prime}$ and $y=$, then:

$\displaystyle!((\operatorname{now}x^{\prime})*($
$\displaystyle=!(\lambda\kappa.((\operatorname{now}x^{\prime})*^{\kappa}($
$\displaystyle=!(\lambda\kappa.$ $\displaystyle=!$
$\displaystyle=(\lambda\kappa.(!(\operatorname{now}x^{\prime})*^{\kappa}y^{\prime}))$
$\displaystyle=!(\operatorname{now}x^{\prime})*y^{\prime}$
$\displaystyle=!(\operatorname{now}x)*!($

The case for $x=$ and $y=\operatorname{now}y^{\prime}$ is similar.

If $x=$ and $y=$, then:

$\displaystyle!(($ $\displaystyle=!(\lambda\kappa.(($
$\displaystyle=!(\lambda\kappa.$ $\displaystyle=!$
$\displaystyle=\lambda\kappa.(x^{\prime}*^{\kappa}y^{\prime})$
$\displaystyle=x^{\prime}*y^{\prime}$ $\displaystyle=!($

This finishes the proof of the second statement.

######  Proof E.242 (Proof of Theorem 6.40).

Given the algebraic monad $T$, presented by a theory with a binary operation
$\operatorname{op}$ that is commutative and idempotent, we assume that there
is a distributive law of type $T{D^{\kappa}}\rightarrow{D^{\kappa}}T$, and
derive a contradiction.

By Lemma 4.2, such a distributive law induces a distributive law of type
$TD\rightarrow DT$. Then by Lemma 6.1 we know that then there exist binary
operations $\operatorname{op_{1}}$ and $\operatorname{op^{\prime}}$ such that
for any $T$-model $X$, the lifting of $\operatorname{op}$ to $DX$ satisfies:

$\operatorname{op}($ (10)

and either

$\displaystyle\operatorname{op}($ $\displaystyle=$
$\displaystyle\operatorname{op^{\prime}}(x,$
$\displaystyle=\operatorname{op_{1}}(x,y),$ (11)

or

$\displaystyle\operatorname{op}($
$\displaystyle=\operatorname{op^{\prime}}(x,y)$
$\displaystyle\operatorname{op^{\prime}}(x,$ $\displaystyle=$ (12)

We show that both cases lead to a contradiction.

First we assume that we are in case (11). The fact that the distributive law
$\zeta:TD\rightarrow DT$ is induced by a distributive law
$\zeta^{\kappa}:T{D^{\kappa}}\rightarrow{D^{\kappa}}T$ means that for any $X$,
and any $x:T(DX)$

$\zeta(x)\,[\kappa]=\zeta^{\kappa}(T(\mathsf{ev}_{\kappa})x)$

where $T(\mathsf{ev}_{\kappa})$ is the functorial action of $T$ applied to the
map $\mathsf{ev}_{\kappa}:DX\to{D^{\kappa}}X$, mapping $y$ to $y\,[\kappa]$.
From this and (11) it follows that for any $T$-model $X$, the $T$-algebra
structure on ${D^{\kappa}}X$ induced by $\zeta^{\kappa}$ satisfies

$\displaystyle\operatorname{op}($ $\displaystyle=$ (13)

for any $x,y:DX$.

Now consider the case of $X=T(2)$. We write $\mathsf{tt},\mathsf{ff}$ for the
two elements of $2$ and, leaving the unit of $T$ implicit, also for the
corresponding two elements of $T(2)$. To arrive at a contradiction, we will
prove $\triangleright^{\kappa}\bot$ by guarded recursion. Since the proof is
parametric in $\kappa$, we can use it to prove
$\forall\kappa.\triangleright^{\kappa}\bot$, which implies
$\forall\kappa.\bot$, in turn implying $\bot$ since $\bot$ is clock
irrelevant.

Note that since $\mathsf{tt}=\mathsf{ff}$ is equivalent to $\bot$, by
extensionality for $\triangleright^{\kappa}$ and injectivity of and
$\operatorname{now}^{\kappa}$, $\triangleright^{\kappa}\bot$ is equivalent to

(14)

where the equality is between elements of ${D^{\kappa}}T(2)$. So we will prove
(14) by guarded recursion. First note

$\displaystyle=\operatorname{op}($ $\displaystyle=$ $\displaystyle=$
$\displaystyle=\operatorname{op}($

using idempotency of $\operatorname{op}$, (13), and the guarded recursion
assumption. By a similar argument

and so by commutativity of $\operatorname{op}$, (14) follows as desired.

Suppose now (12). Again we want to arrive at a contradiction by considering
the $T$-algebra structures on $DX$ and ${D^{\kappa}}X$ induced by one on $X$.
First note that $\operatorname{op_{1}}$ is commutative. This follows by
considering commutativity an equation in $T(2)$ and considering the induced
model on $DT(2)$. In this model we get

$\displaystyle=\operatorname{op}($ $\displaystyle=\operatorname{op}($
$\displaystyle=$

(writing $x,y$ for the two elements of $2$) and so commutativity follows from
injectivity of and $\operatorname{now}$. Similar reasoning shows that
$\operatorname{op_{1}}$ is idempotent:

Next we show that $\operatorname{op_{1}}(x,y)=\operatorname{op_{1}}(z,y)$ for
distinct variables $x,y,z$ leads to a contradiction. Again this can be read as
an equation between elements in $T(3)$. Since we can substitute for $y$ in the
assumed equation we get

$\displaystyle
x=\operatorname{op_{1}}(x,x)=\operatorname{op_{1}}(z,x)=\operatorname{op_{1}}(x,z)=\operatorname{op_{1}}(z,z)=z,$

which is a contradiction, since $x$ and $z$ are distinct. Note that this
argument uses that $3$ has decidable equality.

Similarly, also the equation
$\operatorname{op^{\prime}}(x,y)=\operatorname{op^{\prime}}(z,y)$ for distinct
variables $x,y,z$ leads to a contradiction, since by (12) this leads to

$\displaystyle=$
$\displaystyle=\operatorname{op^{\prime}}(\operatorname{now}(x),$
$\displaystyle=\operatorname{op^{\prime}}(\operatorname{now}(z),$
$\displaystyle=$

and so $\operatorname{op_{1}}(x,y)=\operatorname{op_{1}}(z,y)$, which we have
just proven inconsistent.

Similarly to the argument in the case of (11) we can show that the fact that
the distributive law is induced by one on $T{D^{\kappa}}\to{D^{\kappa}}T$
implies that the model structure on ${D^{\kappa}}X$ for any $T$-model $X$
satisfies

$\operatorname{op}($ (15)

for any $x,y:DX$.

We use the above to prove $\bot$ by guarded recursion. So assume
$\triangleright^{\kappa}\bot$. As we have seen, to prove $\bot$, it suffices
to show $\operatorname{op^{\prime}}(x,y)=\operatorname{op^{\prime}}(z,y)$ for
distinct variables $x,y,z$. We prove that
$\operatorname{now}(\operatorname{op^{\prime}}(x,y))=\operatorname{now}(\operatorname{op^{\prime}}(z,y))$
as elements of ${D^{\kappa}}(T(3))$:

$\displaystyle\operatorname{now}(\operatorname{op^{\prime}}(x,y))$
$\displaystyle=\operatorname{op^{\prime}}(\operatorname{now}(x),\operatorname{now}(y))$
$\displaystyle=\operatorname{op}($ $\displaystyle=\operatorname{op}($
$\displaystyle=\operatorname{op^{\prime}}(\operatorname{now}(z),\operatorname{now}(y))$
$\displaystyle=\operatorname{now}(\operatorname{op^{\prime}}(z,y)),$

where we have applied (15) to $\Lambda\kappa.\operatorname{now}(x)$ and
$\Lambda\kappa.\operatorname{now}(y)$ in the second equality and used the
assumption $\triangleright^{\kappa}\bot$ in the third.

##  Appendix F Omitted proofs Section 7

######  Lemma F.1.

([31]) If $x\sim_{R}^{\kappa}\,y$ then
$\delta^{\kappa}(x)\sim_{R}^{\kappa}\,y$. If then
${{\triangleright}\,(\alpha\\!:\\!\kappa).(x\,[\alpha]\sim_{R}^{\kappa}\,y)}$.

######  Proof F.3.

The proof of the first statement is by cases of $x$ and $y$. If
$y=\operatorname{now}(y^{\prime})$, then the proof is easy. If $y=$ and
$x=\operatorname{now}(x^{\prime})$, then there exists $n$ and
$y^{\prime\prime}$ such that $($, and $R(x,y^{\prime\prime})$. We must show
that
${\triangleright}\,(\alpha\\!:\\!\kappa).(\operatorname{now}(x)\sim_{R}^{\kappa}\,y^{\prime}\,[\alpha])$,
but since $y^{\prime}\,[\alpha]=($, this is easy. Finally, if $y=$ and $x=$ we
must show that ${\triangleright}\,(\alpha\\!:\\!\kappa).($ assuming
${\triangleright}\,(\alpha\\!:\\!\kappa).(x^{\prime}\,[\alpha]\sim_{R}^{\kappa}\,y^{\prime}\,[\alpha])$,
which follows from guarded recursion using that tick-irrelevance implies

$\displaystyle($ $\displaystyle=$ $\displaystyle=$ $\displaystyle=$

For the second statement, suppose . Then by the first statement which unfolds
to
${\triangleright}\,(\alpha\\!:\\!\kappa).(x\,[\alpha]\sim_{R}^{\kappa}\,y)$.

The proof of Lemma F.19 uses the following Lemma.

######  Lemma F.16.

If $x,y:{D^{\kappa}}({D^{\kappa}}(X))$ and $x\sim^{\kappa}\,y$ (omitting the
subscript) then $\mu(x)\sim^{\kappa}\,\mu(y)$

######  Proof F.17.

This is by guarded recursion and cases of $x$ and $y$. If
$x=\operatorname{now}(x^{\prime})$ we get $n$ such that
$y=(\delta^{\kappa})^{n}(\operatorname{now}(y^{\prime}))$ and
$x^{\prime}\sim_{R}^{\kappa}\,y^{\prime}$. We must show
$x^{\prime}\sim_{R}^{\kappa}\,(\delta^{\kappa})^{n}(y^{\prime})$, which is
just an $n$-fold application of Lemma F.1. The case of
$y=\operatorname{now}(y^{\prime})$ is similar, and the case of both $x$, $y$
of the form follows by guarded recursion.

######  Lemma F.19.

Let $T$ be the free model monad of algebraic theory
$\mathbb{T}=(\Sigma^{\mathbb{T}},E^{\mathbb{T}})$, such that $E^{\mathbb{T}}$
contains no drop equations. Parallel lifting defines a natural transformation
$T_{\mathsf{sd}}D_{\mathsf{sd}}\to D_{\mathsf{sd}}T_{\mathsf{sd}}$.

######  Proof F.20.

We show that if $x_{i}\sim_{R}\,y_{i}$ for $i=1,\dots,n$, then
${t}^{par}(x_{1},\dots,x_{n})\sim_{T(R)}\,{t}^{par}(y_{1},\dots,y_{n})$. We do
this in the special case of $t$ being an operation from the signature, which
then generalises by induction to general $t$. We show the special case by
proving the stronger statement that if $x_{i}\sim_{R}^{\kappa}\,y_{i}$ for all
$i$ then

${\operatorname{op}}^{par}(x_{1},\ldots,x_{n})\sim_{T(R)}^{\kappa}\,{\operatorname{op}}^{par}(y_{1},\ldots,y_{n})$

by guarded recursion. Suppose first that all $x_{1},\ldots,x_{n}$ are of the
form $\operatorname{now}(x^{\prime}_{i})$ for $1\leq i\leq n$, then

${\operatorname{op}}^{par}(x_{1},\ldots,x_{n})=\operatorname{now}\operatorname{op}(x^{\prime}_{1},\ldots,x^{\prime}_{n}),$

and since $x_{i}\sim_{R}^{\kappa}\,y_{i}$, there exist $m_{i}$ such that:

$y_{i}=(\delta^{\kappa})^{m_{i}}(\operatorname{now}y^{\prime}_{i}),$

with $R(x_{i}^{\prime},y_{i}^{\prime})$. Let $N=\max_{i}m_{i}$. Then:

$\displaystyle{\operatorname{op}}^{par}(y_{1},\ldots,y_{n})$
$\displaystyle=\;{\operatorname{op}}^{par}((\delta^{\kappa})^{m_{1}}(\operatorname{now}y^{\prime}_{1}),\ldots,(\delta^{\kappa})^{m_{n}}(\operatorname{now}y^{\prime}_{n}))$
$\displaystyle=\;(\delta^{\kappa})^{N}(\operatorname{now}(\operatorname{op}(y^{\prime}_{1},\ldots,y^{\prime}_{n}))).$

and so
${\operatorname{op}}^{par}(x_{1},\ldots,x_{n})\sim_{R}^{\kappa}\,{\operatorname{op}}^{par}(y_{1},\ldots,y_{n})$.
The case of all $y_{i}$ of the form $y_{i}=\operatorname{now}(y_{i}^{\prime})$
is symmetric.

Now suppose some of the $x_{i}$ are of the form and similarly some $y_{i}$ are
of the form . Then

$\displaystyle{\operatorname{op}}^{par}(x_{1},\ldots,x_{n})$ $\displaystyle=$
$\displaystyle{\operatorname{op}}^{par}(y_{1},\ldots,y_{n})$ $\displaystyle=$

where $x_{i}^{\prime\prime}=x_{i}$ if
$x_{i}=\operatorname{now}(x_{i}^{\prime})$ and
$x_{i}^{\prime\prime}=x_{i}^{\prime}\,[\alpha]$ if $x_{i}=$ and likewise for
$y_{i}^{\prime\prime}$. In either of the four possible cases we can prove that
${\triangleright}\,(\alpha\\!:\\!\kappa).(x_{i}^{\prime\prime}\sim_{R}^{\kappa}\,y_{i}^{\prime\prime})$,
using Lemma F.1 in the two non-symmetric cases. By guarded recursion we
therefore get that:

${\triangleright}\,(\alpha\\!:\\!\kappa).({\operatorname{op}}^{par}(x_{1}^{\prime\prime},\ldots,x_{n}^{\prime\prime})\sim_{T(R)}^{\kappa}\,{\operatorname{op}}^{par}(y_{1}^{\prime\prime},\ldots,y_{n}^{\prime\prime})),$

and so
${\operatorname{op}}^{par}(x_{1},\ldots,x_{n})\sim_{T(R)}^{\kappa}\,{\operatorname{op}}^{par}(y_{1},\ldots,y_{n})$.

######  Proof F.26 (Proof of Theorem 7.7).

We must prove that the four laws of Definition 2.7 hold. Three of these can be
easily seen to hold already on the level of representatives. It remains to
show that the natural transformation commutes with the multiplication $\mu$ of
$D$. This boils down to showing that for any term $t$ with $n$ free variabels
and any vector $x_{1},\ldots,x_{n}$ of elements in $DDTX$ the following holds:

${t}^{par}_{DX}(\mu(x_{1}),\ldots,\mu(x_{n}))\sim_{T(R)}\,\mu({t}^{par}_{DDX}{t}(x_{1},\ldots,x_{n})),$

To prove this, it suffices to show that if $x_{i}\sim\,y_{i}$ for all i, then

${t}^{par}_{DX}(\mu(x_{1}),\ldots,\mu(x_{n}))\sim_{T(R)}\,\mu({t}^{par}_{DDX}{t}(y_{1},\ldots,y_{n})),$

We prove this strengthened statement for the case of $t=\operatorname{op}$ for
any n-ary operation $\operatorname{op}$. The general case then follows by
induction using transitivity of $\sim_{T(R)}\,$ as follows

$\displaystyle{\operatorname{op}}^{par}_{DX}({t_{1}}^{par}_{DX}(\mu(\vec{x})),\ldots,{t_{n}}^{par}_{DX}(\mu(\vec{x})))$
$\displaystyle\sim_{T(R)}\,{\operatorname{op}}^{par}_{DX}(\mu({t_{1}}^{par}_{DDX}(\vec{x})),\ldots,\mu({t_{n}}^{par}_{DDX}(\vec{x})))$
$\displaystyle\sim_{T(R)}\,\mu({\operatorname{op}}^{par}_{DDX}({t_{1}}^{par}_{DDX}(\vec{x}),\ldots,{t_{n}}^{par}_{DDX}(\vec{x}))$

where $\mu(x_{1},\dots,x_{m})=(\mu(x_{1}),\dots,\mu(x_{m}))$.

Because we need to use guarded recursion we prove the statement for
$t=\operatorname{op}$ in the case of the guarded delay monad. More precisely,
supposing $x_{i}\sim^{\kappa}\,y_{i}$ for all $i$ (where $\sim^{\kappa}\,$ is
the relation on ${D^{\kappa}}{D^{\kappa}}X$), we show that:

${\operatorname{op}}^{par}_{{D^{\kappa}}X}(\mu(x_{1}),\ldots,\mu(x_{n}))\sim_{T(R)}^{\kappa}\,\mu({\operatorname{op}}^{par}_{{D^{\kappa}}{D^{\kappa}}X}(y_{1},\ldots,y_{n})),$

for any operation $\operatorname{op}$ in the signature.

We prove this by guarded recursion. Suppose first that all $x_{i}$ are on the
form $\operatorname{now}(x_{i}^{\prime})$. Then:

$\displaystyle{\operatorname{op}}^{par}_{{D^{\kappa}}X}(\mu(x_{1}),\ldots,\mu(x_{n}))$
$\displaystyle={\operatorname{op}}^{par}_{{D^{\kappa}}X}(x_{1}^{\prime},\ldots,x_{n}^{\prime})$
$\displaystyle=\mu({\operatorname{op}}^{par}_{{D^{\kappa}}{D^{\kappa}}X}(x_{1},\ldots,x_{n})).$

The proof now follows from operations and $\mu$ preserving weak bisimilarity.
If all $y_{i}$ are of the form $\operatorname{now}(y_{i}^{\prime})$ then:

$\displaystyle\mu({\operatorname{op}}^{par}_{{D^{\kappa}}{D^{\kappa}}X}(y_{1},\ldots,y_{n}))$
$\displaystyle={\operatorname{op}}^{par}_{{D^{\kappa}}X}(y_{1}^{\prime},\ldots,y_{n}^{\prime})$
$\displaystyle={\operatorname{op}}^{par}_{{D^{\kappa}}X}(\mu(y_{1}),\ldots,\mu(y_{n})).$

and so again the proof follows from $\mu$ and operations preserving weak
bisimilarity.

In the remaining cases

$\displaystyle{\operatorname{op}}^{par}_{{D^{\kappa}}X}(\mu(x_{1}),\ldots,\mu(x_{n}))$
$\displaystyle=$
$\displaystyle\mu({\operatorname{op}}^{par}_{{D^{\kappa}}{D^{\kappa}}X}(y_{1},\ldots,y_{n}))$
$\displaystyle=$

where

$x_{i}^{\prime}=\begin{cases}x_{i}&\text{if
}x_{i}=\operatorname{now}(\operatorname{now}(x_{i}^{\prime\prime}))\\\
x_{i}^{\prime\prime}\,[\alpha]&\text{if }x_{i}=\step(x_{i}^{\prime\prime})\\\
\operatorname{now}(x_{i}^{\prime\prime}\,[\alpha])&\text{if
}x_{i}=\operatorname{now}(\step(x_{i}^{\prime\prime})),\end{cases}$

and

$y_{i}^{\prime}=\begin{cases}y_{i}&\text{if
}y_{i}=\operatorname{now}(y_{i}^{\prime\prime})\\\
y_{i}^{\prime\prime}\,[\alpha]&\text{if
}y_{i}=\step(y_{i}^{\prime\prime}).\end{cases}$

It remains to show that in all these cases
${\triangleright}\,(\alpha\\!:\\!\kappa).(x_{i}^{\prime}\sim^{\kappa}\,y_{i}^{\prime})$.
This is done using guarded recursion as follows.

  * •

If $x_{i}=\operatorname{now}(\operatorname{now}(x_{i}^{\prime\prime}))$ and
$y_{i}=\operatorname{now}(y_{i}^{\prime\prime})$, then
$x^{\prime}_{i}\sim^{\kappa}\,y^{\prime}_{i}$ by assumption.

  * •

If
$x^{\prime}_{i}=\operatorname{now}(\operatorname{now}(x_{i}^{\prime\prime}))$
and $y_{i}=$ then the result follows from Lemma F.1.

  * •

The case where $x_{i}=$ and $y_{i}=\operatorname{now}(y_{i}^{\prime\prime})$
also follows from Lemma F.1.

  * •

In the case of $x_{i}=$ and $y_{i}=$ it follows immediately from the
definition of $x_{i}\sim^{\kappa}\,y_{i}$ that
${\triangleright}\,(\alpha\\!:\\!\kappa).(x_{i}^{\prime}\sim^{\kappa}\,y_{i}^{\prime})$.

  * •

If $x_{i}=\operatorname{now}($ and
$y_{i}=\operatorname{now}(y_{i}^{\prime\prime})$, then by definition of
$x_{i}\sim^{\kappa}\,y_{i}$ we get . But then also
${\triangleright}\,(\alpha\\!:\\!\kappa).(x_{i}^{\prime\prime}\,[\alpha]\sim^{\kappa}\,y_{i}^{\prime\prime})$
(Lemma F.1) and therefore
${\triangleright}\,(\alpha\\!:\\!\kappa).(\operatorname{now}(x_{i}^{\prime\prime}\,[\alpha])\sim^{\kappa}\,\operatorname{now}(y_{i}^{\prime\prime}))$.

  * •

If $x_{i}=\operatorname{now}($ and $y_{i}=$, then it follows from
$x_{i}\sim^{\kappa}\,y_{i}$ that there is an $n:\mathbb{N}$ and a
$y_{i}^{\prime\prime\prime}$ such that
$y_{i}=(\delta^{\kappa})^{n}\operatorname{now}(y^{\prime\prime\prime})$, and ,
which implies that
${\triangleright}\,(\alpha\\!:\\!\kappa).(x_{i}^{\prime\prime}\,[\alpha]\sim^{\kappa}\,y_{i}^{\prime\prime\prime})$.
Since $y_{i}=$, we also know that
$y_{i}^{\prime\prime}\,[\alpha]=(\delta^{\kappa})^{n-1}\operatorname{now}(y^{\prime\prime\prime})$.
Hence by definition

${\triangleright}\,(\alpha\\!:\\!\kappa).(\operatorname{now}(x_{i}^{\prime\prime}\,[\alpha])\sim^{\kappa}\,y_{i}^{\prime\prime}\,[\alpha])$

as required.