    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Lists defined in terms of the reflexive-transitive closure, Star
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Star.List where

    open import Data.Star.Nat using (ℕ; _+_; zero)
    open import Data.Unit.Base using (tt)
    open import Relation.Binary.Construct.Always using (Always)
    open import Relation.Binary.Construct.Constant using (Const)
    open import Relation.Binary.Construct.Closure.ReflexiveTransitive
      using (Star; ε; _◅_; fold)

    -- Lists.

    List : ∀ {a} → Set a → Set a
    List A = Star (Const A) tt tt

    -- Nil and cons.

    [] : ∀ {a} {A : Set a} → List A
    [] = ε

    infixr 5 _∷_

    _∷_ : ∀ {a} {A : Set a} → A → List A → List A
    _∷_ = _◅_

    -- The sum of the elements in a list containing natural numbers.

    sum : List ℕ → ℕ
    sum = fold (Star Always) _+_ zero