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

[Nicolai Kraus]

On 02/04/19 22:10, Tom Jack wrote:
> 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.

I think this is what would happen if we were talking about induction 
instead of coinduction. My intuition is that coinduction causes all the 
"chains" to be "one-point-compactified" with the same point `never`.
By "chain", I mean
now(a) = later(now(a)) = later(later(now(a))) = ...

-- Nicolai

>
> 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 
> <mailto: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/cc87e73e/attachment.html>