Adds Algebra.Morphism.Construct.DirectProduct

CHANGELOG.md

@@ -155,6 +155,8 @@ New modules
 
 * `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
 
+* `Algebra.Morphism.Construct.DirectProduct`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -163,7 +165,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/Algebra/Morphism/Construct/DirectProduct.agda

@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The projection morphisms for algebraic structures arising from the
+-- direct product construction
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+module Algebra.Morphism.Construct.DirectProduct where
+
+open import Algebra.Bundles using (RawMagma; RawMonoid)
+open import Algebra.Construct.DirectProduct using (rawMagma; rawMonoid)
+open import Algebra.Morphism.Structures
+  using ( module MagmaMorphisms
+        ; module MonoidMorphisms
+        )
+open import Data.Product as Product
+  using (_,_)
+open import Level using (Level)
+open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Binary.Morphism.Construct.Product
+  using (proj₁; proj₂; <_,_>)
+
+private
+  variable
+    a b c ℓ₁ ℓ₂ ℓ₃ : Level
+
+------------------------------------------------------------------------
+-- Magmas
+
+module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where
+  open MagmaMorphisms
+
+  private
+    module M = RawMagma M
+    module N = RawMagma N
+
+  module Proj₁ (refl : Reflexive M._≈_) where
+
+    isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁
+    isMagmaHomomorphism = record
+      { isRelHomomorphism = proj₁
+      ; homo              = λ _ _ → refl
+      }
+
+  module Proj₂ (refl : Reflexive N._≈_) where
+
+    isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂
+    isMagmaHomomorphism = record
+      { isRelHomomorphism = proj₂
+      ; homo              = λ _ _ → refl
+      }
+
+  module Pair (P : RawMagma c ℓ₃) where
+
+    isMagmaHomomorphism : ∀ {f h} →
+                          IsMagmaHomomorphism P M f →
+                          IsMagmaHomomorphism P N h →
+                          IsMagmaHomomorphism P (rawMagma M N) (Product.< f , h >)
+    isMagmaHomomorphism F H = record
+      { isRelHomomorphism = < F.isRelHomomorphism , H.isRelHomomorphism >
+      ; homo              = λ x y → F.homo x y , H.homo x y
+      }
+      where
+        module F = IsMagmaHomomorphism F
+        module H = IsMagmaHomomorphism H
+
+------------------------------------------------------------------------
+-- Monoids
+
+module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where
+  open MonoidMorphisms
+
+  private
+    module M = RawMonoid M
+    module N = RawMonoid N
+
+  module Proj₁ (refl : Reflexive M._≈_) where
+
+    isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) M Product.proj₁
+    isMonoidHomomorphism = record
+      { isMagmaHomomorphism = Magma.Proj₁.isMagmaHomomorphism M.rawMagma N.rawMagma refl
+      ; ε-homo              = refl
+      }
+
+  module Proj₂ (refl : Reflexive N._≈_) where
+
+    isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) N Product.proj₂
+    isMonoidHomomorphism = record
+      { isMagmaHomomorphism = Magma.Proj₂.isMagmaHomomorphism M.rawMagma N.rawMagma refl
+      ; ε-homo              = refl
+      }
+
+  module Pair (P : RawMonoid c ℓ₃) where
+
+    private
+      module P = RawMonoid P
+
+    isMonoidHomomorphism : ∀ {f h} →
+                          IsMonoidHomomorphism P M f →
+                          IsMonoidHomomorphism P N h →
+                          IsMonoidHomomorphism P (rawMonoid M N) (Product.< f , h >)
+    isMonoidHomomorphism F H = record
+      { isMagmaHomomorphism = Magma.Pair.isMagmaHomomorphism M.rawMagma N.rawMagma P.rawMagma F.isMagmaHomomorphism H.isMagmaHomomorphism
+      ; ε-homo              = F.ε-homo , H.ε-homo }
+      where
+        module F = IsMonoidHomomorphism F
+        module H = IsMonoidHomomorphism H

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._≈_
+