    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Apartness properties
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Core using (Rel)

    module Relation.Binary.Properties.ApartnessRelation
      {a ℓ₁ ℓ₂} {A : Set a}
      {_≈_ : Rel A ℓ₁}
      {_#_ : Rel A ℓ₂}
      where

    open import Function.Base using (_∘₂_)
    open import Relation.Binary.Definitions using (Reflexive)
    open import Relation.Binary.Consequences using (sym⇒¬-sym; cotrans⇒¬-trans)
    open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
    open import Relation.Nullary.Negation using (¬_)

    ¬#-isEquivalence : Reflexive _≈_ → IsApartnessRelation _≈_ _#_ →
                       IsEquivalence (¬_ ∘₂ _#_)
    ¬#-isEquivalence re apart = record
      { refl = irrefl re
      ; sym = λ {a} {b} → sym⇒¬-sym sym {a} {b}
      ; trans = cotrans⇒¬-trans cotrans
      } where open IsApartnessRelation apart