[Agda] finite map

[Sergei Meshveliani]

People,
I have   A : Setoid α α=,  aC = Setoid.Carrier A,  B : Setoid β β=,
         bC = Setoid.Carrier B,

and need to operate with finite maps  f : aC → bC :

membership, lookup, insertion, union, equality.
O(n) lookup/insert  is sufficient, so far.

Has Standard library something ready for this?

Need I to add a number  i : ℕ,  to make pairs  (x , i) : aC × ℕ
compared _<_  by  i,  and to use  AVL  over the TotalOrder key domain of
aC × ℕ
?
(one can consider Bin instead of ℕ).

Thanks,

------
Sergei