# [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
```