diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Revision history for dec
 
+## 0.0.5
+
+- Add `boringYes` and `absurdNo`.
+- Add `Decidable a => Boring (Dec a)` instance.
+- Add `Decidable ()`, `Decidable Void`, `Decidable (a, b)` instances.
+
 ## 0.0.4
 
 - Mark module as explicitly `Safe`.
diff --git a/dec.cabal b/dec.cabal
--- a/dec.cabal
+++ b/dec.cabal
@@ -1,6 +1,6 @@
 cabal-version:      >=1.10
 name:               dec
-version:            0.0.4
+version:            0.0.5
 synopsis:           Decidable propositions.
 category:           Data, Dependent Types
 description:
@@ -31,25 +31,28 @@
    || ==8.4.4
    || ==8.6.5
    || ==8.8.4
-   || ==8.10.3
-   || ==9.0.1
+   || ==8.10.4
+   || ==9.0.2
+   || ==9.2.4
+   || ==9.4.1
 
 source-repository head
   type:     git
-  location: https://github.com/phadej/vec.git
-  subdir:   dec
+  location: https://github.com/phadej/dec.git
 
 library
   default-language: Haskell2010
   hs-source-dirs:   src
   ghc-options:      -Wall -fprint-explicit-kinds
   exposed-modules:  Data.Type.Dec
-  build-depends:    base >=4.7 && <4.16
+  build-depends:
+      base    >=4.7 && <4.18
+    , boring  >=0.2 && <0.3
 
   if !impl(ghc >=7.10)
     build-depends: void >=0.7.3 && <0.8
 
-  if impl(ghc >= 9.0)
+  if impl(ghc >=9.0)
     -- these flags may abort compilation with GHC-8.10
     -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
     ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
diff --git a/src/Data/Type/Dec.hs b/src/Data/Type/Dec.hs
--- a/src/Data/Type/Dec.hs
+++ b/src/Data/Type/Dec.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 module Data.Type.Dec (
     -- * Types
     Neg,
@@ -14,9 +15,15 @@
     decShow,
     decToMaybe,
     decToBool,
+
+    -- * Boring
+    -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'.
+    boringYes,
+    absurdNo,
     ) where
 
 import Data.Void (Void)
+import Data.Boring (Absurd (..), Boring (..))
 
 -- | Intuitionistic negation.
 type Neg a = a -> Void
@@ -38,6 +45,32 @@
     decide :: Dec a
 
 -------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+-- | @()@ is truth.
+--
+-- @since 0.0.5
+instance Decidable () where
+    decide = Yes ()
+
+-- | 'Void' is falsehood.
+--
+-- @since 0.0.5
+instance Decidable Void where
+    decide = No id
+
+-- | Products of decidable propositions are decidable
+--
+-- @since 0.0.5
+instance (Decidable a, Decidable b) => Decidable (a, b) where
+    decide = case decide :: Dec a of
+        No nx -> No (\c -> nx (fst c))
+        Yes x -> case decide :: Dec b of
+            No ny -> No (\c -> ny (snd c))
+            Yes y -> Yes (x, y)
+
+-------------------------------------------------------------------------------
 -- Neg combinators
 -------------------------------------------------------------------------------
 
@@ -106,3 +139,25 @@
 decToBool :: Dec a -> Bool
 decToBool (Yes _) = True
 decToBool (No _)  = False
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense.
+--
+-- @since 0.0.5
+instance Decidable a => Boring (Dec a) where
+    boring = decide
+
+-- | 'Yes', it's 'boring'.
+--
+-- @since 0.0.5
+boringYes :: Boring a => Dec a
+boringYes = Yes boring
+
+-- | 'No', it's 'absurd'.
+--
+-- @since 0.0.5
+absurdNo :: Absurd a => Dec a
+absurdNo = No absurd