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

[Tom Jack]

We cannot have Delay A = A, because there is never : Delay ⊥.

This is puzzling to me, indeed, because Delay looks like:

now : A -> Delay A
later : Delay' A -> Delay A
step : later = force

Normally, I'd expect to be able to 'do path induction' on (later, step),
winding up with just `now`, so that Delay A = A. But this is absurd.

Are there examples like this which don't involve a mutual coinductive type?

On Tue, Apr 2, 2019 at 1:06 PM Nicolai Kraus <nicolai.kraus at gmail.com>
wrote:

> Interesting! So, in case Delay(Unit) does turn out to be contractible, we
> might also expect that Delay(A) = A. This doesn't seem intuitive to me, but
> it could still be true. Do you see a way to construct Delay(A) -> A? If
> there is such a function, it should be quite canonical, and maybe it's
> easier to write this function than to prove the contractibility. But if we
> can't do this, and we also can't distinguish 'now' and 'never', then I have
> no idea what Delay(A) actually is. Does any of the cubical models capture
> such constructions?
> (Maybe, at this point, we shouldn't call it "Delay" :)
> -- Nicolai
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190402/9482029b/attachment.html>