diff --git a/doc/standard-library-doc.agda-lib b/doc/standard-library-doc.agda-lib
index 02aaaba402..67c3ecf8b2 100644
--- a/doc/standard-library-doc.agda-lib
+++ b/doc/standard-library-doc.agda-lib
@@ -2,3 +2,4 @@ name: standard-library-doc
 include: . ../src
 flags:
   --warning=noUnsupportedIndexedMatch
+  --prop
diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index d2647a1f18..d32bf2fbbd 100644
--- a/src/Data/Empty.agda
+++ b/src/Data/Empty.agda
@@ -18,23 +18,31 @@ open import Data.Irrelevant using (Irrelevant)
 -- universe polymorphic variant.
 
 private
-  data Empty : Set where
+  data Empty : Prop where
 
 -- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant
 -- field) so that Agda can judgementally declare that all proofs of ⊥
 -- are equal to each other. In particular this means that all functions
 -- returning a proof of ⊥ are equal.
 
-⊥ : Set
-⊥ = Irrelevant Empty
+record ⊥ : Set where
+  constructor [_]
+  field
+    empty : Empty
+open ⊥ public
 
 {-# DISPLAY Irrelevant Empty = ⊥ #-}
 
 ------------------------------------------------------------------------
 -- Functions
 
+private
+  empty-elim : ∀ {w} {Whatever : Set w} → .Empty → Whatever
+  empty-elim ()
+
 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
-⊥-elim ()
+⊥-elim x = empty-elim (empty x)
 
 ⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
-⊥-elim-irr ()
+⊥-elim-irr x = empty-elim (empty x)
+
diff --git a/src/Data/Irrelevant.agda b/src/Data/Irrelevant.agda
index 7701cfc82e..1a9ebcbb27 100644
--- a/src/Data/Irrelevant.agda
+++ b/src/Data/Irrelevant.agda
@@ -14,6 +14,7 @@
 module Data.Irrelevant where
 
 open import Level using (Level)
+open import Data.Squash as Squash using (Squash; squash)
 
 private
   variable
@@ -27,25 +28,26 @@ private
 
 record Irrelevant (A : Set a) : Set a where
   constructor [_]
-  field .irrelevant : A
+  field
+    irrelevant : Squash A
 open Irrelevant public
 
 ------------------------------------------------------------------------
 -- Algebraic structure: Functor, Appplicative and Monad-like
 
 map : (A → B) → Irrelevant A → Irrelevant B
-map f [ a ] = [ f a ]
+map f [ a ] = [ Squash.map f a ]
 
 pure : A → Irrelevant A
-pure x = [ x ]
+pure x = [ squash x ]
 
 infixl 4 _<*>_
 _<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
-[ f ] <*> [ a ] = [ f a ]
+[ f ] <*> [ a ] = [ f Squash.<*> a ]
 
 infixl 1 _>>=_
-_>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B
-[ a ] >>= f = f a
+_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
+[ a ] >>= f = [ a Squash.>>= (λ x → irrelevant (f x)) ]
 
 ------------------------------------------------------------------------
 -- Other functions
diff --git a/src/Data/Squash.agda b/src/Data/Squash.agda
new file mode 100644
index 0000000000..1b1e7afa42
--- /dev/null
+++ b/src/Data/Squash.agda
@@ -0,0 +1,44 @@
+------------------------------------------------------------------------
+-- 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.Squash where
+
+open import Level using (Level)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Type
+
+data Squash (A : Set a) : Prop a where
+  squash : A → Squash A
+
+------------------------------------------------------------------------
+-- Algebraic structure: Functor, Appplicative and Monad-like
+
+map : (A → B) → Squash A → Squash B
+map f (squash x) = squash (f x)
+
+infixl 4 _<*>_
+_<*>_ : Squash (A → B) → Squash A → Squash B
+squash f <*> squash x = squash (f x)
+
+infixl 1 _>>=_
+_>>=_ : Squash A → (A → Squash B) → Squash B
+squash x >>= f = f x
+
diff --git a/src/Relation/Nullary/Recomputable.agda b/src/Relation/Nullary/Recomputable.agda
index a7671b339c..929854a883 100644
--- a/src/Relation/Nullary/Recomputable.agda
+++ b/src/Relation/Nullary/Recomputable.agda
@@ -9,7 +9,7 @@
 module Relation.Nullary.Recomputable where
 
 open import Data.Empty using (⊥)
-open import Data.Irrelevant using (Irrelevant; irrelevant; [_])
+open import Data.Irrelevant using (Irrelevant; [_])
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
 open import Relation.Nullary.Negation.Core using (¬_)
@@ -29,15 +29,10 @@ open import Relation.Nullary.Recomputable.Core public
 ------------------------------------------------------------------------
 -- Constructions
 
--- Irrelevant types are Recomputable
-
-irrelevant-recompute : Recomputable (Irrelevant A)
-irrelevant (irrelevant-recompute [ a ]) = a
-
--- Corollary: so too is ⊥
+-- ⊥ is Recomputable
 
 ⊥-recompute : Recomputable ⊥
-⊥-recompute = irrelevant-recompute
+⊥-recompute ()
 
 _×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
 (rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
diff --git a/standard-library.agda-lib b/standard-library.agda-lib
index 89a8058e04..b8fb715e30 100644
--- a/standard-library.agda-lib
+++ b/standard-library.agda-lib
@@ -2,3 +2,4 @@ name: standard-library-2.4
 include: src
 flags:
   --warning=noUnsupportedIndexedMatch
+  --prop