diff --git a/CHANGELOG.md b/CHANGELOG.md index 12039b4aed..9ec8c2be30 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,8 @@ Bug-fixes * Fix a typo in `Algebra.Morphism.Construct.DirectProduct`. +* Fix a typo in `Function.Construct.Constant`. + Non-backwards compatible changes -------------------------------- diff --git a/src/Function/Construct/Constant.agda b/src/Function/Construct/Constant.agda index 8d031a3070..ae01e6fa1d 100644 --- a/src/Function/Construct/Constant.agda +++ b/src/Function/Construct/Constant.agda @@ -53,7 +53,7 @@ module _ ------------------------------------------------------------------------ -- Setoid bundles -module _ (S : Setoid a ℓ₂) (T : Setoid b ℓ₂) where +module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where open Setoid