[Agda] "No instance"

[Guillermo Calderón]

Hi,

You have to declare S and S'  as Setoid instances:


------------------------------------------------------------
instance
     foo1 : Setoid _ _
     foo1 = S
     foo2 : Setoid
     foo2 = S'
------------------------------------------------------------

Names and types can be omitted:

------------------------------------------------------------
instance
     _ = S
     _ = S'
------------------------------------------------------------

Best regards,

Guillermo

On 17/11/18 08:35, Sergei Meshveliani wrote:
> Please, what it wrong here?
> 
> ----------------------------------------------------------------------
> open import Level using (suc; _⊔_)
> open import Relation.Binary using (Rel; IsEquivalence; _Preserves_⟶_)
> open import Data.Product using (Σ)
> 
> record Setoid {α} α= (Carrier : Set α) :  Set (suc (α ⊔ α=))  where
>    infix 4 _≈_
>    field
>      _≈_           : Rel Carrier α=
>      isEquivalence : IsEquivalence _≈_
> 
> 
> module _ {α α= β β=} {C : Set α} {C' : Set β}
>                       (S : Setoid α= C) (S' : Setoid β= C')
>    where
>    open Setoid {{...}}
> 
>    CongruentMap :  Set _
>    CongruentMap =  Σ (C → C') (\f → f Preserves _≈_ ⟶ _≈_)
> ---------------------------------------------------------------
> 
> Agda 2.6.0-c5cbc7e :
> 
> "No instance of type Setoid _ℓ₁_29 C was found in scope.
> when checking that the expression _≈_ has type Rel C _ℓ₁_29
> "
> 
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>