diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Revision history for free-categories
 
+## 0.2.0.0 -- 2020-02-12
+
+* Separate into 3 modules.
+* Refactor typeclasses.
+* Rename functions
+
 ## 0.1.0.0 -- 2019-10-01
 
 * First version.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,31 +1,3 @@
-# free-categories
-
-Consider the category of Haskell "quivers" with
-
-* objects are types of higher kind
-  * `p :: k -> k -> Type`
-* morphisms are terms of `RankNType`,
-  * `forall x y. p x y -> q x y`
-* identity is `id`
-* composition is `.`
-
-Now, consider the subcategory of Haskell `Category`s with
-
-* constrained objects `Category c => c`
-* morphisms act functorially
-  * `t :: (Category c, Category d) => c x y -> d x y`
-  * `t id = id`
-  * `t (g . f) = t g . t f`
-
-The [free category functor](https://ncatlab.org/nlab/show/free+category)
-from quivers to `Category`s may be defined up to isomorphism as
-
-* the functor `Path` of type-aligned lists
-
-* the functor `FoldPath` of categorical folds
-
-* abstractly as `CFree path => path`, the class of
-  left adjoints to the functor which
-  forgets the constraint on `Category c => c`
+The free category on a quiver.
 
-* or as any isomorphic data structure
+![quiver](quiver.gif)
diff --git a/free-categories.cabal b/free-categories.cabal
--- a/free-categories.cabal
+++ b/free-categories.cabal
@@ -1,7 +1,7 @@
 cabal-version:       >=1.10
 
 name:                free-categories
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            free categories
 description:         free categories, paths, and categorical folds
 homepage:            http://github.com/morphismtech/free-categories
@@ -16,6 +16,9 @@
 
 library
   exposed-modules:     Control.Category.Free
+                       Data.Quiver
+                       Data.Quiver.Bifunctor
+                       Data.Quiver.Functor
   build-depends:       base >=4.12 && <=5
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Control/Category/Free.hs b/src/Control/Category/Free.hs
--- a/src/Control/Category/Free.hs
+++ b/src/Control/Category/Free.hs
@@ -5,23 +5,21 @@
 Maintainer: eitan@morphism.tech
 Stability: experimental
 
-Consider the category of Haskell "quivers" with
-
-* objects are types of higher kind
-  * @p :: k -> k -> Type@
-* morphisms are terms of @RankNType@,
-  * @forall x y. p x y -> q x y@
-* identity is `id`
-* composition is `.`
-
-Now, consider the subcategory of Haskell `Category`s with
+Consider the category of Haskell `Category`s, a subcategory
+of the category of quivers with,
 
 * constrained objects `Category` @c => c@
-* morphisms act functorially
+* morphisms are functors (which preserve objects)
   * @t :: (Category c, Category d) => c x y -> d x y@
   * @t id = id@
   * @t (g . f) = t g . t f@
 
+Thus, a functor from quivers to `Category`s
+has @(QFunctor c, forall p. Category (c p))@ with.
+
+prop> qmap f id = id
+prop> qmap f (q . p) = qmap f q . qmap f p
+
 The [free category functor](https://ncatlab.org/nlab/show/free+category)
 from quivers to `Category`s may be defined up to isomorphism as
 
@@ -29,18 +27,16 @@
 
 * the functor `FoldPath` of categorical folds
 
-* abstractly as `CFree` @path => path@, the class of
-  left adjoints to the functor which
+* abstractly as `CFree` @path => path@,
+  the class of left adjoints to the functor which
   forgets the constraint on `Category` @c => c@
 
 * or as any isomorphic data structure
 -}
 
 {-# LANGUAGE
-    FlexibleInstances
-  , GADTs
+    GADTs
   , LambdaCase
-  , MultiParamTypeClasses
   , PatternSynonyms
   , PolyKinds
   , QuantifiedConstraints
@@ -52,19 +48,18 @@
   ( Path (..)
   , pattern (:<<)
   , FoldPath (..)
-  , Category (..)
-  , CFunctor (..)
-  , CFoldable (..)
-  , CTraversable (..)
   , CFree (..)
   , toPath
-  , EndoL (..)
-  , EndoR (..)
-  , MCat (..)
-  , ApCat (..)
+  , reversePath
+  , beforeAll
+  , afterAll
+  , Category (..)
   ) where
 
+import Data.Quiver
+import Data.Quiver.Functor
 import Control.Category
+import Control.Monad (join)
 import Prelude hiding (id, (.))
 
 {- | A `Path` with steps in @p@ is a singly linked list of
@@ -75,7 +70,7 @@
   path :: Path (->) String Int
   path = length :>> (\x -> x^2) :>> Done
 in
-  cfold path "hello"
+  qfold path "hello"
 :}
 25
 -}
@@ -88,152 +83,83 @@
 pattern ps :<< p = p :>> ps
 infixl 7 :<<
 deriving instance (forall x y. Show (p x y)) => Show (Path p x y)
-instance x ~ y => Semigroup (Path p x y) where
-  (<>) = (>>>)
-instance x ~ y => Monoid (Path p x y) where
-  mempty = Done
-  mappend = (>>>)
+instance x ~ y => Semigroup (Path p x y) where (<>) = (>>>)
+instance x ~ y => Monoid (Path p x y) where mempty = Done
 instance Category (Path p) where
   id = Done
   (.) path = \case
     Done -> path
     p :>> ps -> p :>> (ps >>> path)
-instance CFunctor Path where
-  cmap _ Done = Done
-  cmap f (p :>> ps) = f p :>> cmap f ps
-instance CFoldable Path where
-  cfoldMap _ Done = id
-  cfoldMap f (p :>> ps) = f p >>> cfoldMap f ps
-  ctoMonoid _ Done = mempty
-  ctoMonoid f (p :>> ps) = f p <> ctoMonoid f ps
-  ctoList _ Done = []
-  ctoList f (p :>> ps) = f p : ctoList f ps
-  ctraverse_ _ Done = pure id
-  ctraverse_ f (p :>> ps) = (>>>) <$> f p <*> ctraverse_ f ps
-instance CTraversable Path where
-  ctraverse _ Done = pure Done
-  ctraverse f (p :>> ps) = (:>>) <$> f p <*> ctraverse f ps
-instance CFree Path where csingleton p = p :>> Done
+instance QFunctor Path where
+  qmap _ Done = Done
+  qmap f (p :>> ps) = f p :>> qmap f ps
+instance QFoldable Path where
+  qfoldMap _ Done = id
+  qfoldMap f (p :>> ps) = f p >>> qfoldMap f ps
+  qtoMonoid _ Done = mempty
+  qtoMonoid f (p :>> ps) = f p <> qtoMonoid f ps
+  qtoList _ Done = []
+  qtoList f (p :>> ps) = f p : qtoList f ps
+  qtraverse_ _ Done = pure id
+  qtraverse_ f (p :>> ps) = (>>>) <$> f p <*> qtraverse_ f ps
+instance QTraversable Path where
+  qtraverse _ Done = pure Done
+  qtraverse f (p :>> ps) = (:>>) <$> f p <*> qtraverse f ps
+instance QPointed Path where qsingle p = p :>> Done
+instance QMonad Path where qjoin = qfold
+instance CFree Path
 
-{- | Encodes a path as its `cfoldMap` function.-}
+{- | Encodes a path as its `qfoldMap` function.-}
 newtype FoldPath p x y = FoldPath
-  {getFoldPath :: forall q. Category q => (forall x y. p x y -> q x y) -> q x y}
-instance x ~ y => Semigroup (FoldPath p x y) where
-  (<>) = (>>>)
-instance x ~ y => Monoid (FoldPath p x y) where
-  mempty = id
-  mappend = (>>>)
+  {getFoldPath :: forall q. Category q
+    => (forall x y. p x y -> q x y) -> q x y}
+instance x ~ y => Semigroup (FoldPath p x y) where (<>) = (>>>)
+instance x ~ y => Monoid (FoldPath p x y) where mempty = id
 instance Category (FoldPath p) where
   id = FoldPath $ \ _ -> id
   FoldPath g . FoldPath f = FoldPath $ \ k -> g k . f k
-instance CFunctor FoldPath where cmap f = cfoldMap (csingleton . f)
-instance CFoldable FoldPath where cfoldMap k (FoldPath f) = f k
-instance CTraversable FoldPath where
-  ctraverse f = getApCat . cfoldMap (ApCat . fmap csingleton . f)
-instance CFree FoldPath where csingleton p = FoldPath $ \ k -> k p
-
-{- | A functor from quivers to `Category`s.
-
-prop> cmap _ id = id
-prop> cmap f (c >>> c') = f c >>> f c'
--}
-class (forall p. Category (c p)) => CFunctor c where
-  cmap :: (forall x y. p x y -> q x y) -> c p x y -> c q x y
-
-{- | Generalizing `Foldable` from `Monoid`s to `Category`s.
-
-prop> cmap f = cfoldMap (csingleton . f)
--}
-class CFunctor c => CFoldable c where
-  {- | Map each element of the structure to a `Category`,
-  and combine the results.-}
-  cfoldMap :: Category q => (forall x y. p x y -> q x y) -> c p x y -> q x y
-  {- | Combine the elements of a structure using a `Category`.-}
-  cfold :: Category q => c q x y -> q x y
-  cfold = cfoldMap id
-  {- | Right-associative fold of a structure.
-
-  In the case of `Path`s, `cfoldr`, when applied to a binary operator,
-  a starting value, and a `Path`, reduces the `Path` using the binary operator,
-  from right to left:
-
-  prop> cfoldr (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == p1 ? (p2 ? ... (pn ? q) ...)
-  -}
-  cfoldr :: (forall x y z . p x y -> q y z -> q x z) -> q y z -> c p x y -> q x z
-  cfoldr (?) q c = getEndoR (cfoldMap (\ x -> EndoR (\ y -> x ? y)) c) q
-  {- | Left-associative fold of a structure.
-
-  In the case of `Path`s, `cfoldl`, when applied to a binary operator,
-  a starting value, and a `Path`, reduces the `Path` using the binary operator,
-  from left to right:
-
-  prop> cfoldl (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == (... ((q ? p1) ? p2) ? ...) ? pn
-  -}
-  cfoldl :: (forall x y z . q x y -> p y z -> q x z) -> q x y -> c p y z -> q x z
-  cfoldl (?) q c = getEndoL (cfoldMap (\ x -> EndoL (\ y -> y ? x)) c) q
-  {- | Map each element of the structure to a `Monoid`,
-  and combine the results.-}
-  ctoMonoid :: Monoid m => (forall x y. p x y -> m) -> c p x y -> m
-  ctoMonoid f = getMCat . cfoldMap (MCat . f)
-  {- | Map each element of the structure, and combine the results in a list.-}
-  ctoList :: (forall x y. p x y -> a) -> c p x y -> [a]
-  ctoList f = ctoMonoid (pure . f)
-  {- | Map each element of a structure to an `Applicative` on a `Category`,
-  evaluate from left to right, and combine the results.-}
-  ctraverse_
-    :: (Applicative m, Category q)
-    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (q x y)
-  ctraverse_ f = getApCat . cfoldMap (ApCat . f)
-
-{- | Generalizing `Traversable` to `Category`s.-}
-class CFoldable c => CTraversable c where
-  {- | Map each element of a structure to an `Applicative` on a quiver,
-  evaluate from left to right, and collect the results.-}
-  ctraverse
-    :: Applicative m
-    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (c q x y)
+instance QFunctor FoldPath where qmap f = qfoldMap (qsingle . f)
+instance QFoldable FoldPath where qfoldMap k (FoldPath f) = f k
+instance QTraversable FoldPath where
+  qtraverse f = getApQ . qfoldMap (ApQ . fmap qsingle . f)
+instance QPointed FoldPath where qsingle p = FoldPath $ \ k -> k p
+instance QMonad FoldPath where qjoin (FoldPath f) = f id
+instance CFree FoldPath
 
 {- | Unpacking the definition of a left adjoint to the forgetful functor
-from `Category`s to quivers, there must be a function `csingleton`,
-such that any function
+from `Category`s to quivers, any
 
 @f :: Category d => p x y -> d x y@
 
-factors uniquely through @c p x y@ as
+factors uniquely through the free `Category` @c@ as
 
-prop> cfoldMap f . csingleton = f
+prop> qfoldMap f . qsingle = f
 -}
-class CTraversable c => CFree c where csingleton :: p x y -> c p x y
+class
+  ( QPointed c
+  , QFoldable c
+  , forall p. Category (c p)
+  ) => CFree c where
 
-{- | `toPath` collapses any `CFoldable` into a `CFree`.
+{- | `toPath` collapses any `QFoldable` into a `CFree`.
 It is the unique isomorphism which exists
 between any two `CFree` functors.
 -}
-toPath :: (CFoldable c, CFree path) => c p x y -> path p x y
-toPath = cfoldMap csingleton
-
-{- | Used in the default definition of `cfoldr`.-}
-newtype EndoR p y x = EndoR {getEndoR :: forall z. p x z -> p y z}
-instance Category (EndoR p) where
-  id = EndoR id
-  EndoR f1 . EndoR f2 = EndoR (f2 . f1)
+toPath :: (QFoldable c, CFree path) => c p x y -> path p x y
+toPath = qfoldMap qsingle
 
-{- | Used in the default definition of `cfoldr`.-}
-newtype EndoL p x y = EndoL {getEndoL :: forall w . p w x -> p w y}
-instance Category (EndoL p) where
-  id = EndoL id
-  EndoL f1 . EndoL f2 = EndoL (f1 . f2)
+{- | Reverse all the arrows in a path. -}
+reversePath :: (QFoldable c, CFree path) => c p x y -> path (OpQ p) y x
+reversePath = getOpQ . qfoldMap (OpQ . qsingle . OpQ)
 
-{- | Turn a `Monoid` into a `Category`,
-used in the default definition of `ctoMonoid`.-}
-newtype MCat m x y = MCat {getMCat :: m} deriving (Eq, Ord, Show)
-instance Monoid m => Category (MCat m) where
-  id = MCat mempty
-  MCat g . MCat f = MCat (f <> g)
+{- | Insert a given loop before each step. -}
+beforeAll
+  :: (QFoldable c, CFree path)
+  => (forall x. p x x) -> c p x y -> path p x y
+beforeAll sep = qfoldMap (\p -> qsingle sep >>> qsingle p)
 
-{- | Turn an `Applicative` over a `Category` into a `Category`,
-used in the default definition of `ctraverse_`.-}
-newtype ApCat m c x y = ApCat {getApCat :: m (c x y)} deriving (Eq, Ord, Show)
-instance (Applicative m, Category c) => Category (ApCat m c) where
-  id = ApCat (pure id)
-  ApCat g . ApCat f = ApCat ((.) <$> g <*> f)
+{- | Insert a given loop before each step. -}
+afterAll
+  :: (QFoldable c, CFree path)
+  => (forall x. p x x) -> c p x y -> path p x y
+afterAll sep = qfoldMap (\p -> qsingle p >>> qsingle sep)
diff --git a/src/Data/Quiver.hs b/src/Data/Quiver.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Quiver.hs
@@ -0,0 +1,169 @@
+{-|
+Module: Data.Quiver
+Description: free categories
+Copyright: (c) Eitan Chatav, 2019
+Maintainer: eitan@morphism.tech
+Stability: experimental
+
+A [quiver](https://ncatlab.org/nlab/show/quiver)
+is a directed graph where loops and multiple arrows
+between vertices are allowed, a multidigraph. A Haskell quiver
+is a higher kinded type,
+
+@p :: k -> k -> Type@
+
+  * where vertices are types @x :: k@,
+  * and arrows from @x@ to @y@ are terms @p :: p x y@.
+
+Many Haskell typeclasses are constraints on quivers, such as
+`Category`, `Data.Bifunctor.Bifunctor`,
+@Profunctor@, and `Control.Arrow.Arrow`.
+-}
+
+{-# LANGUAGE
+    GADTs
+  , PolyKinds
+  , QuantifiedConstraints
+  , RankNTypes
+  , StandaloneDeriving
+#-}
+
+module Data.Quiver
+  ( IQ (..)
+  , OpQ (..)
+  , IsoQ (..)
+  , ApQ (..)
+  , KQ (..)
+  , ProductQ (..)
+  , qswap
+  , HomQ (..)
+  , ReflQ (..)
+  , ComposeQ (..)
+  , LeftQ (..)
+  , RightQ (..)
+  ) where
+
+import Control.Category
+import Control.Monad (join)
+import Prelude hiding (id, (.))
+
+{- | The identity functor on quivers. -}
+newtype IQ c x y = IQ {getIQ :: c x y} deriving (Eq, Ord, Show)
+instance (Category c, x ~ y) => Semigroup (IQ c x y) where (<>) = (>>>)
+instance (Category c, x ~ y) => Monoid (IQ c x y) where mempty = id
+instance Category c => Category (IQ c) where
+  id = IQ id
+  IQ g . IQ f = IQ (g . f)
+
+{- | Reverse all the arrows in a quiver.-}
+newtype OpQ c x y = OpQ {getOpQ :: c y x} deriving (Eq, Ord, Show)
+instance (Category c, x ~ y) => Semigroup (OpQ c x y) where (<>) = (>>>)
+instance (Category c, x ~ y) => Monoid (OpQ c x y) where mempty = id
+instance Category c => Category (OpQ c) where
+  id = OpQ id
+  OpQ g . OpQ f = OpQ (f . g)
+
+{- | Arrows of `IsoQ` are bidirectional edges.-}
+data IsoQ c x y = IsoQ
+  { up :: c x y
+  , down :: c y x
+  } deriving (Eq, Ord, Show)
+instance (Category c, x ~ y) => Semigroup (IsoQ c x y) where (<>) = (>>>)
+instance (Category c, x ~ y) => Monoid (IsoQ c x y) where mempty = id
+instance Category c => Category (IsoQ c) where
+  id = IsoQ id id
+  (IsoQ yz zy) . (IsoQ xy yx) = IsoQ (yz . xy) (yx . zy)
+
+{- | Apply a constructor to the arrows of a quiver.-}
+newtype ApQ m c x y = ApQ {getApQ :: m (c x y)} deriving (Eq, Ord, Show)
+instance (Applicative m, Category c, x ~ y)
+  => Semigroup (ApQ m c x y) where (<>) = (>>>)
+instance (Applicative m, Category c, x ~ y)
+  => Monoid (ApQ m c x y) where mempty = id
+instance (Applicative m, Category c) => Category (ApQ m c) where
+  id = ApQ (pure id)
+  ApQ g . ApQ f = ApQ ((.) <$> g <*> f)
+
+{- | The constant quiver.
+
+@KQ ()@ is an [indiscrete category]
+(https://ncatlab.org/nlab/show/indiscrete+category).
+-}
+newtype KQ r x y = KQ {getKQ :: r} deriving (Eq, Ord, Show)
+instance (Semigroup m, x ~ y) => Semigroup (KQ m x y) where
+  KQ f <> KQ g = KQ (f <> g)
+instance (Monoid m, x ~ y) => Monoid (KQ m x y) where mempty = id
+instance Monoid m => Category (KQ m) where
+  id = KQ mempty
+  KQ g . KQ f = KQ (f <> g)
+
+{- | [Cartesian monoidal product]
+(https://ncatlab.org/nlab/show/cartesian+monoidal+category)
+of quivers.-}
+data ProductQ p q x y = ProductQ
+  { qfst :: p x y
+  , qsnd :: q x y
+  } deriving (Eq, Ord, Show)
+instance (Category p, Category q, x ~ y)
+  => Semigroup (ProductQ p q x y) where (<>) = (>>>)
+instance (Category p, Category q, x ~ y)
+  => Monoid (ProductQ p q x y) where mempty = id
+instance (Category p, Category q) => Category (ProductQ p q) where
+  id = ProductQ id id
+  ProductQ pyz qyz . ProductQ pxy qxy = ProductQ (pyz . pxy) (qyz . qxy)
+
+{- | Symmetry of `ProductQ`.-}
+qswap :: ProductQ p q x y -> ProductQ q p x y
+qswap (ProductQ p q) = ProductQ q p
+
+{- | The quiver of quiver morphisms, `HomQ` is the [internal hom]
+(https://ncatlab.org/nlab/show/internal+hom)
+of the category of quivers.-}
+newtype HomQ p q x y = HomQ { getHomQ :: p x y -> q x y }
+
+{- | A term in @ReflQ r x y@ observes the equality @x ~ y@.
+
+@ReflQ ()@ is the [discrete category]
+(https://ncatlab.org/nlab/show/discrete+category).
+-}
+data ReflQ r x y where ReflQ :: r -> ReflQ r x x
+deriving instance Show r => Show (ReflQ r x y)
+deriving instance Eq r => Eq (ReflQ r x y)
+deriving instance Ord r => Ord (ReflQ r x y)
+instance Monoid m => Category (ReflQ m) where
+  id = ReflQ mempty
+  ReflQ yz . ReflQ xy = ReflQ (xy <> yz)
+
+{- | Compose quivers along matching source and target.-}
+data ComposeQ p q x z = forall y. ComposeQ (p y z) (q x y)
+deriving instance (forall y. Show (p y z), forall y. Show (q x y))
+  => Show (ComposeQ p q x z)
+instance (Category p, p ~ q, x ~ y)
+  => Semigroup (ComposeQ p q x y) where (<>) = (>>>)
+instance (Category p, p ~ q, x ~ y)
+  => Monoid (ComposeQ p q x y) where mempty = id
+instance (Category p, p ~ q) => Category (ComposeQ p q) where
+  id = ComposeQ id id
+  ComposeQ yz xy . ComposeQ wx vw = ComposeQ (yz . xy) (wx . vw)
+
+{- | The left [residual]
+(https://ncatlab.org/nlab/show/residual)
+of `ComposeQ`.-}
+newtype LeftQ p q x y = LeftQ
+  {getLeftQ :: forall w. p w x -> q w y}
+instance (p ~ q, x ~ y) => Semigroup (LeftQ p q x y) where (<>) = (>>>)
+instance (p ~ q, x ~ y) => Monoid (LeftQ p q x y) where mempty = id
+instance p ~ q => Category (LeftQ p q) where
+  id = LeftQ id
+  LeftQ g . LeftQ f = LeftQ (g . f)
+
+{- | The right [residual]
+(https://ncatlab.org/nlab/show/residual)
+of `ComposeQ`.-}
+newtype RightQ p q x y = RightQ
+  {getRightQ :: forall z. p y z -> q x z}
+instance (p ~ q, x ~ y) => Semigroup (RightQ p q x y) where (<>) = (>>>)
+instance (p ~ q, x ~ y) => Monoid (RightQ p q x y) where mempty = id
+instance p ~ q => Category (RightQ p q) where
+  id = RightQ id
+  RightQ f . RightQ g = RightQ (g . f)
diff --git a/src/Data/Quiver/Bifunctor.hs b/src/Data/Quiver/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Quiver/Bifunctor.hs
@@ -0,0 +1,149 @@
+{-|
+Module: Data.Quiver.Bifunctor
+Description: free categories
+Copyright: (c) Eitan Chatav, 2019
+Maintainer: eitan@morphism.tech
+Stability: experimental
+
+The category of quivers forms a closed monoidal
+category in two ways, under `ProductQ` or `ComposeQ`.
+The relations between these and their adjoints can be
+characterized by typeclasses below.
+-}
+
+{-# LANGUAGE
+    FlexibleInstances
+  , FunctionalDependencies
+  , GADTs
+  , PolyKinds
+  , QuantifiedConstraints
+  , RankNTypes
+#-}
+
+module Data.Quiver.Bifunctor
+  ( QBifunctor (..)
+  , QProfunctor (..)
+  , QMonoidal (..)
+  , QClosed (..)
+  ) where
+
+import Data.Quiver
+import Data.Quiver.Functor
+
+{- | A endo-bifunctor on the category of quivers,
+covariant in both its arguments.
+
+prop> qbimap id id = id
+prop> qbimap (g . f) (i . h) = qbimap g i . qbimap f h
+-}
+class (forall q. QFunctor (prod q)) => QBifunctor prod where
+  qbimap
+    :: (forall x y. p x y -> p' x y)
+    -> (forall x y. q x y -> q' x y)
+    -> prod p q x y -> prod p' q' x y
+instance QBifunctor ProductQ where
+  qbimap f g (ProductQ p q) = ProductQ (f p) (g q)
+instance QBifunctor ComposeQ where
+  qbimap f g (ComposeQ p q) = ComposeQ (f p) (g q)
+
+{- | A endo-bifunctor on the category of quivers,
+contravariant in its first argument,
+and covariant in its second argument.
+
+prop> qdimap id id = id
+prop> qdimap (g . f) (i . h) = qdimap f i . qdimap g h
+-}
+class (forall q. QFunctor (hom q)) => QProfunctor hom where
+  qdimap
+    :: (forall x y. p' x y -> p x y)
+    -> (forall x y. q x y -> q' x y)
+    -> hom p q x y -> hom p' q' x y
+instance QProfunctor HomQ where qdimap f h (HomQ g) = HomQ (h . g . f)
+instance QProfunctor LeftQ where qdimap f h (LeftQ g) = LeftQ (h . g . f)
+instance QProfunctor RightQ where qdimap f h (RightQ g) = RightQ (h . g . f)
+
+{-| A [monoidal category]
+(https://ncatlab.org/nlab/show/monoidal+category)
+structure on the category of quivers.
+
+This consists of a product bifunctor, a unit object and
+structure morphisms, an invertible associator,
+
+prop> qassoc . qdisassoc = id
+prop> qdisassoc . qassoc = id
+
+and invertible left and right unitors,
+
+prop> qintro1 . qelim1 = id
+prop> qelim1 . qintro1 = id
+prop> qintro2 . qelim2 = id
+prop> qelim2 . qintro2 = id
+
+that satisfy the pentagon equation,
+
+prop> qbimap id qassoc . qassoc . qbimap qassoc id = qassoc . qassoc
+
+and the triangle equation,
+
+prop> qbimap id qelim1 . qassoc = qbimap qelim2 id
+-}
+class QBifunctor prod => QMonoidal prod unit | prod -> unit where
+  qintro1 :: p x y -> prod unit p x y
+  qintro2 :: p x y -> prod p unit x y
+  qelim1 :: prod unit p x y -> p x y
+  qelim2 :: prod p unit x y -> p x y
+  qassoc :: prod (prod p q) r x y -> prod p (prod q r) x y
+  qdisassoc :: prod p (prod q r) x y -> prod (prod p q) r x y
+instance QMonoidal ProductQ (KQ ()) where
+  qintro1 p = ProductQ (KQ ()) p
+  qintro2 p = ProductQ p (KQ ())
+  qelim1 (ProductQ _ p) = p
+  qelim2 (ProductQ p _) = p
+  qassoc (ProductQ (ProductQ p q) r) = ProductQ p (ProductQ q r)
+  qdisassoc (ProductQ p (ProductQ q r)) = ProductQ (ProductQ p q) r
+instance QMonoidal ComposeQ (ReflQ ()) where
+  qintro1 p = ComposeQ (ReflQ ()) p
+  qintro2 p = ComposeQ p (ReflQ ())
+  qelim1 (ComposeQ (ReflQ ()) p) = p
+  qelim2 (ComposeQ p (ReflQ ())) = p
+  qassoc (ComposeQ (ComposeQ p q) r) = ComposeQ p (ComposeQ q r)
+  qdisassoc (ComposeQ p (ComposeQ q r)) = ComposeQ (ComposeQ p q) r
+
+{- | A [(bi-)closed monoidal category]
+(https://ncatlab.org/nlab/show/closed+monoidal+category)
+is one for which the products
+@prod _ p@ and @prod p _@ both have right adjoint functors,
+the left and right residuals @lhom p@ and @rhom p@.
+If @prod@ is symmetric then the left and right residuals
+coincide as the internal hom.
+
+prop> qcurry  . quncurry = id
+prop> qflurry . qunflurry = id
+
+prop> qlev . (qcurry f `qbimap` id) = f
+prop> qcurry (qlev . (g `qbimap` id)) = g
+prop> qrev . (id `qbimap` qflurry f) = f
+prop> qflurry (qrev . (id `qbimap` g)) = g
+-}
+class (QBifunctor prod, QProfunctor lhom, QProfunctor rhom)
+  => QClosed prod lhom rhom | prod -> lhom, prod -> rhom where
+    qlev :: prod (lhom p q) p x y -> q x y
+    qrev :: prod p (rhom p q) x y -> q x y
+    qcurry :: (forall x y. prod p q x y -> r x y) -> p x y -> lhom q r x y
+    quncurry :: (forall x y. p x y -> lhom q r x y) -> prod p q x y -> r x y
+    qflurry :: (forall x y. prod p q x y -> r x y) -> q x y -> rhom p r x y
+    qunflurry :: (forall x y. q x y -> rhom p r x y) -> prod p q x y -> r x y
+instance QClosed ProductQ HomQ HomQ where
+  qlev (ProductQ (HomQ pq) p) = pq p
+  qrev (ProductQ p (HomQ pq)) = pq p
+  qcurry f p = HomQ (\q -> f (ProductQ p q))
+  quncurry f (ProductQ p q) = getHomQ (f p) q
+  qflurry f q = HomQ (\p -> f (ProductQ p q))
+  qunflurry f (ProductQ p q) = getHomQ (f q) p
+instance QClosed ComposeQ LeftQ RightQ where
+  qlev (ComposeQ (LeftQ pq) p) = pq p
+  qrev (ComposeQ p (RightQ pq)) = pq p
+  qcurry f p = LeftQ (\q -> f (ComposeQ p q))
+  quncurry f (ComposeQ p q) = getLeftQ (f p) q
+  qflurry f q = RightQ (\p -> f (ComposeQ p q))
+  qunflurry f (ComposeQ p q) = getRightQ (f q) p
diff --git a/src/Data/Quiver/Functor.hs b/src/Data/Quiver/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Quiver/Functor.hs
@@ -0,0 +1,152 @@
+{-|
+Module: Data.Quiver.Functor
+Description: free categories
+Copyright: (c) Eitan Chatav, 2019
+Maintainer: eitan@morphism.tech
+Stability: experimental
+
+Consider the category of Haskell quivers with
+
+* objects are types of higher kind
+  * @p :: k -> k -> Type@
+* morphisms are terms of @RankNType@,
+  * @forall x y. p x y -> q x y@
+* identity is `id`
+* composition is `.`
+
+There is a natural hierarchy of typeclasses for
+endofunctors of the category of Haskell quivers,
+analagous to that for Haskell types.
+-}
+
+{-# LANGUAGE
+    PolyKinds
+  , RankNTypes
+#-}
+
+module Data.Quiver.Functor
+  ( QFunctor (..)
+  , QPointed (..)
+  , QFoldable (..)
+  , QTraversable (..)
+  , QMonad (..)
+  ) where
+
+import Control.Category
+import Data.Quiver
+import Prelude hiding (id, (.))
+
+{- | An endfunctor of quivers.
+
+prop> qmap id = id
+prop> qmap (g . f) = qmap g . qmap f
+-}
+class QFunctor c where
+  qmap :: (forall x y. p x y -> q x y) -> c p x y -> c q x y
+instance QFunctor (ProductQ p) where qmap f (ProductQ p q) = ProductQ p (f q)
+instance QFunctor (HomQ p) where qmap g (HomQ f) = HomQ (g . f)
+instance Functor t => QFunctor (ApQ t) where qmap f (ApQ t) = ApQ (f <$> t)
+instance QFunctor OpQ where qmap f = OpQ . f . getOpQ
+instance QFunctor IsoQ where qmap f (IsoQ u d) = IsoQ (f u) (f d)
+instance QFunctor IQ where qmap f = IQ . f . getIQ
+instance QFunctor (ComposeQ p) where qmap f (ComposeQ p q) = ComposeQ p (f q)
+instance QFunctor (LeftQ p) where qmap g (LeftQ f) = LeftQ (g . f)
+instance QFunctor (RightQ p) where qmap g (RightQ f) = RightQ (g . f)
+
+{- | Embed a single quiver arrow with `qsingle`.-}
+class QFunctor c => QPointed c where qsingle :: p x y -> c p x y
+instance QPointed (HomQ p) where qsingle q = HomQ (const q)
+instance Applicative t => QPointed (ApQ t) where qsingle = ApQ . pure
+instance QPointed IQ where qsingle = IQ
+instance Category p => QPointed (ComposeQ p) where qsingle = ComposeQ id
+
+{- | Generalizing `Foldable` from `Monoid`s to `Category`s.
+
+prop> qmap f = qfoldMap (qsingle . f)
+-}
+class QFunctor c => QFoldable c where
+  {- | Map each element of the structure to a `Category`,
+  and combine the results.-}
+  qfoldMap :: Category q => (forall x y. p x y -> q x y) -> c p x y -> q x y
+  {- | Combine the elements of a structure using a `Category`.-}
+  qfold :: Category q => c q x y -> q x y
+  qfold = qfoldMap id
+  {- | Right-associative fold of a structure.
+
+  In the case of `Control.Category.Free.Path`s,
+  `qfoldr`, when applied to a binary operator,
+  a starting value, and a `Control.Category.Free.Path`,
+  reduces the `Control.Category.Free.Path` using the binary operator,
+  from right to left:
+
+  prop> qfoldr (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == p1 ? (p2 ? ... (pn ? q) ...)
+  -}
+  qfoldr :: (forall x y z . p x y -> q y z -> q x z) -> q y z -> c p x y -> q x z
+  qfoldr (?) q c = getRightQ (qfoldMap (\ x -> RightQ (\ y -> x ? y)) c) q
+  {- | Left-associative fold of a structure.
+
+  In the case of `Control.Category.Free.Path`s,
+  `qfoldl`, when applied to a binary operator,
+  a starting value, and a `Control.Category.Free.Path`,
+  reduces the `Control.Category.Free.Path` using the binary operator,
+  from left to right:
+
+  prop> qfoldl (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == (... ((q ? p1) ? p2) ? ...) ? pn
+  -}
+  qfoldl :: (forall x y z . q x y -> p y z -> q x z) -> q x y -> c p y z -> q x z
+  qfoldl (?) q c = getLeftQ (qfoldMap (\ x -> LeftQ (\ y -> y ? x)) c) q
+  {- | Map each element of the structure to a `Monoid`,
+  and combine the results.-}
+  qtoMonoid :: Monoid m => (forall x y. p x y -> m) -> c p x y -> m
+  qtoMonoid f = getKQ . qfoldMap (KQ . f)
+  {- | Map each element of the structure, and combine the results in a list.-}
+  qtoList :: (forall x y. p x y -> a) -> c p x y -> [a]
+  qtoList f = qtoMonoid (pure . f)
+  {- | Map each element of a structure to an `Applicative` on a `Category`,
+  evaluate from left to right, and combine the results.-}
+  qtraverse_
+    :: (Applicative m, Category q)
+    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (q x y)
+  qtraverse_ f = getApQ . qfoldMap (ApQ . f)
+instance QFoldable (ProductQ p) where qfoldMap f (ProductQ _ q) = f q
+instance QFoldable IQ where qfoldMap f (IQ c) = f c
+
+{- | Generalizing `Traversable` to quivers.-}
+class QFoldable c => QTraversable c where
+  {- | Map each element of a structure to an `Applicative` on a quiver,
+  evaluate from left to right, and collect the results.-}
+  qtraverse
+    :: Applicative m
+    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (c q x y)
+instance QTraversable (ProductQ p) where
+  qtraverse f (ProductQ p q) = ProductQ p <$> f q
+instance QTraversable IQ where qtraverse f (IQ c) = IQ <$> f c
+
+{- | Generalize `Monad` to quivers.
+
+Associativity and left and right identity laws hold.
+
+prop> qjoin . qjoin = qjoin . qmap qjoin
+prop> qjoin . qsingle = id
+prop> qjoin . qmap qsingle = id
+
+The functions `qbind` and `qjoin` are related as
+
+prop> qjoin = qbind id
+prop> qbind f p = qjoin (qmap f p)
+-}
+class (QFunctor c, QPointed c) => QMonad c where
+  qjoin :: c (c p) x y -> c p x y
+  qjoin = qbind id
+  qbind :: (forall x y. p x y -> c q x y) -> c p x y -> c q x y
+  qbind f p = qjoin (qmap f p)
+  {-# MINIMAL qjoin | qbind #-}
+instance QMonad (HomQ p) where
+  qjoin (HomQ q) = HomQ (\p -> getHomQ (q p) p)
+instance Monad t => QMonad (ApQ t) where
+  qbind f (ApQ t) = ApQ $ do
+    p <- t
+    getApQ $ f p
+instance QMonad IQ where qjoin = getIQ
+instance Category p => QMonad (ComposeQ p) where
+  qjoin (ComposeQ yz (ComposeQ xy q)) = ComposeQ (yz . xy) q