open import Equivalence

module Homomorphism {a b} (A : Set a) (B : Set b)
    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
    (≈₂-equiv : IsEquivalence B _≈₂_)
    (f : A → B) where

open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Surjective)
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Data.Product using (_,_)
open import Lattice

open IsEquivalence ≈₂-equiv using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; ≈-refl to ≈₂-refl)
open import Relation.Binary.Reasoning.Base.Single _≈₂_ ≈₂-refl ≈₂-trans

infixl 20 _∙₂_
_∙₂_ = ≈₂-trans

record SemilatticeHomomorphism (_⊔₁_ : A → A → A)
                               (_⊔₂_ : B → B → B) : Set (a ⊔ℓ b) where
    field
        f-preserves-≈ : f Preserves _≈₁_ ⟶  _≈₂_
        f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))

module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
         (sh : SemilatticeHomomorphism _⊔₁_ _⊔₂_)
         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
         (surF : Surjective _≈₁_ _≈₂_ f) where

    open SemilatticeHomomorphism sh

    transportSemilattice : IsSemilattice A _≈₁_ _⊔₁_ → IsSemilattice B _≈₂_ _⊔₂_
    transportSemilattice sA = record
        { ≈-equiv = ≈₂-equiv
        ; ≈-⊔-cong = ≈₂-⊔₂-cong
        ; ⊔-assoc = λ b₁ b₂ b₃ →
            let (a₁ , fa₁≈b₁) = surF b₁
                (a₂ , fa₂≈b₂) = surF b₂
                (a₃ , fa₃≈b₃) = surF b₃
            in
               begin
                   (b₁ ⊔₂ b₂) ⊔₂ b₃
               ∼⟨ ≈₂-⊔₂-cong (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) (≈₂-sym fa₃≈b₃) ⟩
                   (f a₁ ⊔₂ f a₂) ⊔₂ f a₃
               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym (f-⊔-distr a₁ a₂)) ≈₂-refl ⟩
                   f (a₁ ⊔₁ a₂) ⊔₂ f a₃
               ∼⟨ ≈₂-sym (f-⊔-distr (a₁ ⊔₁ a₂) a₃) ⟩
                   f ((a₁ ⊔₁ a₂) ⊔₁ a₃)
               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-assoc sA a₁ a₂ a₃) ⟩
                   f (a₁ ⊔₁ (a₂ ⊔₁ a₃))
               ∼⟨ f-⊔-distr a₁ (a₂ ⊔₁ a₃) ⟩
                   f a₁ ⊔₂ f (a₂ ⊔₁ a₃)
               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (f-⊔-distr a₂ a₃) ⟩
                   f a₁ ⊔₂ (f a₂ ⊔₂ f a₃)
               ∼⟨ ≈₂-⊔₂-cong fa₁≈b₁ (≈₂-⊔₂-cong fa₂≈b₂ fa₃≈b₃) ⟩
                   b₁ ⊔₂ (b₂ ⊔₂ b₃)
               ∎
        ; ⊔-comm = λ b₁ b₂ →
            let (a₁ , fa₁≈b₁) = surF b₁
                (a₂ , fa₂≈b₂) = surF b₂
            in
               begin
                   b₁ ⊔₂ b₂
               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂) ⟩
                   f a₁ ⊔₂ f a₂
               ∼⟨ ≈₂-sym (f-⊔-distr a₁ a₂) ⟩
                   f (a₁ ⊔₁ a₂)
               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-comm sA a₁ a₂) ⟩
                   f (a₂ ⊔₁ a₁)
               ∼⟨ f-⊔-distr a₂ a₁ ⟩
                   f a₂ ⊔₂ f a₁
               ∼⟨ ≈₂-⊔₂-cong fa₂≈b₂ fa₁≈b₁ ⟩
                   b₂ ⊔₂ b₁
               ∎
        ; ⊔-idemp = λ b →
            let (a , fa≈b) = surF b
            in
               begin
                   b ⊔₂ b
               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa≈b) (≈₂-sym fa≈b) ⟩
                   f a ⊔₂ f a
               ∼⟨ ≈₂-sym (f-⊔-distr a a) ⟩
                   f (a ⊔₁ a)
               ∼⟨ f-preserves-≈ (IsSemilattice.⊔-idemp sA a) ⟩
                   f a
               ∼⟨ fa≈b ⟩
                   b
               ∎
        }


record LatticeHomomorphism (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
                           (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) : Set (a ⊔ℓ b) where
    field
        ⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
        ⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_

    open SemilatticeHomomorphism ⊔-homomorphism using (f-⊔-distr; f-preserves-≈) public
    open SemilatticeHomomorphism ⊓-homomorphism using () renaming (f-⊔-distr to f-⊓-distr) public

module _ (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
         (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
         (lh : LatticeHomomorphism _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_)
         (≈₂-⊔₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
         (≈₂-⊓₂-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈₂ a₂ → a₃ ≈₂ a₄ → (a₁ ⊓₂ a₃) ≈₂ (a₂ ⊓₂ a₄))
         (surF : Surjective _≈₁_ _≈₂_ f) where

    open LatticeHomomorphism lh

    transportLattice : IsLattice A _≈₁_ _⊔₁_ _⊓₁_ → IsLattice B _≈₂_ _⊔₂_ _⊓₂_
    transportLattice lA = record
        { joinSemilattice = transportSemilattice _⊔₁_ _⊔₂_ (LatticeHomomorphism.⊔-homomorphism lh) ≈₂-⊔₂-cong surF (IsLattice.joinSemilattice lA)
        ; meetSemilattice = transportSemilattice _⊓₁_ _⊓₂_ (LatticeHomomorphism.⊓-homomorphism lh) ≈₂-⊓₂-cong surF (IsLattice.meetSemilattice lA)
        ; absorb-⊔-⊓ = λ b₁ b₂ →
            let (a₁ , fa₁≈b₁) = surF b₁
                (a₂ , fa₂≈b₂) = surF b₂
            in
               begin
                   b₁ ⊔₂ (b₁ ⊓₂ b₂)
               ∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
                   f a₁ ⊔₂ (f a₁ ⊓₂ f a₂)
               ∼⟨ ≈₂-⊔₂-cong ≈₂-refl (≈₂-sym (f-⊓-distr a₁ a₂)) ⟩
                   f a₁ ⊔₂ f (a₁ ⊓₁ a₂)
               ∼⟨ ≈₂-sym (f-⊔-distr a₁ (a₁ ⊓₁ a₂)) ⟩
                   f (a₁ ⊔₁ (a₁ ⊓₁ a₂))
               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊔-⊓ lA a₁ a₂) ⟩
                   f a₁
               ∼⟨ fa₁≈b₁ ⟩
                   b₁
               ∎
        ; absorb-⊓-⊔ = λ b₁ b₂ →
            let (a₁ , fa₁≈b₁) = surF b₁
                (a₂ , fa₂≈b₂) = surF b₂
            in
               begin
                   b₁ ⊓₂ (b₁ ⊔₂ b₂)
               ∼⟨ ≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) ⟩
                   f a₁ ⊓₂ (f a₁ ⊔₂ f a₂)
               ∼⟨ ≈₂-⊓₂-cong ≈₂-refl (≈₂-sym (f-⊔-distr a₁ a₂)) ⟩
                   f a₁ ⊓₂ f (a₁ ⊔₁ a₂)
               ∼⟨ ≈₂-sym (f-⊓-distr a₁ (a₁ ⊔₁ a₂)) ⟩
                   f (a₁ ⊓₁ (a₁ ⊔₁ a₂))
               ∼⟨ f-preserves-≈ (IsLattice.absorb-⊓-⊔ lA a₁ a₂) ⟩
                   f a₁
               ∼⟨ fa₁≈b₁ ⟩
                   b₁
               ∎
        }