diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,15 @@
+ISC License
+
+Copyright (c) 2023 Gautier DI FOLCO
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY
+AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM
+LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR
+OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR
+PERFORMANCE OF THIS SOFTWARE.
diff --git a/kill-bool.cabal b/kill-bool.cabal
new file mode 100644
--- /dev/null
+++ b/kill-bool.cabal
@@ -0,0 +1,84 @@
+cabal-version:       3.0
+name:                kill-bool
+version:             0.1.0.0
+author:              Gautier DI FOLCO
+maintainer:          gautier.difolco@gmail.com
+category:            Data
+build-type:          Simple
+license:             ISC
+license-file:        LICENSE
+synopsis:            Boolean strong typing
+description:         Makes sense of your booleans: strong type them!
+Homepage:            https://github.com/blackheaven/kill-bool
+tested-with:         GHC==9.2.4
+
+library
+  default-language:   Haskell2010
+  build-depends:
+      base == 4.*
+  hs-source-dirs: src
+  exposed-modules:
+      Data.Bool.Kill
+  other-modules:
+      Paths_kill_bool
+  autogen-modules:
+      Paths_kill_bool
+  default-extensions:
+      DataKinds
+      DefaultSignatures
+      DeriveAnyClass
+      DeriveGeneric
+      DerivingStrategies
+      DerivingVia
+      DuplicateRecordFields
+      FlexibleContexts
+      GADTs
+      GeneralizedNewtypeDeriving
+      KindSignatures
+      LambdaCase
+      OverloadedStrings
+      OverloadedRecordDot
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints
+
+test-suite kill-bool-test
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Spec.hs
+  other-modules:
+      Paths_kill_bool
+  autogen-modules:
+      Paths_kill_bool
+  default-extensions:
+      DataKinds
+      DefaultSignatures
+      DeriveAnyClass
+      DeriveGeneric
+      DerivingStrategies
+      DerivingVia
+      DuplicateRecordFields
+      FlexibleContexts
+      GADTs
+      GeneralizedNewtypeDeriving
+      KindSignatures
+      LambdaCase
+      OverloadedStrings
+      OverloadedRecordDot
+      RankNTypes
+      RecordWildCards
+      ScopedTypeVariables
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints
+  build-depends:
+      base
+    , kill-bool
+    , hspec
+    , hspec-core
+  default-language: Haskell2010
diff --git a/src/Data/Bool/Kill.hs b/src/Data/Bool/Kill.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Bool/Kill.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module        : Data.Bool.Kill
+-- Copyright     : Gautier DI FOLCO
+-- License       : ISC
+--
+-- Maintainer    : Gautier DI FOLCO <gautier.difolco@gmail.com>
+-- Stability     : Unstable
+-- Portability   : not portable
+--
+-- Strongly-typed booleans
+--
+-- Example:
+--
+-- > type TT = TBool "missing" "present"
+-- >
+-- > isPresent :: TT
+-- > isPresent = mkIs $ Proxy @"present"
+-- >
+-- > is (Proxy @"missing") isPresent == False
+module Data.Bool.Kill
+  ( TBool (..),
+    is,
+    isNot,
+    mkIs,
+    mkTBool,
+    ShouldBe,
+    ShouldBeVal,
+
+    -- * Reexport
+    Proxy (..),
+  )
+where
+
+import Data.Kind
+import Data.Proxy
+import GHC.TypeLits
+
+-- | Strongly-typed 'Bool'
+data TBool (false :: Symbol) (true :: Symbol)
+  = IsFalse
+  | IsTrue
+
+instance (KnownSymbol f, KnownSymbol t) => Show (TBool f t) where
+  show =
+    \case
+      IsTrue -> "True (" <> symbolVal (Proxy @t) <> ")"
+      IsFalse -> "False (" <> symbolVal (Proxy @f) <> ")"
+
+-- | Check "if 'True'"
+is :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t -> Bool
+is _ = is' (Proxy @(ShouldBe (TBool f t) b))
+
+-- | Check "if 'False'"
+isNot :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t -> Bool
+isNot _ = not . is' (Proxy @(ShouldBe (TBool f t) b))
+
+-- | Create 'True'/'False' from its name
+mkIs :: forall b f t. ShouldBeVal (ShouldBe (TBool f t) b) => Proxy b -> TBool f t
+mkIs _ = mkIs' $ Proxy @(ShouldBe (TBool f t) b)
+
+-- | Create 'TBool' from 'Bool'
+mkTBool :: forall f t. Bool -> TBool f t
+mkTBool p = if p then IsTrue else IsFalse
+
+data TTrue = TTrue deriving (Show)
+
+data TFalse = TFalse deriving (Show)
+
+type family ShouldBe (tbool :: Type) (a :: Symbol) :: Type where
+  ShouldBe (TBool f t) t = TTrue
+  ShouldBe (TBool f t) f = TFalse
+  ShouldBe (TBool f t) o = TypeError ('Text "Cannot find " ':$$: 'ShowType o ':$$: 'Text " valid choices are " ':$$: 'ShowType f ':$$: 'Text " and " ':$$: 'ShowType t)
+
+class ShouldBeVal a where
+  is' :: Proxy a -> TBool t f -> Bool
+  mkIs' :: Proxy a -> TBool t f
+
+instance ShouldBeVal TTrue where
+  is' _ =
+    \case
+      IsTrue -> True
+      IsFalse -> False
+  mkIs' _ = IsTrue
+
+instance ShouldBeVal TFalse where
+  is' _ =
+    \case
+      IsTrue -> False
+      IsFalse -> True
+  mkIs' _ = IsFalse
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,43 @@
+module Main (main) where
+
+import Data.Bool.Kill
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec =
+  describe "Kill-Bool" $ do
+    describe "mkIs" $ do
+      let isPresent :: TT
+          isPresent = mkIs $ Proxy @"present"
+          isMissing :: TT
+          isMissing = mkIs $ Proxy @"missing"
+      describe "isPresent" $ do
+        it "is 'present' should be True" $ is (Proxy @"present") isPresent `shouldBe` True
+        it "isNot 'present' should be False" $ isNot (Proxy @"present") isPresent `shouldBe` False
+        it "is 'missing' should be False" $ is (Proxy @"missing") isPresent `shouldBe` False
+        it "isNot 'missing' should be True" $ isNot (Proxy @"missing") isPresent `shouldBe` True
+      describe "isMissing" $ do
+        it "is 'missing' should be True" $ is (Proxy @"missing") isMissing `shouldBe` True
+        it "isNot 'missing' should be False" $ isNot (Proxy @"missing") isMissing `shouldBe` False
+        it "is 'present' should be False" $ is (Proxy @"present") isMissing `shouldBe` False
+        it "isNot 'present' should be True" $ isNot (Proxy @"present") isMissing `shouldBe` True
+    describe "mkTBool" $ do
+      let isPresent :: TT
+          isPresent = mkTBool True
+          isMissing :: TT
+          isMissing = mkTBool False
+      describe "isPresent" $ do
+        it "is 'present' should be True" $ is (Proxy @"present") isPresent `shouldBe` True
+        it "isNot 'present' should be False" $ isNot (Proxy @"present") isPresent `shouldBe` False
+        it "is 'missing' should be False" $ is (Proxy @"missing") isPresent `shouldBe` False
+        it "isNot 'missing' should be True" $ isNot (Proxy @"missing") isPresent `shouldBe` True
+      describe "isMissing" $ do
+        it "is 'missing' should be True" $ is (Proxy @"missing") isMissing `shouldBe` True
+        it "isNot 'missing' should be False" $ isNot (Proxy @"missing") isMissing `shouldBe` False
+        it "is 'present' should be False" $ is (Proxy @"present") isMissing `shouldBe` False
+        it "isNot 'present' should be True" $ isNot (Proxy @"present") isMissing `shouldBe` True
+
+type TT = TBool "missing" "present"