------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between lattice-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra
open import Algebra.Lattice
open import Algebra.Lattice.Morphism.Structures
import Algebra.Consequences.Setoid as Consequences
import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
import Algebra.Lattice.Properties.Lattice as LatticeProperties
open import Data.Product.Base using (_,_; map)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

module Algebra.Lattice.Morphism.LatticeMonomorphism
  {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
  (isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
  where

open IsLatticeMonomorphism isLatticeMonomorphism
open RawLattice L₁ renaming (_≈_ to _≈₁_; _∨_ to _∨_; _∧_ to _∧_)
open RawLattice L₂ renaming (_≈_ to _≈₂_; _∨_ to _⊔_; _∧_ to _⊓_)

------------------------------------------------------------------------
-- Re-export all properties of magma monomorphisms

open MagmaMonomorphisms ∨-isMagmaMonomorphism public
  using () renaming
  ( cong    to ∨-cong
  ; assoc   to ∨-assoc
  ; comm    to ∨-comm
  ; idem    to ∨-idem
  ; sel     to ∨-sel
  ; cancelˡ to ∨-cancelˡ
  ; cancelʳ to ∨-cancelʳ
  ; cancel  to ∨-cancel
  )

open MagmaMonomorphisms ∧-isMagmaMonomorphism public
  using () renaming
  ( cong    to ∧-cong
  ; assoc   to ∧-assoc
  ; comm    to ∧-comm
  ; idem    to ∧-idem
  ; sel     to ∧-sel
  ; cancelˡ to ∧-cancelˡ
  ; cancelʳ to ∧-cancelʳ
  ; cancel  to ∧-cancel
  )

------------------------------------------------------------------------
-- Lattice-specific properties

module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where

  open IsLattice ⊔-⊓-isLattice using (isEquivalence) renaming
    ( ∨-congˡ     to ⊔-congˡ
    ; ∨-congʳ     to ⊔-congʳ
    ; ∧-cong      to ⊓-cong
    ; ∧-congˡ     to ⊓-congˡ
    ; ∨-absorbs-∧ to ⊔-absorbs-⊓
    ; ∧-absorbs-∨ to ⊓-absorbs-⊔
    )

  setoid : Setoid b ℓ₂
  setoid = record { isEquivalence = isEquivalence }

  open ≈-Reasoning setoid

  ∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_
  ∨-absorbs-∧ x y = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2543}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{2545}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2547}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{2549}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2516}{\htmlId{2551}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$                        ≈⟨ ∨-homo x (x ∧ y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2606}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2614}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{2616}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2516}{\htmlId{2618}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$                    ≈⟨ ⊔-congˡ (∧-homo x y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2673}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2681}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2516}{\htmlId{2689}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$                ≈⟨ ⊔-absorbs-⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2725}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2516}{\htmlId{2731}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2514}{\htmlId{2743}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                                ∎)

  ∧-absorbs-∨ : _Absorbs_ _≈₁_ _∧_ _∨_
  ∧-absorbs-∨ x y = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{2864}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{2866}{\htmlClass{Function Operator}{\text{∧}}}}\, (\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{2869}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{2871}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2837}{\htmlId{2873}{\htmlClass{Bound}{\text{y}}}}\,) \end{pmatrix}$                      ≈⟨ ∧-homo x (x ∨ y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{2927}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{2935}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{2937}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2837}{\htmlId{2939}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$                    ≈⟨ ⊓-congˡ (∨-homo x y) ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{2994}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ ($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{3003}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2837}{\htmlId{3011}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$)              ≈⟨ ⊓-absorbs-⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{3046}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2837}{\htmlId{3052}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2835}{\htmlId{3064}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                                ∎)

  absorptive : Absorptive _≈₁_ _∨_ _∧_
  absorptive = ∨-absorbs-∧ , ∧-absorbs-∨

  distribʳ : _DistributesOverʳ_ _≈₂_ _⊔_ _⊓_ → _DistributesOverʳ_ _≈₁_ _∨_ _∧_
  distribʳ distribʳ x y z = injective (begin
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3314}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{3316}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3318}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{3320}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3322}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                        ≈⟨ ∨-homo (y ∧ z) x ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3377}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{3379}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3381}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3389}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                    ≈⟨ ⊔-congʳ (∧-homo y z) ⟩
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3444}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3452}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3460}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                ≈⟨ distribʳ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3493}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3499}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3505}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
    ($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3518}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3526}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$) ⊓ ($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3536}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3544}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$)    ≈⟨ ⊓-cong (∨-homo y x) (∨-homo z x) ⟨
    $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3596}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{3598}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3600}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3608}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{3610}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3612}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$                ≈⟨ ∧-homo (y ∨ x) (z ∨ x) ⟨
    $\begin{pmatrix} (\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3285}{\htmlId{3666}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{3668}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3670}{\htmlClass{Bound}{\text{x}}}}\,) \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1225}{\htmlId{3673}{\htmlClass{Function Operator}{\text{∧}}}}\, (\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3287}{\htmlId{3676}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1213}{\htmlId{3678}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3283}{\htmlId{3680}{\htmlClass{Bound}{\text{x}}}}\,) \end{pmatrix}$                ∎)

isLattice : IsLattice _≈₂_ _⊔_ _⊓_ → IsLattice _≈₁_ _∨_ _∧_
isLattice isLattice = record
  { isEquivalence = RelMonomorphisms.isEquivalence isRelMonomorphism L.isEquivalence
  ; ∨-comm        = ∨-comm  LP.∨-isMagma L.∨-comm
  ; ∨-assoc       = ∨-assoc LP.∨-isMagma L.∨-assoc
  ; ∨-cong        = ∨-cong  LP.∨-isMagma
  ; ∧-comm        = ∧-comm  LP.∧-isMagma L.∧-comm
  ; ∧-assoc       = ∧-assoc LP.∧-isMagma L.∧-assoc
  ; ∧-cong        = ∧-cong  LP.∧-isMagma
  ; absorptive    = absorptive isLattice
  } where
    module L  = IsLattice isLattice
    module LP = LatticeProperties (record { isLattice = isLattice })

isDistributiveLattice : IsDistributiveLattice _≈₂_ _⊔_ _⊓_ →
                        IsDistributiveLattice _≈₁_ _∨_ _∧_
isDistributiveLattice isDL = isDistributiveLatticeʳʲᵐ (record
  { isLattice     = isLattice L.isLattice
  ; ∨-distribʳ-∧  = distribʳ  L.isLattice L.∨-distribʳ-∧
  }) where module L = IsDistributiveLattice isDL