Skip to content

[ add ] Pointwise lifting of algebra to Data.Vec.Functional #3077

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
JacquesCarette wants to merge 3 commits into
base: master
Choose a base branch
from
Open

[ add ] Pointwise lifting of algebra to Data.Vec.Functional #3077

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a5290b9
[ add ] Pointwise lifting of algebra to
JacquesCarette Jul 16, 2026
872a850
Fix whitespace
JacquesCarette Jul 16, 2026
6710b0a
clean up imports
JacquesCarette Jul 16, 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
80 changes: 80 additions & 0 deletions src/Data/Vec/Functional/Algebra/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Algebraic structure of functional vectors
--
-- These are essentially 'free' because everything lifts pointwise
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Functional.Algebra.Base where

@jamesmckinna jamesmckinna Jul 17, 2026 •
edited
Loading

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.

If the sole contents of this module are to be the re-exports of the Bundles, then this could be almost entirely shortcircuited (Fairbairn?) as:

Suggested change
module Data.Vec.Functional.Algebra.Base where
open import Data.Nat.Base using (ℕ)
module Data.Vec.Functional.Algebra.Base (n : ℕ) where
open import Data.Fin.Base using (Fin)
-- Re-export existing constructions
open import Algebra.Construct.Pointwise (Fin n) public

And indeed, if there is to be more here, then why not refactor in this style anyway? (in the anonymous module you define below).

I think this was the substance of my critique of #2817 , and my suggestions that the corresponding Module additions be moved to Algebra.Module.Construct.Pointwise #2915 , and, if necessary, be re-exported here on the same basis as above?


open import Algebra.Bundles using (Magma; Semigroup; Band; CommutativeSemigroup;
Monoid; CommutativeMonoid; Group; AbelianGroup; NearSemiring; SemiringWithoutOne;
CommutativeSemiringWithoutOne; Semiring; CommutativeSemiring; IdempotentSemiring;
KleeneAlgebra; Quasiring; Ring; CommutativeRing)
import Algebra.Construct.Pointwise as Lift

@jamesmckinna jamesmckinna Jul 17, 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.

Notwithstanding my use of lift for helper functions in Algebra.Construct.Pointwise, I personally hate the use of Lift as a module name for qualified import. I would much prefer

Suggested change
import Algebra.Construct.Pointwise as Lift
import Algebra.Construct.Pointwise as Pointwise

cf. #2280

open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using (ℕ)
open import Level using (Level; _⊔_)

private
variable
a c ℓ : Level

-- only build the Bundles as the structure can be extracted from them
module _ (n : ℕ) where
magma : Magma a ℓ → Magma a ℓ
magma = Lift.magma (Fin n)

semigroup : Semigroup a ℓ → Semigroup a ℓ
semigroup = Lift.semigroup (Fin n)

band : Band a ℓ → Band a ℓ
band = Lift.band (Fin n)

commutativeSemigroup : CommutativeSemigroup a ℓ → CommutativeSemigroup a ℓ
commutativeSemigroup = Lift.commutativeSemigroup (Fin n)

monoid : Monoid a ℓ → Monoid a ℓ
monoid = Lift.monoid (Fin n)

commutativeMonoid : CommutativeMonoid a ℓ → CommutativeMonoid a ℓ
commutativeMonoid = Lift.commutativeMonoid (Fin n)

group : Group a ℓ → Group a ℓ
group = Lift.group (Fin n)

abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
abelianGroup = Lift.abelianGroup (Fin n)

nearSemiring : NearSemiring a ℓ → NearSemiring a ℓ
nearSemiring = Lift.nearSemiring (Fin n)

semiringWithoutOne : SemiringWithoutOne a ℓ → SemiringWithoutOne a ℓ
semiringWithoutOne = Lift.semiringWithoutOne (Fin n)

commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne a ℓ → CommutativeSemiringWithoutOne a ℓ
commutativeSemiringWithoutOne = Lift.commutativeSemiringWithoutOne (Fin n)

semiring : Semiring a ℓ → Semiring a ℓ
semiring = Lift.semiring (Fin n)

commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
commutativeSemiring = Lift.commutativeSemiring (Fin n)

idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
idempotentSemiring = Lift.idempotentSemiring (Fin n)

kleeneAlgebra : KleeneAlgebra a ℓ → KleeneAlgebra a ℓ
kleeneAlgebra = Lift.kleeneAlgebra (Fin n)

quasiring : Quasiring a ℓ → Quasiring a ℓ
quasiring = Lift.quasiring (Fin n)

ring : Ring a ℓ → Ring a ℓ
ring = Lift.ring (Fin n)

commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
commutativeRing = Lift.commutativeRing (Fin n)
Loading