[Agda] partial division property

[Serge D. Mechveliani]

On Mon, Nov 05, 2012 at 10:44:00AM +0100, Nils Anders Danielsson wrote:
> On 2012-11-04 18:09, Serge D. Mechveliani wrote:
>>    (a : A) -> (b : A) -> case divMb a b of н╩
>>                          { (just q) -> (q * b) \~~ a
>>                          ; nothing  -> (x : A) -> \neg ((x * b) \~~ a)
>>                          }
>
> I think your problem is that the two branches above have different
> universe levels. You can use lifting (Level.Lift) to coerce one or both
> branches to a common universe level.

The simplest working code that I find with  Lift  is 

------------------------------------------------------------------------
divMb-sig : {c l : Level} -> CommutativeRing c l -> Set _
divMb-sig R =  let C = CommutativeRing.Carrier R in  C -> C -> Maybe C

PartialDivisionInCommutativeRing? :
                  (c l : Level) -> (R : CommutativeRing c l) ->
                  let A = CommutativeRing.Carrier R in
                                           divMb-sig R -> A -> A -> Set _

PartialDivisionInCommutativeRing? c l R divMb a b =            -- for a/b    

    case divMb a b of \lambda 
                    { nothing  ->  ((x : A) -> \neg ((x * b) ~~ a))
                    ; (just q) ->  Lift {\ell = max c l} ((q * b) ~~ a) }
    where
    A    = CommutativeRing.Carrier R
    _*_  = CommutativeRing._*_     R
    _~~_ = CommutativeRing._\~~_   R
-------------------------------------------------------------------------

Here I use the denotation  \~~, \neg, \lambda, \ell
 
for the corresponding math symbols, and  max  for  Level.\sqcap.

Without the argument  {... = ...}  in Lift,  it reports "unsolved metas".
Hence I am forced to find either the level of  ((q * b) ~~ a)  or the level 
to which it must be lifted. These are expressed via  c and l,  so this 
requires making explicit  (c l : Level).
Right?
I wonder how could this effect the further code.

Also this was a luck that I discovered  (max c l).  I tried also other
expressions, like  (suc $ max c l). 
First several reports about  Set <level>  did not help me.
Finally there appeared a report of that the checker expects  Set (max c l)
for  ((q * b) ~~ a),  and this was a luck.

Is there a simpler way to set things with Lift ?

Thanks,
Sergei.