diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for catalyst
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2021
+
+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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# catalyst
+
+Welcome to catalyst! It's a Category typeclass hierarchy powerful enough to encode full programs.
+
+Please refer to my conference talk: [Deconstructing Lambdas: an awkward guide to programming without functions](https://www.youtube.com/watch?v=xZmPuz9m2t0)
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/catalyst.cabal b/catalyst.cabal
new file mode 100644
--- /dev/null
+++ b/catalyst.cabal
@@ -0,0 +1,46 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 3ff2d7f6f18494c402cb5005bb0958895552a0e6e880e40abfd2a9c523201627
+
+name:           catalyst
+version:        0.0.0.0
+synopsis:       A Category typeclass hierarchy powerful enough to encode full programs.
+description:    Please see the README on GitHub at <https://github.com/githubuser/catalyst#readme>
+homepage:       https://github.com/ChrisPenner/catalyst#readme
+bug-reports:    https://github.com/ChrisPenner/catalyst/issues
+author:         Chris Penner
+maintainer:     example@example.com
+copyright:      2021 Chris Penner
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/ChrisPenner/catalyst
+
+library
+  exposed-modules:
+      Control.Category.Cartesian
+      Control.Category.Closed
+      Control.Category.Free
+      Control.Category.Monoidal
+      Control.Category.Numeric
+      Control.Category.Recursive
+  other-modules:
+      Paths_catalyst
+  hs-source-dirs:
+      src
+  default-extensions: TypeOperators FlexibleInstances FlexibleContexts ScopedTypeVariables LambdaCase ViewPatterns TypeApplications TypeOperators DeriveFunctor DeriveTraversable DeriveGeneric DerivingStrategies StandaloneDeriving TemplateHaskell RankNTypes GADTs PolyKinds
+  ghc-options: -Wall
+  build-depends:
+      base >=4.7 && <5
+    , profunctors
+  default-language: Haskell2010
diff --git a/src/Control/Category/Cartesian.hs b/src/Control/Category/Cartesian.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Cartesian.hs
@@ -0,0 +1,36 @@
+module Control.Category.Cartesian where
+
+import Control.Category.Monoidal
+
+import Control.Category ((>>>))
+
+class MonoidalProduct k => Cartesian k where
+  (&&&) :: (a `k` l) -> (a `k` r) -> (a `k` (l, r))
+  l &&& r = copy >>> (l *** r)
+  consume :: a `k` ()
+  copy :: a `k` (a, a)
+  fst' :: (l, r) `k` l
+  snd' :: (l, r) `k` r
+
+instance Cartesian (->) where
+  copy x = (x, x)
+  consume _ = ()
+  fst' = fst
+  snd' = snd
+
+class MonoidalSum k => Cocartesian k where
+  (|||) :: (al `k` b) -> (ar `k` b) -> (Either al ar `k` b)
+  (|||) l r = (l +++ r) >>> unify
+
+  injectL :: a `k` (Either a b)
+  injectR :: a `k` (Either b a)
+  unify :: Either a a `k` a
+  -- | tags 'Right' when 'True', 'Left' when 'False'
+  tag :: k (Bool, a) (Either a a)
+
+instance Cocartesian (->) where
+  injectL = Left
+  injectR = Right
+  unify = either id id
+  tag (True, a) = Right a
+  tag (False, a) = Left a
diff --git a/src/Control/Category/Closed.hs b/src/Control/Category/Closed.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Closed.hs
@@ -0,0 +1,8 @@
+module Control.Category.Closed where
+
+
+-- class Category k => Closed k where
+--   -- closed :: (a `k` b) -> ((r -> a) `k` (r -> b))
+--   apply :: ((a -> b), a) `k` b
+--   curry' :: ((a, b) `k` c) -> (a `k` (b -> c))
+--   uncurry' :: (a `k` (b -> c)) -> ((a, b) `k` c)
diff --git a/src/Control/Category/Free.hs b/src/Control/Category/Free.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Free.hs
@@ -0,0 +1,240 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Control.Category.Free where
+
+import qualified Control.Category as C
+import Control.Category.Monoidal as C
+import Control.Category.Cartesian as C
+import Control.Category.Recursive as C
+import Data.Kind ( Constraint )
+
+-- Data kinds representing whether each constraint is required.
+-- We could use 'Bool', but using separate Data Kinds helps a lot with producing nicer type errors.
+data IsCategory = HasCategory | NoCategory
+data IsSymmetricProduct = HasSymmetricProduct | NoSymmetricProduct
+data IsSymmetricSum = HasSymmetricSum | NoSymmetricSum
+data IsMonoidalProduct = HasMonoidalProduct | NoMonoidalProduct
+data IsMonoidalSum = HasMonoidalSum | NoMonoidalSum
+data IsCartesian = HasCartesian | NoCartesian
+data IsCocartesian = HasCocartesian | NoCocartesian
+data IsRecursive = HasRecursive | NoRecursive
+data IsFixed = HasFixed | NoFixed
+
+data Requirements =
+    Req
+        IsCategory
+        IsSymmetricProduct
+        IsSymmetricSum
+        IsMonoidalProduct
+        IsMonoidalSum
+        IsCartesian
+        IsCocartesian
+        IsRecursive
+        IsFixed
+
+type family ConstraintsOf (x :: anykind) (k :: * -> * -> *) = (c :: Constraint) where
+  -- The constraints of a 'Requirements' are the constriants of each class-requirement
+  ConstraintsOf ('Req cat symP symS monP monS cart cocart rec fix) k = 
+      ( ConstraintsOf cat k
+      , ConstraintsOf symP k
+      , ConstraintsOf symS k
+      , ConstraintsOf monP k
+      , ConstraintsOf monS k
+      , ConstraintsOf cart k
+      , ConstraintsOf cocart k
+      , ConstraintsOf rec k
+      , ConstraintsOf fix k
+      )
+  -- Each sub-requirement has an associated class
+  ConstraintsOf 'HasCategory cat = C.Category cat
+  ConstraintsOf 'HasSymmetricProduct cat = C.SymmetricProduct cat
+  ConstraintsOf 'HasSymmetricSum cat = C.SymmetricSum cat
+  ConstraintsOf 'HasMonoidalProduct cat = C.MonoidalProduct cat
+  ConstraintsOf 'HasMonoidalSum cat = C.MonoidalSum cat
+  ConstraintsOf 'HasCartesian cat = C.Cartesian cat
+  ConstraintsOf 'HasCocartesian cat = C.Cocartesian cat
+  ConstraintsOf 'HasRecursive cat = C.Recursive cat
+  ConstraintsOf 'HasFixed cat = C.Fixed cat
+
+  ConstraintsOf 'NoCategory cat = ()
+  ConstraintsOf 'NoSymmetricProduct cat = ()
+  ConstraintsOf 'NoSymmetricSum cat = ()
+  ConstraintsOf 'NoMonoidalProduct cat = ()
+  ConstraintsOf 'NoMonoidalSum cat = ()
+  ConstraintsOf 'NoCartesian cat = ()
+  ConstraintsOf 'NoCocartesian cat = ()
+  ConstraintsOf 'NoRecursive cat = ()
+  ConstraintsOf 'NoFixed cat = ()
+
+type FreeFunction c a b =
+    Catalyst
+      ('Req
+          'HasCategory
+          'HasSymmetricProduct
+          'HasSymmetricSum
+          'HasMonoidalProduct
+          'HasMonoidalSum
+          'HasCartesian
+          'HasCocartesian
+          'HasRecursive
+          'HasFixed
+      ) c
+
+data Catalyst (r :: Requirements) (p :: * -> * -> *) a b where
+  ID :: (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec fix) => Catalyst r p x x
+  Comp :: Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x y -> Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p y z -> Catalyst ('Req 'HasCategory symP symS monP monS cart cocart rec fix) p x z
+
+  Swap :: (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => Catalyst r p (a, b) (b, a)
+  Reassoc :: (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => Catalyst r p (a, (b, c)) ((a, b), c)
+
+  SwapE :: (r ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart rec fix) => Catalyst r p (Either a b) (Either b a)
+  ReassocE :: (r ~ 'Req cat symP 'HasSymmetricSum monP monS cart cocart rec fix) => Catalyst r p (Either a (Either b c)) (Either (Either a b) c)
+
+  First :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (a, m) (b, m)
+  Second :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (m, a) (m, b)
+  -- (***)
+  Alongside :: (r ~ 'Req cat symP symS 'HasMonoidalProduct monS cart cocart rec fix) => Catalyst r p a b -> Catalyst r p a' b' -> Catalyst r p (a, a') (b, b')
+  -- (&&&)
+  Fanout :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p a b -> Catalyst r p a b' -> Catalyst r p a (b, b')
+
+  Left' :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (Either a x) (Either b x)
+  Right' :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p (Either x a) (Either x b)
+  -- (+++)
+  EitherOf :: (r ~ 'Req cat symP symS monP 'HasMonoidalSum cart cocart rec fix) => Catalyst r p a b -> Catalyst r p a' b' -> Catalyst r p (Either a a') (Either b b')
+  -- (|||)
+  Fanin :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p a b -> Catalyst r p a' b -> Catalyst r p (Either a a') b
+
+  Copy :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p x (x, x)
+  Consume :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p x ()
+  Fst :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p (a, b) a
+  Snd :: (r ~ 'Req cat symP symS monP monS 'HasCartesian cocart rec fix) => Catalyst r p (a, b) b
+
+  InjectL :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p a (Either a b)
+  InjectR :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p b (Either a b)
+  Unify :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p (Either a a) a
+  Tag :: (r ~ 'Req cat symP symS monP monS cart 'HasCocartesian rec fix) => Catalyst r p (Bool, a) (Either a a)
+
+  RecurseL :: (r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) => Catalyst r p (Either a d) (Either b d) -> Catalyst r p a b
+  RecurseR :: (r ~ 'Req cat symP symS monP monS cart cocart 'HasRecursive fix) => Catalyst r p (Either d a) (Either d b) -> Catalyst r p a b
+
+  FixL :: (r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) => Catalyst r p (a, d) (b, d) -> Catalyst r p a b
+  FixR :: (r ~ 'Req cat symP symS monP monS cart cocart rec 'HasFixed) => Catalyst r p (d, a) (d, b) -> Catalyst r p a b
+
+  LiftC :: p a b -> Catalyst r p a b
+
+instance (forall x y. Show (c x y)) => Show (Catalyst r c a b) where
+  show
+    = \case
+        Fst -> "fst"
+        Snd -> "snd"
+        Copy -> "copy"
+        Consume -> "consume"
+        Swap -> "swap"
+        Reassoc -> "reassoc"
+        SwapE -> "swapE"
+        ReassocE -> "reassocE"
+
+        InjectL -> "injectL"
+        InjectR -> "injectR"
+        Unify -> "unify"
+        Tag -> "tag"
+        (First l) -> "(first' " <> show l <> ")"
+        (Second l) -> "(second' " <> show l <> ")"
+        (Alongside l r) -> "(" <> show l <> " *** " <> show r <>  ")"
+        (Fanout l r) -> "(" <> show l <> " &&& " <> show r  <> ")"
+        (Left' l) -> "(left " <> show l <> ")"
+        (Right' r) -> "(right " <> show r <> ")"
+        (EitherOf l r) -> "(" <> show l <> " +++ " <> show r <> ")"
+        (Fanin l r) -> "(" <> show l <> " +++ " <> show r <> ")"
+        (LiftC cab) -> show cab
+        ID -> "id"
+        (Comp l r) -> "(" <> show l <> " >>> " <> show r <> ")"
+        (RecurseL l) -> "(recurseR " <> show l <> ")"
+        (RecurseR r) -> "(recurseL " <> show r <> ")"
+        (FixL l) -> "(fixL " <> show l <> ")"
+        (FixR r) -> "(fixR " <> show r <> ")"
+
+runFree :: forall r p c a b. (ConstraintsOf r p) => (forall x y. c x y -> p x y) -> Catalyst r c a b -> p a b
+runFree interp = \case
+  LiftC c -> interp c
+  Fst -> fst'
+  Snd -> snd'
+  Copy -> copy
+  Consume -> consume
+  Swap -> swap
+  SwapE -> swapE
+  Reassoc -> reassoc
+  ReassocE -> reassocE
+  InjectL -> injectL
+  InjectR -> injectR
+  Unify -> unify
+  Tag -> tag
+  First p -> first' (runFree interp p)
+  Second p -> second' (runFree interp p)
+  Alongside l r -> runFree interp l C.*** runFree interp r
+  Fanout l r -> runFree interp l C.&&& runFree interp r
+  Left' p -> left (runFree interp p)
+  Right' p -> right (runFree interp p)
+  Fanin l r -> runFree interp l C.||| runFree interp r
+  EitherOf l r -> runFree interp l C.+++ runFree interp r
+  Comp l r -> runFree interp l C.>>> runFree interp r
+  ID -> C.id
+  RecurseL l -> recurseL (runFree interp l)
+  RecurseR r -> recurseR (runFree interp r)
+  FixL l -> fixL (runFree interp l)
+  FixR r -> fixR (runFree interp r)
+
+liftC :: c a b -> Catalyst r c a b
+liftC = LiftC
+
+instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec fix)
+         => C.Category (Catalyst r c) where
+  id = ID
+  (.) = flip Comp
+
+instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS 'HasMonoidalProduct monS 'HasCartesian cocart rec fix)
+  => C.Cartesian (Catalyst r c) where
+  copy = Copy
+  consume = Consume
+  fst' = Fst
+  snd' = Snd
+
+instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP 'HasMonoidalSum cart 'HasCocartesian rec fix)
+         => C.Cocartesian (Catalyst r c) where
+  injectL = InjectL
+  injectR = InjectR
+  unify = Unify
+  tag = Tag
+
+instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS monP monS cart cocart rec fix) => C.SymmetricProduct (Catalyst r c) where
+  swap = Swap
+  reassoc = Reassoc
+
+instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP monS cart cocart rec fix) => C.SymmetricSum (Catalyst r c) where
+  swapE = SwapE
+  reassocE = ReassocE
+
+instance (r ~ 'Req 'HasCategory 'HasSymmetricProduct symS 'HasMonoidalProduct monS cart cocart rec fix) => C.MonoidalProduct (Catalyst r c) where
+  (***) = Alongside
+  first' = First
+  second' = Second
+
+instance (r ~ 'Req 'HasCategory symP 'HasSymmetricSum monP 'HasMonoidalSum cart cocart rec fix) => C.MonoidalSum (Catalyst r c) where
+  (+++) = EitherOf
+  left = Left'
+  right = Right'
+
+instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart 'HasRecursive fix) => Recursive (Catalyst r c) where
+  recurseL = RecurseL
+  recurseR = RecurseR
+
+instance (r ~ 'Req 'HasCategory symP symS monP monS cart cocart rec 'HasFixed) => Fixed (Catalyst r c) where
+  fixL = FixL
+  fixR = FixR
diff --git a/src/Control/Category/Monoidal.hs b/src/Control/Category/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Monoidal.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE DefaultSignatures #-}
+module Control.Category.Monoidal where
+
+import Control.Category (Category, (>>>))
+import qualified Control.Arrow as A
+
+class SymmetricProduct k => MonoidalProduct k where
+  {-# MINIMAL first' | second' #-}
+  (***) :: (al `k` bl) -> (ar `k` br) -> ((al, ar) `k` (bl, br))
+  l *** r = first' l >>> second' r
+  first' :: (a `k` b) -> ((a, c) `k` (b, c))
+  first' f = swap >>> second' f >>> swap
+  second' :: (a `k` b) -> ((c, a) `k` (c, b))
+  second' f = swap >>> first' f >>> swap
+
+instance MonoidalProduct (->) where
+  (***) = (A.***)
+  first' = A.first
+  second' = A.second
+
+class SymmetricSum k => MonoidalSum k where
+  {-# MINIMAL left | right #-}
+  (+++) :: (al `k` bl) -> (ar `k` br) -> ((Either al ar) `k` (Either bl br))
+  l +++ r = left l >>> right r
+  left :: (a `k` b) -> ((Either a c) `k` (Either b c))
+  left f = swapE >>> right f >>> swapE
+  right :: (a `k` b) -> ((Either c a) `k` (Either c b))
+  right f = swapE >>> left f >>> swapE
+
+instance MonoidalSum (->) where
+  l +++ r = l A.+++ r
+  left = A.left
+  right = A.right
+
+class Category k => SymmetricProduct k where
+  swap :: (l, r) `k` (r, l)
+  reassoc :: (a, (b, c)) `k` ((a, b), c)
+
+class Category k => SymmetricSum k where
+  swapE :: (Either l r) `k` (Either r l)
+  reassocE :: (Either a (Either b c)) `k` Either (Either a b) c
+
+instance SymmetricProduct (->) where
+  swap (a, b) = (b, a)
+  reassoc (a, (b, c)) = ((a, b), c)
+
+instance SymmetricSum (->) where
+  swapE (Left a) = Right a
+  swapE (Right a) = Left a
+  reassocE (Left a) = Left (Left a)
+  reassocE (Right (Left b)) = Left (Right b)
+  reassocE (Right (Right c)) = Right c
+
+class CategoryPlus k => CategoryZero k where
+  zeroC :: k a b
+
+class Category k => CategoryPlus k where
+  (<+>) :: k a b -> k a b -> k a b
diff --git a/src/Control/Category/Numeric.hs b/src/Control/Category/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Numeric.hs
@@ -0,0 +1,19 @@
+module Control.Category.Numeric where
+
+
+-- class Numeric k where
+--   num :: Int -> k a Int
+--   add :: k (Int, Int) Int
+--   negate' :: k Int Int
+--   mult :: k (Int, Int) Int
+--   div' :: k (Int, Int) Int
+--   mod' :: k (Int, Int) Int
+
+-- instance Numeric (->) where
+--   num = const
+--   add = uncurry (+)
+--   negate' = negate
+--   mult = uncurry (*)
+--   div' = uncurry div
+--   mod' = uncurry mod
+
diff --git a/src/Control/Category/Recursive.hs b/src/Control/Category/Recursive.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Recursive.hs
@@ -0,0 +1,21 @@
+module Control.Category.Recursive where
+
+import Control.Category (Category)
+import qualified Data.Profunctor.Choice as P
+import qualified Data.Profunctor.Strong as P
+
+class Category k => Recursive k where
+  recurseL :: (Either a s `k` Either b s) -> (a `k` b)
+  recurseR :: (Either s a `k` Either s b) -> (a `k` b)
+
+instance Recursive (->) where
+  recurseL = P.unleft
+  recurseR = P.unright
+
+class Category k => Fixed k where
+  fixL :: ((a, s) `k` (b, s)) -> (a `k` b)
+  fixR :: ((s, a) `k` (s, b)) -> (a `k` b)
+
+instance Fixed (->) where
+  fixL = P.unfirst
+  fixR = P.unsecond