bimap -package:base-prelude -is:module package:Agda

Finite maps from k to v, with a way to quickly get from v to k for certain values of type v (those for which tag is defined). Every value of this type must satisfy biMapInvariant.
The invariant for BiMap.