[Agda] partial division property

[Serge D. Mechveliani]

People, 
can you, please, correct the below piece of code?
(for Agda-2.3.0.1, lib-0.6).

It aims at a definition for a map   divMb : R -> R -> Maybe R
being a  partial division  in a  CommutativeRing R.
This definition maps  (R, divMb)  to the corresponding type of proofs.

Here I use the denotation  \~~, \neg  for the corresponding math symbols,
L-max  for  Level.\sqcap.

----------------------------------------------------------------------
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) ->
                 (divMb : divMb-sig R) -> Set _

PartialDivisionInCommutativeRing? R divMb =

  (a : A) -> (b : A) -> case divMb a b of н╩
                        { (just q) -> (q * b) \~~ a
                        ; nothing  -> (x : A) -> \neg ((x * b) \~~ a)
                        }
  where
  A     = CommutativeRing.Carrier R
  _*_   = CommutativeRing._*_ R
  _\~~_ = CommutativeRing._\~~_ R
-----------------------------------------------------------------------

This `case' means that
if  divMb a b  returns a just value  q  then for these  (a, b)  it must 
return a proof for  (q * b) \~~ a,
otherwise it must return a proof for that  (x * b) \~~ a  has not any 
solution in  x : A. 
The latter proof is respresented as the type  
                                        (x : A) -> \neg ((x * b) \~~ a)
-- that is for each  x : A  the inequality proof is provided.


1. The type checker reports
--------------------------------
.l L-max .c != .l  of type Level                                               
when checking that the expression  ((x : A) -> \neg (x * b) \~~ a) 
has type  Set .l         
--------------------------------

2. Replacing this expression with  \neg (a \~~ b)   
   (which breaks the intended meaning) makes the code type checked.

3. I tried to replace  Set _  in PartialDivisionInCommutativeRing? 
   with  Set (expr c l)
   with various expressions for  expr, 
   like                     L-suc $ L-suc $ setoidLevel c l.
                            where 
                            setoidLevel c l = L-suc (c L-max l).
But this does not help.   

Another question:
for  A : Set l1,  B : Set l1   what is the level of   
                                       A -> B,  A \times B,  List A  ?

Sometimes I try setting  (Set ?),  but Agda does not compute this "?".  

Thank you in advance for explanation.
                        
Sergei.