[ add ] product structure on RawSetoid

CHANGELOG.md

@@ -163,7 +163,9 @@ New modules
 
 * `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
 
-* `Data.Sign.Show` to show a sign
+* `Data.Sign.Show` to show a sign.
+
+* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`.
 
 Additions to existing modules
 -----------------------------

src/Relation/Binary/Morphism/Construct/Product.agda

@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- 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._≈_
+