------------------------------------------------------------------------
-- The Agda standard library
--
-- Notation for freely adding extrema to any set
------------------------------------------------------------------------

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

module Relation.Nullary.Construct.Add.Extrema where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Nullary.Construct.Add.Infimum  as Infimum  using (_₋)
open import Relation.Nullary.Construct.Add.Supremum as Supremum using (_⁺)

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

_± : ∀ {a} → Set a → Set a
A ± = A ₋ ⁺

pattern ⊥±    = Supremum.[ Infimum.⊥₋ ]
pattern [_] k = Supremum.[ Infimum.[ k ] ]
pattern ⊤±    = Supremum.⊤⁺

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

[_]-injective : ∀ {a} {A : Set a} {k l : A} → [ k ] ≡ [ l ] → k ≡ l
[_]-injective refl = refl