Source code on Github
------------------------------------------------------------------------
-- 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

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