    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Type constructors giving rise to a semigroup at every type
    -- e.g. (List, _++_)
    ------------------------------------------------------------------------

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

    module Effect.Choice where

    open import Level

    private
      variable
        ℓ ℓ′ : Level
        A  : Set ℓ

    record RawChoice (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
      infixr 3 _<|>_ _∣_
      field
        _<|>_ : F A → F A → F A

      -- backwards compatibility: unicode variants
      _∣_ : F A → F A → F A
      _∣_ = _<|>_