From aa736df734ce732697cc2e3deefb52c413ed1584 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 23 Jul 2026 08:27:42 +0100 Subject: [PATCH 1/3] [ refactor ] generalise `Data.Sum.Relation.Binary.Pointwise.elim` #3079 --- CHANGELOG.md | 6 ++++-- src/Data/Sum/Relation/Binary/Pointwise.agda | 20 +++++++++++++------- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c78b4f95a..ba8c8c5aa9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -482,8 +482,10 @@ Additions to existing modules * In `Data.Sum.Relation.Binary.Pointwise`: ```agda - elim : R =[ f ]⇒ T → S =[ g ]⇒ T → - Pointwise R S =[ Sum.[ f , g ]′ ]⇒ T + elim : R =[ f ]⇒ T → S =[ g ]⇒ T → Sum.[ f , g ]′ ≗ h → + Pointwise R S =[ h ]⇒ T + elim′ : R =[ f ]⇒ T → S =[ g ]⇒ T → + Pointwise R S =[ Sum.[ f , g ]′ ]⇒ T ``` * In `Data.Vec.Properties`: diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index f66740f761..06f109a63c 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -17,7 +17,8 @@ open import Function.Bundles using (Inverse; mk↔) open import Relation.Nullary.Decidable.Core as Dec using (yes; no; map′) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Binary -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ + using (_≡_; _≗_) import Relation.Binary.PropositionalEquality.Properties as ≡ private @@ -39,16 +40,21 @@ data Pointwise {A : Set a} {B : Set b} {C : Set c} {D : Set d} ---------------------------------------------------------------------- -- Functions -elim : ∀ {f : A → C} {g : B → C} → - R =[ f ]⇒ T → S =[ g ]⇒ T → - Pointwise R S =[ Sum.[ f , g ]′ ]⇒ T -elim R⇒T S⇒T (inj₁ xRy) = R⇒T xRy -elim R⇒T S⇒T (inj₂ xSy) = S⇒T xSy +module _ {f : A → C} {g : B → C} + (T : Rel C ℓ) (R⇒T : R =[ f ]⇒ T) (S⇒T : S =[ g ]⇒ T) + where + + elim : ∀ {h} → Sum.[ f , g ]′ ≗ h → Pointwise R S =[ h ]⇒ T + elim H (inj₁ xRy) = ≡.subst₂ T (H (inj₁ _)) (H (inj₁ _)) (R⇒T xRy) + elim H (inj₂ xSy) = ≡.subst₂ T (H (inj₂ _)) (H (inj₂ _)) (S⇒T xSy) + + elim′ : Pointwise R S =[ Sum.[ f , g ]′ ]⇒ T + elim′ = elim λ _ → ≡.refl map : ∀ {f : A → C} {g : B → D} → R =[ f ]⇒ T → S =[ g ]⇒ U → Pointwise R S =[ Sum.map f g ]⇒ Pointwise T U -map R⇒T S⇒U = elim {T = Pointwise _ _} (inj₁ ∘ R⇒T) (inj₂ ∘ S⇒U) +map R⇒T S⇒U = elim′ (Pointwise _ _) (inj₁ ∘ R⇒T) (inj₂ ∘ S⇒U) ------------------------------------------------------------------------ -- Relational properties From d384f6181403c6e63805d9bfe56cdf95b525c478 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 24 Jul 2026 09:32:15 +0100 Subject: [PATCH 2/3] add: extensive comments in code --- src/Data/Sum/Relation/Binary/Pointwise.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 06f109a63c..14ef40e947 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -40,6 +40,18 @@ data Pointwise {A : Set a} {B : Set b} {C : Set c} {D : Set d} ---------------------------------------------------------------------- -- Functions +-- General eliminator arising from initiality of `Pointwise`. +-- +-- Ttype-theoreticaly/logically, `elim` is an inference rule for the +-- consequence relation given by (indexed) inclusion between relations, +-- describing what 'conclusion' T is derivable from what 'principal formula' +-- `Pointwise R S` by appeal to the ancillary sequents witnessing that +-- 'T follows from R' and 'T follows from S'. +-- +-- Categorically, it expresses `Pointwise R S` as a suitably indexed +-- generalisation of a coproduct, with elim generalising the usual +-- arrow-out-of-a-colimit. + module _ {f : A → C} {g : B → C} (T : Rel C ℓ) (R⇒T : R =[ f ]⇒ T) (S⇒T : S =[ g ]⇒ T) where From 45316a1025ac6109332b13ce9426f14808727ffc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 3 Aug 2026 17:51:37 +0100 Subject: [PATCH 3/3] fix: typo --- src/Data/Sum/Relation/Binary/Pointwise.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 14ef40e947..344756ff91 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -42,7 +42,7 @@ data Pointwise {A : Set a} {B : Set b} {C : Set c} {D : Set d} -- General eliminator arising from initiality of `Pointwise`. -- --- Ttype-theoreticaly/logically, `elim` is an inference rule for the +-- Type-theoreticaly/logically, `elim` is an inference rule for the -- consequence relation given by (indexed) inclusion between relations, -- describing what 'conclusion' T is derivable from what 'principal formula' -- `Pointwise R S` by appeal to the ancillary sequents witnessing that