------------------------------------------------------------------------
-- 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."
#-}