[ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079 - #3085
[ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079#3085jamesmckinna wants to merge 2 commits into
Data.Sum.Relation.Binary.Pointwise.elim #3079#3085Conversation
| (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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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!?
There was a problem hiding this comment.
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...
There was a problem hiding this comment.
Oh, and subst is only there to make use of the generalisation via extensionality...
There was a problem hiding this comment.
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 ?
There was a problem hiding this comment.
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?
2 participants
This takes the #3079 definition and generalises it to any
hextensionally equivalent toSum.[ f , g ]′.Opportunity for @JacquesCarette (or anyone else!) to reconsider the chosen names here!