diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Constrained.hs
@@ -0,0 +1,90 @@
+module Control.Category.Constrained (Semigroupoid (..), Category (..), Groupoid (..), Valid, NT (..), mkNT', nt') where
+
+import Control.Categorical.Functor (map)
+import qualified Control.Category as Base
+import qualified Control.Category.Groupoid as Base
+import Data.Constraint.Lifting
+import Data.Type.Coercion
+import Data.Type.Equality
+
+class Semigroupoid (s :: α -> α -> Type) where
+    (∘) :: s b c -> s a b -> s a c
+
+type family Valid (s :: α -> α -> Type) :: α -> Constraint
+
+class Semigroupoid s => Category s where
+    id :: Valid s a => s a a
+    id = id' Dict
+
+    id' :: Dict (Valid s a) -> s a a
+    id' Dict = id
+
+class Category s => Groupoid s where
+    invert :: (Valid s a, Valid s b) => s a b -> s b a
+    invert = invert' Dict Dict
+
+    invert' :: Dict (Valid s a) -> Dict (Valid s b) -> s a b -> s b a
+    invert' Dict Dict = invert
+
+instance {-# INCOHERENT #-} Base.Category s => Semigroupoid s where (∘) = (Base..)
+instance {-# INCOHERENT #-} (Base.Category s, Valid s ~ Unconstrained1) => Category s where id = Base.id
+instance {-# INCOHERENT #-} (Base.Groupoid s, Valid s ~ Unconstrained1) => Groupoid s where invert = Base.invert
+
+instance {-# INCOHERENT #-} (Category s, Valid s ~ Unconstrained1) => Base.Category s where
+    id = id
+    (.) = (∘)
+
+instance {-# INCOHERENT #-} (Groupoid s, Valid s ~ Unconstrained1) => Base.Groupoid s where
+    invert = invert
+
+type instance Valid (:~:) = Unconstrained1
+instance Category (:~:) where id = Refl
+instance Groupoid (:~:) where invert Refl = Refl
+
+type instance Valid (:~~:) = Unconstrained1
+instance Category (:~~:) where id = HRefl
+instance Groupoid (:~~:) where invert HRefl = HRefl
+
+type instance Valid Coercion = Unconstrained1
+instance Category Coercion where id = Coercion
+instance Groupoid Coercion where invert Coercion = Coercion
+
+instance Semigroupoid (,) where (_, c) ∘ (a, _) = (a, c)
+instance Semigroupoid Const where _ ∘ Const a = Const a
+
+type instance Valid (->) = Unconstrained1
+type instance Valid (:-) = Unconstrained1
+instance Category (->) where id = Base.id
+instance Category (:-) where id = Base.id
+
+newtype NT s f g = NT { nt :: ∀ a . Valid s a => s (f a) (g a) }
+
+instance Semigroupoid s => Semigroupoid (NT s) where NT f ∘ NT g = NT (f ∘ g)
+
+type instance Valid (NT s) = Endolifting (Valid s)
+instance Category s => Category (NT s) where
+    id' d = NT (id' (lift' d))
+
+instance Groupoid s => Groupoid (NT s) where
+    invert' ad bd (NT f) = NT (invert' (lift' ad) (lift' bd) f)
+
+lift' :: c a => Dict (Lifting c d f) -> Dict (d (f a))
+lift' d = map (go d) Dict
+  where go :: Dict (Lifting c d f) -> c a :- d (f a)
+        go d = withDict d lift
+
+instance Semigroupoid k => Semigroupoid (Dual k) where
+    Dual f ∘ Dual g = Dual (g ∘ f)
+
+type instance Valid (Dual k) = Valid k
+instance Category k => Category (Dual k) where
+    id = Dual id
+
+instance Groupoid k => Groupoid (Dual k) where
+    invert = Dual ∘ invert ∘ dual
+
+nt' :: NT s f g -> Dict (Valid s a) -> s (f a) (g a)
+nt' (NT f) Dict = f
+
+mkNT' :: (∀ a . Dict (Valid s a) -> s (f a) (g a)) -> NT s f g
+mkNT' f = NT (f Dict)
diff --git a/Data/Functor/Constrained.hs b/Data/Functor/Constrained.hs
new file mode 100644
--- /dev/null
+++ b/Data/Functor/Constrained.hs
@@ -0,0 +1,107 @@
+module Data.Functor.Constrained where
+
+import qualified Control.Categorical.Functor as U
+import Control.Category.Constrained
+import qualified Data.Functor as Base
+
+-- | Laws:
+--
+-- @
+-- 'map' (f '∘' g) = 'map' f '∘' 'map' g
+-- @
+class (Semigroupoid s, Semigroupoid t) => SGM (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β) where
+    map :: s a b -> t (f a) (f b)
+
+-- | Laws:
+--
+-- @
+-- 'map' 'id' = 'id'
+-- @
+class (SGM s t f, Category s, Category t) => Functor s t f
+
+type Endofunctor s = Functor s s
+
+infixl 4 <$>
+(<$>) :: SGM s (->) f => s a b -> f a -> f b
+(<$>) = map
+
+instance {-# INCOHERENT #-} Base.Functor f => SGM (->) (->) f where map = Base.fmap
+instance {-# INCOHERENT #-} Base.Functor f => Functor (->) (->) f
+
+instance SGM (:-) (->) Dict where map = U.map
+instance Functor (:-) (->) Dict
+
+instance (SGM s (->) f, Valid s ~ Unconstrained1) => SGM (NT s) (NT (->)) (Compose f) where
+    map (NT f) = NT (\ (Compose x) -> Compose (map f x))
+instance (Functor s (->) f, Valid s ~ Unconstrained1) => Functor (NT s) (NT (->)) (Compose f)
+
+instance SGM (NT (->)) (NT (NT (->))) Compose where
+    map (NT f) = NT (NT (\ (Compose x) -> Compose (f x)))
+instance Functor (NT (->)) (NT (NT (->))) Compose
+
+instance (SGM s (->) f, SGM s (->) g) => SGM s (->) (Sum f g) where
+    map f (InL x) = InL (f <$> x)
+    map f (InR y) = InR (f <$> y)
+instance (Functor s (->) f, Functor s (->) g) => Functor s (->) (Sum f g)
+
+instance SGM (NT (->)) (NT (->)) (Sum f) where
+    map (NT f) = NT (\ case InL x -> InL x
+                            InR y -> InR (f y))
+instance Functor (NT (->)) (NT (->)) (Sum f)
+
+instance SGM (NT (->)) (NT (NT (->))) Sum where
+    map (NT f) = NT (NT (\ case InL x -> InL (f x)
+                                InR y -> InR y))
+instance Functor (NT (->)) (NT (NT (->))) Sum
+
+instance (SGM s (->) f, SGM s (->) g) => SGM s (->) (Product f g) where
+    map f (Pair x y) = Pair (f <$> x) (f <$> y)
+instance (Functor s (->) f, Functor s (->) g) => Functor s (->) (Product f g)
+
+instance SGM (NT (->)) (NT (->)) (Product f) where
+    map (NT f) = NT (\ (Pair x y) -> Pair x (f y))
+instance Functor (NT (->)) (NT (->)) (Product f)
+
+instance SGM (NT (->)) (NT (NT (->))) Product where
+    map (NT f) = NT (NT (\ (Pair x y) -> Pair (f x) y))
+instance Functor (NT (->)) (NT (NT (->))) Product
+
+instance Semigroupoid s => SGM s (->) (Const a) where
+    map _ (Const a) = Const a
+instance Category s => Functor s (->) (Const a)
+
+instance SGM (->) (NT (->)) Const where
+    map f = NT (\ (Const a) -> Const (f a))
+instance Functor (->) (NT (->)) Const
+
+instance SGM (->) (->) Identity where
+    map f (Identity a) = Identity (f a)
+instance Functor (->) (->) Identity
+
+instance Semigroupoid s => SGM s (->) Proxy where
+    map _ Proxy = Proxy
+instance Category s => Functor s (->) Proxy
+
+instance SGM (->) (->) ((,) a) where
+    map f (a, b) = (a, f b)
+instance Functor (->) (->) ((,) a)
+
+instance SGM (->) (NT (->)) (,) where
+    map f = NT (\ (a, b) -> (f a, b))
+instance Functor (->) (NT (->)) (,)
+
+instance SGM (->) (->) (Either a) where
+    map _ (Left a) = Left a
+    map f (Right b) = Right (f b)
+instance Functor (->) (->) (Either a)
+
+instance SGM (->) (NT (->)) Either where
+    map f = NT (\ case Left a -> Left (f a)
+                       Right b -> Right b)
+instance Functor (->) (NT (->)) Either
+
+instance Semigroupoid s => SGM s (->) (s a) where map = (∘)
+instance Category s => Functor s (->) (s a)
+
+instance Semigroupoid s => SGM (Dual s) (NT (->)) s where map (Dual f) = NT (∘ f)
+instance Category s => Functor (Dual s) (NT (->)) s
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here © 2018
+
+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 Author name here 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/Prelude.hs b/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/Prelude.hs
@@ -0,0 +1,14 @@
+module Prelude (module A) where
+
+import Algebra as A (Semigroup (..), Monoid (..), Group)
+import Control.Category.Dual as A (Dual (..))
+import Data.Constraint as A
+import Data.Either as A (Either (..))
+import Data.Functor.Compose as A (Compose (..))
+import Data.Functor.Identity as A (Identity (..))
+import Data.Functor.Const as A (Const (..))
+import Data.Functor.Product as A (Product (..))
+import Data.Functor.Sum as A (Sum (..))
+import Data.Proxy as A (Proxy (..))
+import Data.Kind as A (Constraint, Type)
+import Unconstrained as A (Unconstrained1)
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# constrained-category
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/bench/Main.hs b/bench/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Criterion.Main
+
+main :: IO ()
+main = defaultMain []
diff --git a/constrained-category.cabal b/constrained-category.cabal
new file mode 100644
--- /dev/null
+++ b/constrained-category.cabal
@@ -0,0 +1,111 @@
+name:                constrained-category
+version:             0.1.0.0
+synopsis:            Constrained Categories
+-- description:
+license:             BSD3
+license-file:        LICENSE
+author:              Author name here
+maintainer:          example@example.com
+copyright:           2018 Author name here
+-- category:            
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      .
+  exposed-modules:     Control.Category.Constrained
+                     , Data.Functor.Constrained
+  other-modules:       Prelude
+  build-depends:       base >= 4.7 && < 5
+                     , alg >=0.2 && <0.3
+                     , category >= 0.2.2 && < 0.3
+                     , constraint >= 0.1.3 && < 0.2
+                     , unconstrained >= 0.1 && < 0.2
+  default-language:    Haskell2010
+  default-extensions:  UnicodeSyntax
+                     , LambdaCase
+                     , EmptyCase
+                     , TypeOperators
+                     , InstanceSigs
+                     , PartialTypeSignatures
+                     , RankNTypes
+                     , PolyKinds
+                     , ConstraintKinds
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , TypeFamilies
+                     , MultiParamTypeClasses
+                     , MonadComprehensions
+                     , StandaloneDeriving
+                     , GeneralizedNewtypeDeriving
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       -Werror=incomplete-patterns
+                       -Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods
+
+test-suite test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Main.hs
+  build-depends:       base >=4.11 && <5
+                     , smallcheck >=1.1.4
+                     , tasty >=1.0
+                     , tasty-smallcheck >=0.8
+                     , constrained-category
+  default-language:    Haskell2010
+  default-extensions:  UnicodeSyntax
+                     , LambdaCase
+                     , EmptyCase
+                     , InstanceSigs
+                     , PartialTypeSignatures
+                     , PolyKinds
+                     , ConstraintKinds
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , MonadComprehensions
+                     , StandaloneDeriving
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       -Werror=incomplete-patterns
+                       -Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods
+
+benchmark bench
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      bench
+  main-is:             Main.hs
+  build-depends:       base >=4.11 && <5
+                     , criterion >=1.4.1
+                     , constrained-category
+  default-language:    Haskell2010
+  default-extensions:  UnicodeSyntax
+                     , LambdaCase
+                     , EmptyCase
+                     , InstanceSigs
+                     , PartialTypeSignatures
+                     , PolyKinds
+                     , ConstraintKinds
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , MonadComprehensions
+                     , StandaloneDeriving
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       -Werror=incomplete-patterns
+                       -Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods
+
+source-repository head
+  type:     git
+  location: https://github.com/githubuser/constrained-category.hs
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,8 @@
+module Main where
+
+import Test.SmallCheck
+import Test.Tasty
+import Test.Tasty.SmallCheck
+
+main :: IO ()
+main = defaultMain $ testGroup "" []
