Fix universe level typo (#2841)

jacquescomeaux · web-flow · commit bb57f4937eac · 2025-10-25T12:36:59.000Z
diff --git 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
@@ -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
 
