<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" 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="moz-cite-prefix">On 29/03/19 18:40, Jesper Cockx wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAEm=boy4k5FDBbxcqUWH-nP-H78YY-R2p9oW_cn7q_u3kEKAcw@mail.gmail.com">
      <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"
                moz-do-not-send="true">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="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>