[ add ] `Relation.Binary.Morphism.Construct.On`#2872

Merged

JacquesCarette merged 3 commits intoagda:masterfrom

jamesmckinna:on-morphisms

Nov 21, 2025

Commits on Nov 12, 2025

add: `Relation.Binary.Morphism.Construct.On`
jamesmckinna
committed

Commits on Nov 18, 2025

fix: top-level descriptive comment
jamesmckinna
committed

Commits on Nov 20, 2025

fix: remove `module ι`, and better description in `CHANGELOG`
jamesmckinna
committed