[Agda] partial division property

[Serge D. Mechveliani]

On Sun, Nov 04, 2012 at 09:09:48PM +0400, Serge D. Mechveliani wrote:
> [..]
> 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 \lambda
>                         { (just q) -> (q * b) \~~ a
>                         ; nothing  -> (x : A) -> \neg ((x * b) \~~ a)
>                         }
>   where
>   A     = CommutativeRing.Carrier R
>   _*_   = CommutativeRing._*_ R
>   _\~~_ = CommutativeRing._\~~_ R
> -----------------------------------------------------------------------
> [..]
> 
> 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         
> --------------------------------

Then, I lifted  " let A = CommutativeRing.Carrier R in  A -> A -> A "  
to the signature of PartialDivisionInCommutativeRing?
and added   " (a b x : A)"  to its arguments. 
This way it does work.

But the initial definition 
1) looks more natural (because  x  is not used in the `just' branch),
2) I do not know, may be a subject for curiosity, or may present a bug 
   in Agda.

Regards,
Sergei.