From 78f32d83eb15021e95deaa0913d10033c3f0edf3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 26 May 2025 09:52:56 +0100 Subject: [PATCH 1/7] [ add ] product structure on `RawSetoid` --- CHANGELOG.md | 2 + .../Binary/Morphism/Construct/Product.agda | 74 +++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 src/Relation/Binary/Morphism/Construct/Product.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 1a6315c7e2..7564d1c1b4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -165,6 +165,8 @@ New modules * `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 ----------------------------- diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda new file mode 100644 index 0000000000..ede2827bcb --- /dev/null +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -0,0 +1,74 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The projection morphisms for relational structures arising from the +-- 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.Construct using () +open import Relation.Binary.Bundles.Raw using (RawSetoid) +open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) + +private + variable + a b c ℓ₁ ℓ₂ ℓ : Level + + +------------------------------------------------------------------------ +-- product construction on RawSetoid belongs in Relation.Binary.Construct.Product? + +module _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where + + private + + module M = RawSetoid M + module N = RawSetoid N + + P : RawSetoid _ _ + P = record { _≈_ = Pointwise M._≈_ N._≈_ } + + module P = RawSetoid P + + module Proj₁ where + + isRelHomomorphism : IsRelHomomorphism P._≈_ M._≈_ Product.proj₁ + isRelHomomorphism = record { cong = λ z → z .Product.proj₁ } + + + module Proj₂ where + + isRelHomomorphism : IsRelHomomorphism P._≈_ N._≈_ Product.proj₂ + isRelHomomorphism = record { cong = λ z → z .Product.proj₂ } + + + module Pair (X : RawSetoid c ℓ) where + + private module X = RawSetoid X + + isRelHomomorphism : ∀ {h k} → + IsRelHomomorphism X._≈_ M._≈_ h → + IsRelHomomorphism X._≈_ N._≈_ k → + IsRelHomomorphism X._≈_ P._≈_ 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 ℓ₂} {P : RawSetoid c ℓ} where + + proj₁ = Proj₁.isRelHomomorphism M N + proj₂ = Proj₂.isRelHomomorphism M N + <_,_> = Pair.isRelHomomorphism M N P + From b8efc2cbd4793c235bf82a646f7c9e357a0d5bfb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 26 May 2025 10:19:07 +0100 Subject: [PATCH 2/7] fix: export parametrisation --- src/Relation/Binary/Morphism/Construct/Product.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda index ede2827bcb..3c6379e487 100644 --- a/src/Relation/Binary/Morphism/Construct/Product.agda +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -66,9 +66,12 @@ module _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where ------------------------------------------------------------------------ -- package up for export -module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} {P : RawSetoid c ℓ} where +module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} where proj₁ = Proj₁.isRelHomomorphism M N proj₂ = Proj₂.isRelHomomorphism M N + +module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} {P : RawSetoid c ℓ} where + <_,_> = Pair.isRelHomomorphism M N P From 6d937c33002797ed13f23dca7085f13904b72c0b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 26 May 2025 10:22:59 +0100 Subject: [PATCH 3/7] fix: eta contract definitions --- src/Relation/Binary/Morphism/Construct/Product.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda index 3c6379e487..a9b7955fb9 100644 --- a/src/Relation/Binary/Morphism/Construct/Product.agda +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -40,13 +40,13 @@ module _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where module Proj₁ where isRelHomomorphism : IsRelHomomorphism P._≈_ M._≈_ Product.proj₁ - isRelHomomorphism = record { cong = λ z → z .Product.proj₁ } + isRelHomomorphism = record { cong = Product.proj₁ } module Proj₂ where isRelHomomorphism : IsRelHomomorphism P._≈_ N._≈_ Product.proj₂ - isRelHomomorphism = record { cong = λ z → z .Product.proj₂ } + isRelHomomorphism = record { cong = Product.proj₂ } module Pair (X : RawSetoid c ℓ) where From ad511e9ea162e30be9cb74dfeef35c8bc1c924ed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 27 May 2025 10:35:04 +0100 Subject: [PATCH 4/7] fix: full stops --- CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7564d1c1b4..db5262e23e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -163,9 +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` +* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`. Additions to existing modules ----------------------------- From 7af0256ace1a8c07a5aa1889f12bb9e2709c275e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 27 May 2025 10:35:30 +0100 Subject: [PATCH 5/7] fix: redundant comments/imports --- src/Relation/Binary/Morphism/Construct/Product.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda index a9b7955fb9..fcc3f635ad 100644 --- a/src/Relation/Binary/Morphism/Construct/Product.agda +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -13,7 +13,6 @@ 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.Construct using () open import Relation.Binary.Bundles.Raw using (RawSetoid) open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) @@ -23,7 +22,7 @@ private ------------------------------------------------------------------------ --- product construction on RawSetoid belongs in Relation.Binary.Construct.Product? +-- definitions module _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where From 81cb31e2f94c397c1babaff39722c48f48cd7d1c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 29 May 2025 06:31:19 +0100 Subject: [PATCH 6/7] unbundle definitions; leave exports bundled --- .../Binary/Morphism/Construct/Product.agda | 45 ++++++++++--------- 1 file changed, 25 insertions(+), 20 deletions(-) diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda index fcc3f635ad..fe10a64c27 100644 --- a/src/Relation/Binary/Morphism/Construct/Product.agda +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -14,48 +14,44 @@ 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 _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where +module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where private - module M = RawSetoid M - module N = RawSetoid N - - P : RawSetoid _ _ - P = record { _≈_ = Pointwise M._≈_ N._≈_ } - - module P = RawSetoid P + _≈_ = Pointwise _≈₁_ _≈₂_ module Proj₁ where - isRelHomomorphism : IsRelHomomorphism P._≈_ M._≈_ Product.proj₁ + isRelHomomorphism : IsRelHomomorphism _≈_ _≈₁_ Product.proj₁ isRelHomomorphism = record { cong = Product.proj₁ } module Proj₂ where - isRelHomomorphism : IsRelHomomorphism P._≈_ N._≈_ Product.proj₂ + isRelHomomorphism : IsRelHomomorphism _≈_ _≈₂_ Product.proj₂ isRelHomomorphism = record { cong = Product.proj₂ } - module Pair (X : RawSetoid c ℓ) where - - private module X = RawSetoid X + module Pair (_≈′_ : Rel C ℓ) where isRelHomomorphism : ∀ {h k} → - IsRelHomomorphism X._≈_ M._≈_ h → - IsRelHomomorphism X._≈_ N._≈_ k → - IsRelHomomorphism X._≈_ P._≈_ Product.< 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 @@ -67,10 +63,19 @@ module _ (M : RawSetoid a ℓ₁) (N : RawSetoid b ℓ₂) where module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} where - proj₁ = Proj₁.isRelHomomorphism M N - proj₂ = Proj₂.isRelHomomorphism M N + 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 _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} {P : RawSetoid c ℓ} where + module P = RawSetoid P - <_,_> = Pair.isRelHomomorphism M N P + <_,_> = Pair.isRelHomomorphism M._≈_ N._≈_ P._≈_ From c4253344c39d10097bb9ffd119f4cf795df720b3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 3 Jun 2025 08:11:57 +0100 Subject: [PATCH 7/7] fix: cosmetic comment to trigger fresh test run --- src/Relation/Binary/Morphism/Construct/Product.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda index fe10a64c27..b531fd9b72 100644 --- a/src/Relation/Binary/Morphism/Construct/Product.agda +++ b/src/Relation/Binary/Morphism/Construct/Product.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- The projection morphisms for relational structures arising from the --- product construction +-- non-dependent product construction ------------------------------------------------------------------------ {-# OPTIONS --safe --cubical-compatible #-}