{-# 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
data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
refl : Reflexive (ReflClosure _∼_)
[_] : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y
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
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
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 = [_]
Refl = ReflClosure
{-# WARNING_ON_USAGE Refl
"Warning: Refl was deprecated in v1.5.
Please use ReflClosure instead."
#-}