------------------------------------------------------------------------
-- 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
_∣_
=
_<|>_