## Quotiented delay monad as the initial ω-join classifying monad

Institute of Cybernetics at TUT

Monday, 29 August 2016, 14:00 (note the unusual weekday)

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: The delay monad was introduced by Capretta as a
means to deal with partial functions (possibly non-terminating
programs) in type theory. It is often desirable to consider two
delayed computations equal, if they terminate with equal values,
whenever one of them terminates. The equivalence relation underlying
this identification is called weak bisimilarity. In previous work, we
have shown that the delay datatype quotiented by weak bisimilarity is
also a monad, if we extend type theory with extra principles such as
countable choice and propositional extensionality. Moreover, we proved
that the quotiented delay datatype delivers free ω-complete pointed
partial orders (ωCPPO for short). As a consequence, homsets in the
Kleisli category of the quotiented delay monad are endowed with a
ωCPPO structure.

In this talk we introduce the notion of ω-join classifying
monad. A classifying monad is a monad whose Kleisli category is a
restriction category (that is, an axiomatic formulation of categories
of *partial functions* introduced by Cockett and Lack). In every
restriction category, it is possible to define an order on homsets,
the so-called restriction order, and this order specifies a
Poset-enrichment on the category. A ω-join classifying monad is
a classifying monad whose restriction order specifies a
ωCPPO-enrichment. We show, using the results from previous work,
that the quotiented delay monad is a ω-join classifying
monad. Interestingly, it is also the initial such monad.

Tarmo Uustalu

Last update 24 August 2016