{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : A left cone on I is I with another object called the cone point and a single morphism from the cone point to every other object of I. 
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A left cone on I is I with another object called the cone point and a single morphism from the cone point to every other object of I.

See Category Theory for the Sciences (2014) David I. Spivak for more details.

An usual cone on C is then a functor from a left cone on I to C.
-}

module ConeCategory.LeftCone
(
    -- * Cone related functions and types.

    LeftCone(..),
    inclusionFunctor,
    ConeCategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import IO.PrettyPrint
    import Diagram.Diagram
    import FunctorCategory.FunctorCategory
    import Utils.AssociationList
    
    -- | Object in a `LeftCone` category, either an original object or the cone point.

    data LeftConeObject o =   OriginalObject o
                            | ConePoint
                            deriving (LeftConeObject o -> LeftConeObject o -> Bool
(LeftConeObject o -> LeftConeObject o -> Bool)
-> (LeftConeObject o -> LeftConeObject o -> Bool)
-> Eq (LeftConeObject o)
forall o. Eq o => LeftConeObject o -> LeftConeObject o -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LeftConeObject o -> LeftConeObject o -> Bool
$c/= :: forall o. Eq o => LeftConeObject o -> LeftConeObject o -> Bool
== :: LeftConeObject o -> LeftConeObject o -> Bool
$c== :: forall o. Eq o => LeftConeObject o -> LeftConeObject o -> Bool
Eq, Int -> LeftConeObject o -> ShowS
[LeftConeObject o] -> ShowS
LeftConeObject o -> String
(Int -> LeftConeObject o -> ShowS)
-> (LeftConeObject o -> String)
-> ([LeftConeObject o] -> ShowS)
-> Show (LeftConeObject o)
forall o. Show o => Int -> LeftConeObject o -> ShowS
forall o. Show o => [LeftConeObject o] -> ShowS
forall o. Show o => LeftConeObject o -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LeftConeObject o] -> ShowS
$cshowList :: forall o. Show o => [LeftConeObject o] -> ShowS
show :: LeftConeObject o -> String
$cshow :: forall o. Show o => LeftConeObject o -> String
showsPrec :: Int -> LeftConeObject o -> ShowS
$cshowsPrec :: forall o. Show o => Int -> LeftConeObject o -> ShowS
Show)
    
    instance (PrettyPrintable o) => PrettyPrintable (LeftConeObject o) where
        pprint :: LeftConeObject o -> String
pprint (OriginalObject o
o) = o -> String
forall a. PrettyPrintable a => a -> String
pprint o
o
        pprint LeftConeObject o
ConePoint = String
"Left cone point"
    
    -- | Morphism in a `LeftCone` category, it is either an original morphism, a cone leg or the cone point identity.

    data LeftConeMorphism m o = OriginalMorphism m
                              | ConeLeg o
                              | ConePointIdentity
                              deriving (LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
(LeftConeMorphism m o -> LeftConeMorphism m o -> Bool)
-> (LeftConeMorphism m o -> LeftConeMorphism m o -> Bool)
-> Eq (LeftConeMorphism m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall m o.
(Eq m, Eq o) =>
LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
/= :: LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
$c/= :: forall m o.
(Eq m, Eq o) =>
LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
== :: LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
$c== :: forall m o.
(Eq m, Eq o) =>
LeftConeMorphism m o -> LeftConeMorphism m o -> Bool
Eq, Int -> LeftConeMorphism m o -> ShowS
[LeftConeMorphism m o] -> ShowS
LeftConeMorphism m o -> String
(Int -> LeftConeMorphism m o -> ShowS)
-> (LeftConeMorphism m o -> String)
-> ([LeftConeMorphism m o] -> ShowS)
-> Show (LeftConeMorphism m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m o.
(Show m, Show o) =>
Int -> LeftConeMorphism m o -> ShowS
forall m o. (Show m, Show o) => [LeftConeMorphism m o] -> ShowS
forall m o. (Show m, Show o) => LeftConeMorphism m o -> String
showList :: [LeftConeMorphism m o] -> ShowS
$cshowList :: forall m o. (Show m, Show o) => [LeftConeMorphism m o] -> ShowS
show :: LeftConeMorphism m o -> String
$cshow :: forall m o. (Show m, Show o) => LeftConeMorphism m o -> String
showsPrec :: Int -> LeftConeMorphism m o -> ShowS
$cshowsPrec :: forall m o.
(Show m, Show o) =>
Int -> LeftConeMorphism m o -> ShowS
Show)
                                
    instance (PrettyPrintable m, PrettyPrintable o) => PrettyPrintable (LeftConeMorphism m o) where
        pprint :: LeftConeMorphism m o -> String
pprint (OriginalMorphism m
m) = m -> String
forall a. PrettyPrintable a => a -> String
pprint m
m
        pprint (ConeLeg o
o) = String
"Leg "String -> ShowS
forall a. [a] -> [a] -> [a]
++(o -> String
forall a. PrettyPrintable a => a -> String
pprint o
o)
        pprint LeftConeMorphism m o
ConePointIdentity = String
"Id Cone Point"
        
    instance (Morphism m o, Eq o) => Morphism (LeftConeMorphism m o) (LeftConeObject o) where
        @ :: LeftConeMorphism m o
-> LeftConeMorphism m o -> LeftConeMorphism m o
(@) (OriginalMorphism m
g) (OriginalMorphism m
f) = m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f)
        (@) (ConeLeg o
_) (OriginalMorphism m
_) = String -> LeftConeMorphism m o
forall a. HasCallStack => String -> a
error String
"Cannot compose an original morphism with a cone leg."
        (@) LeftConeMorphism m o
ConePointIdentity (OriginalMorphism m
_) = String -> LeftConeMorphism m o
forall a. HasCallStack => String -> a
error String
"Cannot compose an original morphism with a cone point identity."
        (@) (OriginalMorphism m
f) (ConeLeg o
o)
            | (m -> o
forall m o. Morphism m o => m -> o
source m
f) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
o = (o -> LeftConeMorphism m o
forall m o. o -> LeftConeMorphism m o
ConeLeg (m -> o
forall m o. Morphism m o => m -> o
target m
f))
            | Bool
otherwise = String -> LeftConeMorphism m o
forall a. HasCallStack => String -> a
error String
"Source of original morphism is not target of cone leg."
        (@) (ConeLeg o
_) (ConeLeg o
_) = String -> LeftConeMorphism m o
forall a. HasCallStack => String -> a
error String
"Cannot compose two cone legs."
        (@) LeftConeMorphism m o
ConePointIdentity (ConeLeg o
_) = String -> LeftConeMorphism m o
forall a. HasCallStack => String -> a
error String
"Cannot compose a cone leg with a cone point identity"
        (@) (ConeLeg o
o) LeftConeMorphism m o
ConePointIdentity = o -> LeftConeMorphism m o
forall m o. o -> LeftConeMorphism m o
ConeLeg o
o
        (@) LeftConeMorphism m o
ConePointIdentity LeftConeMorphism m o
ConePointIdentity = LeftConeMorphism m o
forall m o. LeftConeMorphism m o
ConePointIdentity

                                    
        source :: LeftConeMorphism m o -> LeftConeObject o
source (OriginalMorphism m
m) = o -> LeftConeObject o
forall o. o -> LeftConeObject o
OriginalObject (m -> o
forall m o. Morphism m o => m -> o
source m
m)
        source (ConeLeg o
_) = LeftConeObject o
forall o. LeftConeObject o
ConePoint
        source LeftConeMorphism m o
ConePointIdentity = LeftConeObject o
forall o. LeftConeObject o
ConePoint
        target :: LeftConeMorphism m o -> LeftConeObject o
target (OriginalMorphism m
m) = o -> LeftConeObject o
forall o. o -> LeftConeObject o
OriginalObject (m -> o
forall m o. Morphism m o => m -> o
target m
m)
        target (ConeLeg o
o) = o -> LeftConeObject o
forall o. o -> LeftConeObject o
OriginalObject o
o
        target LeftConeMorphism m o
ConePointIdentity = LeftConeObject o
forall o. LeftConeObject o
ConePoint
    
    -- | The left cone category associated to a category.

    data LeftCone c m o = LeftCone c deriving (LeftCone c m o -> LeftCone c m o -> Bool
(LeftCone c m o -> LeftCone c m o -> Bool)
-> (LeftCone c m o -> LeftCone c m o -> Bool)
-> Eq (LeftCone c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o. Eq c => LeftCone c m o -> LeftCone c m o -> Bool
/= :: LeftCone c m o -> LeftCone c m o -> Bool
$c/= :: forall c m o. Eq c => LeftCone c m o -> LeftCone c m o -> Bool
== :: LeftCone c m o -> LeftCone c m o -> Bool
$c== :: forall c m o. Eq c => LeftCone c m o -> LeftCone c m o -> Bool
Eq, Int -> LeftCone c m o -> ShowS
[LeftCone c m o] -> ShowS
LeftCone c m o -> String
(Int -> LeftCone c m o -> ShowS)
-> (LeftCone c m o -> String)
-> ([LeftCone c m o] -> ShowS)
-> Show (LeftCone c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o. Show c => Int -> LeftCone c m o -> ShowS
forall c m o. Show c => [LeftCone c m o] -> ShowS
forall c m o. Show c => LeftCone c m o -> String
showList :: [LeftCone c m o] -> ShowS
$cshowList :: forall c m o. Show c => [LeftCone c m o] -> ShowS
show :: LeftCone c m o -> String
$cshow :: forall c m o. Show c => LeftCone c m o -> String
showsPrec :: Int -> LeftCone c m o -> ShowS
$cshowsPrec :: forall c m o. Show c => Int -> LeftCone c m o -> ShowS
Show)
    
    instance (PrettyPrintable c) => PrettyPrintable (LeftCone c m o) where
        pprint :: LeftCone c m o -> String
pprint (LeftCone c
cat) = String
"Left cone of "String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
cat
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o) where
        ob :: LeftCone c m o -> [LeftConeObject o]
ob (LeftCone c
cat) = LeftConeObject o
forall o. LeftConeObject o
ConePointLeftConeObject o -> [LeftConeObject o] -> [LeftConeObject o]
forall a. a -> [a] -> [a]
: (o -> LeftConeObject o
forall o. o -> LeftConeObject o
OriginalObject (o -> LeftConeObject o) -> [o] -> [LeftConeObject o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat))
        
        identity :: Morphism (LeftConeMorphism m o) (LeftConeObject o) =>
LeftCone c m o -> LeftConeObject o -> LeftConeMorphism m o
identity (LeftCone c
cat) (OriginalObject o
o) = m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
cat o
o)
        identity (LeftCone c
cat) LeftConeObject o
ConePoint = LeftConeMorphism m o
forall m o. LeftConeMorphism m o
ConePointIdentity
        
        ar :: Morphism (LeftConeMorphism m o) (LeftConeObject o) =>
LeftCone c m o
-> LeftConeObject o -> LeftConeObject o -> [LeftConeMorphism m o]
ar (LeftCone c
cat) (OriginalObject o
s) (OriginalObject o
t) = m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (m -> LeftConeMorphism m o) -> [m] -> [LeftConeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
s o
t
        ar (LeftCone c
cat) (OriginalObject o
s) LeftConeObject o
ConePoint = []
        ar (LeftCone c
cat) LeftConeObject o
ConePoint (OriginalObject o
t) = [o -> LeftConeMorphism m o
forall m o. o -> LeftConeMorphism m o
ConeLeg o
t]
        ar (LeftCone c
cat) LeftConeObject o
ConePoint LeftConeObject o
ConePoint = [LeftConeMorphism m o
forall m o. LeftConeMorphism m o
ConePointIdentity]
        
    instance (GeneratedFiniteCategory c m o, Morphism m o) => GeneratedFiniteCategory (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o) where
        genAr :: Morphism (LeftConeMorphism m o) (LeftConeObject o) =>
LeftCone c m o
-> LeftConeObject o -> LeftConeObject o -> [LeftConeMorphism m o]
genAr (LeftCone c
cat) (OriginalObject o
s) (OriginalObject o
t) = m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (m -> LeftConeMorphism m o) -> [m] -> [LeftConeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr c
cat o
s o
t
        genAr (LeftCone c
cat) (OriginalObject o
s) LeftConeObject o
ConePoint = []
        genAr (LeftCone c
cat) LeftConeObject o
ConePoint (OriginalObject o
t) = [o -> LeftConeMorphism m o
forall m o. o -> LeftConeMorphism m o
ConeLeg o
t]
        genAr (LeftCone c
cat) LeftConeObject o
ConePoint LeftConeObject o
ConePoint = [LeftConeMorphism m o
forall m o. LeftConeMorphism m o
ConePointIdentity]
        
        decompose :: Morphism (LeftConeMorphism m o) (LeftConeObject o) =>
LeftCone c m o -> LeftConeMorphism m o -> [LeftConeMorphism m o]
decompose (LeftCone c
cat) (OriginalMorphism m
m) = m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (m -> LeftConeMorphism m o) -> [m] -> [LeftConeMorphism m o]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c
cat m
m)
        decompose (LeftCone c
cat) (ConeLeg o
o) = [o -> LeftConeMorphism m o
forall m o. o -> LeftConeMorphism m o
ConeLeg o
o]
        decompose (LeftCone c
cat) LeftConeMorphism m o
ConePointIdentity = [LeftConeMorphism m o
forall m o. LeftConeMorphism m o
ConePointIdentity]
    
    -- | Inclusion functor from a category to its left cone category.

    inclusionFunctor :: (FiniteCategory c m o, Morphism m o) => LeftCone c m o -> Diagram c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
    inclusionFunctor :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
LeftCone c m o
-> Diagram
     c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
inclusionFunctor lc :: LeftCone c m o
lc@(LeftCone c
cat) = 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 :: c
src=c
cat
                                                , tgt :: LeftCone c m o
tgt=LeftCone c m o
lc
                                                , omap :: AssociationList o (LeftConeObject o)
omap=(o -> LeftConeObject o)
-> [o] -> AssociationList o (LeftConeObject o)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList o -> LeftConeObject o
forall o. o -> LeftConeObject o
OriginalObject (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat)
                                                , mmap :: AssociationList m (LeftConeMorphism m o)
mmap=(m -> LeftConeMorphism m o)
-> [m] -> AssociationList m (LeftConeMorphism m o)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList m -> LeftConeMorphism m o
forall m o. m -> LeftConeMorphism m o
OriginalMorphism (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
cat)
                                                }
    
    -- | The category of cones defined according to the left cone definition.

    --

    -- It is less efficient than the `ConeCategory.ConeCategory` implementation. This is only defined for pedagogical purposes.

    data ConeCategory c1 m1 o1 c2 m2 o2 =  ConeCategory (Diagram c1 m1 o1 c2 m2 o2) deriving (ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
(ConeCategory c1 m1 o1 c2 m2 o2
 -> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> (ConeCategory c1 m1 o1 c2 m2 o2
    -> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (ConeCategory c1 m1 o1 c2 m2 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
/= :: ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
== :: ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> ConeCategory c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS
[ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS
ConeCategory c1 m1 o1 c2 m2 o2 -> String
(Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS)
-> (ConeCategory c1 m1 o1 c2 m2 o2 -> String)
-> ([ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (ConeCategory c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
ConeCategory c1 m1 o1 c2 m2 o2 -> String
showList :: [ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[ConeCategory c1 m1 o1 c2 m2 o2] -> ShowS
show :: ConeCategory c1 m1 o1 c2 m2 o2 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
ConeCategory c1 m1 o1 c2 m2 o2 -> String
showsPrec :: Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> ConeCategory c1 m1 o1 c2 m2 o2 -> ShowS
Show)
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1
            , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => FiniteCategory 
        (ConeCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2)
        (Diagram (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2) where
        ob :: ConeCategory c1 m1 o1 c2 m2 o2
-> [Diagram
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
ob (ConeCategory Diagram c1 m1 o1 c2 m2 o2
diag) = [Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
s | Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
s <- FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> [Diagram
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: LeftCone c1 m1 o1
sourceCat = LeftCone c1 m1 o1
forall {m} {o}. LeftCone c1 m o
lcone, targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag}, Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
s Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> Diagram
     c1
     m1
     o1
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
-> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` (LeftCone c1 m1 o1
-> Diagram
     c1
     m1
     o1
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
LeftCone c m o
-> Diagram
     c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
inclusionFunctor LeftCone c1 m1 o1
forall {m} {o}. LeftCone c1 m o
lcone) Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram c1 m1 o1 c2 m2 o2
diag]
            where lcone :: LeftCone c1 m o
lcone = c1 -> LeftCone c1 m o
forall c m o. c -> LeftCone c m o
LeftCone (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag)
        
        identity :: Morphism
  (NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2)
  (Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
identity (ConeCategory Diagram c1 m1 o1 c2 m2 o2
diag) Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone = FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: LeftCone c1 m1 o1
sourceCat = c1 -> LeftCone c1 m1 o1
forall c m o. c -> LeftCone c m o
LeftCone (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag), targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag} Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone
        
        ar :: Morphism
  (NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2)
  (Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
ar (ConeCategory Diagram c1 m1 o1 c2 m2 o2
diag) Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone1 Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone2 = [NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
nt | NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
nt <- FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
forall {m} {o} {m1} {o1} {m2} {o2}.
FunctorCategory (LeftCone c1 m o) m1 o1 c2 m2 o2
functCat Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone1 Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone2, NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> Diagram
     c1
     m1
     o1
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
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) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
preWhiskering NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
nt (LeftCone c1 m1 o1
-> Diagram
     c1
     m1
     o1
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
LeftCone c m o
-> Diagram
     c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
inclusionFunctor LeftCone c1 m1 o1
forall {m} {o}. LeftCone c1 m o
lcone) NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== (FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity FunctorCategory c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c2 m2 o2
functCatDiag Diagram c1 m1 o1 c2 m2 o2
diag)]
            where 
                lcone :: LeftCone c1 m o
lcone =  c1 -> LeftCone c1 m o
forall c m o. c -> LeftCone c m o
LeftCone (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag)
                functCat :: FunctorCategory (LeftCone c1 m o) m1 o1 c2 m2 o2
functCat = FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: LeftCone c1 m o
sourceCat = LeftCone c1 m o
forall {m} {o}. LeftCone c1 m o
lcone, targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag}
                functCatDiag :: FunctorCategory c1 m1 o1 c2 m2 o2
functCatDiag = FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: c1
sourceCat = Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag, targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag}
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1
            , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => GeneratedFiniteCategory 
        (ConeCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2)
        (Diagram (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2) where
        genAr :: Morphism
  (NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2)
  (Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
genAr (ConeCategory Diagram c1 m1 o1 c2 m2 o2
diag) Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone1 Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone2 = FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: LeftCone c1 m1 o1
sourceCat = c1 -> LeftCone c1 m1 o1
forall c m o. c -> LeftCone c m o
LeftCone (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag), targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag} Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone1 Diagram
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone2
        decompose :: Morphism
  (NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2)
  (Diagram
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2) =>
ConeCategory c1 m1 o1 c2 m2 o2
-> NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
decompose (ConeCategory Diagram c1 m1 o1 c2 m2 o2
diag) NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone = FunctorCategory
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
-> NaturalTransformation
     (LeftCone c1 m1 o1)
     (LeftConeMorphism m1 o1)
     (LeftConeObject o1)
     c2
     m2
     o2
-> [NaturalTransformation
      (LeftCone c1 m1 o1)
      (LeftConeMorphism m1 o1)
      (LeftConeObject o1)
      c2
      m2
      o2]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: LeftCone c1 m1 o1
sourceCat = c1 -> LeftCone c1 m1 o1
forall c m o. c -> LeftCone c m o
LeftCone (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag), targetCat :: c2
targetCat = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag} NaturalTransformation
  (LeftCone c1 m1 o1)
  (LeftConeMorphism m1 o1)
  (LeftConeObject o1)
  c2
  m2
  o2
cone