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

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)

{a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Function.Base using (_∘′_)

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

private

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