[Agda] partial division property

Serge D. Mechveliani mechvel at botik.ru
Mon Nov 5 13:00:54 CET 2012

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.