[Agda] Boolean And in Pair

[mechvel at scico.botik.ru]

On 2020-05-03 19:50, Philippe de Rochambeau wrote:
> Hello,
> 
> when I load the following script, I get a « not in scope ∧ »
> error.
> Why is that?
> Furthermore, how can I make the _eq_ function generic, whichever the
> types used in the Pair, as long as the first type is equal to the
> second?
> Many thanks.
> Philippe
> 
> open import Agda.Builtin.Nat
> open import Agda.Builtin.String
> open import Agda.Builtin.Bool
> 
> record Pair (A B : Set) : Set where
>   field
>     fst : A
>     snd : B
> 
> _eq_ : (a : Pair Nat Nat) → (b : Pair Nat Nat) → Bool
> a eq b = (Pair.fst a == Pair.fst b) ∧ (Pair.snd a == Pair.snd b)


If you add

open import Data.Bool using (_∧_)

then it is type-checked.
But I never used "Agda.Builtin" explicitly, and do not know what is the 
goal.

Regards,

------
Sergei