[imports] Algebra.Apartness.Bundles .. Algebra.Construct.NaturalChoice.Base
#2597
Conversation
JacquesCarette
changed the title
Algebra.Apartness.Bundles .. Algebra.Construct.NaturalChoice.Base
| @@ -13,7 +13,7 @@ open import Relation.Binary.Core using (Rel) | |||
| open import Relation.Binary.Bundles using (ApartnessRelation) | |||
| open import Algebra.Core using (Op₁; Op₂) | |||
| open import Algebra.Bundles using (CommutativeRing) | |||
| open import Algebra.Apartness.Structures | |||
| open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField) | |||
There was a problem hiding this comment.
Actually, I'm against this change: the design of the various hierarchies is such that for each X.Structures, there will be a corresponding X.Bundles reifying the corresponding structures. So that if new structures get added, then Bundles will need to know about them.
The contra view would be that by being explicit, it catches potential bugs caused by not adding the corresponding structures, but I think (hope!) that's a minor consideration?
I've raised this as a point on the originating issue #2339 .
There was a problem hiding this comment.
I'm definitely a "I want to know, by reading, where something came from" kind of person. Importing 'everything' means you need to use interaction to do that.
It's not at all obvious that Algebra.Apartness.Structures defines anything with Heyting in the name (unless you know a lot already), so this serves as extra documentation too.
There was a problem hiding this comment.
@JacquesCarette All good points.
The specific use of 'Heyting' is a separate issue... #2588 and we might wish to completely revise these downstream one day, but yes, your general point stands.
(off-topic, but related: does increasing the information content/redundant recoding by making using directives so precise affect, positively, how AI systems might exploit this data? certainly the orthodox cognitive dimensions story about redundant recoding implies a trade-off with viscosity, but that's for humans, not machines... )
There was a problem hiding this comment.
My guess was that AI would feed from decoded .agdai information which have all of that in them [i.e. all traceability information is visible there, regardless of what humans did in the source.]
No description provided.