------------------------------------------------------------------------
-- 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