[Agda] level setting problem

[Georgi Lyubenov]

This seems to be essentially the same definition:
module levels where

open import Agda.Primitive

data Two : Set where
  ff tt : Two

if_then_else_ : {A : Set} -> Two -> A -> A -> A
if ff then t else e = e
if tt then t else e = t

data Setoid (a b : Level) : Set where

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

mkConstr : (t : Two) -> Setoid (if t then a else (a ⊔ b)) (if t then b else
a ⊔ b)
mkConstr ff = constr setoid0
mkConstr tt = setoid0

Am I missing something?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210411/779d3d25/attachment.html>