diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for squares
+
+## 0 -- 2020-05-22
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2020, Sjoerd Visscher
+
+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 Sjoerd Visscher 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/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/squares.cabal b/squares.cabal
new file mode 100644
--- /dev/null
+++ b/squares.cabal
@@ -0,0 +1,30 @@
+cabal-version:       >=1.10
+
+name:                squares
+version:             0
+synopsis:            The double category of Hask functors and profunctors
+homepage:            https://github.com/sjoerdvisscher/squares
+bug-reports:         https://github.com/sjoerdvisscher/squares/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Sjoerd Visscher
+maintainer:          sjoerd@w3future.com
+category:            Math
+build-type:          Simple
+extra-source-files:  CHANGELOG.md
+
+library
+  exposed-modules:     Data.Square
+                       Data.Type.List
+                       Data.Functor.Compose.List
+                       Data.Profunctor.Composition.List
+                       Data.Profunctor.Square
+                       Data.Traversable.Square
+                       Control.Monad.Square
+  build-depends:       base == 4.*, profunctors == 5.*
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: git://github.com/sjoerdvisscher/squares.git
diff --git a/src/Control/Monad/Square.hs b/src/Control/Monad/Square.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Square.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Square
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Control.Monad.Square where
+
+import Prelude hiding (return)
+import Data.Square
+import Data.Profunctor
+import Data.Profunctor.Square
+import qualified Control.Monad as M
+
+-- |
+-- > +-----+
+-- > |     |
+-- > |  R->m
+-- > |     |
+-- > +-----+
+return :: Monad m => Square '[] '[Star m] '[] '[]
+return = toHom ||| proNat (Star . (M.return .))
+
+-- |
+-- > +--m--+
+-- > |  v  |
+-- > m>-B  |
+-- > |  v  |
+-- > +--m--+
+--
+-- `(>>=)`
+--
+-- Left identity law:
+--
+-- > +-------+
+-- > | R>-\  +     +-----+
+-- > |    v  |     |     |
+-- > m>---B  | === m>-\  |
+-- > |    v  |     |  v  |
+-- > +----m--+     +--m--+
+--
+-- Right identity law:
+--
+-- > +----m--+     +--m--+
+-- > |    v  |     |  |  |
+-- > | R>-B  | === |  v  |
+-- > |    v  |     |  |  |
+-- > +----m--+     +--m--+
+--
+-- Associativity law:
+--
+-- > +--m--+     +-----m--+
+-- > |  v  |     m>-\  v  |
+-- > m>-B  |     |  v  |  |
+-- > |  v  | === m>-B  |  |
+-- > m>-B  |     |  \->B  |
+-- > |  v  |     |     v  |
+-- > +--m--+     +-----m--+
+bind :: Monad m => Square '[Star m] '[] '[m] '[m]
+bind = mkSquare (flip (>>=) . runStar) ||| fromHom
+
+-- |
+-- > +-m-m-+
+-- > | v v |
+-- > | \-@ |
+-- > |   v |
+-- > +---m-+
+--
+-- @join = toRight ||| bind@
+join :: Monad m => Square '[] '[] '[m, m] '[m]
+join = toRight ||| bind
+
+-- |
+-- > +-----+
+-- > m>-\  |
+-- > m>-@  |
+-- > |  \->m
+-- > +-----+
+--
+-- Kleisli composition `(M.>=>)`
+kleisli :: Monad m => Square '[Star m, Star m] '[Star m] '[] '[]
+kleisli = fromLeft === bind === toRight
diff --git a/src/Data/Functor/Compose/List.hs b/src/Data/Functor/Compose/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Compose/List.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Functor.Compose.List
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Functor.Compose.List where
+
+import Data.Type.List
+
+-- | N-ary composition of functors.
+--
+-- > FList '[] a ~ a
+-- > FList '[f, g, h] a ~ h (g (f a))
+data FList (fs :: [* -> *]) (a :: *) where
+  Id :: { unId :: a } -> FList '[] a
+  F :: { unF :: f a } -> FList '[f] a
+  FComp :: { unFComp :: FList (g ': gs) (f a) } -> FList (f ': g ': gs) a
+
+instance Functor (FList '[]) where
+  fmap f = Id . f . unId
+instance Functor f => Functor (FList '[f]) where
+  fmap f = F . fmap f . unF
+instance (Functor f, Functor (FList (g ': gs))) => Functor (FList (f ': g ': gs)) where
+  fmap f = FComp . fmap (fmap f) . unFComp
+
+
+-- | Combining and splitting nested `FList`s.
+class FAppend f where
+  fappend :: Functor (FList g) => FList g (FList f a) -> FList (f ++ g) a
+  funappend :: Functor (FList g) => FList (f ++ g) a -> FList g (FList f a)
+instance FAppend '[] where
+  fappend = fmap unId
+  funappend = fmap Id
+instance FAppend '[f] where
+  fappend (Id fa) = F (unF fa)
+  fappend f@F{} = FComp $ fmap unF f
+  fappend f@FComp{} = FComp $ fmap unF f
+  funappend fa@F{} = Id fa
+  funappend (FComp fga@F{}) = fmap F fga
+  funappend (FComp fga@FComp{}) = fmap F fga
+instance (Functor f, FAppend (g ': gs)) => FAppend (f ': g ': gs) where
+  fappend = FComp . fappend . fmap unFComp
+  funappend = fmap FComp . funappend . unFComp
+
+
+-- | Natural transformations between two functors. (Why is this still not in base??)
+type f ~> g = forall a. f a -> g a
diff --git a/src/Data/Profunctor/Composition/List.hs b/src/Data/Profunctor/Composition/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Composition/List.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Profunctor.Composition.List
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Profunctor.Composition.List where
+
+import Data.Profunctor
+import Data.Profunctor.Composition
+import Data.Type.List
+
+-- | N-ary composition of profunctors.
+data PList (ps :: [* -> * -> *]) (a :: *) (b :: *) where
+  Hom :: { unHom :: a -> b } -> PList '[] a b
+  P :: { unP :: p a b } -> PList '[p] a b
+  PComp :: p a x -> PList (q ': qs) x b -> PList (p ': q ': qs) a b
+
+instance Profunctor (PList '[]) where
+  dimap l r (Hom f) = Hom (r . f . l)
+instance Profunctor p => Profunctor (PList '[p]) where
+  dimap l r (P p) = P (dimap l r p)
+instance (Profunctor p, Profunctor (PList (q ': qs))) => Profunctor (PList (p ': q ': qs)) where
+  dimap l r (PComp p ps) = PComp (lmap l p) (rmap r ps)
+
+-- | Combining and splitting nested `PList`s.
+class PAppend p where
+  pappend :: Profunctor (PList q) => Procompose (PList q) (PList p) a b -> PList (p ++ q) a b
+  punappend :: PList (p ++ q) a b -> Procompose (PList q) (PList p) a b
+instance PAppend '[] where
+  pappend (Procompose q (Hom f)) = lmap f q
+  punappend q = Procompose q (Hom id)
+instance Profunctor p => PAppend '[p] where
+  pappend (Procompose (Hom f) (P p)) = P (rmap f p)
+  pappend (Procompose q@P{} (P p)) = PComp p q
+  pappend (Procompose q@PComp{} (P p)) = PComp p q
+  punappend p@P{} = Procompose (Hom id) p
+  punappend (PComp p qs) = Procompose qs (P p)
+instance (Profunctor p, PAppend (q ': qs)) => PAppend (p ': q ': qs) where
+  pappend (Procompose q (PComp p ps)) = PComp p (pappend (Procompose q ps))
+  punappend (PComp p pq) = case punappend pq of Procompose q ps -> Procompose q (PComp p ps)
diff --git a/src/Data/Profunctor/Square.hs b/src/Data/Profunctor/Square.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Square.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Profunctor.Square
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Profunctor.Square where
+
+import Data.Square
+import Data.Functor.Compose.List
+import Data.Profunctor.Composition.List
+import qualified Data.Profunctor as P
+import Data.Profunctor.Composition
+
+-- * Squares for profunctor subclasses
+
+-- |
+-- > +-a⊗_-+
+-- > |  v  |
+-- > p--@--p
+-- > |  v  |
+-- > +-a⊗_-+
+second :: P.Strong p => Square '[p] '[p] '[(,) a] '[(,) a]
+second = mkSquare P.second'
+
+-- |
+-- > +-a⊕_-+
+-- > |  v  |
+-- > p--@--p
+-- > |  v  |
+-- > +-a⊕_-+
+right :: P.Choice p => Square '[p] '[p] '[Either a] '[Either a]
+right = mkSquare P.right'
+
+-- |
+-- > +-a→_-+
+-- > |  v  |
+-- > p--@--p
+-- > |  v  |
+-- > +-a→_-+
+closed :: P.Closed p => Square '[p] '[p] '[(->) a] '[(->) a]
+closed = mkSquare P.closed
+
+-- |
+-- > +--f--+
+-- > |  v  |
+-- > p--@--p
+-- > |  v  |
+-- > +--f--+
+map :: (P.Mapping p, Functor f) => Square '[p] '[p] '[f] '[f]
+map = mkSquare P.map'
+
+-- * Squares for @(->)@
+
+-- |
+-- >  +-----+
+-- >  |     |
+-- > (→)-@  |
+-- >  |     |
+-- >  +-----+
+fromHom :: Square '[(->)] '[] '[] '[]
+fromHom = Square (Hom . P.dimap unId Id . unP)
+
+-- |
+-- > +-----+
+-- > |     |
+-- > |  @-(→)
+-- > |     |
+-- > +-----+
+toHom :: Square '[] '[(->)] '[] '[]
+toHom = Square (P . P.dimap unId Id . unHom)
+
+-- * Squares for `Procompose`
+
+-- |
+-- >  +-----+
+-- >  |   /-p
+-- > q.p-@  |
+-- >  |   \-q
+-- >  +-----+
+fromProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[Procompose q p] '[p, q] '[] '[]
+fromProcompose = Square ((\(Procompose q p) -> PComp (P.lmap unId p) (P (P.rmap Id q))) . unP)
+
+-- |
+-- >  +-----+
+-- >  p-\   |
+-- >  |  @-q.p
+-- >  q-/   |
+-- >  +-----+
+toProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[p, q] '[Procompose q p] '[] '[]
+toProcompose = Square (P . (\(PComp p (P q)) -> Procompose (P.rmap Id q) (P.lmap unId p)))
diff --git a/src/Data/Square.hs b/src/Data/Square.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Square.hs
@@ -0,0 +1,337 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE FlexibleContexts #-}
+#if __GLASGOW_HASKELL__ >= 810
+{-# LANGUAGE StandaloneKindSignatures #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Square
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+
+module Data.Square where
+
+import Data.Functor.Compose.List
+import Data.Profunctor
+import qualified Data.Profunctor.Composition as P
+import Data.Profunctor.Composition.List
+import Data.Type.List
+#if __GLASGOW_HASKELL__ >= 810
+import Data.Kind
+#endif
+
+-- * Double category
+
+-- $doubleCategory
+-- There is a double category of Haskell functors and profunctors.
+--
+-- The squares in this double category are natural transformations.
+
+-- |
+-- > +-----+
+-- > |     |
+-- > |     |
+-- > |     |
+-- > +-----+
+--
+-- > forall a b. (a -> b) -> (a -> b)
+--
+-- The empty square is the identity transformation.
+emptySquare :: Square '[] '[] '[] '[]
+emptySquare = Square $ dimap unId Id
+
+-- |
+-- > +-----+
+-- > |     |
+-- > p-----p
+-- > |     |
+-- > +-----+
+--
+-- > forall a b. p a b -> p a b
+--
+-- Profunctors are drawn as horizontal lines.
+--
+-- Note that `emptySquare` is `proId` for the profunctor @(->)@.
+-- We don't draw a line for @(->)@ because it is the identity for profunctor composition.
+proId :: Profunctor p => Square '[p] '[p] '[] '[]
+proId = Square $ dimap unId Id
+
+-- |
+-- > +--f--+
+-- > |  |  |
+-- > |  v  |
+-- > |  |  |
+-- > +--f--+
+--
+-- > forall a b. (a -> b) -> (f a -> f b)
+--
+-- Functors are drawn with vertical lines with arrow heads.
+-- You will recognize the above type as `fmap`!
+--
+-- We don't draw lines for the identity functor, because it is the identity for functor composition.
+funId :: Functor f => Square '[] '[] '[f] '[f]
+funId = Square \(Hom f) -> Hom (fmap f)
+
+-- |
+-- > +--f--+
+-- > |  |  |
+-- > |  @  |
+-- > |  |  |
+-- > +--g--+
+--
+-- > forall a b. (a -> b) -> (f a -> g b)
+--
+-- Non-identity transformations are drawn with an @\@@ in the middle.
+-- Natural transformations between haskell functors are usualy given the type
+-- @forall a. f a -> g a@. The type above you get when `fmap`ping before or after.
+-- (It doesn't matter which, because of naturality!)
+funNat :: (Functor f, Functor g) => (f ~> g) -> Square '[] '[] '[f] '[g]
+funNat n = Square $ Hom . dimap unF F . (.) n . fmap . unHom
+
+-- |
+-- > +-----+
+-- > |     |
+-- > p--@--q
+-- > |     |
+-- > +-----+
+--
+-- > forall a b. p a b -> q a b
+--
+-- Natural transformations between profunctors.
+proNat :: (Profunctor p, Profunctor q) => (p :-> q) -> Square '[p] '[q] '[] '[]
+proNat n = Square $ P . dimap unId Id . n . unP
+
+-- |
+-- > +--f--+
+-- > |  v  |
+-- > p--@--q
+-- > |  v  |
+-- > +--g--+
+--
+-- > forall a b. p a b -> q (f a) (g b)
+--
+-- The complete definition of a square is a combination of natural transformations
+-- between functors and natural transformations between profunctors.
+--
+-- To make type inferencing easier the above type is wrapped by a newtype.
+#if __GLASGOW_HASKELL__ >= 810
+type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
+#endif
+newtype SquareNT p q f g = Square { unSquare :: forall a b. p a b -> q (f a) (g b) }
+
+-- | To make composing squares associative, this library uses squares with lists of functors and profunctors,
+-- which are composed together.
+--
+-- > FList '[] a ~ a
+-- > FList '[f, g, h] a ~ h (g (f a))
+-- > PList '[] a b ~ a -> b
+-- > PList '[p, q, r] a b ~ (p a x, q x y, r y b)
+type Square ps qs fs gs = SquareNT (PList ps) (PList qs) (FList fs) (FList gs)
+
+-- | A helper function to add the wrappers needed for `PList` and `FList`,
+-- if the square has exactly one (pro)functor on each side (which is common).
+mkSquare :: Profunctor q => (forall a b. p a b -> q (f a) (g b)) -> Square '[p] '[q] '[f] '[g]
+mkSquare f = Square (P . dimap unF F . f . unP)
+
+-- |
+-- > +--f--+     +--h--+       +--f--h--+
+-- > |  v  |     |  v  |       |  v  v  |
+-- > p--@--q ||| q--@--r  ==>  p--@--@--r
+-- > |  v  |     |  v  |       |  v  v  |
+-- > +--g--+     +--i--+       +--g--i--+
+--
+-- Horizontal composition of squares. `proId` is the identity of `(|||)`.
+infixl 6 |||
+(|||) :: (Profunctor (PList rs), FAppend fs, FAppend gs, Functor (FList hs), Functor (FList is))
+      => Square ps qs fs gs -> Square qs rs hs is -> Square ps rs (fs ++ hs) (gs ++ is) -- ^
+Square pq ||| Square qr = Square $ dimap funappend fappend . qr . pq
+
+-- |
+-- > +--f--+
+-- > |  v  |
+-- > p--@--q              +--f--+
+-- > |  v  |              |  v  |
+-- > +--g--+              p--@--q
+-- >   ===        ==>     |  v  |
+-- > +--g--+              r--@--s
+-- > |  v  |              |  v  |
+-- > r--@--s              +--h--+
+-- > |  v  |
+-- > +--h--+
+--
+-- Vertical composition of squares. `funId` is the identity of `(===)`.
+infixl 5 ===
+(===) :: (PAppend ps, PAppend qs, Profunctor (PList ss))
+      => Square ps qs fs gs -> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs -- ^
+Square pq === Square rs = Square \pr -> case punappend pr of P.Procompose r p -> pappend (P.Procompose (rs r) (pq p))
+
+
+-- * Proarrow equipment
+--
+-- $proarrowEquipment
+-- The double category of haskell functors and profunctors is a proarrow equipment.
+-- Which means that we can "bend" functors to become profunctors.
+
+-- |
+-- > +--f--+
+-- > |  v  |
+-- > |  \->f
+-- > |     |
+-- > +-----+
+--
+-- A functor @f@ can be bent to the right to become the profunctor @`Star` f@.
+toRight :: Functor f => Square '[] '[Star f] '[f] '[]
+toRight = Square \(Hom f) -> P (Star (fmap (Id . f) . unF))
+
+-- |
+-- > +--f--+
+-- > |  v  |
+-- > f<-/  |
+-- > |     |
+-- > +-----+
+--
+-- A functor @f@ can be bent to the left to become the profunctor @`Costar` f@.
+toLeft :: Square '[Costar f] '[] '[f] '[]
+toLeft = Square \(P (Costar f)) -> Hom (Id . f . unF)
+
+-- |
+-- > +-----+
+-- > |     |
+-- > |  /-<f
+-- > |  v  |
+-- > +--f--+
+--
+-- The profunctor @`Costar` f@ can be bent down to become the functor @f@ again.
+fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]
+fromRight = Square \(Hom f) -> P (Costar (F . fmap (f . unId)))
+
+-- |
+-- > +-----+
+-- > |     |
+-- > f>-\  |
+-- > |  v  |
+-- > +--f--+
+--
+-- The profunctor @`Star` f@ can be bent down to become the functor @f@ again.
+fromLeft :: Square '[Star f] '[] '[] '[f]
+fromLeft = Square \(P (Star f)) -> Hom (F . f . unId)
+
+-- |
+-- > +-----+
+-- > f>-\  |         fromLeft
+-- > |  v  |         ===
+-- > f<-/  |         toLeft
+-- > +-----+
+--
+-- `fromLeft` and `toLeft` can be composed vertically to bend @`Star` f@ back to @`Costar` f@.
+uLeft :: Functor f => Square '[Star f, Costar f] '[] '[] '[]
+uLeft =
+  fromLeft
+  ===
+  toLeft
+
+-- |
+-- > +-----+
+-- > |  /-<f         fromRight
+-- > |  v  |         ===
+-- > |  \->f         toRight
+-- > +-----+
+--
+-- `fromRight` and `toRight` can be composed vertically to bend @`Costar` f@ to @`Star` f@.
+uRight :: Functor f => Square '[] '[Costar f, Star f] '[] '[]
+uRight =
+  fromRight
+  ===
+  toRight
+
+-- |
+-- > +f-f-f+     +--f--+     spiderLemma n =
+-- > |v v v|     f> v <f       fromLeft ||| funId ||| fromRight
+-- > | \|/ |     | \|/ |       ===
+-- > p--@--q ==> p--@--q       n
+-- > | /|\ |     | /|\ |       ===
+-- > |v v v|     g< v >g       toLeft ||| funId ||| toRight
+-- > +g-g-g+     +--g--+
+--
+-- The spider lemma is an example how bending wires can also be seen as sliding functors around corners.
+spiderLemma :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
+  => Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]
+  -> Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2] -- ^
+spiderLemma n =
+  fromLeft ||| funId ||| fromRight
+  ===
+  n
+  ===
+  toLeft ||| funId ||| toRight
+
+-- |> spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)
+--
+-- The spider lemma in the other direction.
+spiderLemma' :: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)
+  => Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]
+  -> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3] -- ^
+spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)
+
+-- * In other categories than Hask
+
+-- $otherCategories
+-- > A--f--C
+-- > |  v  |
+-- > p--@--q
+-- > |  v  |
+-- > B--g--D
+--
+-- Squares can be generalized further by choosing a different category for each quadrant.
+-- To use this, `SquareNT` has been made kind polymorphic:
+--
+-- > type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
+--
+-- This library is mostly about staying in Hask, but it is interesting to use f.e. the
+-- product category @Hask × Hask@ or the unit category.
+
+-- |
+-- > H²-f--H
+-- > |  v  |
+-- > p--@--q     H = Hask, H² = Hask x Hask
+-- > |  v  |
+-- > H²-g--H
+--
+type Square21 ps1 ps2 qs f g = SquareNT (PList ps1 :**: PList ps2) (PList qs) (UncurryF f) (UncurryF g)
+
+-- | Combine two profunctors from Hask to a profunctor from Hask x Hask
+data (p1 :**: p2) a b where
+  (:**:) :: p1 a1 b1 -> p2 a2 b2 -> (p1 :**: p2) '(a1, a2) '(b1, b2)
+
+-- | Uncurry the kind of a bifunctor.
+--
+-- > type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
+#if __GLASGOW_HASKELL__ >= 810
+type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
+#endif
+data UncurryF f a where
+  UncurryF :: { curryF :: f a b } -> UncurryF f '(a, b)
+
+-- |
+-- > 1--a--H
+-- > |  v  |
+-- > U--@--q     1 = Hask^0 = (), H = Hask
+-- > |  v  |
+-- > 1--b--H
+--
+type Square01 q a b = SquareNT Unit (PList q) (ValueF a) (ValueF b)
+
+-- | The boring profunctor from and to the unit category.
+data Unit a b where
+  Unit :: Unit '() '()
+
+-- | Values as a functor from the unit category.
+data ValueF x u where
+  ValueF :: a -> ValueF a '()
diff --git a/src/Data/Traversable/Square.hs b/src/Data/Traversable/Square.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Traversable/Square.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Traversable.Square
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Traversable.Square where
+
+import Prelude hiding (traverse)
+import Data.Square
+import Data.Profunctor
+import qualified Data.Traversable as T
+
+-- |
+-- > +--t--+
+-- > |  v  |
+-- > f>-T->f
+-- > |  v  |
+-- > +--t--+
+--
+-- `traverse` as a square.
+--
+-- Naturality law:
+--
+-- > +-----t--+     +--t-----+
+-- > |     v  |     |  v     |
+-- > f>-@->T->g === f>-T->@->g
+-- > |     v  |     |  v     |
+-- > +-----t--+     +--t-----+
+--
+-- Identity law:
+--
+-- > +--t--+     +--t--+
+-- > |  v  |     |  |  |
+-- > |  T  | === |  v  |
+-- > |  v  |     |  |  |
+-- > +--t--+     +--t--+
+--
+-- Composition law:
+--
+-- > +--t--+     +--t--+
+-- > |  v  |     |  v  |
+-- > f>-T->f     f>\|/>f
+-- > |  v  | === |  T  |
+-- > g>-T->g     g>/|\>g
+-- > |  v  |     |  v  |
+-- > +--t--+     +--t--+
+traverse :: (Traversable t, Applicative f) => Square '[Star f] '[Star f] '[t] '[t]
+traverse = mkSquare (Star . T.traverse . runStar)
+
+-- |
+-- > +-f-t---+
+-- > | v v   |
+-- > | \-@-\ |
+-- > |   v v |
+-- > +---t-f-+
+--
+-- @sequence = toRight ||| traverse ||| fromLeft@
+sequence :: (Traversable t, Applicative f) => Square '[] '[] '[f, t] '[t, f]
+sequence = toRight ||| traverse ||| fromLeft
diff --git a/src/Data/Type/List.hs b/src/Data/Type/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/List.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.List
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  sjoerd@w3future.com
+--
+-- Utilities for type level lists.
+-----------------------------------------------------------------------------
+module Data.Type.List where
+
+-- | Type level list append
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+  '[] ++ bs = bs
+  (a ': as) ++ bs = a ': (as ++ bs)