diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,13 @@
+dist
+docs
+wiki
+TAGS
+tags
+wip
+.DS_Store
+.*.swp
+.*.swo
+*.o
+*.hi
+*~
+*#
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,57 @@
+language: haskell
+
+env:
+  - GHCVER=7.8.3
+  - GHCVER=head
+
+matrix:
+  allow_failures:
+    - env: GHCVER=head
+
+before_install:
+  # If $GHCVER is the one travis has, don't bother reinstalling it.
+  # We can also have faster builds by installing some libraries with
+  # `apt`. If it isn't, install the GHC we want from hvr's PPA along
+  # with cabal-1.18.
+  - |
+    if [ $GHCVER = `ghc --numeric-version` ]; then
+      # Try installing some of the build-deps with apt-get for speed.
+      travis/cabal-apt-install --enable-tests $MODE
+      export CABAL=cabal
+    else
+      # Install the GHC we want from hvr's PPA
+      travis_retry sudo add-apt-repository -y ppa:hvr/ghc
+      travis_retry sudo apt-get update
+      travis_retry sudo apt-get install cabal-install-1.18 ghc-$GHCVER happy
+      export CABAL=cabal-1.18
+      export PATH=/opt/ghc/$GHCVER/bin:$PATH
+    fi
+  # Uncomment whenever hackage is down.
+  # - mkdir -p ~/.cabal && cp travis/config ~/.cabal/config && $CABAL update
+  - $CABAL update
+
+  # Update happy when building with GHC head
+  - |
+    if [ $GHCVER = "head" ] || [ $GHCVER = "7.8.3" ]; then
+      $CABAL install happy alex
+      export PATH=$HOME/.cabal/bin:$PATH
+    fi
+  - $CABAL install packdeps # packunused --constraint 'packunused >= 0.1.1.2'
+
+install:
+  - $CABAL install --dependencies-only --enable-tests $MODE
+  - $CABAL configure -flib-Werror --enable-tests $MODE
+
+script:
+  - $CABAL build --ghc-options=-ddump-minimal-imports
+  - $CABAL test --show-details=always
+  - packdeps hask.cabal
+  # - packunused
+
+notifications:
+  irc:
+    channels:
+      - "irc.freenode.org#haskell-lens"
+    skip_join: true
+    template:
+      - "\x0313hask\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
diff --git a/.vim.custom b/.vim.custom
new file mode 100644
--- /dev/null
+++ b/.vim.custom
@@ -0,0 +1,31 @@
+" Add the following to your .vimrc to automatically load this on startup
+
+" if filereadable(".vim.custom")
+"     so .vim.custom
+" endif
+
+function StripTrailingWhitespace()
+  let myline=line(".")
+  let mycolumn = col(".")
+  silent %s/  *$//
+  call cursor(myline, mycolumn)
+endfunction
+
+" enable syntax highlighting
+syntax on
+
+" search for the tags file anywhere between here and /
+set tags=TAGS;/
+
+" highlight tabs and trailing spaces
+set listchars=tab:‗‗,trail:‗
+set list
+
+" f2 runs hasktags
+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>
+
+" strip trailing whitespace before saving
+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()
+
+" rebuild hasktags after saving
+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,3 @@
+0
+-
+* Repository Initialized
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2008-2014 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.markdown b/README.markdown
new file mode 100644
--- /dev/null
+++ b/README.markdown
@@ -0,0 +1,15 @@
+hask
+====
+
+[![Build Status](https://secure.travis-ci.org/ekmett/hask.png?branch=master)](http://travis-ci.org/ekmett/hask)
+
+Kind-indexed category theory for Haskell with a strong lens-like flavor.
+
+Contact Information
+-------------------
+
+Contributions and bug reports are welcome!
+
+Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
+
+-Edward Kmett
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/hask.cabal b/hask.cabal
new file mode 100644
--- /dev/null
+++ b/hask.cabal
@@ -0,0 +1,55 @@
+name:          hask
+category:      Control
+version:       0
+license:       BSD3
+cabal-version: >= 1.10
+license-file:  LICENSE
+author:        Edward A. Kmett
+maintainer:    Edward A. Kmett <ekmett@gmail.com>
+stability:     experimental
+homepage:      http://github.com/ekmett/categories
+bug-reports:   http://github.com/ekmett/categories/issues
+synopsis:      Categories
+copyright:     Copyright (C) 2008-2014, Edward A. Kmett
+description:   Kind-polymorphic category theory in Haskell
+build-type:    Simple
+tested-with:   GHC == 7.8.2
+extra-source-files:
+  .gitignore
+  .travis.yml
+  .vim.custom
+  README.markdown
+  CHANGELOG.markdown
+
+flag Optimize
+  description: Enable optimizations
+  default:     False
+
+library
+  default-language: Haskell2010
+
+  exposed-modules:
+    Hask.Adjunction
+    Hask.Category
+    Hask.Category.Polynomial
+    Hask.Functor.Faithful
+    Hask.Iso
+    Hask.Prof
+    Hask.Tensor
+    Hask.Tensor.Compose
+    Hask.Tensor.Day
+
+  build-depends:
+    base >= 4       && < 5,
+    constraints,
+    ghc-prim,
+    reflection,
+    transformers,
+    tagged,
+    void >= 0.5.4.2 && < 1
+
+  hs-source-dirs: src
+  ghc-options: -Wall -fno-warn-missing-signatures
+
+  if flag(Optimize)
+    ghc-options: -funbox-strict-fields -O2
diff --git a/src/Hask/Adjunction.hs b/src/Hask/Adjunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Adjunction.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE PolyKinds, KindSignatures, MultiParamTypeClasses, FunctionalDependencies, TypeFamilies, TypeOperators #-}
+module Hask.Adjunction 
+  ( (-|)(..)
+  , swap
+  , Curried(..)
+  ) where
+
+import Hask.Category
+import Hask.Iso
+import qualified Prelude
+
+--------------------------------------------------------------------------------
+-- * Adjunctions
+--------------------------------------------------------------------------------
+
+class (Functor f, Functor g, Dom f ~ Cod g, Cod g ~ Dom f) => (f :: j -> i) -| (g :: i -> j) | f -> g, g -> f where
+  adj :: Iso (->) (->) (->) (Cod f (f a) b) (Cod f (f a') b') (Cod g a (g b)) (Cod g a' (g b'))
+
+instance (,) e -| (->) e where
+  adj = dimap (. swap) (. swap) . curried
+
+swap :: (a,b) -> (b,a)
+swap (a,b) = (b,a)
+
+--------------------------------------------------------------------------------
+-- * Currying
+--------------------------------------------------------------------------------
+
+class (Bifunctor p, Bifunctor q) => Curried (p :: k -> i -> j) (q :: i -> j -> k) | p -> q, q -> p where
+  curried :: Iso (->) (->) (->)
+    (Dom2 p (p a b) c) (Dom2 p (p a' b') c')
+    (Dom2 q a (q b c)) (Dom2 q a' (q b' c'))
+
+instance Curried (,) (->) where
+  curried = dimap Prelude.curry Prelude.uncurry
diff --git a/src/Hask/Category.hs b/src/Hask/Category.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Category.hs
@@ -0,0 +1,341 @@
+{-# LANGUAGE CPP, KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, DefaultSignatures, NoMonomorphismRestriction #-}
+
+module Hask.Category
+  (
+  -- * Category
+    Category'(..)
+  , Category''
+  , Category
+  -- * Functors
+  -- ** Regular
+  , Functor(..)
+  , FunctorOf
+  , ob, obOf
+  , contramap
+  -- ** (Curried) Bifunctors
+  , Bifunctor
+  , Cod2, Dom2
+  , fmap1, first
+  , bimap
+  , dimap
+  -- * Vacuous
+  , Vacuous
+  -- * Categories
+  -- ** Constraints
+  , Constraint, (:-)(Sub), Dict(..), (\\), sub, Class(cls), (:=>)(ins)
+  -- ** Op
+  , Yoneda(..), Op, Opd
+  -- ** Nat
+  , Nat(..), NatId, Endo, nat, (!)
+  , Presheaves, Copresheaves
+  , NatDom, NatCod
+  -- * Prelude
+  , ($), Either(..)
+  , Fix(..)
+  ) where
+
+import Data.Constraint (Constraint, (:-)(Sub), Dict(..), (\\), Class(cls), (:=>)(ins))
+import qualified Data.Constraint as Constraint
+import Data.Proxy (Proxy(..))
+import Prelude (($), Either(..))
+
+--------------------------------------------------------------------------------
+-- * Categories (Part 1)
+--------------------------------------------------------------------------------
+
+-- | The <http://ncatlab.org/nlab/show/Yoneda+embedding Yoneda embedding>.
+--
+-- Yoneda_C :: C -> [ C^op, Set ]
+newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a }
+
+type family Op (p :: i -> i -> *) :: i -> i -> * where
+  Op (Yoneda p) = p
+  Op p = Yoneda p
+
+-- | Side-conditions moved to 'Functor' to work around GHC bug #9200.
+--
+-- You should produce instances of 'Category'' and consume instances of 'Category'.
+--
+-- All of our categories are "locally small", and we curry the Hom-functor
+-- as a functor to the category of copresheaves rather than present it as a
+-- bifunctor directly. The benefit of this encoding is that a bifunctor is
+-- just a functor to a functor category!
+--
+-- @
+-- C :: C^op -> [ C, Set ]
+-- @
+
+class Category' (p :: i -> i -> *) where
+  type Ob p :: i -> Constraint
+  id :: Ob p a => p a a
+  observe :: p a b -> Dict (Ob p a, Ob p b)
+  (.) :: p b c -> p a b -> p a c
+
+  unop :: Op p b a -> p a b
+  default unop :: Op p ~ Yoneda p => Op p b a -> p a b
+  unop = getOp
+
+  op :: p b a -> Op p a b
+  default op :: Op p ~ Yoneda p => p b a -> Op p a b
+  op = Op
+
+type Endo p a = p a a
+
+--------------------------------------------------------------------------------
+-- * Functors
+--------------------------------------------------------------------------------
+
+class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where
+  type Dom f :: i -> i -> *
+  type Cod f :: j -> j -> *
+  fmap :: Dom f a b -> Cod f (f a) (f b)
+
+class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
+instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
+
+ob :: forall f a. Functor f => Ob (Dom f) a :- Ob (Cod f) (f a)
+ob = Sub $ case observe (fmap (id :: Dom f a a) :: Cod f (f a) (f a)) of
+  Dict -> Dict
+
+data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
+  Nat :: ( FunctorOf p q f
+         , FunctorOf p q g
+         ) => {
+           runNat :: forall a. Ob p a => q (f a) (g a)
+         } -> Nat p q f g
+
+type NatId p = Endo (Nat (Dom p) (Cod p)) p
+
+obOf :: (Category (Dom f), Category (Cod f)) => NatId f -> Endo (Dom f) a
+     -> Dict (Ob (Nat (Dom f) (Cod f)) f, Ob (Dom f) a, Ob (Cod f) (f a))
+obOf f a = case observe f of
+  Dict -> case observe a of
+    Dict -> case observe (f ! a) of
+      Dict -> Dict
+
+type Copresheaves p = Nat p (->)
+type Presheaves p = Nat (Op p) (->)
+
+instance (Category' p, Category' q) => Functor (FunctorOf p q) where
+  type Dom (FunctorOf p q) = Nat p q
+  type Cod (FunctorOf p q) = (:-)
+  fmap Nat{} = Sub Dict
+
+--------------------------------------------------------------------------------
+-- * Bifunctors
+--------------------------------------------------------------------------------
+
+type family NatDom (f :: (i -> j) -> (i -> j) -> *) :: (i -> i -> *) where
+  NatDom (Nat p q) = p
+
+type family NatCod (f :: (i -> j) -> (i -> j) -> *) :: (j -> j -> *) where
+  NatCod (Nat p q) = q
+
+type Dom2 p = NatDom (Cod p)
+type Cod2 p = NatCod (Cod p)
+
+class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor (p :: i -> j -> k)
+instance  (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor (p :: i -> j -> k)
+
+fmap1 :: forall p a b c. (Bifunctor p, Ob (Dom p) c) => Dom2 p a b -> Cod2 p (p c a) (p c b)
+fmap1 f = case ob :: Ob (Dom p) c :- FunctorOf (Dom2 p) (Cod2 p) (p c) of
+  Sub Dict -> fmap f
+
+
+bimap :: Bifunctor p => Dom p a b -> Dom2 p c d -> Cod2 p (p a c) (p b d)
+bimap f g = case observe f of
+  Dict -> case observe g of
+    Dict -> runNat (fmap f) . fmap1 g
+
+type Opd f = Op (Dom f)
+
+contramap :: Functor f => Opd f b a -> Cod f (f a) (f b)
+contramap = fmap . unop
+
+-- | E-Enriched profunctors f : C -/-> D are represented by a functor of the form:
+--
+-- C^op -> [ D, E ]
+--
+-- The variance here matches Haskell's order, which means that the contravariant
+-- argument comes first!
+
+dimap :: Bifunctor p => Opd p b a -> Dom2 p c d -> Cod2 p (p a c) (p b d)
+dimap = bimap . unop
+
+{-
+type Iso
+  (c :: i -> i -> *) (d :: j -> j -> *) (e :: k -> k -> *)
+  (s :: i) (t :: j) (a :: i) (b :: j) = forall (p :: i -> j -> k).
+  (Bifunctor p, Opd p ~ c, Dom2 p ~ d, Cod2 p ~ e) => e (p a b) (p s t)
+-}
+
+--------------------------------------------------------------------------------
+-- * Categories (Part 2)
+--------------------------------------------------------------------------------
+
+class    (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p
+instance (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p
+
+-- | The full definition for a (locally-small) category.
+class    (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p
+instance (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p
+
+--------------------------------------------------------------------------------
+-- * Vacuous
+--------------------------------------------------------------------------------
+
+class Vacuous (c :: i -> i -> *) (a :: i)
+instance Vacuous c a
+
+instance Functor Dict where
+  type Dom Dict = (:-)
+  type Cod Dict = (->)
+  fmap f Dict = case f of Sub g -> g
+
+instance (Category' c, Ob c ~ Vacuous c) => Functor (Vacuous c) where
+  type Dom (Vacuous c) = c
+  type Cod (Vacuous c) = (:-)
+  fmap _ = Sub Dict
+
+--------------------------------------------------------------------------------
+-- * The Category of Constraints
+--------------------------------------------------------------------------------
+
+instance Functor (:-) where
+  type Dom (:-) = Op (:-)
+  type Cod (:-) = Nat (:-) (->) -- copresheaves
+  fmap (Op f) = Nat (. f)
+
+instance Functor ((:-) b) where
+  type Dom ((:-) a) = (:-)
+  type Cod ((:-) a) = (->)
+  fmap = (.)
+
+instance Category' (:-) where
+  type Ob (:-) = Vacuous (:-)
+  id = Constraint.refl
+  observe _ = Dict
+  (.) = Constraint.trans
+  unop = getOp
+
+sub :: (a => Proxy a -> Dict b) -> a :- b
+sub k = Sub (k Proxy)
+
+--------------------------------------------------------------------------------
+-- * Hask
+--------------------------------------------------------------------------------
+
+instance Functor (->) where
+  type Dom (->) = Op (->)
+  type Cod (->) = Nat (->) (->)
+  fmap (Op f) = Nat (. f)
+
+instance Functor ((->)a) where
+  type Dom ((->) a) = (->)
+  type Cod ((->) a) = (->)
+  fmap = (.)
+
+instance Category' (->) where
+  type Ob (->) = Vacuous (->)
+  id x = x
+  observe _ = Dict
+  (.) f g x = f (g x)
+  unop = getOp
+
+--------------------------------------------------------------------------------
+-- * Yoneda :: i -> [ Op i, Set ]
+--------------------------------------------------------------------------------
+
+instance (Category p, Op p ~ Yoneda p) => Functor (Yoneda p) where
+  type Dom (Yoneda p) = p
+  type Cod (Yoneda p) = Nat (Yoneda p) (->)
+  fmap f = Nat (. Op f)
+
+instance (Category p, Op p ~ Yoneda p) => Functor (Yoneda p a) where
+  type Dom (Yoneda p a) = Yoneda p
+  type Cod (Yoneda p a) = (->)
+  fmap = (.)
+
+instance (Category p, Op p ~ Yoneda p) => Category' (Yoneda p) where
+  type Ob (Yoneda p) = Ob p
+  id = Op id
+  Op f . Op g = Op (g . f)
+  observe (Op f) = case observe f of
+    Dict -> Dict
+  unop = Op
+  op = getOp
+
+--------------------------------------------------------------------------------
+-- * Nat
+--------------------------------------------------------------------------------
+
+instance (Category' p, Category q) => Functor (Nat p q) where
+  type Dom (Nat p q) = Op (Nat p q)
+  type Cod (Nat p q) = Nat (Nat p q) (->)
+  fmap (Op f) = Nat (. f)
+
+instance (Category' p, Category q) => Functor (Nat p q a) where
+  type Dom (Nat p q f) = Nat p q
+  type Cod (Nat p q f) = (->)
+  fmap = (.)
+
+instance (Category' p, Category' q) => Category' (Nat p q) where
+   type Ob (Nat p q) = FunctorOf p q
+   id = Nat id1 where
+     id1 :: forall f x. (Functor f, Dom f ~ p, Cod f ~ q, Ob p x) => q (f x) (f x)
+     id1 = id \\ (ob :: Ob p x :- Ob q (f x))
+   observe Nat{} = Dict
+   Nat f . Nat g = Nat (f . g)
+   unop = getOp
+
+nat :: (Category p ,Category q, FunctorOf p q f, FunctorOf p q g) => (forall a. Ob p a => Endo p a -> q (f a) (g a)) -> Nat p q f g
+nat k = Nat (k id)
+
+infixr 1 !
+(!) :: Nat p q f g -> p a a -> q (f a) (g a)
+Nat n ! f = case observe f of
+  Dict -> n
+
+--------------------------------------------------------------------------------
+-- * Instances
+--------------------------------------------------------------------------------
+
+instance Functor (,) where
+  type Dom (,) = (->)
+  type Cod (,) = Nat (->) (->)
+  fmap f = Nat $ \(a,b) -> (f a, b)
+
+instance Functor ((,) a) where
+  type Dom ((,) a) = (->)
+  type Cod ((,) a) = (->)
+  fmap f (a,b) = (a, f b)
+
+instance Functor Either where
+  type Dom Either = (->)
+  type Cod Either = Nat (->) (->)
+  fmap f0 = Nat (go f0) where
+    go :: (a -> b) -> Either a c -> Either b c
+    go f (Left a)  = Left (f a)
+    go _ (Right b) = Right b
+
+instance Functor (Either a) where
+  type Dom (Either a) = (->)
+  type Cod (Either a) = (->)
+  fmap _ (Left a) = Left a
+  fmap f (Right b) = Right (f b)
+
+first :: (Functor f, Cod f ~ Nat d e, Ob d c) => Dom f a b -> e (f a c) (f b c)
+first = runNat . fmap
+
+newtype Fix (f :: * -> * -> *) (a :: *) = In { out :: f (Fix f a) a }
+
+instance Functor Fix where
+  type Dom Fix = Nat (->) (Nat (->) (->))
+  type Cod Fix = Nat (->) (->)
+  fmap f = case observe f of 
+    Dict -> Nat $ \ (In mu) -> In (first (first f) (runNat (runNat f) mu))
+
+instance FunctorOf (->) (Nat (->) (->)) p => Functor (Fix p) where
+  type Dom (Fix f) = (->)
+  type Cod (Fix f) = (->)
+  fmap f (In b) = In (bimap (fmap f) f b)
diff --git a/src/Hask/Category/Polynomial.hs b/src/Hask/Category/Polynomial.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Category/Polynomial.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE RankNTypes, PolyKinds, DataKinds, ConstraintKinds, ScopedTypeVariables, KindSignatures, TypeFamilies, MultiParamTypeClasses, UndecidableInstances, GADTs, AllowAmbiguousTypes, FlexibleInstances #-}
+module Hask.Category.Polynomial
+  ( 
+  -- * Product Category
+    Product(..), ProductOb, Fst, Snd
+  -- * Coproduct Category
+  , Coproduct(..), CoproductOb(..)
+  -- * Unit Category
+  , Unit(..)
+  -- * Empty Category
+  , Empty
+  , Void, absurd
+
+  ) where
+
+import Hask.Category
+import Data.Void
+import Hask.Functor.Faithful
+import Prelude (error)
+
+--------------------------------------------------------------------------------
+-- * Products
+--------------------------------------------------------------------------------
+
+-- TODO: do this as a product of profunctors instead?
+data Product (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i, j)) (b :: (i, j)) =
+  Product (p (Fst a) (Fst b)) (q (Snd a) (Snd b))
+
+type family Fst (p :: (i,j)) :: i
+type instance Fst '(a,b) = a
+
+type family Snd (q :: (i,j)) :: j
+type instance Snd '(a,b) = b
+
+class    (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
+instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
+
+instance (Category p, Category q) => Functor (Product p q) where
+  type Dom (Product p q) = Op (Product (Opd p) (Opd q))
+  type Cod (Product p q) = Nat (Product (Dom2 p) (Dom2 q)) (->)
+  fmap f = case observe f of
+    Dict -> Nat (. unop f)
+
+instance (Category p, Category q, ProductOb p q a) => Functor (Product p q a) where
+  type Dom (Product p q a) = Product (Dom2 p) (Dom2 q)
+  type Cod (Product p q a) = (->)
+  fmap = (.)
+
+instance (Category p, Category q) => Category' (Product p q) where
+  type Ob (Product p q) = ProductOb p q
+  id = Product id id
+  Product f f' . Product g g' = Product (f . g) (f' . g')
+  observe (Product f g) = case observe f of
+    Dict -> case observe g of
+      Dict -> Dict
+
+
+--------------------------------------------------------------------------------
+-- * Coproducts
+--------------------------------------------------------------------------------
+
+data Coproduct (c :: i -> i -> *) (d :: j -> j -> *) (a :: Either i j) (b :: Either i j) where
+  Inl :: c x y -> Coproduct c d (Left x) (Left y)
+  Inr :: d x y -> Coproduct c d (Right x) (Right y)
+
+class CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: Either i j) where
+  side :: Endo (Coproduct p q) a -> (forall x. (a ~ Left x, Ob p x) => r) -> (forall y. (a ~ Right y, Ob q y) => r) -> r
+  coproductId :: Endo (Coproduct p q) a
+
+instance (Category p, Ob p x) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Left x :: Either i j) where
+  side _ r _ = r
+  coproductId = Inl id
+
+instance (Category q, Ob q y) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Right y :: Either i j) where
+  side _ _ r = r
+  coproductId = Inr id
+
+instance (Category p, Category q) => Functor (Coproduct p q) where
+  type Dom (Coproduct p q) = Op (Coproduct p q)
+  type Cod (Coproduct p q) = Nat (Coproduct p q) (->)
+  fmap (Op f) = Nat (. f)
+
+instance (Category p, Category q) => Functor (Coproduct p q a) where
+  type Dom (Coproduct p q a) = Coproduct p q
+  type Cod (Coproduct p q a) = (->)
+  fmap = (.)
+
+instance (Category p, Category q) => Category' (Coproduct p q) where
+  type Ob (Coproduct p q) = CoproductOb p q
+  id = coproductId
+  observe (Inl f) = case observe f of
+    Dict -> Dict
+  observe (Inr f) = case observe f of
+    Dict -> Dict
+  Inl f . Inl g = Inl (f . g)
+  Inr f . Inr g = Inr (f . g)
+  _ . _ = error "Type error"
+
+--------------------------------------------------------------------------------
+-- * The Unit category
+--------------------------------------------------------------------------------
+
+data Unit a b = Unit
+
+instance Functor Unit where
+  type Dom Unit = Op Unit
+  type Cod Unit = Nat Unit (->)
+  fmap _ = Nat $ \_ -> Unit
+
+instance Functor (Unit a) where
+  type Dom (Unit a) = Unit
+  type Cod (Unit a) = (->)
+  fmap _ _ = Unit
+
+instance Category' Unit where
+  type Ob Unit = Vacuous Unit
+  id = Unit
+  Unit . Unit = Unit
+  observe _ = Dict
+
+instance FullyFaithful Unit where
+  unfmap _ = Op Unit
+
+instance FullyFaithful (Unit a) where
+  unfmap _ = Unit
+
+
+--------------------------------------------------------------------------------
+-- * The Empty category
+--------------------------------------------------------------------------------
+
+data Empty (a :: Void) (b :: Void)
+
+{-
+instance Functor Empty where
+  type Dom Empty = Op Empty
+  type Cod Empty = Nat Empty (->)
+  fmap f = case f of {}
+
+instance No (:-) a => Functor (Empty a) where
+  type Dom (Empty a) = Empty
+  type Cod (Empty a) = (->)
+  fmap f = case f of {}
+
+data NO = No
+
+-- | the functor from the empty category to every category
+type No = (Any 'No :: (i -> i -> *) -> Void -> i)
+
+-- | the empty category
+instance Category' c => Functor (No c) where
+  type Dom (No c) = Empty
+  type Cod (No c) = c
+  fmap f = case f of {}
+
+instance Category' Empty where
+  type Ob Empty = No (:-)
+  id = undefined -- no
+  f . _ = case f of {}
+  observe f = case f of {}
+-}
+
diff --git a/src/Hask/Functor/Faithful.hs b/src/Hask/Functor/Faithful.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Functor/Faithful.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE NoImplicitPrelude, ConstraintKinds, PolyKinds #-}
+
+module Hask.Functor.Faithful where
+
+import Hask.Category
+
+--------------------------------------------------------------------------------
+-- * Fully Faithful Functors
+--------------------------------------------------------------------------------
+
+class Functor f => FullyFaithful f where
+  unfmap :: Cod f (f a) (f b) -> Dom f a b
+
+instance FullyFaithful Dict where
+  unfmap f = Sub $ f Dict
+
+instance FullyFaithful (->) where
+  unfmap (Nat f) = Op (f id)
+
+instance FullyFaithful (:-) where
+  unfmap (Nat f) = Op (f id)
diff --git a/src/Hask/Iso.hs b/src/Hask/Iso.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Iso.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE NoImplicitPrelude, KindSignatures, PolyKinds, ConstraintKinds, TypeFamilies, UndecidableInstances, DataKinds, ScopedTypeVariables, RankNTypes, AllowAmbiguousTypes, FlexibleContexts #-}
+module Hask.Iso
+  ( 
+  -- * Iso
+    Iso
+  -- * Get
+  , Get, _Get, get
+  -- * Beget
+  , Beget, _Beget, beget, (#)
+  -- * Yoneda 
+  , yoneda
+  ) where
+
+import Hask.Category
+
+--------------------------------------------------------------------------------
+-- *  Iso
+--------------------------------------------------------------------------------
+
+type Iso c d e s t a b = forall p. (Bifunctor p, Opd p ~ c, Dom2 p ~ d, Cod2 p ~ e) => p a b -> p s t
+
+--------------------------------------------------------------------------------
+-- *  Get (Lens)
+--------------------------------------------------------------------------------
+
+newtype Get (c :: i -> i -> *) (r :: i) (a :: i) (b :: i) = Get { runGet :: c a r }
+
+_Get :: Iso (->) (->) (->) (Get c r a b) (Get c r' a' b') (c a r) (c a' r')
+_Get = dimap runGet Get
+
+instance Category c => Functor (Get c) where
+  type Dom (Get c) = c
+  type Cod (Get c) = Nat (Op c) (Nat c (->))
+  fmap = fmap' where
+    fmap' :: c a b -> Nat (Op c) (Nat c (->)) (Get c a) (Get c b)
+    fmap' f = case observe f of
+      Dict -> Nat $ Nat $ _Get (f .)
+
+instance (Category c, Ob c r) => Functor (Get c r) where
+  type Dom (Get c r) = Op c
+  type Cod (Get c r) = Nat c (->)
+  fmap f = case observe f of
+    Dict -> Nat $ _Get $ (. unop f)
+
+instance (Category c, Ob c r, Ob c a) => Functor (Get c r a) where
+  type Dom (Get c r a) = c
+  type Cod (Get c r a) = (->)
+  fmap _ = _Get id
+
+get :: (Category c, Ob c a) => (Get c a a a -> Get c a s s) -> c s a
+get l = runGet $ l (Get id)
+
+--------------------------------------------------------------------------------
+-- * Beget (Lens)
+--------------------------------------------------------------------------------
+
+newtype Beget (c :: i -> i -> *) (r :: i) (a :: i) (b :: i) = Beget { runBeget :: c r b }
+
+_Beget :: Iso (->) (->) (->) (Beget c r a b) (Beget c r' a' b') (c r b) (c r' b')
+_Beget = dimap runBeget Beget
+
+instance Category c => Functor (Beget c) where
+  type Dom (Beget c) = Op c
+  type Cod (Beget c) = Nat (Op c) (Nat c (->))
+  fmap = fmap' where
+    fmap' :: Op c a b -> Nat (Op c) (Nat c (->)) (Beget c a) (Beget c b)
+    fmap' f = case observe f of
+      Dict -> Nat $ Nat $ _Beget (. op f)
+
+instance (Category c, Ob c r) => Functor (Beget c r) where
+  type Dom (Beget c r) = Op c
+  type Cod (Beget c r) = Nat c (->)
+  fmap f = case observe f of
+    Dict -> Nat $ _Beget id
+
+instance (Category c, Ob c r, Ob c a) => Functor (Beget c r a) where
+  type Dom (Beget c r a) = c
+  type Cod (Beget c r a) = (->)
+  fmap f = _Beget (f .)
+
+beget :: (Category c, Ob c b) => (Beget c b b b -> Beget c b t t) -> c b t
+beget l = runBeget $ l (Beget id)
+
+(#) :: (Beget (->) b b b -> Beget (->) b t t) -> b -> t
+(#) = beget
+
+--------------------------------------------------------------------------------
+-- * The Yoneda Lemma
+--------------------------------------------------------------------------------
+
+yoneda :: forall p f g a b. (Ob p a, FunctorOf p (->) g, FunctorOf p (->) (p b))
+       => Iso (->) (->) (->)
+          (Nat p (->) (p a) f)
+          (Nat p (->) (p b) g)
+          (f a)
+          (g b)
+yoneda = dimap hither yon where
+  hither :: Nat p (->) (p a) f -> f a
+  hither (Nat f) = f id
+  yon :: g b -> Nat p (->) (p b) g
+  yon gb = Nat $ \pba -> fmap pba gb
+
diff --git a/src/Hask/Prof.hs b/src/Hask/Prof.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Prof.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE CPP, KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, DefaultSignatures #-}
+module Hask.Prof 
+  ( Prof, ProfunctorOf, Procompose(..)
+  ) where
+
+import Hask.Category
+
+type Prof c d = Nat (Op c) (Nat d (->))
+
+class    (Bifunctor f, Dom f ~ Op p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
+instance (Bifunctor f, Dom f ~ Op p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
+
+data Procompose (c :: i -> i -> *) (d :: j -> j -> *) (e :: k -> k -> *)
+                (p :: j -> k -> *) (q :: i -> j -> *) (a :: i) (b :: k) where
+  Procompose :: Ob d x => p x b -> q a x -> Procompose c d e p q a b
+
+instance (Category c, Category d, Category e) => Functor (Procompose c d e) where
+  type Dom (Procompose c d e) = Prof d e
+  type Cod (Procompose c d e) = Nat (Prof c d) (Prof c e)
+  fmap = fmap' where
+    fmap' :: Prof d e a b -> Nat (Prof c d) (Prof c e) (Procompose c d e a) (Procompose c d e b)
+    fmap' (Nat n) = Nat $ Nat $ Nat $ \(Procompose p q) -> Procompose (runNat n p) q
+
+instance (Category c, Category d, Category e, ProfunctorOf d e p) => Functor (Procompose c d e p) where
+  type Dom (Procompose c d e p) = Prof c d
+  type Cod (Procompose c d e p) = Prof c e
+  fmap = fmap' where
+    fmap' :: Prof c d a b -> Prof c e (Procompose c d e p a) (Procompose c d e p b)
+    fmap' (Nat n) = Nat $ Nat $ \(Procompose p q) -> Procompose p (runNat n q)
+
+instance (Category c, Category d, Category e, ProfunctorOf d e p, ProfunctorOf c d q) => Functor (Procompose c d e p q) where
+  type Dom (Procompose c d e p q) = Op c
+  type Cod (Procompose c d e p q) = Nat e (->)
+  fmap f = case observe f of
+    Dict -> Nat $ \(Procompose p q) -> Procompose p (runNat (fmap f) q)
+
+instance (Category c, Category d, Category e, ProfunctorOf d e p, ProfunctorOf c d q, Ob c a) => Functor (Procompose c d e p q a) where
+  type Dom (Procompose c d e p q a) = e
+  type Cod (Procompose c d e p q a) = (->)
+  fmap f (Procompose p q) = Procompose (fmap1 f p) q
+
+-- TODO
+
+{-
+associateProcompose :: Iso (Prof c e) (Prof c e) (->)
+  (Procompose c d f (Procompose d e f p q) r) (Procompose c' d' f' (Procompose d' e' f' p' q') r')
+  (Procompose c e f p (Procompose c d e q r)) (Procompose c' e' f' p' (Procompose c' d' e' q' r'))
+associateProcompose = dimap
+  (Nat $ Nat $ \ (Procompose (Procompose a b) c) -> Procompose a (Procompose b c))
+  (Nat $ Nat $ \ (Procompose a (Procompose b c)) -> Procompose (Procompose a b) c)
+-}
diff --git a/src/Hask/Tensor.hs b/src/Hask/Tensor.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Tensor.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, AllowAmbiguousTypes, LambdaCase, DefaultSignatures, EmptyCase #-}
+module Hask.Tensor
+  ( 
+  -- * Tensors
+    Semitensor(..), I, Tensor'(..), Tensor, semitensorClosed
+  -- * Monoids
+  , Semigroup(..), Monoid'(..), Monoid
+  -- * Comonoids (Opmonoids)
+  , Cosemigroup(..), Comonoid'(..), Comonoid
+  ) where
+
+import Hask.Category
+import Hask.Iso
+import Data.Void
+
+--------------------------------------------------------------------------------
+-- * Monoidal Tensors and Monoids
+--------------------------------------------------------------------------------
+
+class (Bifunctor p, Dom p ~ Dom2 p, Dom p ~ Cod2 p) => Semitensor p where
+  associate :: (Ob (Dom p) a, Ob (Dom p) b, Ob (Dom p) c, Ob (Dom p) a', Ob (Dom p) b', Ob (Dom p) c')
+            => Iso (Dom p) (Dom p) (->) 
+                (p (p a b) c)     (p (p a' b') c')
+                (p a (p b c))     (p a' (p b' c'))
+
+semitensorClosed :: forall c t x y. (Semitensor t, Category c, Dom t ~ c, Ob c x, Ob c y) => Dict (Ob c (t x y))
+semitensorClosed = case ob :: Ob c x :- FunctorOf c c (t x) of
+  Sub Dict -> case ob :: Ob c y :- Ob c (t x y) of
+    Sub Dict -> Dict
+
+type family I (p :: i -> i -> i) :: i
+
+class Semitensor p => Tensor' p where
+  lambda :: (Ob (Dom p) a, Ob (Dom p) a') => Iso (Dom p) (Dom p) (->) (p (I p) a) (p (I p) a') a a'
+  rho    :: (Ob (Dom p) a, Ob (Dom p) a') => Iso (Dom p) (Dom p) (->) (p a (I p)) (p a' (I p)) a a'
+
+class (Monoid' p (I p), Tensor' p) => Tensor p
+instance (Monoid' p (I p), Tensor' p) => Tensor p
+
+class Semitensor p => Semigroup p m where
+  mu :: Dom p (p m m) m
+
+class (Semigroup p m, Tensor' p) => Monoid' p m where
+  eta :: NatId p -> Dom p (I p) m
+
+class (Monoid' p (I p), Comonoid' p (I p), Tensor' p, Monoid' p m) => Monoid p m
+instance (Monoid' p (I p), Comonoid' p (I p), Tensor' p, Monoid' p m) => Monoid p m
+
+class Semitensor p => Cosemigroup p w where
+  delta :: Dom p w (p w w)
+
+class (Cosemigroup p w, Tensor' p) => Comonoid' p w where
+  epsilon :: NatId p -> Dom p w (I p)
+
+class (Monoid' p (I p), Comonoid' p (I p), Tensor' p, Comonoid' p w) => Comonoid p w
+instance (Monoid' p (I p), Comonoid' p (I p), Tensor' p, Comonoid' p w) => Comonoid p w
+
+--------------------------------------------------------------------------------
+-- * (&)
+--------------------------------------------------------------------------------
+
+class (p, q) => p & q
+instance (p, q) => p & q
+
+instance Functor (&) where
+  type Dom (&) = (:-)
+  type Cod (&) = Nat (:-) (:-)
+  fmap f = Nat $ Sub $ Dict \\ f
+
+instance Functor ((&) a) where
+  type Dom ((&) a) = (:-)
+  type Cod ((&) a) = (:-)
+  fmap f = Sub $ Dict \\ f
+
+instance Semitensor (&) where
+  associate = dimap (Sub Dict) (Sub Dict)
+
+type instance I (&) = (() :: Constraint)
+
+instance Tensor' (&) where
+  lambda = dimap (Sub Dict) (Sub Dict)
+  rho    = dimap (Sub Dict) (Sub Dict)
+
+instance Semigroup (&) a where
+  mu = Sub Dict
+
+instance Monoid' (&) (() :: Constraint) where
+  eta _ = Sub Dict
+
+instance Cosemigroup (&) a where
+  delta = Sub Dict
+
+instance Comonoid' (&) a where
+  epsilon _ = Sub Dict
+
+--------------------------------------------------------------------------------
+-- * (,) and ()
+--------------------------------------------------------------------------------
+
+instance Semitensor (,) where
+  associate = dimap (\((a,b),c) -> (a,(b,c))) (\(a,(b,c)) -> ((a,b),c))
+
+type instance I (,) = ()
+
+instance Tensor' (,) where
+  lambda = dimap (\ ~(_,a) -> a) ((,)())
+  rho    = dimap (\ ~(a,_) -> a) (\a -> (a,()))
+
+instance Semigroup (,) () where
+  mu ((),()) = ()
+
+instance Monoid' (,) () where
+  eta _ = id
+
+instance Cosemigroup (,) a where
+  delta a = (a,a)
+
+instance Comonoid' (,) a where
+  epsilon _ _ = ()
+
+--------------------------------------------------------------------------------
+-- * Either and Void
+--------------------------------------------------------------------------------
+
+instance Semitensor Either where
+  associate = dimap hither yon where
+    hither (Left (Left a))  = Left a
+    hither (Left (Right b)) = Right (Left b)
+    hither (Right c)        = Right (Right c)
+    yon (Left a)            = Left (Left a)
+    yon (Right (Left b))    = Left (Right b)
+    yon (Right (Right c))   = Right c
+
+type instance I Either = Void
+
+instance Tensor' Either where
+  lambda = dimap (\(Right a) -> a) Right
+  rho = dimap (\(Left a) -> a) Left
+
+instance Semigroup (,) Void where
+  mu (a,_) = a
+
+instance Semigroup Either Void where
+  mu (Left a)  = a
+  mu (Right b) = b
+
+instance Monoid' Either Void where
+  eta _ = absurd
+
+instance Cosemigroup Either Void  where
+  delta = absurd
+
+instance Comonoid' Either Void where
+  epsilon _ = id
diff --git a/src/Hask/Tensor/Compose.hs b/src/Hask/Tensor/Compose.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Tensor/Compose.hs
@@ -0,0 +1,143 @@
+{-# LANGUAGE KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, AllowAmbiguousTypes, LambdaCase, DefaultSignatures, EmptyCase #-}
+module Hask.Tensor.Compose where
+
+import Data.Constraint.Unsafe (unsafeCoerceConstraint)
+import GHC.Prim (Any)
+import Hask.Category
+import Hask.Iso
+import Hask.Tensor
+import Unsafe.Coerce (unsafeCoerce)
+
+--------------------------------------------------------------------------------
+-- * Compose
+--------------------------------------------------------------------------------
+
+data COMPOSE = Compose
+type Compose = (Any 'Compose :: (i -> i -> *) -> (j -> j -> *) -> (k -> k -> *) -> (j -> k) -> (i -> j) -> i -> k)
+
+class Category e => Composed (e :: k -> k -> *) where
+  _Compose :: (FunctorOf d e f, FunctorOf d e f', FunctorOf c d g, FunctorOf c d g') => Iso
+    e e (->)
+    (Compose c d e f g a) (Compose c d e f' g' a')
+    (f (g a))             (f' (g' a'))
+
+instance Composed (->) where
+  _Compose = unsafeCoerce
+
+instance Composed (:-) where
+  _Compose = unsafeCoerce
+
+instance (Category c, Composed d) => Composed (Nat c d) where
+  _Compose = unsafeCoerce -- really evil, like super-villain evil
+
+instance (Category c, Category d, Category e) => Class (f (g a)) (Compose c d e f g a) where cls = unsafeCoerceConstraint
+instance (Category c, Category d, Category e) => f (g a) :=> Compose c d e f g a where ins = unsafeCoerceConstraint
+
+instance (Category c, Category d, Composed e) => Functor (Compose c d e) where
+  type Dom (Compose c d e) = Nat d e
+  type Cod (Compose c d e) = Nat (Nat c d) (Nat c e)
+  fmap = fmap' where
+    fmap' :: Nat d e a b -> Nat (Nat c d) (Nat c e) (Compose c d e a) (Compose c d e b)
+    fmap' n@Nat{} = nat $ \g -> nat $ \a -> _Compose $ n ! g ! a
+
+instance (Category c, Category d, Composed e, Functor f, e ~ Cod f, d ~ Dom f) => Functor (Compose c d e f) where
+  type Dom (Compose c d e f) = Nat c d
+  type Cod (Compose c d e f) = Nat c e
+  fmap (Nat f) = Nat $ _Compose $ fmap f
+
+instance (Category c, Category d, Composed e, Functor f, Functor g, e ~ Cod f, d ~ Cod g, d ~ Dom f, c ~ Dom g) => Functor (Compose c d e f g) where
+  type Dom (Compose c d e f g) = c
+  type Cod (Compose c d e f g) = e
+  fmap f = _Compose $ fmap $ fmap f
+
+instance (Composed c, c ~ c', c' ~ c'') => Semitensor (Compose c c' c'' :: (i -> i) -> (i -> i) -> (i -> i)) where
+  associate = associateCompose
+
+data ID = Id
+type Id = (Any 'Id :: (i -> i -> *) -> i -> i)
+
+class Category c => Identified (c :: i -> i -> *) where
+  _Id :: Iso c c (->) (Id c a) (Id c a') a a'
+
+instance Identified (->) where
+  _Id = unsafeCoerce
+
+instance Identified (:-) where
+  _Id = unsafeCoerce
+
+instance (Category c, Identified d) => Identified (Nat c d) where
+  _Id = unsafeCoerce
+
+instance Category c => Class a (Id c a) where cls = unsafeCoerceConstraint
+instance Category c => a :=> Id c a where ins = unsafeCoerceConstraint
+
+instance Identified c => Functor (Id c) where
+  type Dom (Id c) = c
+  type Cod (Id c) = c
+  fmap = _Id
+
+type instance I (Compose c c c) = Id c
+
+instance (Identified c, Composed c) => Semigroup (Compose c c c) (Id c) where
+  mu = dimap (get lambda) id id
+
+instance (Identified c, Composed c) => Monoid' (Compose c c c) (Id c) where
+  eta _ = Nat $ _Id id
+
+instance (Identified c, Composed c) => Cosemigroup (Compose c c c) (Id c) where
+  delta = dimap id (beget lambda) id
+
+instance (Identified c, Composed c) => Comonoid' (Compose c c c) (Id c) where
+  epsilon _ = Nat $ _Id id
+
+instance (Identified c, Composed c) => Tensor' (Compose c c c :: (i -> i) -> (i -> i) -> (i -> i)) where
+  lambda = lambdaCompose
+  rho = rhoCompose
+
+associateCompose :: forall b c d e f g h f' g' h'.
+   ( Category b, Category c, Composed d, Composed e
+   , FunctorOf d e f, FunctorOf c d g, FunctorOf b c h
+   , FunctorOf d e f', FunctorOf c d g', FunctorOf b c h'
+   ) => Iso (Nat b e) (Nat b e) (->)
+  (Compose b c e (Compose c d e f g) h) (Compose b c e (Compose c d e f' g') h')
+  (Compose b d e f (Compose b c d g h)) (Compose b d e f' (Compose b c d g' h'))
+associateCompose = dimap hither yon where
+  hither = nat $ \a -> case obOf (id :: NatId f) $ (id :: NatId g) ! (id :: NatId h) ! a of
+    Dict -> case obOf (id :: NatId f) $ (id :: NatId (Compose b c d g h)) ! a of
+      Dict -> case obOf (id :: NatId (Compose c d e f g)) $ (id :: NatId h) ! a of
+        Dict -> beget _Compose . fmap (beget _Compose) . get _Compose . get _Compose
+  yon = nat $ \a -> case obOf (id :: NatId f') $ (id :: NatId g') ! (id :: NatId h') ! a of
+    Dict -> case obOf (id :: NatId f') $ (id :: NatId (Compose b c d g' h')) ! a of
+      Dict -> case obOf (id :: NatId (Compose c d e f' g')) $ (id :: NatId h') ! a of
+        Dict -> beget _Compose . beget _Compose . fmap (get _Compose) . get _Compose
+
+lambdaCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a')
+              => Iso (Nat c c) (Nat c c) (->) (Compose c c c (Id c) a) (Compose c c c (Id c) a') a a'
+lambdaCompose = dimap hither yon where
+  hither = nat $ \z -> case obOf (id :: NatId (Id c)) $ (id :: NatId a) ! z of
+    Dict -> get _Id . get _Compose
+  yon = nat $ \z -> case obOf (id :: NatId (Id c)) $ (id :: NatId a') ! z of
+    Dict -> beget _Compose . beget _Id
+
+rhoCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a')
+           => Iso (Nat c c) (Nat c c) (->) (Compose c c c a (Id c)) (Compose c c c a' (Id c)) a a'
+rhoCompose = dimap hither yon where
+  hither = nat $ \z -> case obOf (id :: NatId a) $ (id :: NatId (Id c)) ! z of
+    Dict -> fmap (get _Id) . get _Compose
+  yon = nat $ \z -> case obOf (id :: NatId a') $ (id :: NatId (Id c)) ! z of
+    Dict -> beget _Compose . fmap (beget _Id)
+
+--------------------------------------------------------------------------------
+-- ** Monads
+--------------------------------------------------------------------------------
+
+class    (Functor m, Dom m ~ Cod m, Monoid (Compose (Dom m) (Dom m) (Dom m)) m, Identified (Dom m), Composed (Dom m)) => Monad m
+instance (Functor m, Dom m ~ Cod m, Monoid (Compose (Dom m) (Dom m) (Dom m)) m, Identified (Dom m), Composed (Dom m)) => Monad m
+
+return :: forall m a. (Monad m, Ob (Dom m) a) => Dom m a (m a)
+return = runNat (eta (id :: NatId (Compose (Dom m) (Dom m) (Dom m)))) . beget _Id
+
+bind :: forall m a b. (Monad m, Ob (Dom m) b) => Dom m a (m b) -> Dom m (m a) (m b)
+bind f = case observe f of
+  Dict -> case obOf (id :: NatId m) (id :: Endo (Cod m) (m b)) of
+    Dict -> runNat mu . beget _Compose . fmap f
diff --git a/src/Hask/Tensor/Day.hs b/src/Hask/Tensor/Day.hs
new file mode 100644
--- /dev/null
+++ b/src/Hask/Tensor/Day.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, AllowAmbiguousTypes, LambdaCase, DefaultSignatures, EmptyCase #-}
+module Hask.Tensor.Day where
+
+import Hask.Category
+import Hask.Iso
+import Hask.Tensor
+import Prelude ()
+
+--------------------------------------------------------------------------------
+-- * Day Convolution
+--------------------------------------------------------------------------------
+
+class FunctorOf c (->) f => CopresheafOf c f
+instance FunctorOf c (->) f => CopresheafOf c f
+
+data Day (t :: i -> i -> i) (f :: i -> *) (g :: i -> *) (a :: i) where
+  Day :: (Dom t ~ c, CopresheafOf c f, CopresheafOf c g, Ob c x, Ob c y)
+      => c (t x y) a -> f x -> g y -> Day t f g a
+
+--Day convolution of copresheaves is a copresheaf
+
+instance (Dom t ~ c, CopresheafOf c f, CopresheafOf c g) => Functor (Day t f g) where
+  type Dom (Day t f g) = Dom t
+  type Cod (Day t f g) = (->)
+  fmap c' (Day c fx gy) = Day (c' . c) fx gy
+
+--Day convolution is a bifunctor of copresheaves
+
+instance (Dom t ~ c, CopresheafOf c f) => Functor (Day t f) where
+  type Dom (Day t f) = Copresheaves (Dom t)
+  type Cod (Day t f) = Copresheaves (Dom t)
+  fmap = fmap' where
+    fmap' :: Copresheaves c g g' -> Copresheaves c (Day t f g) (Day t f g')
+    fmap' (Nat natg) = Nat $ \(Day c fx gy) -> Day c fx (natg gy)
+
+instance (Dom t ~ c, Category c) => Functor (Day t) where
+  type Dom (Day t) = Copresheaves (Dom t)
+  type Cod (Day t) = Nat (Copresheaves (Dom t)) (Copresheaves (Dom t))
+  fmap = fmap' where
+    fmap' :: Copresheaves c f f' -> Nat (Copresheaves c) (Copresheaves c) (Day t f) (Day t f')
+    fmap' (Nat natf) = Nat $ Nat $ \(Day c fx gy) -> Day c (natf fx) gy
+
+--Day convolution on a monoidal category is associative
+
+instance (Semitensor t, Dom t ~ c, Category c) => Semitensor (Day t) where
+  associate = dimap (Nat hither) (Nat yon) where
+    hither :: Day t (Day t f g) h a -> Day t f (Day t g h) a
+    hither (Day (c' :: c (t b z) a) (Day (c :: c (t x y) b) fx gy) hz) =
+      case semitensorClosed :: Dict (Ob c (t y z)) of
+        Dict -> case semitensorClosed :: Dict (Ob c (t x (t y z))) of
+          Dict -> Day (c' . runNat (fmap c) . beget associate) fx (Day id gy hz)
+    yon :: Day t f (Day t g h) a -> Day t (Day t f g) h a
+    yon (Day (c' :: c (t x b) a) fx (Day (c :: c (t y z) b) gy hz)) =
+      case semitensorClosed :: Dict (Ob c (t x y)) of
+        Dict -> case semitensorClosed :: Dict (Ob c (t y z)) of
+          Dict -> case semitensorClosed :: Dict (Ob c (t x (t y z))) of
+            Dict -> Day (c' . fmap1 c . get associate) (Day id fx gy) hz
+
+--Day convolution on a monoidal category is left & right unital
+
+--type instance (Dom t ~ c, Category c) => I (Day t) = c (I t)