<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
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?<br>
(Maybe, at this point, we shouldn't call it "Delay" :)<br>
-- Nicolai<br>
<br>
<br>
<div class="moz-cite-prefix">On 02/04/19 15:08, Jesper Cockx wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAEm=boz1Zm2LKVrHT2AuxVSUrZK=VYPES9x7B+i7T9uH-8c4yA@mail.gmail.com">
<div dir="ltr">
<div>Hi Nicolai,</div>
<div><br>
</div>
<div>Yes, Christian and I suspected the same thing (that this
definition of the delay monad is actually a unit type), but I
haven't managed to prove that either because of some
mysterious termination checker problem.</div>
<div><br>
</div>
<div>I'm currently trying a different approach where I define
the Delay type mutually with the ⇓ type so I can quotient by
the relation "normalize to the same value in a finite number
of steps". I'll let you know later if it works.</div>
<div><br>
</div>
<div>-- Jesper<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at 3:15 PM
Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com"
moz-do-not-send="true">nicolai.kraus@gmail.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> Hi Jesper,<br>
<br>
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. <br>
<br>
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).<br>
<br>
Thus, my guess is that Delay(Unit) could be contractible.
One could try to prove that every element is equal to 'now'.<br>
<br>
Cheers,<br>
Nicolai<br>
<br>
<br>
<div class="gmail-m_5865528187534997207moz-cite-prefix">On
29/03/19 18:40, Jesper Cockx wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div>Hi all,</div>
<div><br>
</div>
<div>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:</div>
<div><br>
</div>
<div>
<div style="margin-left:40px"><span
style="font-family:monospace,monospace">data
Delay (A : Set ℓ) : Set ℓ</span><br>
<span style="font-family:monospace,monospace"></span><br>
<span style="font-family:monospace,monospace">record
Delay′ (A : Set ℓ) : Set ℓ where</span><br>
<span style="font-family:monospace,monospace">
coinductive</span><br>
<span style="font-family:monospace,monospace">
field</span><br>
<span style="font-family:monospace,monospace">
force : Delay A</span><br>
<span style="font-family:monospace,monospace"></span><br>
<span style="font-family:monospace,monospace">open
Delay′ public</span><br>
<span style="font-family:monospace,monospace"></span><br>
<span style="font-family:monospace,monospace">data
Delay A where</span><br>
<span style="font-family:monospace,monospace">
now : A → Delay A</span><br>
<span style="font-family:monospace,monospace">
later : Delay′ A → Delay A</span><br>
<span style="font-family:monospace,monospace">
step : (x : Delay′ A) → later x ≡ x .force</span><br>
</div>
<br>
</div>
<div> 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: <a
href="https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9"
target="_blank" moz-do-not-send="true">https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9</a>
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.)<br>
</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Jesper<br>
</div>
</div>
</div>
</div>
<br>
<fieldset
class="gmail-m_5865528187534997207mimeAttachmentHeader"></fieldset>
<br>
<pre>_______________________________________________
Agda mailing list
<a class="gmail-m_5865528187534997207moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="gmail-m_5865528187534997207moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
<br>
</body>
</html>