[Agda] level setting problem

[mechvel at scico.botik.ru]

On 2021-04-11 19:42, Georgi Lyubenov wrote:
> 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?


Probably this is not the same. My function was

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


It has an argument  xs : List String.
Also constr is composed (length xs) times, and each time the levels 
increase.
?

--
SM