## Quotienting the delay monad by weak bisimilarity

Institute of Cybernetics at TUT

Thursday, 30 April 2015, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: The delay datatype has been introduced by Capretta
as a means to represent general recursive functions in intensional
type theory. It is a (strong) monad and it constitutes a constructive
alternative to the maybe monad. In several applications two delayed
computations are considered equal if they either converge to the same
value of if they diverge. Such equivalence relation is called weak
bisimilarity. Typically in type theory one represents quotients via
setoids, and using this approach the delay monad quotiented by weak
bisimilarity is still a (strong) monad.

In this talk we consider an extension of type theory with quotient
types, following Hofmann's approach. In this theory we investigate
under which conditions the delay monad quotiented by weak bisimilarity
is still a monad. In particular we will thoroughly discuss the issues
in constructing the monad multiplication. A solution will be given
postulating a couple of non-classical axioms: the axiom of countable
choice and the univalence axiom for mere propositions.

This is joint work with James
Chapman and Tarmo
Uustalu.

Tarmo Uustalu

Last update 29 April 2015