<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" 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="moz-cite-prefix">On 29/03/19 18:40, Jesper Cockx wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAEm=boy4k5FDBbxcqUWH-nP-H78YY-R2p9oW_cn7q_u3kEKAcw@mail.gmail.com">
<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"
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="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>