<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal">Our presentation using chains as functions from Nat isn’t really so different to the coinductive definition. The delay monad can be equivalently described as functions f : Nat -> Maybe(A) with the property that if f n = just a -> f(n+1)
= just a. Hence the definition in our paper corresponds to the delay monad of they are flat, i.e. if we don’t iterate the lub constructor and use only bottom or eta a. Hence if you want to model the partiality monad using a coninductive type you should allow
to iterate it that is use something like Delay^n(A) and quotient this e.g. by collapsing layers. Our definition of the partiality monad seems quite natural because it is simply the free omega-CPO over a given set. However, maybe one can define this coniductively
instead of using functions to describe chains.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thorsten<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Nicolai Kraus <nicolai.kraus@gmail.com><br>
<b>Date: </b>Tuesday, 2 April 2019 at 22:17<br>
<b>To: </b>Tom Jack <tom@tomjack.co><br>
<b>Cc: </b>agda list <agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] Defining the Delay monad as a HIT in cubical agda<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt">On 02/04/19 22:10, Tom Jack wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
</div>
</div>
</blockquote>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
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`.<br>
By "chain", I mean<br>
now(a) = later(now(a)) = later(later(now(a))) = ...<br>
<br>
-- Nicolai<br>
<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Are there examples like this which don't involve a mutual coinductive type?<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">On Tue, Apr 2, 2019 at 1:06 PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com">nicolai.kraus@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<p class="MsoNormal" style="margin-left:36.0pt">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<o:p></o:p></p>
</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>