------------------------------------------------------------------------
-- The Agda standard library
--
-- A pointwise lifting of a relation to incorporate new extrema.
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Extrema

open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures
  using (IsEquivalence; IsDecEquivalence)
open import Relation.Binary.Definitions
  using (Reflexive; Symmetric; Transitive; Decidable; Irrelevant; Substitutive)

module Relation.Binary.Construct.Add.Extrema.Equality
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Function.Base using (_∘′_)
import Relation.Binary.Construct.Add.Infimum.Equality as AddInfimum
import Relation.Binary.Construct.Add.Supremum.Equality as AddSupremum
open import Relation.Nullary.Construct.Add.Extrema

------------------------------------------------------------------------
-- Definition

private
  module Inf = AddInfimum _≈_
  module Sup = AddSupremum (Inf._≈₋_)

open Sup using () renaming (_≈⁺_ to _≈±_) public

------------------------------------------------------------------------
-- Useful pattern synonyms

pattern ⊥±≈⊥± = Sup.[ Inf.⊥₋≈⊥₋ ]
pattern [_] p = Sup.[ Inf.[ p ] ]
pattern ⊤±≈⊤± = Sup.⊤⁺≈⊤⁺

------------------------------------------------------------------------
-- Relational properties

[≈]-injective : ∀ {k l} → [ k ] ≈± [ l ] → k ≈ l
[≈]-injective = Inf.[≈]-injective ∘′ Sup.[≈]-injective

≈±-refl : Reflexive _≈_ → Reflexive _≈±_
≈±-refl = Sup.≈⁺-refl ∘′ Inf.≈₋-refl

≈±-sym : Symmetric _≈_ → Symmetric _≈±_
≈±-sym = Sup.≈⁺-sym ∘′ Inf.≈₋-sym

≈±-trans : Transitive _≈_ → Transitive _≈±_
≈±-trans = Sup.≈⁺-trans ∘′ Inf.≈₋-trans

≈±-dec : Decidable _≈_ → Decidable _≈±_
≈±-dec = Sup.≈⁺-dec ∘′ Inf.≈₋-dec

≈±-irrelevant : Irrelevant _≈_ → Irrelevant _≈±_
≈±-irrelevant = Sup.≈⁺-irrelevant ∘′ Inf.≈₋-irrelevant

≈±-substitutive : ∀ {ℓ} → Substitutive _≈_ ℓ → Substitutive _≈±_ ℓ
≈±-substitutive = Sup.≈⁺-substitutive ∘′ Inf.≈₋-substitutive

------------------------------------------------------------------------
-- Structures

≈±-isEquivalence : IsEquivalence _≈_ → IsEquivalence _≈±_
≈±-isEquivalence = Sup.≈⁺-isEquivalence ∘′ Inf.≈₋-isEquivalence

≈±-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence _≈±_
≈±-isDecEquivalence = Sup.≈⁺-isDecEquivalence ∘′ Inf.≈₋-isDecEquivalence