<div dir="ltr"><div dir="ltr"><div dir="ltr">We cannot have Delay A = A, because there is never : Delay ⊥.</div><div dir="ltr"><br></div><div>This is puzzling to me, indeed, because Delay looks like:</div><div><br></div><div>now : A -> Delay A</div><div>later : Delay' A -> Delay A</div><div>step : later = force</div><div><br></div><div>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><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">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>