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

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

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

    open import Relation.Binary.Core using (Rel)

    module Relation.Binary.Construct.Add.Infimum.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
      )