diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda
index 24428a5843..170b5abb07 100644
--- a/src/Data/Star/Decoration.agda
+++ b/src/Data/Star/Decoration.agda
@@ -28,7 +28,7 @@ data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r)
 -- Decorating an edge with more information.
 
 data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T)
-       : Rel (NonEmpty (Star T)) p where
+       : Rel (NonEmpty (Star T)) (ℓ ⊔ r ⊔ p) where
   ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
       (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)
 
diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda
index ed606807ce..bc86786f74 100644
--- a/src/Data/Star/Pointer.agda
+++ b/src/Data/Star/Pointer.agda
@@ -26,7 +26,7 @@ private
 
 data Pointer {T : Rel I r}
              (P : EdgePred p T) (Q : EdgePred q T)
-             : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where
+             : Rel (Maybe (NonEmpty (Star T))) (ℓ ⊔ r ⊔ p ⊔ q) where
   step : ∀ {i j k} {x : T i j} {xs : Star T j k}
          (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs)))
                                  (just (nonEmpty xs))
diff --git a/src/Reflection/AnnotatedAST.agda b/src/Reflection/AnnotatedAST.agda
index 61d55def7d..8ebc54b919 100644
--- a/src/Reflection/AnnotatedAST.agda
+++ b/src/Reflection/AnnotatedAST.agda
@@ -35,8 +35,8 @@ Annotation : ∀ ℓ → Set (suc ℓ)
 Annotation ℓ = ∀ {u} → ⟦ u ⟧ → Set ℓ
 
 -- An annotated type is a family over an Annotation and a reflected term.
-Typeₐ : ∀ ℓ → Univ → Set (suc ℓ)
-Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set ℓ
+Typeₐ : ∀ ℓ → Univ → Set (suc (suc ℓ))
+Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set (suc ℓ)
 
 private
   variable
@@ -168,7 +168,7 @@ mutual
 
 -- An annotation function computes the top-level annotation given a
 -- term annotated at all sub-terms.
-AnnotationFun : Annotation ℓ → Set ℓ
+AnnotationFun : Annotation ℓ → Set (suc ℓ)
 AnnotationFun Ann = ∀ u {t : ⟦ u ⟧} → Annotated′ Ann t → Ann t