[ irrelevant-projections ] clean version of #3012

src/Data/Irrelevant.agda

@@ -14,7 +14,6 @@
 module Data.Irrelevant where
 
 open import Level using (Level)
-open import Relation.Nullary.Recomputable.Core using (Recomputable)
 
 private
   variable
@@ -32,23 +31,20 @@ record Irrelevant (A : Set a) : Set a where
 open Irrelevant public
 
 ------------------------------------------------------------------------
--- Relationship with the . modality: wrapped/unwrapped abstraction
+-- Relationship with the . modality: wrapped/unwrapped application
 
-λ∙⁻ : (.A → B) → Irrelevant A → B
-λ∙⁻ f [ a ] = f a
-{-# INLINE λ∙⁻ #-}
+infixr -1 _$⁺_ _$⁻_
 
-λ∙⁺ : (Irrelevant A → B) → .A → B
-λ∙⁺ f a = f [ a ]
-{-# INLINE λ∙⁺ #-}
+_$⁺_ : (.A → B) → Irrelevant A → B
+f $⁺ [ a ] = f a
+{-# INLINE _$⁺_ #-}
 
--- Irrelevant types are Recomputable
-
-recompute : Recomputable (Irrelevant A)
-irrelevant (recompute [ a ]) = a
+_$⁻_ : (Irrelevant A → B) → .A → B
+f $⁻ a = f [ a ]
+{-# INLINE _$⁻_ #-}
 
 ------------------------------------------------------------------------
--- Algebraic structure: Functor, Appplicative and Monad
+-- Algebraic structure: Functor, Appplicative and Monad-like
 
 map : (A → B) → Irrelevant A → Irrelevant B
 map f [ a ] = [ f a ]
@@ -61,8 +57,8 @@ _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
 [ f ] <*> [ a ] = [ f a ]
 
 infixl 1 _>>=_
-_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
-[ a ] >>= f = recompute (f a)
+_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = f a
 
 ------------------------------------------------------------------------
 -- Other functions

src/Data/Irrelevant/Unsafe.agda

@@ -0,0 +1,35 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe properties of the proof irrelevance modality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --irrelevant-projections #-}
+
+module Data.Irrelevant.Unsafe where
+
+open import Data.Irrelevant hiding (_>>=_)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+
+------------------------------------------------------------------------
+-- Irrelevant types are Recomputable
+
+open import Relation.Nullary.Recomputable.Unsafe public
+  using () renaming (irrelevant-recompute to recompute)
+
+------------------------------------------------------------------------
+-- Algebraic structure: Monadic bind and join
+
+join : Irrelevant (Irrelevant A) → Irrelevant A
+join = recompute $⁺_
+
+infixl 1 _>>=_
+_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = recompute (f a)

src/Relation/Nullary/Recomputable.agda

@@ -20,20 +20,15 @@ private
     B : Set b
 
 ------------------------------------------------------------------------
--- Re-export core definitions
+-- Re-export
 
 open import Relation.Nullary.Recomputable.Core public
 
--- Irrelevant types are Recomputable
-
-open import Data.Irrelevant public
-  using () renaming (recompute to irrelevant-recompute)
-
 ------------------------------------------------------------------------
 -- Constructions
 
 ⊥-recompute : Recomputable ⊥
-⊥-recompute = irrelevant-recompute
+⊥-recompute ()
 
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
@@ -51,4 +46,3 @@ _→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B)
 
 ¬-recompute : Recomputable (¬ A)
 ¬-recompute {A = A} = A →-recompute ⊥-recompute
-

src/Relation/Nullary/Recomputable/Unsafe.agda

@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Irrelevant types are Recomputable
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --irrelevant-projections #-}
+
+module Relation.Nullary.Recomputable.Unsafe where
+
+open import Data.Irrelevant using (Irrelevant; irrelevant)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+
+------------------------------------------------------------------------
+-- Re-export
+
+open import Relation.Nullary.Recomputable public
+
+------------------------------------------------------------------------
+-- Constructions
+
+-- Irrelevant types are Recomputable
+
+irrelevant-recompute : Recomputable (Irrelevant A)
+irrelevant (irrelevant-recompute a) = irrelevant a