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