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

[Jesper Cockx]

Hi all,

As an experiment with cubical agda, I was trying to define a quotiented
version of the Delay monad as a higher inductive type. I'm using this
definition:

data Delay (A : Set ℓ) : Set ℓ

record Delay′ (A : Set ℓ) : Set ℓ where
  coinductive
  field
    force : Delay A

open Delay′ public

data Delay A where
  now   : A → Delay A
  later : Delay′ A → Delay A
  step  : (x : Delay′ A) → later x ≡ x .force

I managed to implement some basic functions on it but I got stuck on trying
to prove the looping computation 'never' does not in fact evaluate to any
value. My code is available here:
https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9
I looked at the problem together with Christian Sattler and we are not even
sure it is actually provable. Does anyone have an idea how to proceed? Or
has someone already experimented with coinductive types in cubical and
encountered similar problems? (I looked at the paper "Partiality revisited"
by Thorsten, Nisse and Nicolai but they use a very different definition of
the partiality monad.)

Cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190329/6f4f8a55/attachment.html>