------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for morphisms between binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Morphism.Bundles where

open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
open import Relation.Binary.Morphism.Structures
  using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism
        ; IsOrderHomomorphism; IsOrderMonomorphism; IsOrderIsomorphism)
open import Relation.Binary.Consequences using (mono⇒cong)

private
  variable
    ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level

------------------------------------------------------------------------
-- Setoids
------------------------------------------------------------------------

module _ (S₁ : Setoid ℓ₁ ℓ₂) (S₂ : Setoid ℓ₃ ℓ₄) where

  record SetoidHomomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    open Setoid
    field
      ⟦_⟧               : Carrier S₁ → Carrier S₂
      isRelHomomorphism : IsRelHomomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧

    open IsRelHomomorphism isRelHomomorphism public


  record SetoidMonomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    open Setoid
    field
      ⟦_⟧               : Carrier S₁ → Carrier S₂
      isRelMonomorphism : IsRelMonomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧

    open IsRelMonomorphism isRelMonomorphism public

    homomorphism : SetoidHomomorphism
    homomorphism = record { isRelHomomorphism = isHomomorphism }


  record SetoidIsomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
    open Setoid
    field
      ⟦_⟧              : Carrier S₁ → Carrier S₂
      isRelIsomorphism : IsRelIsomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧

    open IsRelIsomorphism isRelIsomorphism public

    monomorphism : SetoidMonomorphism
    monomorphism = record { isRelMonomorphism = isMonomorphism }

    open SetoidMonomorphism monomorphism public
      using (homomorphism)


------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record PreorderHomomorphism (S₁ : Preorder ℓ₁ ℓ₂ ℓ₃)
                            (S₂ : Preorder ℓ₄ ℓ₅ ℓ₆)
                            : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ ℓ₅ ⊔ ℓ₆) where
  open Preorder
  field
    ⟦_⟧                 : Carrier S₁ → Carrier S₂
    isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_≲_ S₁) (_≲_ S₂) ⟦_⟧

  open IsOrderHomomorphism isOrderHomomorphism public

------------------------------------------------------------------------
-- Posets
------------------------------------------------------------------------

module _ (P : Poset ℓ₁ ℓ₂ ℓ₃) (Q : Poset ℓ₄ ℓ₅ ℓ₆) where

  private
    module P = Poset P
    module Q = Poset Q

  record PosetHomomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ ℓ₅ ⊔ ℓ₆) where
    field
      ⟦_⟧                 : P.Carrier → Q.Carrier
      isOrderHomomorphism : IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ ⟦_⟧

    open IsOrderHomomorphism isOrderHomomorphism public


  -- Smart constructor that automatically constructs the congruence
  -- proof from the monotonicity proof
  mkPosetHomo : ∀ f → f Preserves P._≤_ ⟶ Q._≤_ → PosetHomomorphism
  mkPosetHomo f mono = record
    { ⟦_⟧ = f
    ; isOrderHomomorphism = record
      { cong = mono⇒cong P._≈_ Q._≈_ P.Eq.sym P.reflexive Q.antisym mono
      ; mono = mono
      }
    }