<div dir="ltr"><div>Well, if `never` is equal to `now x`, then by transitivity `now x` is equal to `now y` for any `x` and `y`, which would mean I found a very complicated way to define the constant unit type :P</div><div><br></div><div>About terminology: Nisse informed me that `Delay` is used for the (non-truncated) coinductive type with two constructors `now` and `later`, while the properly truncated variant where `later^n x` = `now x` for any finite `n` is called the partiality monad. So my question is actually whether the partiality monad is definable as a higher coinductive type with two point constructors `now` and `later` plus some path constructor(s).</div><div><br></div><div>The problem with defining such a higher coinductive type `D` is that all attempts at proving two of its elements are *not* equal seem to fail:</div><div><br></div><div>- Pattern matching on an equality between two constructors with an absurd pattern () obviously doesn't work for higher inductive types.</div><div></div><div>- Defining a function `f : D -> Bool` or `D -> Set` which distinguishes the two elements doesn't work either because both `Bool` and `Set` are inductively defined, so `f` can only depend on a finite prefix of its input (i.e. f must be continuous).</div><div></div><div>- Defining an indexed datatype `data P : D -> Set` that is empty at one index but not at another seems to work, but then we get into trouble when we actually want to prove that it is empty for that particular index (this is not really surprising because indexed datatypes can be explained with normal datatypes + the equality type, so this is essentially the same as the first option).</div><div><br></div><div>This exhausts my bag of tricks when it comes to proving two constructor forms are not equal. This seems to be an essential problem that would pop up any time one tries to mix coinduction with higher constructors. It would be an interesting research topic to try and define a suitable notion of "higher coinductive type" which does not have this problem.<br></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 10: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<br>
    <br>
    <br>
    <div class="gmail-m_-2314557868947509404moz-cite-prefix">On 02/04/19 15:08, Jesper Cockx wrote:<br>
    </div>
    <blockquote type="cite">
      <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" target="_blank">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_-2314557868947509404gmail-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_-2314557868947509404gmail-m_5865528187534997207mimeAttachmentHeader"></fieldset>
              <br>
              <pre>_______________________________________________
Agda mailing list
<a class="gmail-m_-2314557868947509404gmail-m_5865528187534997207moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="gmail-m_-2314557868947509404gmail-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>
    </blockquote>
    <br>
  </div>

</blockquote></div>