    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The projection morphisms for relational structures arising from the
    -- non-dependent product construction
    ------------------------------------------------------------------------

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

    module Relation.Binary.Morphism.Construct.Product where

    import Data.Product.Base as Product using (<_,_>; proj₁; proj₂)
    open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
      using (Pointwise)
    open import Level using (Level)
    open import Relation.Binary.Bundles.Raw using (RawSetoid)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)

    private
      variable
        a b c ℓ₁ ℓ₂ ℓ : Level
        A : Set a
        B : Set b
        C : Set c

    ------------------------------------------------------------------------
    -- definitions

    module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where

      private

        _≈_ = Pointwise _≈₁_ _≈₂_

      module Proj₁ where

        isRelHomomorphism : IsRelHomomorphism _≈_ _≈₁_ Product.proj₁
        isRelHomomorphism = record { cong = Product.proj₁ }

      module Proj₂ where

        isRelHomomorphism : IsRelHomomorphism _≈_ _≈₂_ Product.proj₂
        isRelHomomorphism = record { cong = Product.proj₂ }

      module Pair (_≈′_ : Rel C ℓ)  where

        isRelHomomorphism : ∀ {h k} →
                            IsRelHomomorphism _≈′_ _≈₁_ h →
                            IsRelHomomorphism _≈′_ _≈₂_ k →
                            IsRelHomomorphism _≈′_ _≈_ Product.< h , k >
        isRelHomomorphism H K = record { cong = Product.< H.cong , K.cong > }
          where
          module H = IsRelHomomorphism H
          module K = IsRelHomomorphism K

    ------------------------------------------------------------------------
    -- package up for export

    module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} where

      private

        module M = RawSetoid M
        module N = RawSetoid N

      proj₁ = Proj₁.isRelHomomorphism M._≈_ N._≈_
      proj₂ = Proj₂.isRelHomomorphism M._≈_ N._≈_

      module _ {P : RawSetoid c ℓ} where

        private

          module P = RawSetoid P

        <_,_> = Pair.isRelHomomorphism M._≈_ N._≈_ P._≈_