<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>