[ refactor ] make Relation.Binary.Morphism.Definitions obsolete#2922
[ refactor ] make Relation.Binary.Morphism.Definitions obsolete#2922jamesmckinna wants to merge 5 commits intoagda:masterfrom
Relation.Binary.Morphism.Definitions obsolete#2922Conversation
jamesmckinna
requested review from
JacquesCarette,
MatthewDaggitt and
gallais
and removed request for
JacquesCarette
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Putting as comment, since I don't want to block merge on just this.
| Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧ = ∀ {x y} → x ∼₁ y → ⟦ x ⟧ ∼₂ ⟦ y ⟧ | ||
| open import Function.Definitions public | ||
| using () | ||
| renaming (Congruent to Homomorphic₂) |
There was a problem hiding this comment.
If this is a stub module, should we be deprecating Homomorphic₂? Otherwise, where is it going to live?
There was a problem hiding this comment.
My only reason for not deprecating, is that there seemed to be a request from @pnlph a number of years ago, to retain this name for client compatibility (and hence the public re-export from this module, where it originated). If there is no longer any such demand, then I'd be more radical wrt the surgery being carried out here, and mark the whole module as DEPRECATED...
There was a problem hiding this comment.
UPDATED: I've deprecated the lemmas, but not the module, and we'll do that in v3.0
| open import Algebra.Morphism.Structures | ||
| open import Level using (Level; suc; _⊔_) | ||
| --open import Relation.Binary.Morphism using (IsRelHomomorphism) | ||
| --open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism) |
There was a problem hiding this comment.
Blast, I thought that I had caught these two.
There was a problem hiding this comment.
Wait, won't this PR do the deletion when merged?
There was a problem hiding this comment.
And yes, they are commented out (never mind unused) on master, so should be deleted!?
| of the termination checker for some `Vector`-defined operations. | ||
|
|
||
| * `Relation.Binary.Morphism.Definitions` is no longer imported by any module, | ||
| but retained as a stub for compatibility with external users. |
There was a problem hiding this comment.
Should it be deprecated then?
There was a problem hiding this comment.
Well, see my comment on the module. I'd be happy to, if we no longer have external clients requesting this.
But now I think about it, let's just deprecate anyway?
There was a problem hiding this comment.
I tried a middle course, deprecating the two names, but not the whole module, but now, against expectations, a warning is raised whenever Function.Definitions.Congruent is used... ???
UPDATED: seemingly fixed now, but let's see what make test does remotely...
|
Is this an Agda bug now? Or simply that I don't understand the semantics of |
3 participants
This tackles the first part of #2875 , retaining the module solely for compatibility per #1206 / #1213 as requested by @pnlph , so no actual
deprecationat this stage.Knock-on consequences include:
Function.Definitionsvs. alternativesHomomorphic₂throughout byFunction.Definitions.Congruent(but the name is still exported aspublicby the obsolete stub; and hence also exported byRelation.Binary.Morphism, but this could be removed/deprecated?)TL;DR: the 'cause' of the problem is yet again [ DRY ] with some basic concepts duplicated across the
Function/Relation/Algebrahierarchies as various specialisations (or not even that) of 'common' (very) general abstractions (eg 'monotonicity'/'congruence'/'respects') which different authors have, at different times, identified asCoreto one or other hierarchy... cf. #2917