Skip to content

[ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079 #3085

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jamesmckinna wants to merge 3 commits into
base: master
Choose a base branch
from
Open

[ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079 #3085

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
aa736df
[ refactor ] generalise `Data.Sum.Relation.Binary.Pointwise.elim` #3079
jamesmckinna Jul 23, 2026
d384f61
add: extensive comments in code
jamesmckinna Jul 24, 2026
45316a1
fix: typo
jamesmckinna Aug 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`:
Expand Down
32 changes: 25 additions & 7 deletions src/Data/Sum/Relation/Binary/Pointwise.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -39,16 +40,33 @@ 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
-- General eliminator arising from initiality of `Pointwise`.
--
-- Ttype-theoreticaly/logically, `elim` is an inference rule for the
Comment thread
jamesmckinna marked this conversation as resolved.
Outdated
-- 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

elim : ∀ {h} → Sum.[ f , g ]′ ≗ h → Pointwise R S =[ h ]⇒ T

@JacquesCarette JacquesCarette Jul 23, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not really an eliminator, is it? It is much more like a transport (hence the subst-based implementation!)

Starting bid of transport-[,]-=[]⇒. I hate it, but have to start somewhere! Now that I've had more time to think about it, I definitely dislike elim as this isn't an eliminator at all.

@jamesmckinna jamesmckinna Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I happen to disagree, but I suppose in fairness It All Depends what you mean by... 'eliminator'...

... within the 'logic' / consequence relation given by inclusion/implication between relations, this is exactly an eliminator: it is an inference rule which describes what 'conclusion' T is derivable from what 'principal formula' Pointwise R S by appeal to the ancillary sequents witnessing that 'T follows from R' (resp. S)...

Categorically, it expresses Pointwise R S as a (suitable indexed generalisation of a) coproduct, with elim generalising the usual arrow-out-of-a-colimit.

What's not like an eliminator about that!?

@jamesmckinna jamesmckinna Jul 23, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And, FTR, I derived these while trying to think about #3081 in terms of product diagrams, with corresponding rule intro as a staging post on the way to generalising Product.zip... so it seems important to me, at least, to characterise these (dual!) constructions not only type-theoretically, but also categorically.

Or perhaps rather, given the contested terminology, not only categorically, but also type-theoretically!!! ;-)

Hope you'll change your mind on this...

@jamesmckinna jamesmckinna Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, and subst is only there to make use of the generalisation via extensionality...

@JacquesCarette JacquesCarette Jul 23, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Put that way (which should be in the comments!!!), I do see how this is an eliminator.

In which case, given our naming convention for many other eliminators, maybe it should be called pointwise ?

@jamesmckinna jamesmckinna Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting suggestion! And something I have suggested in the past...

... just as this new departure with intro and elim is a fresh experiment... in a more 'semantics'-oriented approach to naming?

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
Expand Down
Loading