[Agda] Defining the Delay monad as a HIT in cubical agda

[Nils Anders Danielsson]

On 02/04/2019 12.25, Thorsten Altenkirch wrote:
> The problem with the quotiented delay monad is that you cannot even
> prove that it is a monad.

Has this been proved now?

-- 
/NAD