    {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Module    : Control.Category.Monoidal
    -- Copyright : 2008,2012 Edward Kmett
    -- License   : BSD
    --
    -- Maintainer : Edward Kmett <ekmett@gmail.com>
    -- Stability  : experimental
    -- Portability: non-portable (class-associated types)
    --
    -- A 'Monoidal' category is a category with an associated biendofunctor that has an identity,
    -- which satisfies Mac Lane''s pentagonal and triangular coherence conditions
    -- Technically we usually say that category is 'Monoidal', but since
    -- most interesting categories in our world have multiple candidate bifunctors that you can
    -- use to enrich their structure, we choose here to think of the bifunctor as being
    -- monoidal. This lets us reuse the same 'Bifunctor' over different categories without
    -- painful newtype wrapping.

    -------------------------------------------------------------------------------------------

    module Control.Category.Monoidal
      ( Monoidal(..)
      ) where

    import Control.Category.Associative
    import Data.Void

    -- | Denotes that we have some reasonable notion of 'Identity' for a particular 'Bifunctor' in this 'Category'. This
    -- notion is currently used by both 'Monoidal' and 'Comonoidal'

    {- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
     the triangle identities hold:

    > first idr = second idl . associate
    > second idl = first idr . associate
    > first idr = disassociate . second idl
    > second idl = disassociate . first idr
    > idr . coidr = id
    > idl . coidl = id
    > coidl . idl = id
    > coidr . idr = id

    -}

    class Associative k p => Monoidal (k :: * -> * -> *) (p :: * -> * -> *) where
      type Id (k :: * -> * -> *) (p :: * -> * -> *) :: *
      idl   :: k (p (Id k p) a) a
      idr   :: k (p a (Id k p)) a
      coidl :: k a (p (Id k p) a)
      coidr :: k a (p a (Id k p))

    instance Monoidal (->) (,) where
      type Id (->) (,) = ()
      idl :: forall a. (Id (->) (,), a) -> a
    idl = ((), a) -> a
    (Id (->) (,), a) -> a
    forall a b. (a, b) -> b
    snd
      idr :: forall a. (a, Id (->) (,)) -> a
    idr = (a, ()) -> a
    (a, Id (->) (,)) -> a
    forall a b. (a, b) -> a
    fst
      coidl :: forall a. a -> (Id (->) (,), a)
    coidl a
    a = ((),a
    a)
      coidr :: forall a. a -> (a, Id (->) (,))
    coidr a
    a = (a
    a,())

    instance Monoidal (->) Either where
      type Id (->) Either = Void
      idl :: forall a. Either (Id (->) Either) a -> a
    idl = (Void -> a) -> (a -> a) -> Either Void a -> a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either Void -> a
    forall a. Void -> a
    absurd a -> a
    forall a. a -> a
    id
      idr :: forall a. Either a (Id (->) Either) -> a
    idr = (a -> a) -> (Void -> a) -> Either a Void -> a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> a
    forall a. a -> a
    id Void -> a
    forall a. Void -> a
    absurd
      coidl :: forall a. a -> Either (Id (->) Either) a
    coidl = a -> Either Void a
    a -> Either (Id (->) Either) a
    forall a b. b -> Either a b
    Right
      coidr :: forall a. a -> Either a (Id (->) Either)
    coidr = a -> Either a Void
    a -> Either a (Id (->) Either)
    forall a b. a -> Either a b
    Left

    {-- RULES
    -- "bimap id idl/associate"   second idl . associate = first idr
    -- "bimap idr id/associate"   first idr . associate = second idl
    -- "disassociate/bimap id idl"  disassociate . second idl = first idr
    -- "disassociate/bimap idr id"  disassociate . first idr = second idl
    "idr/coidr" idr . coidr = id
    "idl/coidl"  idl . coidl = id
    "coidl/idl"  coidl . idl = id
    "coidr/idr"  coidr . idr = id
    "idr/braid" idr . braid = idl
    "idl/braid" idl . braid = idr
    "braid/coidr" braid . coidr = coidl
    "braid/coidl" braid . coidl = coidr
     --}