{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, FlexibleContexts, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Product
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Product where

import Data.Category


data (:**:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
  (:**:) :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)

-- | The product category of categories @c1@ and @c2@.
instance (Category c1, Category c2) => Category (c1 :**: c2) where
  
  src :: (:**:) c1 c2 a b -> Obj (c1 :**: c2) a
src (c1 a1 b1
a1 :**: c2 a2 b2
a2)            = c1 a1 b1 -> Obj c1 a1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c1 a1 b1
a1 Obj c1 a1 -> c2 a2 a2 -> (:**:) c1 c2 (a1, a2) (a1, a2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 a2 b2 -> c2 a2 a2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c2 a2 b2
a2
  tgt :: (:**:) c1 c2 a b -> Obj (c1 :**: c2) b
tgt (c1 a1 b1
a1 :**: c2 a2 b2
a2)            = c1 a1 b1 -> Obj c1 b1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c1 a1 b1
a1 Obj c1 b1 -> c2 b2 b2 -> (:**:) c1 c2 (b1, b2) (b1, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c2 a2 b2 -> c2 b2 b2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c2 a2 b2
a2
  
  (c1 a1 b1
a1 :**: c2 a2 b2
a2) . :: (:**:) c1 c2 b c -> (:**:) c1 c2 a b -> (:**:) c1 c2 a c
. (c1 a1 b1
b1 :**: c2 a2 b2
b2) = (c1 a1 b1
a1 c1 a1 b1 -> c1 a1 a1 -> c1 a1 b1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c1 a1 a1
c1 a1 b1
b1) c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: (c2 a2 b2
a2 c2 a2 b2 -> c2 a2 a2 -> c2 a2 b2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c2 a2 a2
c2 a2 b2
b2)