------------------------------------------------------------------------ -- The Agda standard library -- -- Wrapper for the proof irrelevance modality -- -- This allows us to store proof irrelevant witnesses in a record and -- use projections to manipulate them without having to turn on the -- unsafe option --irrelevant-projections. -- Cf. Data.Refinement for a use case ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Irrelevant where open import Level using (Level) private variable a b c : Level A : Set a B : Set b C : Set c ------------------------------------------------------------------------ -- Type record Irrelevant (A : Set a) : Set a where constructor [_] field .irrelevant : A open Irrelevant public ------------------------------------------------------------------------ -- Algebraic structure: Functor, Appplicative and Monad-like map : (A → B) → Irrelevant A → Irrelevant B map f [ a ] = [ f a ] pure : A → Irrelevant A pure x = [ x ] infixl 4 _<*>_ _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B [ f ] <*> [ a ] = [ f a ] infixl 1 _>>=_ _>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B [ a ] >>= f = f a ------------------------------------------------------------------------ -- Other functions zipWith : (A → B → C) → Irrelevant A → Irrelevant B → Irrelevant C zipWith f a b = ⦇ f a b ⦈