# [Agda] partial division property

Serge D. Mechveliani mechvel at botik.ru
Sun Nov 4 18:09:48 CET 2012

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.
`