{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Currying a functor @(A x B) -> C@ yields a functor @A -> [B,C]@.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Currying a functor @(A x B) -> C@ yields a functor @A -> [B,C]@.
-}
module Currying.Currying
(
curryDiagram,
uncurryDiagram,
switchArg,
)
where
    import FiniteCategory.FiniteCategory
    import ProductCategory.ProductCategory
    import FunctorCategory.FunctorCategory
    import Diagram.Diagram
    import Utils.AssociationList
    
    -- | Curry a functor @D : A x B -> C@ into a functor @D' : A -> [B,C]@.

    curryDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                     FiniteCategory c3 m3 o3, Morphism m3 o3) =>
                     Diagram (ProductCategory c1 m1 o1 c2 m2 o2) (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) c3 m3 o3 -> Diagram c1 m1 o1 (FunctorCategory c2 m2 o2 c3 m3 o3) (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c2 m2 o2 c3 m3 o3)
    curryDiagram :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
curryDiagram Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram{ 
                            src :: c1
src = (ProductCategory c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)),
                            tgt :: FunctorCategory c2 m2 o2 c3 m3 o3
tgt = FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{ sourceCat :: c2
sourceCat = (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)), targetCat :: c3
targetCat = (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)},
                            omap :: AssociationList o1 (Diagram c2 m2 o2 c3 m3 o3)
omap = [(o1
a, o1 -> Diagram c2 m2 o2 c3 m3 o3
diagFromA o1
a) | o1
a <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (ProductCategory c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag))],
                            mmap :: AssociationList m1 (NaturalTransformation c2 m2 o2 c3 m3 o3)
mmap = [(m1
f, m1 -> NaturalTransformation c2 m2 o2 c3 m3 o3
natFromF m1
f) | m1
f <- c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (ProductCategory c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag))]
                        }
        where
            diagFromA :: o1 -> Diagram c2 m2 o2 c3 m3 o3
diagFromA o1
a = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram{
                            src :: c2
src = (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)),
                            tgt :: c3
tgt = (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag),
                            omap :: AssociationList o2 o3
omap = [ (o2
b, (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> AssociationList (ProductObject o1 o2) o3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) AssociationList (ProductObject o1 o2) o3
-> ProductObject o1 o2 -> o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (o1 -> o2 -> ProductObject o1 o2
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject o1
a o2
b) ) | o2
b <- c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag))],
                            mmap :: AssociationList m2 m3
mmap = [ (m2
g, (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> AssociationList (ProductMorphism m1 o1 m2 o2) m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) AssociationList (ProductMorphism m1 o1 m2 o2) m3
-> ProductMorphism m1 o1 m2 o2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism (c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (ProductCategory c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)) o1
a) m2
g) ) | m2
g <- c2 -> [m2]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag))]
                          }
            natFromF :: m1 -> NaturalTransformation c2 m2 o2 c3 m3 o3
natFromF m1
f = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation{
                            srcNT :: Diagram c2 m2 o2 c3 m3 o3
srcNT = (o1 -> Diagram c2 m2 o2 c3 m3 o3
diagFromA (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
f)),
                            tgtNT :: Diagram c2 m2 o2 c3 m3 o3
tgtNT = (o1 -> Diagram c2 m2 o2 c3 m3 o3
diagFromA (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f)),
                            component :: o2 -> m3
component = (\o2
b -> (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> AssociationList (ProductMorphism m1 o1 m2 o2) m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) AssociationList (ProductMorphism m1 o1 m2 o2) m3
-> ProductMorphism m1 o1 m2 o2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m1
f (c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)) o2
b)))
                        }
    
    -- | Uncurry a functor @D : A -> [B,C]@ into a functor @D' : A x B -> C@.

    uncurryDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                     FiniteCategory c3 m3 o3, Morphism m3 o3) =>
                     Diagram c1 m1 o1 (FunctorCategory c2 m2 o2 c3 m3 o3) (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c2 m2 o2 c3 m3 o3) -> Diagram (ProductCategory c1 m1 o1 c2 m2 o2) (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) c3 m3 o3
    uncurryDiagram :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
uncurryDiagram Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram{ src :: ProductCategory c1 m1 o1 c2 m2 o2
src = c1 -> c2 -> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> ProductCategory c1 m1 o1 c2 m2 o2
ProductCategory (Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag) (FunctorCategory c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat(FunctorCategory c2 m2 o2 c3 m3 o3 -> c2)
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> FunctorCategory c2 m2 o2 c3 m3 o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram
   c1
   m1
   o1
   (FunctorCategory c2 m2 o2 c3 m3 o3)
   (NaturalTransformation c2 m2 o2 c3 m3 o3)
   (Diagram c2 m2 o2 c3 m3 o3)
 -> c2)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall a b. (a -> b) -> a -> b
$ Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag),
                                 tgt :: c3
tgt = (FunctorCategory c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c2
targetCat(FunctorCategory c2 m2 o2 c3 m3 o3 -> c3)
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> FunctorCategory c2 m2 o2 c3 m3 o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c3
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram
   c1
   m1
   o1
   (FunctorCategory c2 m2 o2 c3 m3 o3)
   (NaturalTransformation c2 m2 o2 c3 m3 o3)
   (Diagram c2 m2 o2 c3 m3 o3)
 -> c3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c3
forall a b. (a -> b) -> a -> b
$ Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag),
                                 omap :: AssociationList (ProductObject o1 o2) o3
omap = [(o1 -> o2 -> ProductObject o1 o2
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject o1
a o2
b, (Diagram c2 m2 o2 c3 m3 o3 -> AssociationList o2 o3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap ((Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> AssociationList o1 (Diagram c2 m2 o2 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag) AssociationList o1 (Diagram c2 m2 o2 c3 m3 o3)
-> o1 -> Diagram c2 m2 o2 c3 m3 o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! o1
a)) AssociationList o2 o3 -> o2 -> o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! o2
b ) | o1
a <- (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag)), o2
b <- (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob (FunctorCategory c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat(FunctorCategory c2 m2 o2 c3 m3 o3 -> c2)
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> FunctorCategory c2 m2 o2 c3 m3 o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram
   c1
   m1
   o1
   (FunctorCategory c2 m2 o2 c3 m3 o3)
   (NaturalTransformation c2 m2 o2 c3 m3 o3)
   (Diagram c2 m2 o2 c3 m3 o3)
 -> c2)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall a b. (a -> b) -> a -> b
$ Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag))],
                                 mmap :: AssociationList (ProductMorphism m1 o1 m2 o2) m3
mmap = [(m1 -> m2 -> ProductMorphism m1 o1 m2 o2
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m1
f m2
g, ((Diagram c2 m2 o2 c3 m3 o3 -> AssociationList m2 m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap ((Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> AssociationList o1 (Diagram c2 m2 o2 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag) AssociationList o1 (Diagram c2 m2 o2 c3 m3 o3)
-> o1 -> Diagram c2 m2 o2 c3 m3 o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f))) AssociationList m2 m3 -> m2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! m2
g) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ ((NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component ((Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> AssociationList m1 (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag) AssociationList m1 (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> m1 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
f)) (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
g)) ) | m1
f <- (c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag)), m2
g <- (c2 -> [m2]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (FunctorCategory c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. FunctorCategory c1 m1 o1 c2 m2 o2 -> c1
sourceCat(FunctorCategory c2 m2 o2 c3 m3 o3 -> c2)
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> FunctorCategory c2 m2 o2 c3 m3 o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram
   c1
   m1
   o1
   (FunctorCategory c2 m2 o2 c3 m3 o3)
   (NaturalTransformation c2 m2 o2 c3 m3 o3)
   (Diagram c2 m2 o2 c3 m3 o3)
 -> c2)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> c2
forall a b. (a -> b) -> a -> b
$ Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
diag))]
        }
        
    -- | Switches argument of a diagram @D : A x B -> C@ to create a diagram @D' : B x A -> C@.

    switch ::  (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                FiniteCategory c3 m3 o3, Morphism m3 o3) =>
                Diagram (ProductCategory c1 m1 o1 c2 m2 o2) (ProductMorphism m1 o1 m2 o2) (ProductObject o1 o2) c3 m3 o3 -> Diagram (ProductCategory c2 m2 o2 c1 m1 o1) (ProductMorphism m2 o2 m1 o1) (ProductObject o2 o1) c3 m3 o3
    switch :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> Diagram
     (ProductCategory c2 m2 o2 c1 m1 o1)
     (ProductMorphism m2 o2 m1 o1)
     (ProductObject o2 o1)
     c3
     m3
     o3
switch Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {
                    src :: ProductCategory c2 m2 o2 c1 m1 o1
src = (c2 -> c1 -> ProductCategory c2 m2 o2 c1 m1 o1
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> ProductCategory c1 m1 o1 c2 m2 o2
ProductCategory (ProductCategory c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c2
secondCategory(ProductCategory c1 m1 o1 c2 m2 o2 -> c2)
-> (Diagram
      (ProductCategory c1 m1 o1 c2 m2 o2)
      (ProductMorphism m1 o1 m2 o2)
      (ProductObject o1 o2)
      c3
      m3
      o3
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (ProductCategory c1 m1 o1 c2 m2 o2)
   (ProductMorphism m1 o1 m2 o2)
   (ProductObject o1 o2)
   c3
   m3
   o3
 -> c2)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> c2
forall a b. (a -> b) -> a -> b
$ Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) (ProductCategory c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. ProductCategory c1 m1 o1 c2 m2 o2 -> c1
firstCategory(ProductCategory c1 m1 o1 c2 m2 o2 -> c1)
-> (Diagram
      (ProductCategory c1 m1 o1 c2 m2 o2)
      (ProductMorphism m1 o1 m2 o2)
      (ProductObject o1 o2)
      c3
      m3
      o3
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (ProductCategory c1 m1 o1 c2 m2 o2)
   (ProductMorphism m1 o1 m2 o2)
   (ProductObject o1 o2)
   c3
   m3
   o3
 -> c1)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> c1
forall a b. (a -> b) -> a -> b
$ Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)),
                    tgt :: c3
tgt = (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag),
                    omap :: AssociationList (ProductObject o2 o1) o3
omap = [((o2 -> o1 -> ProductObject o2 o1
forall o1 o2. o1 -> o2 -> ProductObject o1 o2
ProductObject o2
b o1
a), (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> AssociationList (ProductObject o1 o2) o3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) AssociationList (ProductObject o1 o2) o3
-> ProductObject o1 o2 -> o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! ProductObject o1 o2
o) | o :: ProductObject o1 o2
o@(ProductObject o1
a o2
b) <- (ProductCategory c1 m1 o1 c2 m2 o2 -> [ProductObject o1 o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob(ProductCategory c1 m1 o1 c2 m2 o2 -> [ProductObject o1 o2])
-> (Diagram
      (ProductCategory c1 m1 o1 c2 m2 o2)
      (ProductMorphism m1 o1 m2 o2)
      (ProductObject o1 o2)
      c3
      m3
      o3
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> [ProductObject o1 o2]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (ProductCategory c1 m1 o1 c2 m2 o2)
   (ProductMorphism m1 o1 m2 o2)
   (ProductObject o1 o2)
   c3
   m3
   o3
 -> [ProductObject o1 o2])
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> [ProductObject o1 o2]
forall a b. (a -> b) -> a -> b
$ Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)],
                    mmap :: AssociationList (ProductMorphism m2 o2 m1 o1) m3
mmap = [((m2 -> m1 -> ProductMorphism m2 o2 m1 o1
forall m1 o1 m2 o2. m1 -> m2 -> ProductMorphism m1 o1 m2 o2
ProductMorphism m2
b m1
a), (Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> AssociationList (ProductMorphism m1 o1 m2 o2) m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag) AssociationList (ProductMorphism m1 o1 m2 o2) m3
-> ProductMorphism m1 o1 m2 o2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! ProductMorphism m1 o1 m2 o2
o) | o :: ProductMorphism m1 o1 m2 o2
o@(ProductMorphism m1
a m2
b) <- (ProductCategory c1 m1 o1 c2 m2 o2 -> [ProductMorphism m1 o1 m2 o2]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows(ProductCategory c1 m1 o1 c2 m2 o2
 -> [ProductMorphism m1 o1 m2 o2])
-> (Diagram
      (ProductCategory c1 m1 o1 c2 m2 o2)
      (ProductMorphism m1 o1 m2 o2)
      (ProductObject o1 o2)
      c3
      m3
      o3
    -> ProductCategory c1 m1 o1 c2 m2 o2)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> [ProductMorphism m1 o1 m2 o2]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> ProductCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (ProductCategory c1 m1 o1 c2 m2 o2)
   (ProductMorphism m1 o1 m2 o2)
   (ProductObject o1 o2)
   c3
   m3
   o3
 -> [ProductMorphism m1 o1 m2 o2])
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
-> [ProductMorphism m1 o1 m2 o2]
forall a b. (a -> b) -> a -> b
$ Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
diag)]
        }
        
    -- | Switches argument of a curried diagram.

    switchArg :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                  FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                  FiniteCategory c3 m3 o3, Morphism m3 o3) =>
                  Diagram c1 m1 o1 (FunctorCategory c2 m2 o2 c3 m3 o3) (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c2 m2 o2 c3 m3 o3) -> Diagram c2 m2 o2 (FunctorCategory c1 m1 o1 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3)
    switchArg :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
switchArg = Diagram
  (ProductCategory c2 m2 o2 c1 m1 o1)
  (ProductMorphism m2 o2 m1 o1)
  (ProductObject o2 o1)
  c3
  m3
  o3
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
curryDiagram(Diagram
   (ProductCategory c2 m2 o2 c1 m1 o1)
   (ProductMorphism m2 o2 m1 o1)
   (ProductObject o2 o1)
   c3
   m3
   o3
 -> Diagram
      c2
      m2
      o2
      (FunctorCategory c1 m1 o1 c3 m3 o3)
      (NaturalTransformation c1 m1 o1 c3 m3 o3)
      (Diagram c1 m1 o1 c3 m3 o3))
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> Diagram
         (ProductCategory c2 m2 o2 c1 m1 o1)
         (ProductMorphism m2 o2 m1 o1)
         (ProductObject o2 o1)
         c3
         m3
         o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> Diagram
     (ProductCategory c2 m2 o2 c1 m1 o1)
     (ProductMorphism m2 o2 m1 o1)
     (ProductObject o2 o1)
     c3
     m3
     o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  (ProductCategory c1 m1 o1 c2 m2 o2)
  (ProductMorphism m1 o1 m2 o2)
  (ProductObject o1 o2)
  c3
  m3
  o3
-> Diagram
     (ProductCategory c2 m2 o2 c1 m1 o1)
     (ProductMorphism m2 o2 m1 o1)
     (ProductObject o2 o1)
     c3
     m3
     o3
switch(Diagram
   (ProductCategory c1 m1 o1 c2 m2 o2)
   (ProductMorphism m1 o1 m2 o2)
   (ProductObject o1 o2)
   c3
   m3
   o3
 -> Diagram
      (ProductCategory c2 m2 o2 c1 m1 o1)
      (ProductMorphism m2 o2 m1 o1)
      (ProductObject o2 o1)
      c3
      m3
      o3)
-> (Diagram
      c1
      m1
      o1
      (FunctorCategory c2 m2 o2 c3 m3 o3)
      (NaturalTransformation c2 m2 o2 c3 m3 o3)
      (Diagram c2 m2 o2 c3 m3 o3)
    -> Diagram
         (ProductCategory c1 m1 o1 c2 m2 o2)
         (ProductMorphism m1 o1 m2 o2)
         (ProductObject o1 o2)
         c3
         m3
         o3)
-> Diagram
     c1
     m1
     o1
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     (ProductCategory c2 m2 o2 c1 m1 o1)
     (ProductMorphism m2 o2 m1 o1)
     (ProductObject o2 o1)
     c3
     m3
     o3
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3) =>
Diagram
  c1
  m1
  o1
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
-> Diagram
     (ProductCategory c1 m1 o1 c2 m2 o2)
     (ProductMorphism m1 o1 m2 o2)
     (ProductObject o1 o2)
     c3
     m3
     o3
uncurryDiagram