{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Core
open import Algebra.Construct.NaturalChoice.Base
import Algebra.Construct.NaturalChoice.MinOp as MinOp
open import Function.Base using (flip)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.Bundles using (TotalPreorder)
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
renaming (totalPreorder to flipOrder)
module Algebra.Construct.NaturalChoice.MaxOp
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
where
open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
open MaxOperator maxOp
private
module Min = MinOp (MaxOp⇒MinOp maxOp)
open Min public
using ()
renaming
( ⊓-cong to ⊔-cong
; ⊓-congʳ to ⊔-congʳ
; ⊓-congˡ to ⊔-congˡ
; ⊓-idem to ⊔-idem
; ⊓-sel to ⊔-sel
; ⊓-assoc to ⊔-assoc
; ⊓-comm to ⊔-comm
; ⊓-identityˡ to ⊔-identityˡ
; ⊓-identityʳ to ⊔-identityʳ
; ⊓-identity to ⊔-identity
; ⊓-zeroˡ to ⊔-zeroˡ
; ⊓-zeroʳ to ⊔-zeroʳ
; ⊓-zero to ⊔-zero
; ⊓-isMagma to ⊔-isMagma
; ⊓-isSemigroup to ⊔-isSemigroup
; ⊓-isCommutativeSemigroup to ⊔-isCommutativeSemigroup
; ⊓-isBand to ⊔-isBand
; ⊓-isMonoid to ⊔-isMonoid
; ⊓-isSelectiveMagma to ⊔-isSelectiveMagma
; ⊓-magma to ⊔-magma
; ⊓-semigroup to ⊔-semigroup
; ⊓-commutativeSemigroup to ⊔-commutativeSemigroup
; ⊓-band to ⊔-band
; ⊓-monoid to ⊔-monoid
; ⊓-selectiveMagma to ⊔-selectiveMagma
; x⊓y≈y⇒y≤x to x⊔y≈y⇒x≤y
; x⊓y≈x⇒x≤y to x⊔y≈x⇒y≤x
; x⊓y≤x to x≤x⊔y
; x⊓y≤y to x≤y⊔x
; x≤y⇒x⊓z≤y to x≤y⇒x≤y⊔z
; x≤y⇒z⊓x≤y to x≤y⇒x≤z⊔y
; x≤y⊓z⇒x≤y to x⊔y≤z⇒x≤z
; x≤y⊓z⇒x≤z to x⊔y≤z⇒y≤z
; ⊓-glb to ⊔-lub
; ⊓-triangulate to ⊔-triangulate
; ⊓-mono-≤ to ⊔-mono-≤
; ⊓-monoˡ-≤ to ⊔-monoˡ-≤
; ⊓-monoʳ-≤ to ⊔-monoʳ-≤
)
mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≤_ →
∀ x y → f (x ⊔ y) ≈ f x ⊔ f y
mono-≤-distrib-⊔ cong pres = Min.mono-≤-distrib-⊓ cong pres