[Agda] "No instance"

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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 _≈_ ⟶ _≈_)
---------------------------------------------------------------
"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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Sergei Meshveliani
Hi,
------------------------------------------------------------
instance
foo1 : Setoid _ _
foo1 = S
foo2 : Setoid
foo2 = S'
------------------------------------------------------------
------------------------------------------------------------
instance
_ = S
_ = S'
------------------------------------------------------------

It helps. Thank you!

------
Sergei

Post by Sergei Meshveliani

Post by Sergei Meshveliani
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 _≈_ ⟶ _≈_)
---------------------------------------------------------------
"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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda