<div dir="ltr"><div>Hi Nicolai,</div><div><br></div><div>Yes, Christian and I suspected the same thing (that this definition of the delay monad is actually a unit type), but I haven't managed to prove that either because of some mysterious termination checker problem.</div><div><br></div><div>I'm currently trying a different approach where I define the Delay type mutually with the ⇓ type so I can quotient by the relation "normalize to the same value in a finite number of steps". I'll let you know later if it works.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at 3:15 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">
    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="gmail-m_5865528187534997207moz-cite-prefix">On 29/03/19 18:40, Jesper Cockx wrote:<br>
    </div>
    <blockquote type="cite">
      <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" target="_blank">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="gmail-m_5865528187534997207mimeAttachmentHeader"></fieldset>
      <br>
      <pre>_______________________________________________
Agda mailing list
<a class="gmail-m_5865528187534997207moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="gmail-m_5865528187534997207moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>