[Agda] Decidable _\~~_ of Semiring
Serge D. Mechveliani
mechvel at botik.ru
Fri Nov 9 12:42:52 CET 2012
Please, what is wrong in the following program?
(for Agda-2.3.0.1, MAlonzo, lib-0.6, lib-0.6 used heavily)
------------------------------------------------------------------------
...
open import Relation.Unary using ( Decidable )
open import Algebra using ( Semiring; module Semiring; ...
)
open import Relation.Binary using
( IsDecEquivalence; module IsDecEquivalence )
test : {c l : Level} -> {R : Semiring c l} ->
let open Semiring {{...}}
C = Carrier
in
C ->
IsDecEquivalence {A = C} _~~_ -> -- (1)
-- Decidable {A = C} _~~_ -> -- (2)
C
test x
isDE = -- (1)
-- eq = -- (2)
case eq x 0# of н╩ { (yes _) -> 0# ; _ -> 1# }
where
open Semiring {{...}}
eq = IsDecEquivalence._?=_ isDE -- (1)
------------------------------------------------------------------------
-- here I replace the math symbols as \~~ -> ~~, \?= -> ?=
Now I need to simplify this varant (1) to variant (2).
Because
1) IsDecEquivalence {A : Set A} _~~_
has the fields isEquivalence : IsEquivalence _~~_
_?=_ : Decidable _~~_,
2) `test' uses only the field ?=,
it does not need checking isEquivalence, because it takes _~~_
from R : Semiring _ _,
and there _~~_ is declared as an equivalence,
3) so, instead of isDE, `test' needs only
eq : Decidable {A = C} _~~_, where _~~_ is of R.
Right?
So I comment out the three lines marked by (1)
and un-comment the two lines marked by (2).
The checker reports
(Semiring.Carrier R -> Set l) !=< (Set _540) of type
(Set (L-suc l L-max c))
when checking that the expression _~~_ has type (Carrier -> Set _540)
for the line of " Decidable {A = C} _~~_ -> "
Skipping here {A = C} does not change this.
So, for _~~_ taken from R we have that
1) _?=_ : Decidable _~~_ is accepted in IsDecEquivalence
2) Decidable _~~_ is rejected in the signature of `test'.
This looks like a contradiction. How to fix the variant (2) ?
Thank you in advance for explanation,
------
Sergei
More information about the Agda
mailing list