------------------------------------------------------------------------
-- The Agda standard library
--
-- Order morphisms
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Core using (Rel)
 
module Relation.Binary.Morphism.Structures
  {a b} {A : Set a} {B : Set b}
  where
 
open import Data.Product.Base using (_,_)
open import Function.Definitions
open import Level using (Level; _⊔_)
open import Relation.Binary.Morphism.Definitions A B
 
private
  variable
    ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
 
------------------------------------------------------------------------
-- Relations
------------------------------------------------------------------------
 
record IsRelHomomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                         (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    cong : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧
 
 
record IsRelMonomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                         (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isHomomorphism : IsRelHomomorphism _∼₁_ _∼₂_ ⟦_⟧
    injective      : Injective _∼₁_ _∼₂_ ⟦_⟧
 
  open IsRelHomomorphism isHomomorphism public
 
 
record IsRelIsomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                        (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧
    surjective     : Surjective _∼₁_ _∼₂_ ⟦_⟧
 
  open IsRelMonomorphism isMonomorphism public
 
  bijective : Bijective _∼₁_ _∼₂_ ⟦_⟧
  bijective = injective , surjective
 
 
------------------------------------------------------------------------
-- Orders
------------------------------------------------------------------------
 
record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                           (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                           (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                           where
  field
    cong  : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧
    mono  : Homomorphic₂ _≲₁_ _≲₂_ ⟦_⟧
 
  module Eq where
    isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelHomomorphism = record { cong = cong }
 
  isRelHomomorphism : IsRelHomomorphism _≲₁_ _≲₂_ ⟦_⟧
  isRelHomomorphism = record { cong = mono }
 
 
record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                           (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                           (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                           where
  field
    isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧
    injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
    cancel              : Injective _≲₁_ _≲₂_ ⟦_⟧
 
  open IsOrderHomomorphism isOrderHomomorphism public
    hiding (module Eq)
 
  module Eq where
    isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelMonomorphism = record
      { isHomomorphism = IsOrderHomomorphism.Eq.isRelHomomorphism isOrderHomomorphism
      ; injective      = injective
      }
 
  isRelMonomorphism : IsRelMonomorphism _≲₁_ _≲₂_ ⟦_⟧
  isRelMonomorphism = record
    { isHomomorphism = isRelHomomorphism
    ; injective      = cancel
    }
 
 
record IsOrderIsomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                          (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                          (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                          where
  field
    isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧
    surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
  open IsOrderMonomorphism isOrderMonomorphism public
    hiding (module Eq)
 
  module Eq where
    isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelIsomorphism = record
      { isMonomorphism = IsOrderMonomorphism.Eq.isRelMonomorphism isOrderMonomorphism
      ; surjective     = surjective
      }