<div dir="ltr">This seems to be essentially the same definition:<br>module levels where<br><br>open import Agda.Primitive<br><br>data Two : Set where<br>  ff tt : Two<br><br>if_then_else_ : {A : Set} -> Two -> A -> A -> A<br>if ff then t else e = e<br>if tt then t else e = t<br><br>data Setoid (a b : Level) : Set where<br><br>postulate<br>   a b     : Level<br>   setoid0 : Setoid a b<br>   constr  : ∀ {c d} → Setoid c d → Setoid (c ⊔ d) (c ⊔ d)<br><br>mkConstr : (t : Two) -> Setoid (if t then a else (a ⊔ b)) (if t then b else a ⊔ b)<br>mkConstr ff = constr setoid0<br>mkConstr tt = setoid0<br><br>Am I missing something?</div>