------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definition of an operator that computes the min/max value
-- with respect to a total preorder.
------------------------------------------------------------------------
{-#
OPTIONS
--cubical-compatible
--safe
#-}
open
import
Algebra.Core
using
(
Op₂
)
open
import
Level
as
L
hiding
(
_⊔_
)
open
import
Function.Base
using
(
flip
)
open
import
Relation.Binary.Bundles
using
(
TotalPreorder
)
open
import
Relation.Binary.Construct.Flip.EqAndOrd
using
()
renaming
(
totalPreorder
to
flipOrder
)
import
Relation.Binary.Properties.TotalOrder
as
TotalOrderProperties
module
Algebra.Construct.NaturalChoice.Base
where
private
variable
a
ℓ₁
ℓ₂
:
Level
O
:
TotalPreorder
a
ℓ₁
ℓ₂
------------------------------------------------------------------------
-- Definition
module
_
(
O
:
TotalPreorder
a
ℓ₁
ℓ₂
)
where
open
TotalPreorder
O
renaming
(
_≲_
to
_≤_
)
private
_≥_
=
flip
_≤_
record
MinOperator
:
Set
(
a
L.⊔
ℓ₁
L.⊔
ℓ₂
)
where
infixl
7
_⊓_
field
_⊓_
:
Op₂
Carrier
x≤y⇒x⊓y≈x
:
∀
{
x
y
}
→
x
≤
y
→
x
⊓
y
≈
x
x≥y⇒x⊓y≈y
:
∀
{
x
y
}
→
x
≥
y
→
x
⊓
y
≈
y
record
MaxOperator
:
Set
(
a
L.⊔
ℓ₁
L.⊔
ℓ₂
)
where
infixl
6
_⊔_
field
_⊔_
:
Op₂
Carrier
x≤y⇒x⊔y≈y
:
∀
{
x
y
}
→
x
≤
y
→
x
⊔
y
≈
y
x≥y⇒x⊔y≈x
:
∀
{
x
y
}
→
x
≥
y
→
x
⊔
y
≈
x
------------------------------------------------------------------------
-- Properties
MinOp⇒MaxOp
:
MinOperator
O
→
MaxOperator
(
flipOrder
O
)
MinOp⇒MaxOp
minOp
=
record
{
_⊔_
=
_⊓_
;
x≤y⇒x⊔y≈y
=
x≥y⇒x⊓y≈y
;
x≥y⇒x⊔y≈x
=
x≤y⇒x⊓y≈x
}
where
open
MinOperator
minOp
MaxOp⇒MinOp
:
MaxOperator
O
→
MinOperator
(
flipOrder
O
)
MaxOp⇒MinOp
maxOp
=
record
{
_⊓_
=
_⊔_
;
x≤y⇒x⊓y≈x
=
x≥y⇒x⊔y≈x
;
x≥y⇒x⊓y≈y
=
x≤y⇒x⊔y≈y
}
where
open
MaxOperator
maxOp