Fix level for FixPoint in Induction.WellFounded (#1265)

Author: JorisCeulemans

CHANGELOG.md

@@ -18,6 +18,9 @@ Bug-fixes
 * Fixed various algebraic bundles not correctly re-exporting
   `commutativeSemigroup` proofs.
 
+* Fix in `Induction.WellFounded.FixPoint`, where the well-founded relation `_<_` and
+  the predicate `P` were required to live at the same universe level.
+
 Non-backwards compatible changes
 --------------------------------
 

src/Induction/WellFounded.agda

@@ -106,7 +106,7 @@ module All {_<_ : Rel A r} (wf : WellFounded _<_) ℓ where
   #-}
 
 module FixPoint
-  {_<_ : Rel A ℓ} (wf : WellFounded _<_)
+  {_<_ : Rel A r} (wf : WellFounded _<_)
   (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P)
   (f-ext : (x : A) {IH IH′ : WfRec _<_ P x} → (∀ {y} y<x → IH y y<x ≡ IH′ y y<x) → f x IH ≡ f x IH′)
   where