{-# OPTIONS --safe #-}
open import Axiom.Set using (Theory)
module abstract-set-theory.Axiom.Set.Map.Extra (th : Theory) where
open import abstract-set-theory.Prelude using (Type; ¬_)
open import Axiom.Set.Map th
private variable
A : Type
B : Type
infix 4 _≢ᵐ_
_≢ᵐ_ : Map A B → Map A B → Type
a ≢ᵐ b = ¬ a ≡ᵐ b