[Agda] partial division property
Serge D. Mechveliani
mechvel at botik.ru
Mon Nov 5 10:51:13 CET 2012
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.
More information about the Agda
mailing list