{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Construct.NaturalChoice.Base
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
open import Data.Product.Base using (_,_)
open import Function.Base using (id; _∘_; flip)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.Bundles using (TotalPreorder)
open import Relation.Binary.Consequences
module Algebra.Construct.NaturalChoice.MinMaxOp
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂}
(minOp : MinOperator O)
(maxOp : MaxOperator O)
where
open TotalPreorder O renaming
( Carrier to A
; _≲_ to _≤_
; ≲-resp-≈ to ≤-resp-≈
; ≲-respʳ-≈ to ≤-respʳ-≈
; ≲-respˡ-≈ to ≤-respˡ-≈
)
open MinOperator minOp
open MaxOperator maxOp
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Algebra.Consequences.Setoid Eq.setoid
open import Relation.Binary.Reasoning.Preorder preorder
open import Algebra.Construct.NaturalChoice.MinOp minOp public
open import Algebra.Construct.NaturalChoice.MaxOp maxOp public
⊓-distribˡ-⊔ : _⊓_ DistributesOverˡ _⊔_
⊓-distribˡ-⊔ x y z with total y z
... | inj₁ y≤z = begin-equality
x ⊓ (y ⊔ z) ≈⟨ ⊓-congˡ x (x≤y⇒x⊔y≈y y≤z) ⟩
x ⊓ z ≈⟨ x≤y⇒x⊔y≈y (⊓-monoʳ-≤ x y≤z) ⟨
(x ⊓ y) ⊔ (x ⊓ z) ∎
... | inj₂ y≥z = begin-equality
x ⊓ (y ⊔ z) ≈⟨ ⊓-congˡ x (x≥y⇒x⊔y≈x y≥z) ⟩
x ⊓ y ≈⟨ x≥y⇒x⊔y≈x (⊓-monoʳ-≤ x y≥z) ⟨
(x ⊓ y) ⊔ (x ⊓ z) ∎
⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_
⊓-distribʳ-⊔ = comm+distrˡ⇒distrʳ ⊔-cong ⊓-comm ⊓-distribˡ-⊔
⊓-distrib-⊔ : _⊓_ DistributesOver _⊔_
⊓-distrib-⊔ = ⊓-distribˡ-⊔ , ⊓-distribʳ-⊔
⊔-distribˡ-⊓ : _⊔_ DistributesOverˡ _⊓_
⊔-distribˡ-⊓ x y z with total y z
... | inj₁ y≤z = begin-equality
x ⊔ (y ⊓ z) ≈⟨ ⊔-congˡ x (x≤y⇒x⊓y≈x y≤z) ⟩
x ⊔ y ≈⟨ x≤y⇒x⊓y≈x (⊔-monoʳ-≤ x y≤z) ⟨
(x ⊔ y) ⊓ (x ⊔ z) ∎
... | inj₂ y≥z = begin-equality
x ⊔ (y ⊓ z) ≈⟨ ⊔-congˡ x (x≥y⇒x⊓y≈y y≥z) ⟩
x ⊔ z ≈⟨ x≥y⇒x⊓y≈y (⊔-monoʳ-≤ x y≥z) ⟨
(x ⊔ y) ⊓ (x ⊔ z) ∎
⊔-distribʳ-⊓ : _⊔_ DistributesOverʳ _⊓_
⊔-distribʳ-⊓ = comm+distrˡ⇒distrʳ ⊓-cong ⊔-comm ⊔-distribˡ-⊓
⊔-distrib-⊓ : _⊔_ DistributesOver _⊓_
⊔-distrib-⊓ = ⊔-distribˡ-⊓ , ⊔-distribʳ-⊓
⊓-absorbs-⊔ : _⊓_ Absorbs _⊔_
⊓-absorbs-⊔ x y with total x y
... | inj₁ x≤y = begin-equality
x ⊓ (x ⊔ y) ≈⟨ ⊓-congˡ x (x≤y⇒x⊔y≈y x≤y) ⟩
x ⊓ y ≈⟨ x≤y⇒x⊓y≈x x≤y ⟩
x ∎
... | inj₂ y≤x = begin-equality
x ⊓ (x ⊔ y) ≈⟨ ⊓-congˡ x (x≥y⇒x⊔y≈x y≤x) ⟩
x ⊓ x ≈⟨ ⊓-idem x ⟩
x ∎
⊔-absorbs-⊓ : _⊔_ Absorbs _⊓_
⊔-absorbs-⊓ x y with total x y
... | inj₁ x≤y = begin-equality
x ⊔ (x ⊓ y) ≈⟨ ⊔-congˡ x (x≤y⇒x⊓y≈x x≤y) ⟩
x ⊔ x ≈⟨ ⊔-idem x ⟩
x ∎
... | inj₂ y≤x = begin-equality
x ⊔ (x ⊓ y) ≈⟨ ⊔-congˡ x (x≥y⇒x⊓y≈y y≤x) ⟩
x ⊔ y ≈⟨ x≥y⇒x⊔y≈x y≤x ⟩
x ∎
⊔-⊓-absorptive : Absorptive _⊔_ _⊓_
⊔-⊓-absorptive = ⊔-absorbs-⊓ , ⊓-absorbs-⊔
⊓-⊔-absorptive : Absorptive _⊓_ _⊔_
⊓-⊔-absorptive = ⊓-absorbs-⊔ , ⊔-absorbs-⊓
private _≥_ = flip _≤_
antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≥_ →
∀ x y → f (x ⊓ y) ≈ f x ⊔ f y
antimono-≤-distrib-⊓ {f} cong antimono x y with total x y
... | inj₁ x≤y = begin-equality
f (x ⊓ y) ≈⟨ cong (x≤y⇒x⊓y≈x x≤y) ⟩
f x ≈⟨ x≥y⇒x⊔y≈x (antimono x≤y) ⟨
f x ⊔ f y ∎
... | inj₂ y≤x = begin-equality
f (x ⊓ y) ≈⟨ cong (x≥y⇒x⊓y≈y y≤x) ⟩
f y ≈⟨ x≤y⇒x⊔y≈y (antimono y≤x) ⟨
f x ⊔ f y ∎
antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≥_ →
∀ x y → f (x ⊔ y) ≈ f x ⊓ f y
antimono-≤-distrib-⊔ {f} cong antimono x y with total x y
... | inj₁ x≤y = begin-equality
f (x ⊔ y) ≈⟨ cong (x≤y⇒x⊔y≈y x≤y) ⟩
f y ≈⟨ x≥y⇒x⊓y≈y (antimono x≤y) ⟨
f x ⊓ f y ∎
... | inj₂ y≤x = begin-equality
f (x ⊔ y) ≈⟨ cong (x≥y⇒x⊔y≈x y≤x) ⟩
f x ≈⟨ x≤y⇒x⊓y≈x (antimono y≤x) ⟨
f x ⊓ f y ∎
x⊓y≤x⊔y : ∀ x y → x ⊓ y ≤ x ⊔ y
x⊓y≤x⊔y x y = begin
x ⊓ y ∼⟨ x⊓y≤x x y ⟩
x ∼⟨ x≤x⊔y x y ⟩
x ⊔ y ∎