diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Revision history for dec
+
+## 0.0.3
+
+- First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019, Oleg Grenrus
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Oleg Grenrus nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/dec.cabal b/dec.cabal
new file mode 100644
--- /dev/null
+++ b/dec.cabal
@@ -0,0 +1,42 @@
+cabal-version:      >=1.10
+name:               dec
+version:            0.0.3
+synopsis:           Decidable propositions.
+category:           Data, Dependent Types
+description:
+  This package provides a @Dec@ type.
+  .
+  @
+  type Not a = a -> Void
+  .
+  data Dec a
+  \    = Yes a
+  \    | No (Not a)
+  @
+
+homepage:           https://github.com/phadej/vec
+bug-reports:        https://github.com/phadej/vec/issues
+license:            BSD3
+license-file:       LICENSE
+author:             Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
+copyright:          (c) 2019 Oleg Grenrus
+build-type:         Simple
+extra-source-files: ChangeLog.md
+tested-with:
+  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4
+
+source-repository head
+  type:     git
+  location: https://github.com/phadej/vec.git
+
+library
+  exposed-modules:  Data.Type.Dec
+  build-depends:    base >=4.7 && <4.13
+
+  if !impl(ghc >=7.10)
+    build-depends: void >=0.7.2 && <0.8
+
+  ghc-options:      -Wall -fprint-explicit-kinds
+  hs-source-dirs:   src
+  default-language: Haskell2010
diff --git a/src/Data/Type/Dec.hs b/src/Data/Type/Dec.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Dec.hs
@@ -0,0 +1,107 @@
+module Data.Type.Dec (
+    -- * Types
+    Neg,
+    Dec (..),
+    Decidable (..),
+    -- * Neg combinators
+    toNegNeg,
+    tripleNeg,
+    contradict,
+    contraposition,
+    -- * Dec combinators
+    decNeg,
+    decShow,
+    decToMaybe,
+    decToBool,
+    ) where
+
+import Data.Void          (Void)
+
+-- | Intuitionistic negation.
+type Neg a = a -> Void
+
+-- | Decidable (nullary) relations.
+data Dec a
+    = Yes a
+    | No (Neg a)
+
+-- | Class of decidable types.
+--
+-- == Law
+--
+-- @a@ should be a Proposition, i.e. the 'Yes' answers should be unique.
+--
+-- /Note:/ We'd want to have decidable equality @:~:@ here too,
+-- but that seems to be a deep dive into singletons.
+class Decidable a where
+    decide :: Dec a
+
+-------------------------------------------------------------------------------
+-- Neg combinators
+-------------------------------------------------------------------------------
+
+-- | We can negate anything twice.
+--
+-- Double-negation elimination is inverse of 'toNegNeg' and generally
+-- impossible.
+toNegNeg :: a -> Neg (Neg a)
+toNegNeg x = ($ x)
+
+-- | Triple negation can be reduced to a single one.
+tripleNeg :: Neg (Neg (Neg a)) -> Neg a
+tripleNeg f a = f (toNegNeg a)
+
+-- | Weak contradiction.
+contradict :: (a -> Neg b) -> b -> Neg a
+contradict f b a = f a b
+
+-- | A variant of contraposition.
+contraposition :: (a -> b) -> Neg b -> Neg a
+contraposition f nb a = nb (f a)
+
+-------------------------------------------------------------------------------
+-- Dec combinators
+-------------------------------------------------------------------------------
+
+instance Eq a => Eq (Dec a) where
+    Yes x == Yes y = x == y
+    Yes _ == No _   = False
+    No _  == Yes _  = False
+    No _  == No _   = True  -- @'Not a' is a /h-Prop/ so all values are equal.
+
+-- | 'decToBool' respects this ordering.
+--
+-- /Note:/ yet if you have @p :: a@ and @p :: 'Neg' a@, something is wrong.
+--
+instance Ord a => Ord (Dec a) where
+    compare (Yes a) (Yes b) = compare a b
+    compare (No _)  (Yes _) = compare False True
+    compare (Yes _) (No _)  = compare True False
+    compare (No _)  (No _)  = EQ
+
+-- | Flip 'Dec' branches.
+decNeg :: Dec a -> Dec (Neg a)
+decNeg (Yes p) = No (toNegNeg p)
+decNeg (No np) = Yes np
+
+-- | Show 'Dec'.
+--
+-- >>> decShow $ Yes ()
+-- "Yes ()"
+--
+-- >>> decShow $ No id
+-- "No <toVoid>"
+--
+decShow :: Show a => Dec a -> String
+decShow (Yes x) = "Yes " ++ showsPrec 11 x ""
+decShow (No _)  = "No <toVoid>"
+
+-- | Convert @'Dec' a@ to @'Maybe' a@, forgetting the 'No' evidence.
+decToMaybe :: Dec a -> Maybe a
+decToMaybe (Yes p) = Just p
+decToMaybe (No _)  = Nothing
+
+-- | Convert 'Dec' to 'Bool', forgetting the evidence.
+decToBool :: Dec a -> Bool
+decToBool (Yes _) = True
+decToBool (No _)  = False