------------------------------------------------------------------------
-- The Agda standard library
--
-- Every decidable setoid induces tight apartness relation.
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (DecSetoid; ApartnessRelation)

module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where

open import Data.Product using (_,_)
open import Data.Sum using (inj₁; inj₂)
open import Relation.Binary.Definitions
  using (Cotransitive; Tight)
import Relation.Binary.Properties.Setoid as SetoidProperties
open import Relation.Binary.Structures
  using (IsApartnessRelation; IsDecEquivalence)
open import Relation.Nullary.Decidable.Core
  using (yes; no; decidable-stable)

open DecSetoid S using (_≈_; _≉_; _≟_; setoid; trans)
open SetoidProperties setoid

≉-cotrans : Cotransitive _≉_
≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
... | _ | no z≉y = inj₂ z≉y
... | no x≉z | _ = inj₁ x≉z
... | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y)

≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
≉-isApartnessRelation = record
  { irrefl = ≉-irrefl
  ; sym = ≉-sym
  ; cotrans = ≉-cotrans
  }

≉-apartnessRelation : ApartnessRelation c ℓ ℓ
≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }

≉-tight : Tight _≈_ _≉_
≉-tight x y = decidable-stable (x ≟ y) , ≉-irrefl