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

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

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

    open import Relation.Binary.Core using (Rel)

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

    open import Relation.Binary.Construct.Add.Point.Equality _≈_ public
      renaming
      (_≈∙_                 to _≈⁺_
      ; ∙≈∙                 to ⊤⁺≈⊤⁺
      ; ≈∙-refl             to ≈⁺-refl
      ; ≈∙-sym              to ≈⁺-sym
      ; ≈∙-trans            to ≈⁺-trans
      ; ≈∙-dec              to ≈⁺-dec
      ; ≈∙-irrelevant       to ≈⁺-irrelevant
      ; ≈∙-substitutive     to ≈⁺-substitutive
      ; ≈∙-isEquivalence    to ≈⁺-isEquivalence
      ; ≈∙-isDecEquivalence to ≈⁺-isDecEquivalence
      )