[Agda] how to set level

[Sergei Meshveliani]

Today I wrote about the level setting problem:


> I find now the needed code:

>  _<e_ :  Rel Expression (α= ⊔ β) 
>
>  (cf a) <e (cf b)   =  Lift {β} {α=} (a < b)   -- **  
>  (cf _) <e (var _)  =  Lift ⊤ 
>  (cf _) <e (_ :+ _) =  Lift ⊤ 
>
>  (var i) <e (var j)  =  Lift (i <n j)
>  (var _) <e (cf _)   =  Lift ⊥
>  (var _) <e (_ :+ _) =  Lift ⊤

> (_ :+ _) <e (cf _)   =  Lift ⊥ 
> (_ :+ _) <e (var _)  =  Lift ⊥
> (x :+ y) <e (z :+ u) =  Lift (x <e z  ⊎  (x =e z × y <e u))
    

This works, but leads to complications in using _<e_.
For example, a proof for 

    from-cf-mono-< :  ∀ {a b} → cf a <e cf b → a < b

needs inserting Lift and `lift' in various places.
I was not able to prove it. Instead I prove 

    from-cf-mono-< :  ∀ {a b} → cf a <e cf b → Lift {_} {_} (a < b)

Deriving  _<e?_ : Decidable _<e_  from  _<?_  involves more
complications with levels.

I think now that the source of these complications is defining _<e_ as a
function.
Defining it as `data' removes the problem:

  data _<e_ : Expression → Expression → Set β
    where
    cf<cf  :  ∀ {a b} → a < b → cf a <e cf b
    cf<var :  ∀ {a i} → cf a <e var i
    cf<+   :  ∀ {a e e'} → cf a <e (e :+ e')

    var<+ :  ∀ {i e e'} → var i <e (e :+ e')


  from-cf-mono-< :  ∀ {a b} → cf a <e cf b → (a < b)
  from-cf-mono-< (cf<cf a<b) = a<b

  open IsStrictTotalOrder isSTO using (_<?_)

  _<e?_ : Decidable₂ _<e_

  (cf a) <e? (cf b) =  case a <? b of \
                              { (yes a<b) → yes (cf<cf a<b)
                              ; (no a≮b)  → no (a≮b ∘ from-cf-mono-<)
                              }
  (cf _) <e? (var _)  =  yes cf<var
  (cf _) <e? (_ :+ _) =  yes cf<+

  (var _) <e? (cf _) =  no λ()
  ...


This seems to work fine.

------
Sergei