------------------------------------------------------------------------
-- The Agda standard library
--
-- Refinement type: a value together with a proof irrelevant witness.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Refinement.Base where
open import Data.Irrelevant as Irrelevant using (Irrelevant)
open import Function.Base using (id)
open import Level using (Level; _⊔_)
open import Relation.Unary using (IUniversal; _⇒_; _⊢_)
private
variable
a b p q : Level
A : Set a
B : Set b
P : A → Set p
------------------------------------------------------------------------
-- Definition
record Refinement (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
constructor _,_
field value : A
proof : Irrelevant (P value)
infixr 4 _,_
open Refinement public
-- The syntax declaration below is meant to mimic set comprehension.
-- It is attached to Refinement-syntax, to make it easy to import
-- Data.Refinement without the special syntax.
infix 2 Refinement-syntax
Refinement-syntax = Refinement
syntax Refinement-syntax A (λ x → P) = [ x ∈ A ∣ P ]
------------------------------------------------------------------------
-- Basic operations
module _ {Q : B → Set q} where
map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
[ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
map f prf (a , p) = f a , Irrelevant.map prf p
module _ {Q : A → Set q} where
refine : ∀[ P ⇒ Q ] → [ a ∈ A ∣ P a ] → [ a ∈ A ∣ Q a ]
refine = map id
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