------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic lattice structures
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Morphism
open import Algebra.Lattice.Bundles
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
open import Function.Definitions
open import Relation.Binary.Morphism.Structures
open import Relation.Binary.Core
 
module Algebra.Lattice.Morphism.Structures where
 
private
  variable
    a b ℓ₁ ℓ₂ : Level
 
------------------------------------------------------------------------
-- Morphisms over lattice-like structures
------------------------------------------------------------------------
 
module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂) where
 
  open RawLattice L₁ renaming
    ( Carrier to A; _≈_ to _≈₁_
    ; _∧_ to _∧₁_; _∨_ to _∨₁_
    ; ∧-rawMagma to ∧-rawMagma₁
    ; ∨-rawMagma to ∨-rawMagma₁)
 
  open RawLattice L₂ renaming
    ( Carrier to B; _≈_ to _≈₂_
    ; _∧_ to _∧₂_; _∨_ to _∨₂_
    ; ∧-rawMagma to ∧-rawMagma₂
    ; ∨-rawMagma to ∨-rawMagma₂)
 
  module ∨ = MagmaMorphisms ∨-rawMagma₁ ∨-rawMagma₂
  module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂
 
  open MorphismDefinitions A B _≈₂_
 
 
  record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
      ∧-homo            : Homomorphic₂ ⟦_⟧ _∧₁_ _∧₂_
      ∨-homo            : Homomorphic₂ ⟦_⟧ _∨₁_ _∨₂_
 
    open IsRelHomomorphism isRelHomomorphism public
      renaming (cong to ⟦⟧-cong)
 
    ∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧
    ∧-isMagmaHomomorphism = record
      { isRelHomomorphism = isRelHomomorphism
      ; homo = ∧-homo
      }
 
    ∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧
    ∨-isMagmaHomomorphism = record
      { isRelHomomorphism = isRelHomomorphism
      ; homo = ∨-homo
      }
 
  record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧
      injective             : Injective _≈₁_ _≈₂_ ⟦_⟧
 
    open IsLatticeHomomorphism isLatticeHomomorphism public
 
    ∨-isMagmaMonomorphism : ∨.IsMagmaMonomorphism ⟦_⟧
    ∨-isMagmaMonomorphism = record
      { isMagmaHomomorphism = ∨-isMagmaHomomorphism
      ; injective           = injective
      }
 
    ∧-isMagmaMonomorphism : ∧.IsMagmaMonomorphism ⟦_⟧
    ∧-isMagmaMonomorphism = record
      { isMagmaHomomorphism = ∧-isMagmaHomomorphism
      ; injective           = injective
      }
 
    open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public
      using (isRelMonomorphism)
 
 
  record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧
      surjective            : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
    open IsLatticeMonomorphism isLatticeMonomorphism public
 
    ∨-isMagmaIsomorphism : ∨.IsMagmaIsomorphism ⟦_⟧
    ∨-isMagmaIsomorphism = record
      { isMagmaMonomorphism = ∨-isMagmaMonomorphism
      ; surjective          = surjective
      }
 
    ∧-isMagmaIsomorphism : ∧.IsMagmaIsomorphism ⟦_⟧
    ∧-isMagmaIsomorphism = record
      { isMagmaMonomorphism = ∧-isMagmaMonomorphism
      ; surjective          = surjective
      }
 
    open ∧.IsMagmaIsomorphism ∧-isMagmaIsomorphism public
      using (isRelIsomorphism)
 
------------------------------------------------------------------------
-- Re-export contents of modules publicly
 
open LatticeMorphisms public