Skip to content

[ fix ] universe levels in Data.Product.Relation.Binary.Pointwise.Dependent.POINTWISE - #3092

Merged
jamesmckinna merged 2 commits into
agda:masterfrom
jamesmckinna:correct-Product-levels
Jul 28, 2026
Merged

[ fix ] universe levels in Data.Product.Relation.Binary.Pointwise.Dependent.POINTWISE#3092
jamesmckinna merged 2 commits into
agda:masterfrom
jamesmckinna:correct-Product-levels

Conversation

@jamesmckinna

Copy link
Copy Markdown
Collaborator

Salvaged from #3081 . Does this need a CHANGELOG entry?

@jamesmckinna jamesmckinna added this to the v3.0 milestone Jul 28, 2026

@gallais gallais left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

It is technically a breaking change so should probably have a CHANGELOG entry associated to it

@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

It is technically a breaking change so should probably have a CHANGELOG entry associated to it

Fine, but I assumed that lowering a universe level would be backwards compatible, by cumulativity, and hence that this is a 'minor improvement'... but happy to make a note.

@jamesmckinna
jamesmckinna enabled auto-merge July 28, 2026 13:44
@jamesmckinna
jamesmckinna added this pull request to the merge queue Jul 28, 2026
Merged via the queue into agda:master with commit 21278b6 Jul 28, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants