    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Reflexive closures
    ------------------------------------------------------------------------

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

    module Relation.Binary.Construct.Closure.Reflexive where

    open import Data.Unit.Base
    open import Level
    open import Function.Base using (_∋_)
    open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
    open import Relation.Binary.Definitions using (Reflexive)
    open import Relation.Binary.Construct.Constant.Core using (Const)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)

    private
      variable
        a ℓ ℓ₁ ℓ₂ : Level
        A B : Set a

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

    data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
      refl : Reflexive (ReflClosure _∼_)
      [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y

    ------------------------------------------------------------------------
    -- Operations

    map : ∀ {R : Rel A ℓ₁} {S : Rel B ℓ₂} {f : A → B} →
          R =[ f ]⇒ S → ReflClosure R =[ f ]⇒ ReflClosure S
    map R⇒S [ xRy ] = [ R⇒S xRy ]
    map R⇒S refl    = refl

    ------------------------------------------------------------------------
    -- Properties

    -- The reflexive closure has no effect on reflexive relations.
    drop-refl : {R : Rel A ℓ} → Reflexive R → ReflClosure R ⇒ R
    drop-refl rfl [ xRy ] = xRy
    drop-refl rfl refl    = rfl

    reflexive : {R : Rel A ℓ} → _≡_ ⇒ ReflClosure R
    reflexive refl = refl

    []-injective : {R : Rel A ℓ} → ∀ {x y p q} →
                   (ReflClosure R x y ∋ [ p ]) ≡ [ q ] → p ≡ q
    []-injective refl = refl

    ------------------------------------------------------------------------
    -- Example usage

    private
      module Maybe where
        Maybe : Set a → Set a
        Maybe A = ReflClosure (Const A) tt tt

        nothing : Maybe A
        nothing = refl

        just : A → Maybe A
        just = [_]

    ------------------------------------------------------------------------
    -- Deprecations
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- v1.5

    Refl = ReflClosure
    {-# WARNING_ON_USAGE Refl
    "Warning: Refl was deprecated in v1.5.
    Please use ReflClosure instead."
    #-}