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.