[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.
More information about the Agda
mailing list