Another Prop experiment

src/Data/Bool/Base.agda

@@ -8,8 +8,8 @@
 
 module Data.Bool.Base where
 
-open import Data.Unit.Base using (⊤)
-open import Data.Empty using (⊥)
+open import Data.Unit.Base using (⊤ₚ)
+open import Data.Empty using (⊥ₚ)
 open import Level using (Level)
 
 private
@@ -57,13 +57,13 @@ true  xor b = not b
 false xor b = b
 
 ------------------------------------------------------------------------
--- Conversion to Set
+-- Conversion to Prop
 
 -- A function mapping true to an inhabited type and false to an empty
 -- type.
-T : Bool → Set
-T true  = ⊤
-T false = ⊥
+T : Bool → Prop
+T true  = ⊤ₚ
+T false = ⊥ₚ
 
 ------------------------------------------------------------------------
 -- Other operations

src/Data/Empty.agda

@@ -8,8 +8,6 @@
 
 module Data.Empty where
 
-open import Data.Irrelevant using (Irrelevant)
-
 ------------------------------------------------------------------------
 -- Definition
 
@@ -20,15 +18,16 @@ open import Data.Irrelevant using (Irrelevant)
 private
   data Empty : Set 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.
+-- ⊥ is defined a record with a single irrelevant 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
+data ⊥ₚ : Prop where
 
-{-# DISPLAY Irrelevant Empty = ⊥ #-}
+-- TOOD: make a generic Prop → Set record
+record ⊥ : Set where
+  constructor [_]
+  field bot : ⊥ₚ
 
 ------------------------------------------------------------------------
 -- Functions

src/Data/Unit/Base.agda

@@ -19,3 +19,9 @@ module Data.Unit.Base where
 
 open import Agda.Builtin.Unit public
   using (⊤; tt)
+
+------------------------------------------------------------------------
+-- A propositional variant of ⊤
+
+record ⊤ₚ : Prop where
+  instance constructor tt

standard-library.agda-lib

@@ -1,2 +1,3 @@
 name: standard-library-3.0
 include: src
+flags: --prop