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

[Nils Anders Danielsson]

On 11/04/2019 18.17, Jesper Cockx wrote:
>    norm  : {d : Delay′ A i} {j : Size< i}
>          → Delay↘ A j i (d .force) x → later d ≡ now x

Is there a reason for including a later constructor here? Is this to
avoid extra proofs of now x ≡ now x?

> data Delay↘ A i i′ where
>    now↘   : ∀ x → Delay↘ A i i′ (now x) x
>    later↘ : {d : Delay′ A i} {j : Size< i}
>           → Delay↘ A j i′ (d .force) x → Delay↘ A i i′ (later d) x

I suppose that the second size could be omitted.

-- 
/NAD