[Agda] level setting problem

[mechvel at scico.botik.ru]

Can, anyone, please, suggest a simplification for the below mConstr ?
I mean the level values in the signature.
Is there a way to get rid of implementing makeLevels ?

(may be by using wildcard, Lift, \omega ...)

Thanks,

------
Sergei


-------------------------------------------
open import Data.List using (List; []; _∷_)
open import Data.Product using (_×_; _,_)
open import Data.String using (String)
open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid)

postulate
   a b     : Level
   setoid0 : Setoid a b
   constr  : ∀ {c d} → Setoid c d → Setoid (c ⊔ d) (c ⊔ d)

makeLevels : List String → Level × Level
makeLevels []       =  (a , b)
makeLevels (_ ∷ xs) =  let (c , d) = makeLevels xs
                        in  (c ⊔ d , c ⊔ d)

mConstr : (xs : List String) → let (c , d) = makeLevels xs
                                in  Setoid c d
mConstr []       =  setoid0
mConstr (_ ∷ xs) =  constr (mConstr xs)