Skip to content

Refactor unique and add IsWeakPullback and MonoWeakPullback#512

Merged
JacquesCarette merged 2 commits intoagda:masterfrom
sergey-goncharov:master
Apr 2, 2026
Merged

Refactor unique and add IsWeakPullback and MonoWeakPullback#512
JacquesCarette merged 2 commits intoagda:masterfrom
sergey-goncharov:master

Conversation

@sergey-goncharov
Copy link
Copy Markdown
Collaborator

Added unique′ and refactored unique through it; added jmono; added IsWeakPullback and MonoWeakPullback⇒Pullback

@JacquesCarette JacquesCarette merged commit e2bbef9 into agda:master Apr 2, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants