Skip to content

[imports] Algebra.Apartness.Bundles .. Algebra.Construct.NaturalChoice.Base #2597

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

Merged
merged 2 commits into from
Feb 28, 2025
Merged

[imports] Algebra.Apartness.Bundles .. Algebra.Construct.NaturalChoice.Base #2597

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
62aa5c1
Apartness & Construct
jmougeot Feb 19, 2025
d159345
Merge branch 'master' into import0
JacquesCarette Feb 26, 2025
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
2 changes: 1 addition & 1 deletion src/Algebra/Apartness/Bundles.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Contributor

@jamesmckinna jamesmckinna Feb 26, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

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 .

Copy link
Contributor

Choose a reason for hiding this comment

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

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.

Copy link
Contributor

Choose a reason for hiding this comment

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

@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... )

Copy link
Contributor

Choose a reason for hiding this comment

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

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.]


record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Construct/Add/Identity.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ open import Algebra.Core using (Op₂)
open import Algebra.Definitions
using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
open import Data.Product.Base using (_,_)
open import Level using (Level; _⊔_)
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Binary.Structures using (IsEquivalence)
Expand Down