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

[Nicolai Kraus]

Hi Jesper,

I find this construction very interesting since it's the first "cubical 
higher co-inductive type" that I've seen! Unfortunately, I don't know 
how these "CHCIT's" behave in Agda.

If I had to guess, I would expect that you *cannot* distinguish now and 
never, which would mean that your construction doesn't give you what you 
wanted. The difference to the quotiented delay monad (or, for what it's 
worth, the QIT/QIIT partiality monad) is that your construction inserts 
the equations "coinductively" (usually, only the later-steps are 
coinductive).

Thus, my guess is that Delay(Unit) could be contractible. One could try 
to prove that every element is equal to 'now'.

Cheers,
Nicolai


On 29/03/19 18:40, Jesper Cockx wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190402/b6946291/attachment.html>