<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
On 02/04/19 22:10, Tom Jack wrote:<br>
<blockquote type="cite"
cite="mid:CAK0rV7cEtD9Vh8cgUqvLwiz=rD8V8t3CMrHRBjYNR5HqURzbew@mail.gmail.com">
<div dir="ltr">
<div dir="ltr">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.</div>
</div>
</blockquote>
<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>
<blockquote type="cite"
cite="mid:CAK0rV7cEtD9Vh8cgUqvLwiz=rD8V8t3CMrHRBjYNR5HqURzbew@mail.gmail.com">
<div dir="ltr">
<div dir="ltr">
<div><br>
</div>
<div>Are there examples like this which don't involve a mutual
coinductive type?</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at
1:06 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"> 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</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
<br>
</body>
</html>