[Agda] Defining the Delay monad as a HIT in cubical agda

[Nils Anders Danielsson]

On 03/04/2019 00.57, Thorsten Altenkirch wrote:
> However, maybe one can define this coniductively instead of using
> functions to describe chains.

I'm wondering whether a definition along the lines of the following code
(perhaps with some truncation constructors added) would work:

   mutual

     -- The partiality monad.

     data Partial (A : Set a) (i : Size) : Set a where
       now          : A → Partial A i
       later        : Partial′ A i → Partial A i
       antisymmetry : ∀ {x y} →
                      [ i , i , i ] x ⊑ y → [ i , i , i ] y ⊑ x → x ≡ y

     record Partial′ (A : Set a) (i : Size) : Set a where
       coinductive
       field
         force : {j : Size< i} → Partial A j

     -- An ordering relation.

     infix 4 [_,_,_]_⊑_ [_,_,_]_⊑′_

     data [_,_,_]_⊑_ {A : Set a} (i j₁ j₂ : Size) :
                     Partial A j₁ → Partial A j₂ → Set a where
       now    : ∀ {x} → [ i , j₁ , j₂ ] now x ⊑ now x
       laterʳ : ∀ {x₁ x₂} →
                ({j₂′ : Size< j₂} →
                 [ i , j₁ , j₂′ ] x₁ ⊑ x₂ .Partial′.force) →
                [ i , j₁ , j₂ ] x₁ ⊑ later x₂
       laterˡ : ∀ {x₁ x₂} →
                ({j₁′ : Size< j₁} →
                 [ i , j₁′ , j₂ ] x₁ .Partial′.force ⊑′ x₂) →
                [ i , j₁ , j₂ ] later x₁ ⊑ x₂

     record [_,_,_]_⊑′_ {A : Set a} (i j₁ j₂ : Size)
                        (x₁ : Partial A j₁) (x₂ : Partial A j₂) :
                        Set a where
       coinductive
       field
         force : {j : Size< i} → [ j , j₁ , j₂ ] x₁ ⊑ x₂

However, I don't think I've ever managed to work productively with
relations like the one above, where the related values are not
necessarily fully defined (of size ∞).

-- 
/NAD