    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The Cowriter type and some operations
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --sized-types #-}

    module Codata.Sized.Cowriter where

    open import Size using (Size; ∞)
    open import Level as L using (Level)
    open import Codata.Sized.Thunk using (Thunk; force)
    open import Codata.Sized.Conat using (Conat; zero; suc)
    open import Codata.Sized.Delay using (Delay; later; now)
    open import Codata.Sized.Stream as Stream using (Stream; _∷_)
    open import Data.Unit.Base using (⊤)
    open import Data.List.Base using (List; []; _∷_)
    open import Data.List.NonEmpty.Base using (List⁺; _∷_)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
    open import Data.Product.Base as Product using (_×_; _,_)
    open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
    open import Data.Vec.Base using (Vec; []; _∷_)
    open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)
    open import Function.Base using (_$_; _∘′_; id)

    private
      variable
        a b w x : Level
        A : Set a
        B : Set b
        W : Set w
        X : Set x

    ------------------------------------------------------------------------
    -- Definition

    data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
      [_] : A → Cowriter W A i
      _∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i

    infixr 5 _∷_

    ------------------------------------------------------------------------
    -- Relationship to Delay.

    fromDelay : ∀ {i} → Delay A i → Cowriter ⊤ A i
    fromDelay (now a)    = [ a ]
    fromDelay (later da) = _ ∷ λ where .force → fromDelay (da .force)

    toDelay : ∀ {i} → Cowriter W A i → Delay A i
    toDelay [ a ]    = now a
    toDelay (_ ∷ ca) = later λ where .force → toDelay (ca .force)

    ------------------------------------------------------------------------
    -- Basic functions.

    fromStream : ∀ {i} → Stream W i → Cowriter W A i
    fromStream (w ∷ ws) = w ∷ λ where .force → fromStream (ws .force)

    repeat : W → Cowriter W A ∞
    repeat = fromStream ∘′ Stream.repeat

    length : ∀ {i} → Cowriter W A i → Conat i
    length [ _ ]    = zero
    length (w ∷ cw) = suc λ where .force → length (cw .force)

    splitAt : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (Vec≤ W n × A)
    splitAt zero    cw       = inj₁ ([] , cw)
    splitAt (suc n) [ a ]    = inj₂ (Vec≤.[] , a)
    splitAt (suc n) (w ∷ cw) = Sum.map (Product.map₁ (w ∷_)) (Product.map₁ (w Vec≤.∷_))
                             $ splitAt n (cw .force)

    take : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (Vec≤ W n × A)
    take n = Sum.map₁ Product.proj₁ ∘′ splitAt n

    infixr 5 _++_ _⁺++_
    _++_ : ∀ {i} → List W → Cowriter W A i → Cowriter W A i
    []       ++ ca = ca
    (w ∷ ws) ++ ca = w ∷ λ where .force → ws ++ ca

    _⁺++_ : ∀ {i} → List⁺ W → Thunk (Cowriter W A) i → Cowriter W A i
    (w ∷ ws) ⁺++ ca = w ∷ λ where .force → ws ++ ca .force

    concat : ∀ {i} → Cowriter (List⁺ W) A i → Cowriter W A i
    concat [ a ]    = [ a ]
    concat (w ∷ ca) = w ⁺++ λ where .force → concat (ca .force)

    ------------------------------------------------------------------------
    -- Functor, Applicative and Monad

    map : ∀ {i} → (W → X) → (A → B) → Cowriter W A i → Cowriter X B i
    map f g [ a ]    = [ g a ]
    map f g (w ∷ cw) = f w ∷ λ where .force → map f g (cw .force)

    map₁ : ∀ {i} → (W → X) → Cowriter W A i → Cowriter X A i
    map₁ f = map f id

    map₂ : ∀ {i} → (A → X) → Cowriter W A i → Cowriter W X i
    map₂ = map id

    ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i
    ap [ f ]    ca = map₂ f ca
    ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca

    infixl 1 _>>=_

    _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
    [ a ]    >>= f = f a
    (w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f

    ------------------------------------------------------------------------
    -- Construction.

    unfold : ∀ {i} → (X → (W × X) ⊎ A) → X → Cowriter W A i
    unfold next seed =
      Sum.[ (λ where (w , seed′) → w ∷ λ where .force → unfold next seed′)
          , [_]
          ] (next seed)