------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of refinement types
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Refinement.Properties where
open import Data.Refinement.Base
open import Level using (Level; _⊔_)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
import Relation.Nullary.Decidable.Core as Dec
private
variable
a p : Level
A : Set a
P : A → Set p
v w : [ x ∈ A ∣ P x ]
------------------------------------------------------------------------
-- Basic properties
value-injective : value v ≡ value w → v ≡ w
value-injective refl = refl
module _ (eq? : DecidableEquality A) where
infix 4 _≟_
_≟_ : DecidableEquality [ x ∈ A ∣ P x ]
v ≟ w = Dec.map′ value-injective (cong value) (eq? (value v) (value w))
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4