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