{-|
Module      : Internal.TwoCatOfCats
Description : Defines categories, functors, and natural transformations
Copyright   : Anthony Wang, 2021
License     : MIT
Maintainer  : anthony.y.wang.math@gmail.com

@Internal.TwoCatOfCats@ defines data structures used to represent the categories,
    functors and natural transformations which are to be rendered by @tikzsd@
    into TikZ picture code.

Currently, the structures defined in this module include data relating
    how they are displayed by @tikzsd@, while the functions in the module
    relate purely to category theory.
I plan on rewriting this module so that it is only about category theory,
    separating out the display aspects in another module.
In the future, this may allow greater flexibility in how objects are displayed.
-}
module Internal.TwoCatOfCats where

import Prelude hiding (Functor)
import Control.Monad.Trans.Except (Except, runExcept, throwE)
import Data.Either (isRight)

-- | A representation of a category.
data Category = Category
    { Category -> String
cat_id :: !String -- ^ the name of the category
    , Category -> String
cat_displayString :: !String -- ^ LaTeX code for displaying the category 
    } deriving (Category -> Category -> Bool
(Category -> Category -> Bool)
-> (Category -> Category -> Bool) -> Eq Category
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Category -> Category -> Bool
$c/= :: Category -> Category -> Bool
== :: Category -> Category -> Bool
$c== :: Category -> Category -> Bool
Eq)

instance Show Category where
    show :: Category -> String
show Category
c = String
"Category "String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Category -> String
cat_displayString Category
c)

-- | A @ZeroGlobelet@ is the structure representing the boundary of a functor (i.e.
--    1-morphism).
-- It consists of a source 'Category' and a target 'Category'.
data ZeroGlobelet = ZeroGlobelet
    { ZeroGlobelet -> Category
glob0_source :: !Category -- ^ source category
    , ZeroGlobelet -> Category
glob0_target :: !Category -- ^ target category
    } deriving (ZeroGlobelet -> ZeroGlobelet -> Bool
(ZeroGlobelet -> ZeroGlobelet -> Bool)
-> (ZeroGlobelet -> ZeroGlobelet -> Bool) -> Eq ZeroGlobelet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ZeroGlobelet -> ZeroGlobelet -> Bool
$c/= :: ZeroGlobelet -> ZeroGlobelet -> Bool
== :: ZeroGlobelet -> ZeroGlobelet -> Bool
$c== :: ZeroGlobelet -> ZeroGlobelet -> Bool
Eq)

instance Show ZeroGlobelet where
    show :: ZeroGlobelet -> String
show ZeroGlobelet
g = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Category -> String
forall a. Show a => a -> String
show (Category -> String) -> Category -> String
forall a b. (a -> b) -> a -> b
$ ZeroGlobelet -> Category
glob0_source ZeroGlobelet
g) String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Category -> String
forall a. Show a => a -> String
show (Category -> String) -> Category -> String
forall a b. (a -> b) -> a -> b
$ ZeroGlobelet -> Category
glob0_target ZeroGlobelet
g) String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"

-- | A representation of a functor between categories.
data Functor = 
    -- | A data structure specifying a new functor.
    -- We shall call 'Functor's of the form @(Functor id ds bg o)@
    -- /basic functors/.
    Functor
    { Functor -> String
func_id :: !String -- ^ the name of the functor
    , Functor -> String
func_displayString :: !String -- ^ LaTeX code for displaying the functor
    , Functor -> ZeroGlobelet
func_boundaryGlobelet :: !ZeroGlobelet -- ^ the boundary of the functor
    , Functor -> String
func_options :: !String -- ^ LaTeX for discribing options in TikZ
    } |
    -- | A data structure for specifying compositions of functors.
    -- A 'Functor' of the form @(CompositeFunctor bg fl)@ is assumed to satisfy the
    -- axiom that the functors in the list @fl@ can be composed and that
    -- @bg@ is a valid boundary for the composition.
    -- We shall call such functors /composite functors/.
    --
    -- Explicitly, the target of each functor in @fl@ is the source of the next functor
    --  in the list.
    -- Moreover, if @fl@ is empty, then the source and target of @bg@ must be the same.
    -- (This represents an identity functor).
    -- Otherwise, the source of @bg@ is equal to the source of the first functor in @fl@,
    --    and the target of @bg@ is equal to the target of the last functor in @fl@.
    --
    -- See 'identityFunctor', 'func_compose' and 'func_compose_with_error' for 
    -- functions which compose functors safely.
    CompositeFunctor
    { Functor -> ZeroGlobelet
cfs_boundaryGlobelet :: !ZeroGlobelet -- ^ The boundary globelet of the composite functor.
    , Functor -> [Functor]
cfs_functorList :: ![Functor] -- ^ The list of functors to compose.
                                    -- The composition order is from left to right, so the list
                                    -- [F,G] represents a composition of F : A -> B and G : B -> C.
    } deriving Int -> Functor -> ShowS
[Functor] -> ShowS
Functor -> String
(Int -> Functor -> ShowS)
-> (Functor -> String) -> ([Functor] -> ShowS) -> Show Functor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Functor] -> ShowS
$cshowList :: [Functor] -> ShowS
show :: Functor -> String
$cshow :: Functor -> String
showsPrec :: Int -> Functor -> ShowS
$cshowsPrec :: Int -> Functor -> ShowS
Show

-- | A boundary globelet function which works for both basic and composite functors.
func_boundary :: Functor -> ZeroGlobelet
func_boundary :: Functor -> ZeroGlobelet
func_boundary (Functor String
_i String
_d ZeroGlobelet
bg String
_o) = ZeroGlobelet
bg
func_boundary (CompositeFunctor ZeroGlobelet
bg [Functor]
_fs) = ZeroGlobelet
bg

-- | 'func_source' gives the source category of a functor.
func_source :: Functor -> Category
func_source :: Functor -> Category
func_source = ZeroGlobelet -> Category
glob0_source(ZeroGlobelet -> Category)
-> (Functor -> ZeroGlobelet) -> Functor -> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Functor -> ZeroGlobelet
func_boundary

-- | 'func_target' gives the target category of a functor.
func_target :: Functor -> Category
func_target :: Functor -> Category
func_target = ZeroGlobelet -> Category
glob0_target(ZeroGlobelet -> Category)
-> (Functor -> ZeroGlobelet) -> Functor -> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Functor -> ZeroGlobelet
func_boundary

-- | 'identityFunctor' takes a category @C@ and returns the identity functor of
-- that category.
-- The identity functor is represented by a composite functor whose underlying
--     @cfg_functorList@ is empty.
identityFunctor :: Category -> Functor
identityFunctor :: Category -> Functor
identityFunctor Category
c = ZeroGlobelet -> [Functor] -> Functor
CompositeFunctor (Category -> Category -> ZeroGlobelet
ZeroGlobelet Category
c Category
c) []

-- | 'func_composable' takes a list of functors and returns @True@
-- if the list of functors can be composed (without specifying additional information),
-- and @False@ otherwise.
-- 'func_composable' will return @False@ on an empty list, since a source (or target) category
-- needs to be specified.
-- Function composition is left to right, so [F,G] represents a composition of F : A -> B and
-- G : B -> C.
func_composable :: [Functor] -> Bool
func_composable :: [Functor] -> Bool
func_composable = Either FuncCompositionError Functor -> Bool
forall a b. Either a b -> Bool
isRight (Either FuncCompositionError Functor -> Bool)
-> ([Functor] -> Either FuncCompositionError Functor)
-> [Functor]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except FuncCompositionError Functor
-> Either FuncCompositionError Functor
forall e a. Except e a -> Either e a
runExcept (Except FuncCompositionError Functor
 -> Either FuncCompositionError Functor)
-> ([Functor] -> Except FuncCompositionError Functor)
-> [Functor]
-> Either FuncCompositionError Functor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Functor] -> Except FuncCompositionError Functor
func_compose_with_error

-- | 'func_compose' takes a list of functors and returns @Just@ their composite if
-- 'func_composable' is @True@ and @Nothing@ if 'func_composable' is @False@.
func_compose :: [Functor] -> Maybe Functor
func_compose :: [Functor] -> Maybe Functor
func_compose = ((FuncCompositionError -> Maybe Functor)
-> (Functor -> Maybe Functor)
-> Either FuncCompositionError Functor
-> Maybe Functor
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe Functor -> FuncCompositionError -> Maybe Functor
forall a b. a -> b -> a
const Maybe Functor
forall a. Maybe a
Nothing) Functor -> Maybe Functor
forall a. a -> Maybe a
Just) (Either FuncCompositionError Functor -> Maybe Functor)
-> ([Functor] -> Either FuncCompositionError Functor)
-> [Functor]
-> Maybe Functor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except FuncCompositionError Functor
-> Either FuncCompositionError Functor
forall e a. Except e a -> Either e a
runExcept (Except FuncCompositionError Functor
 -> Either FuncCompositionError Functor)
-> ([Functor] -> Except FuncCompositionError Functor)
-> [Functor]
-> Either FuncCompositionError Functor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Functor] -> Except FuncCompositionError Functor
func_compose_with_error

-- | 'FuncCompositionError' is the type of error which can be thrown by 'func_compose_with_error'.
-- 
-- @FunctorCompositionError []@ is the error for an empty composition.
-- 
-- Otherwise, an error is given by @(FuncCompositionError list)@ where @list@ is a list of positions 
-- where the functors do not compose.
-- @n@ is in @list@ if the functors in positions @n@ and @n+1@ do not compose.
-- (Indexing starts at 0).
data FuncCompositionError = FuncCompositionError [Int] 

-- | 'func_compose_with_error' takes a list of functors and composes them.
-- It throws a 'FuncCompositionError' describing why composition failed if 
-- the functors in the list could not be composed.
func_compose_with_error :: [Functor] -> Except FuncCompositionError Functor
func_compose_with_error :: [Functor] -> Except FuncCompositionError Functor
func_compose_with_error [] = FuncCompositionError -> Except FuncCompositionError Functor
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (FuncCompositionError -> Except FuncCompositionError Functor)
-> FuncCompositionError -> Except FuncCompositionError Functor
forall a b. (a -> b) -> a -> b
$ [Int] -> FuncCompositionError
FuncCompositionError []
func_compose_with_error [Functor]
fs 
    | [(Bool, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, Int)]
errs = let bd :: ZeroGlobelet
bd = Category -> Category -> ZeroGlobelet
ZeroGlobelet (Functor -> Category
func_source (Functor -> Category) -> Functor -> Category
forall a b. (a -> b) -> a -> b
$ [Functor] -> Functor
forall a. [a] -> a
head [Functor]
fs) (Functor -> Category
func_target (Functor -> Category) -> Functor -> Category
forall a b. (a -> b) -> a -> b
$ [Functor] -> Functor
forall a. [a] -> a
last [Functor]
fs)
                      sfs :: [Functor]
sfs = (Functor -> [Functor]) -> [Functor] -> [Functor]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Functor -> [Functor]
func_to_single_list [Functor]
fs
                      in Functor -> Except FuncCompositionError Functor
forall (m :: * -> *) a. Monad m => a -> m a
return (Functor -> Except FuncCompositionError Functor)
-> Functor -> Except FuncCompositionError Functor
forall a b. (a -> b) -> a -> b
$ ZeroGlobelet -> [Functor] -> Functor
CompositeFunctor ZeroGlobelet
bd [Functor]
sfs
    | Bool
otherwise = FuncCompositionError -> Except FuncCompositionError Functor
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (FuncCompositionError -> Except FuncCompositionError Functor)
-> FuncCompositionError -> Except FuncCompositionError Functor
forall a b. (a -> b) -> a -> b
$ [Int] -> FuncCompositionError
FuncCompositionError ([Int] -> FuncCompositionError) -> [Int] -> FuncCompositionError
forall a b. (a -> b) -> a -> b
$ (Bool, Int) -> Int
forall a b. (a, b) -> b
snd ((Bool, Int) -> Int) -> [(Bool, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Bool, Int)]
errs
    where 
        composable :: Functor -> Functor -> Bool
composable Functor
f1 Functor
f2 = Functor -> Category
func_target Functor
f1 Category -> Category -> Bool
forall a. Eq a => a -> a -> Bool
== Functor -> Category
func_source Functor
f2
        comp_list :: [Functor] -> [Bool]
comp_list [Functor]
fs = (Functor -> Functor -> Bool) -> [Functor] -> [Functor] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Functor -> Functor -> Bool
composable [Functor]
fs ([Functor] -> [Functor]
forall a. [a] -> [a]
tail [Functor]
fs)
        errs :: [(Bool, Int)]
errs = ((Bool, Int) -> Bool) -> [(Bool, Int)] -> [(Bool, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Bool
x,Int
y) -> Bool -> Bool
not Bool
x) ([(Bool, Int)] -> [(Bool, Int)]) -> [(Bool, Int)] -> [(Bool, Int)]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Int] -> [(Bool, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Functor] -> [Bool]
comp_list [Functor]
fs) [Int
0..]

-- | 'func_to_single_composition' of @f@
-- gives a functor of the form @(CompositeFunctor bd fl)@ which is equal to @f@,
-- where @fl@ is a list of basic functors.
func_to_single_composition :: Functor -> Functor
func_to_single_composition :: Functor -> Functor
func_to_single_composition Functor
f = ZeroGlobelet -> [Functor] -> Functor
CompositeFunctor (Functor -> ZeroGlobelet
func_boundary Functor
f) (Functor -> [Functor]
func_to_single_list Functor
f)

-- | 'func_to_single_list' @f@ returns the empty list if @f@
-- is an identity functor.
-- Otherwise, it returns a list of basic functors whose composition is equal to @f@.
func_to_single_list :: Functor -> [Functor]
func_to_single_list :: Functor -> [Functor]
func_to_single_list (Functor String
i String
ds ZeroGlobelet
bg String
o) = [(String -> String -> ZeroGlobelet -> String -> Functor
Functor String
i String
ds ZeroGlobelet
bg String
o)]
func_to_single_list (CompositeFunctor ZeroGlobelet
_bg [Functor]
fl) = (Functor -> [Functor]) -> [Functor] -> [Functor]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Functor -> [Functor]
func_to_single_list [Functor]
fl

-- | 'func_reduced_length' returns the length of 'func_to_single_list'.
-- For example @func_reduced_length@ of an identity functor is 0,
-- while @func_reduced_length@ of a basic functor is 1.
func_reduced_length :: Functor -> Int
func_reduced_length :: Functor -> Int
func_reduced_length = [Functor] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Functor] -> Int) -> (Functor -> [Functor]) -> Functor -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Functor -> [Functor]
func_to_single_list

-- | Two basic functors are deemed equal if @func_id@ and @func_boundaryGlobelet@ are equal.
-- After this identification, two 'Functor's are equal if they describe the same
-- morphism in the free category generated by the basic functors.
instance Eq Functor where
    Functor
f1 == :: Functor -> Functor -> Bool
== Functor
f2 = (Functor -> ZeroGlobelet
func_boundary Functor
f1)ZeroGlobelet -> ZeroGlobelet -> Bool
forall a. Eq a => a -> a -> Bool
==(Functor -> ZeroGlobelet
func_boundary Functor
f2) Bool -> Bool -> Bool
&& ([Functor] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Functor]
list1)Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==([Functor] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Functor]
list2)
                Bool -> Bool -> Bool
&& ((Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bool -> Bool -> Bool
(&&) Bool
True ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Functor -> Functor -> Bool) -> [Functor] -> [Functor] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Functor -> Functor -> Bool
basicCompare [Functor]
list1 [Functor]
list2)
        where
            list1 :: [Functor]
list1 = Functor -> [Functor]
func_to_single_list Functor
f1
            list2 :: [Functor]
list2 = Functor -> [Functor]
func_to_single_list Functor
f2
            basicCompare :: Functor -> Functor -> Bool
basicCompare (Functor String
i1 String
_d1 ZeroGlobelet
bg1 String
_o1) (Functor String
i2 String
_d2 ZeroGlobelet
bg2 String
_o2) 
                = (String
i1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
i2) Bool -> Bool -> Bool
&& (ZeroGlobelet
bg1 ZeroGlobelet -> ZeroGlobelet -> Bool
forall a. Eq a => a -> a -> Bool
== ZeroGlobelet
bg2) 
            basicCompare Functor
_ Functor
_ = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"func_to_single_list should be a list of basic functors "
                                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"so this shouldn't be matched."

-- | 'is_identity_func' of a functor is @True@ if the functor is an identity functor
-- and @False@ otherwise.
is_identity_func :: Functor -> Bool
is_identity_func :: Functor -> Bool
is_identity_func Functor
f = Functor -> Int
func_reduced_length Functor
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0

-- | 'is_basic_func' of a functor is @True@ if the functor is a basic functor,
-- and @False@ otherwise.
is_basic_func :: Functor -> Bool
is_basic_func :: Functor -> Bool
is_basic_func (Functor {}) = Bool
True
is_basic_func Functor
_ = Bool
False

-- | 'OneGlobelet' is the structure representing the boundary of a natural transformation
-- (i.e. 2-morphism).
-- @(OneGlobelet s t)@ represents a globelet with source functor @s@ and target functor @t@,
--  and is assumed to satisfy the following axiom:
--
-- @func_boundary s == func_boundary t@
--
-- See 'funcs_to_globelet' for safe construction of @OneGlobelet@s.
data OneGlobelet  = OneGlobelet
    { OneGlobelet -> Functor
glob1_source :: !Functor -- ^ source functor
    , OneGlobelet -> Functor
glob1_target :: !Functor -- ^ target functor
    } deriving Int -> OneGlobelet -> ShowS
[OneGlobelet] -> ShowS
OneGlobelet -> String
(Int -> OneGlobelet -> ShowS)
-> (OneGlobelet -> String)
-> ([OneGlobelet] -> ShowS)
-> Show OneGlobelet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OneGlobelet] -> ShowS
$cshowList :: [OneGlobelet] -> ShowS
show :: OneGlobelet -> String
$cshow :: OneGlobelet -> String
showsPrec :: Int -> OneGlobelet -> ShowS
$cshowsPrec :: Int -> OneGlobelet -> ShowS
Show
   
-- | @(funcs_globeletable source target)@ is @True@ if the 'Functor's
--  @source@ and @target@ have the same boundary globelet, i.e. they have 
--  the same source category and the same target category,
--  and @False@ otherwise.
funcs_globeletable :: Functor -> Functor -> Bool
funcs_globeletable :: Functor -> Functor -> Bool
funcs_globeletable Functor
north Functor
south = Functor -> ZeroGlobelet
func_boundary Functor
north ZeroGlobelet -> ZeroGlobelet -> Bool
forall a. Eq a => a -> a -> Bool
== Functor -> ZeroGlobelet
func_boundary Functor
south
    
-- | @(funcs_to_globelet source target)@ is @Just@ the
-- 'OneGlobelet' with source @source@ and target @target@ if
-- @(funcs_globeletable source target)=True@, and @Nothing@ otherwise.
funcs_to_globelet :: Functor -> Functor -> Maybe OneGlobelet
funcs_to_globelet :: Functor -> Functor -> Maybe OneGlobelet
funcs_to_globelet Functor
north Functor
south
    | Functor -> Functor -> Bool
funcs_globeletable Functor
north Functor
south = OneGlobelet -> Maybe OneGlobelet
forall a. a -> Maybe a
Just (Functor -> Functor -> OneGlobelet
OneGlobelet Functor
north Functor
south)
    | Bool
otherwise                      = Maybe OneGlobelet
forall a. Maybe a
Nothing

-- | 'glob1_pos' of a @OneGlobelet@ is equal to the source category
-- of the source functor of the @OneGlobelet@.
-- Equivalently, it is equal to the source category of the target functor
-- of the @OneGlobelet@.
-- We shall refer to this category as the /positive pole/
-- of the @OneGlobelet@.
glob1_pos :: OneGlobelet -> Category
glob1_pos :: OneGlobelet -> Category
glob1_pos = Functor -> Category
func_source(Functor -> Category)
-> (OneGlobelet -> Functor) -> OneGlobelet -> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OneGlobelet -> Functor
glob1_source

-- | 'glob1_neg' of a @OneGlobelet@ is equal to the target category
-- of the target functor of the @OneGlobelet@.
-- Equivalently, it is equal to the target category of the source functor
-- of the @OneGlobelet@.
-- We shall refer to this category as the /negative pole/
-- of the @OneGlobelet@.
glob1_neg :: OneGlobelet -> Category
glob1_neg :: OneGlobelet -> Category
glob1_neg = Functor -> Category
func_target(Functor -> Category)
-> (OneGlobelet -> Functor) -> OneGlobelet -> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.OneGlobelet -> Functor
glob1_target

-- | A representation of a natural transformation between functors.
data NaturalTransformation = 
    -- | A data structure specifying a new natural transformation.
    -- We shall call natural transformations of the form
    -- @(NaturalTransformation id ds ss bg o)@ /basic natural transformations/.
    NaturalTransformation
    { NaturalTransformation -> String
nt_id :: !String -- ^ name of the natural transformation
    , NaturalTransformation -> String
nt_displayString :: !String -- ^ LaTeX code for displaying the natural transformation
    , NaturalTransformation -> String
nt_shapeString :: !String -- ^ LaTeX code for the shape of the node used for the natural transformation
    , NaturalTransformation -> OneGlobelet
nt_boundaryGlobelet :: !OneGlobelet -- ^ boundary globelet of the natural transformation
    , NaturalTransformation -> String
nt_options :: !String -- ^ LaTeX code for options when displaying the natural transformation
    } |
    -- | A data structure for specifying a horizontal composition of natural transformations.
    -- A 'NaturalTransformation' of the form @(NatTransHorizontalComposite bg ntl)@
    -- is assumed to satisfy the axiom that @ntl@ is a list of natural transformations which
    -- can be horizontally composed, with @bg@ the boundary for the composition.
    --
    -- Explicitly, @ntl@ is a non-empty list of @NaturalTransformation@s
    -- such that the negative pole of each natural transformation in the list is the positive pole
    -- of the next element in the list.
    -- The source of @bg@ is equal to the composition of the source functors of the natural transformations
    -- in @ntl@
    -- and the target of @bg@ is equal to the composition of the target functors of the natural
    -- transformations in @ntl@.
    --
    -- See the 'nat_horz_compose' and 'nat_horz_compose_with_error' functions for safe horizontal
    -- composition of natural transformations.
    NatTransHorizontalComposite
    { NaturalTransformation -> OneGlobelet
nt_horz_comp_boundaryGlobelet :: !OneGlobelet -- ^ the boundary globelet of the horizontal composition
    , NaturalTransformation -> [NaturalTransformation]
nt_horz_comp_list :: ![NaturalTransformation] -- ^ the list of natural transformations to be horizontally
                                                    -- composed. Composition is from left to right.
    } |
    -- | A data structure for specifying a vertical composition of natural transformations.
    -- A 'NaturalTransformation' of the form @(NatTransVerticalComposite bg ntl)@
    -- is assumed to satisfy the axiom that @ntl@ is a list of natural transformations
    -- which can be vertically composed, with @bg@ a valid boundary for the composition.
    --
    -- Explicitly, @ntl@ is a list of @NaturalTransformation@s
    -- such that the target functor of each natural transformation in the list is
    -- equal to the source functor of the next natural transformation.
    -- If @ntl@ is empty, then the source and target functors of @bg@ must be equal.
    -- (This represents an identity natural transformation.)
    -- Otherwise, the source functor of @bg@ is equal to the source functor of the first
    -- natural transformation in @ntl@ and the target functor of @bg@ is equal to the target
    -- functor of the last natural transformation in @ntl@.
    --
    -- See 'identityNaturalTransformation' and 'nat_vert_compose' for functions which
    -- vertically compose natural transformations safely.
    NatTransVerticalComposite
    { NaturalTransformation -> OneGlobelet
nt_vert_comp_boundaryGlobelet :: !OneGlobelet -- ^ the boundary globelet of the vertical composition
    , NaturalTransformation -> [NaturalTransformation]
nt_vert_comp_list :: ![NaturalTransformation] -- ^ the list of natural transformations to be vertically composed.
                                                    -- Composition is from left to right.
    } deriving Int -> NaturalTransformation -> ShowS
[NaturalTransformation] -> ShowS
NaturalTransformation -> String
(Int -> NaturalTransformation -> ShowS)
-> (NaturalTransformation -> String)
-> ([NaturalTransformation] -> ShowS)
-> Show NaturalTransformation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NaturalTransformation] -> ShowS
$cshowList :: [NaturalTransformation] -> ShowS
show :: NaturalTransformation -> String
$cshow :: NaturalTransformation -> String
showsPrec :: Int -> NaturalTransformation -> ShowS
$cshowsPrec :: Int -> NaturalTransformation -> ShowS
Show

-- | 'nat_boundary' of a natural transformation is its boundary globelet.
nat_boundary :: NaturalTransformation -> OneGlobelet
nat_boundary :: NaturalTransformation -> OneGlobelet
nat_boundary (NaturalTransformation String
_i String
_ds String
_ss OneGlobelet
bg String
_o) = OneGlobelet
bg
nat_boundary (NatTransHorizontalComposite OneGlobelet
bg [NaturalTransformation]
_nl) = OneGlobelet
bg
nat_boundary (NatTransVerticalComposite OneGlobelet
bg [NaturalTransformation]
_nl) = OneGlobelet
bg

-- | 'nat_source' of a natural transformation is its source functor.
nat_source :: NaturalTransformation -> Functor
nat_source :: NaturalTransformation -> Functor
nat_source = OneGlobelet -> Functor
glob1_source(OneGlobelet -> Functor)
-> (NaturalTransformation -> OneGlobelet)
-> NaturalTransformation
-> Functor
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> OneGlobelet
nat_boundary

-- | 'nat_target' of a natural transforamtion is its target functor.
nat_target :: NaturalTransformation -> Functor
nat_target :: NaturalTransformation -> Functor
nat_target = OneGlobelet -> Functor
glob1_target(OneGlobelet -> Functor)
-> (NaturalTransformation -> OneGlobelet)
-> NaturalTransformation
-> Functor
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> OneGlobelet
nat_boundary

-- | 'nat_pos' of a natural transformation is its /positive pole/
-- which we define to be the positive pole of its boundary globelet,
-- i.e. the source of its source, or equivalently, the source of its target.
nat_pos :: NaturalTransformation -> Category
nat_pos :: NaturalTransformation -> Category
nat_pos = OneGlobelet -> Category
glob1_pos(OneGlobelet -> Category)
-> (NaturalTransformation -> OneGlobelet)
-> NaturalTransformation
-> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> OneGlobelet
nat_boundary

-- | 'nat_neg' of a natural transformation is its /negative pole/
-- which we define to be the negative pole of its boundary globelet,
-- i.e. the target of its target, or equivalently, the target of its source.
nat_neg :: NaturalTransformation -> Category
nat_neg :: NaturalTransformation -> Category
nat_neg = OneGlobelet -> Category
glob1_neg(OneGlobelet -> Category)
-> (NaturalTransformation -> OneGlobelet)
-> NaturalTransformation
-> Category
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> OneGlobelet
nat_boundary

-- | 'identityNaturalTransformation' takes a 'Functor' as an argument and returns
-- its identity natural transformation.
-- The identity natural transformation is represented by a vertical composition
-- whose @nt_vert_comp_list@ is empty.
identityNaturalTransformation :: Functor -> NaturalTransformation 
identityNaturalTransformation :: Functor -> NaturalTransformation
identityNaturalTransformation Functor
f = OneGlobelet -> [NaturalTransformation] -> NaturalTransformation
NatTransVerticalComposite (Functor -> Functor -> OneGlobelet
OneGlobelet Functor
f Functor
f) []

-- | 'nat_horz_composable' takes a list of natural transformations and returns
-- @True@ if the natural transformations can be horizontally composed,
-- and @False@ otherwise.
nat_horz_composable :: [NaturalTransformation] -> Bool
nat_horz_composable :: [NaturalTransformation] -> Bool
nat_horz_composable = [Functor] -> Bool
func_composable ([Functor] -> Bool)
-> ([NaturalTransformation] -> [Functor])
-> [NaturalTransformation]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((NaturalTransformation -> Functor)
-> [NaturalTransformation] -> [Functor]
forall a b. (a -> b) -> [a] -> [b]
map NaturalTransformation -> Functor
nat_source) 

-- | 'nat_horz_compose' takes a list of natural transformations and returns
-- @Just@ their horizontal composition if they are horizontally composable,
-- and @Nothing@ otherwise.
nat_horz_compose :: [NaturalTransformation] -> Maybe NaturalTransformation
nat_horz_compose :: [NaturalTransformation] -> Maybe NaturalTransformation
nat_horz_compose = ((NatHorzCompositionError -> Maybe NaturalTransformation)
-> (NaturalTransformation -> Maybe NaturalTransformation)
-> Either NatHorzCompositionError NaturalTransformation
-> Maybe NaturalTransformation
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe NaturalTransformation
-> NatHorzCompositionError -> Maybe NaturalTransformation
forall a b. a -> b -> a
const Maybe NaturalTransformation
forall a. Maybe a
Nothing) NaturalTransformation -> Maybe NaturalTransformation
forall a. a -> Maybe a
Just) (Either NatHorzCompositionError NaturalTransformation
 -> Maybe NaturalTransformation)
-> ([NaturalTransformation]
    -> Either NatHorzCompositionError NaturalTransformation)
-> [NaturalTransformation]
-> Maybe NaturalTransformation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except NatHorzCompositionError NaturalTransformation
-> Either NatHorzCompositionError NaturalTransformation
forall e a. Except e a -> Either e a
runExcept (Except NatHorzCompositionError NaturalTransformation
 -> Either NatHorzCompositionError NaturalTransformation)
-> ([NaturalTransformation]
    -> Except NatHorzCompositionError NaturalTransformation)
-> [NaturalTransformation]
-> Either NatHorzCompositionError NaturalTransformation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NaturalTransformation]
-> Except NatHorzCompositionError NaturalTransformation
nat_horz_compose_with_error

-- | 'NatHorzCompositionError' is the possible error thrown by 'nat_horz_compose_with_error'.
--
-- @(NatHorzCompositionError [])@ represents an empty horizontal composition.
--
-- Otherwise, an error is given by @(NatHorzCompositionError list)@ where
-- @list@ is a list of positions where the natural transformations do not 
--  horizontally compose.
-- @n@ is in @list@ if the negative pole of the natural transformation in position
-- @n@ is not equal to the positive pole of the natural transformation in position
-- @n+1@.
-- (Indexing starts at 0).
data NatHorzCompositionError = NatHorzCompositionError [Int]

-- | 'nat_horz_compose_with_error' takes a list of natural transformations and returns their
-- horizontal composition.
-- It throws a 'NatHorzCompositionError' describing why composition failed if the
-- list of natural transformations cannot be horizontally composed.
-- Composition is from left to right.
nat_horz_compose_with_error :: [NaturalTransformation] -> Except NatHorzCompositionError NaturalTransformation
nat_horz_compose_with_error :: [NaturalTransformation]
-> Except NatHorzCompositionError NaturalTransformation
nat_horz_compose_with_error [] = NatHorzCompositionError
-> Except NatHorzCompositionError NaturalTransformation
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (NatHorzCompositionError
 -> Except NatHorzCompositionError NaturalTransformation)
-> NatHorzCompositionError
-> Except NatHorzCompositionError NaturalTransformation
forall a b. (a -> b) -> a -> b
$ [Int] -> NatHorzCompositionError
NatHorzCompositionError []
nat_horz_compose_with_error  [NaturalTransformation]
nats
    | [(Bool, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, Int)]
errs = let pos :: Category
pos = NaturalTransformation -> Category
nat_pos (NaturalTransformation -> Category)
-> NaturalTransformation -> Category
forall a b. (a -> b) -> a -> b
$ [NaturalTransformation] -> NaturalTransformation
forall a. [a] -> a
head [NaturalTransformation]
nats
                      neg :: Category
neg = NaturalTransformation -> Category
nat_neg (NaturalTransformation -> Category)
-> NaturalTransformation -> Category
forall a b. (a -> b) -> a -> b
$ [NaturalTransformation] -> NaturalTransformation
forall a. [a] -> a
last [NaturalTransformation]
nats
                      podes :: ZeroGlobelet
podes = Category -> Category -> ZeroGlobelet
ZeroGlobelet Category
pos Category
neg
                      bd_north :: Functor
bd_north = ZeroGlobelet -> [Functor] -> Functor
CompositeFunctor ZeroGlobelet
podes ([Functor] -> Functor) -> [Functor] -> Functor
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation -> [Functor])
-> [NaturalTransformation] -> [Functor]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Functor -> [Functor]
func_to_single_list(Functor -> [Functor])
-> (NaturalTransformation -> Functor)
-> NaturalTransformation
-> [Functor]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> Functor
nat_source) [NaturalTransformation]
nats
                      bd_south :: Functor
bd_south = ZeroGlobelet -> [Functor] -> Functor
CompositeFunctor ZeroGlobelet
podes ([Functor] -> Functor) -> [Functor] -> Functor
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation -> [Functor])
-> [NaturalTransformation] -> [Functor]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Functor -> [Functor]
func_to_single_list(Functor -> [Functor])
-> (NaturalTransformation -> Functor)
-> NaturalTransformation
-> [Functor]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation -> Functor
nat_target) [NaturalTransformation]
nats
                      bd :: OneGlobelet
bd = Functor -> Functor -> OneGlobelet
OneGlobelet Functor
bd_north Functor
bd_south
                      in NaturalTransformation
-> Except NatHorzCompositionError NaturalTransformation
forall (m :: * -> *) a. Monad m => a -> m a
return (OneGlobelet -> [NaturalTransformation] -> NaturalTransformation
NatTransHorizontalComposite OneGlobelet
bd [NaturalTransformation]
nats)
    | Bool
otherwise = NatHorzCompositionError
-> Except NatHorzCompositionError NaturalTransformation
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (NatHorzCompositionError
 -> Except NatHorzCompositionError NaturalTransformation)
-> NatHorzCompositionError
-> Except NatHorzCompositionError NaturalTransformation
forall a b. (a -> b) -> a -> b
$ [Int] -> NatHorzCompositionError
NatHorzCompositionError ([Int] -> NatHorzCompositionError)
-> [Int] -> NatHorzCompositionError
forall a b. (a -> b) -> a -> b
$ (Bool, Int) -> Int
forall a b. (a, b) -> b
snd ((Bool, Int) -> Int) -> [(Bool, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Bool, Int)]
errs
    where 
        h_composable :: NaturalTransformation -> NaturalTransformation -> Bool
h_composable NaturalTransformation
n1 NaturalTransformation
n2 = (NaturalTransformation -> Category
nat_neg NaturalTransformation
n1) Category -> Category -> Bool
forall a. Eq a => a -> a -> Bool
== (NaturalTransformation -> Category
nat_pos NaturalTransformation
n2)
        comp_list :: [NaturalTransformation] -> [Bool]
comp_list [NaturalTransformation]
ns = (NaturalTransformation -> NaturalTransformation -> Bool)
-> [NaturalTransformation] -> [NaturalTransformation] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith NaturalTransformation -> NaturalTransformation -> Bool
h_composable [NaturalTransformation]
nats ([NaturalTransformation] -> [NaturalTransformation]
forall a. [a] -> [a]
tail [NaturalTransformation]
ns)
        errs :: [(Bool, Int)]
errs = ((Bool, Int) -> Bool) -> [(Bool, Int)] -> [(Bool, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Bool
x,Int
y) -> Bool -> Bool
not Bool
x) ([(Bool, Int)] -> [(Bool, Int)]) -> [(Bool, Int)] -> [(Bool, Int)]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Int] -> [(Bool, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([NaturalTransformation] -> [Bool]
comp_list [NaturalTransformation]
nats) [Int
0..]

-- | 'nat_vert_composable' takes a list of natural transformations and returns @True@ if the list
--  of natural transformations can be vertically composed (without specifying additional information),
--  and @False@ otherwise.
-- 'nat_vert_composable' will return @False@ on an empty list since a source
-- (or target) functor needs to be specified.
nat_vert_composable :: [NaturalTransformation] -> Bool
nat_vert_composable :: [NaturalTransformation] -> Bool
nat_vert_composable [] = Bool
False 
nat_vert_composable [NaturalTransformation]
ns = (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bool -> Bool -> Bool
(&&) Bool
True ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation -> NaturalTransformation -> Bool)
-> [NaturalTransformation] -> [NaturalTransformation] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith NaturalTransformation -> NaturalTransformation -> Bool
composable [NaturalTransformation]
ns ([NaturalTransformation] -> [NaturalTransformation]
forall a. [a] -> [a]
tail [NaturalTransformation]
ns)
    where
        composable :: NaturalTransformation -> NaturalTransformation -> Bool
composable NaturalTransformation
n1 NaturalTransformation
n2 = (NaturalTransformation -> Functor
nat_target NaturalTransformation
n1) Functor -> Functor -> Bool
forall a. Eq a => a -> a -> Bool
== (NaturalTransformation -> Functor
nat_source NaturalTransformation
n2)

-- | 'nat_vert_compose' takes a list of natural transformations and returns @Just@ their vertical
-- composition if the list is vertically composable, and @Nothing@ otherwise.
nat_vert_compose :: [NaturalTransformation] -> Maybe NaturalTransformation
nat_vert_compose :: [NaturalTransformation] -> Maybe NaturalTransformation
nat_vert_compose [NaturalTransformation]
ns
    | [NaturalTransformation] -> Bool
nat_vert_composable [NaturalTransformation]
ns = let bd :: OneGlobelet
bd = Functor -> Functor -> OneGlobelet
OneGlobelet (NaturalTransformation -> Functor
nat_source (NaturalTransformation -> Functor)
-> NaturalTransformation -> Functor
forall a b. (a -> b) -> a -> b
$ [NaturalTransformation] -> NaturalTransformation
forall a. [a] -> a
head [NaturalTransformation]
ns) (NaturalTransformation -> Functor
nat_target (NaturalTransformation -> Functor)
-> NaturalTransformation -> Functor
forall a b. (a -> b) -> a -> b
$ [NaturalTransformation] -> NaturalTransformation
forall a. [a] -> a
last [NaturalTransformation]
ns)
                                   in NaturalTransformation -> Maybe NaturalTransformation
forall a. a -> Maybe a
Just (OneGlobelet -> [NaturalTransformation] -> NaturalTransformation
NatTransVerticalComposite OneGlobelet
bd [NaturalTransformation]
ns)
    | Bool
otherwise              = Maybe NaturalTransformation
forall a. Maybe a
Nothing

-- | 'nat_source_length' of a natural transformation is the 'func_reduced_length' of its source
-- functor.
nat_source_length :: NaturalTransformation -> Int
nat_source_length :: NaturalTransformation -> Int
nat_source_length = Functor -> Int
func_reduced_length (Functor -> Int)
-> (NaturalTransformation -> Functor)
-> NaturalTransformation
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NaturalTransformation -> Functor
nat_source

-- | 'nat_target_length' of a natural transformation is the 'func_reduced_length' of its target
-- functor.
nat_target_length :: NaturalTransformation -> Int
nat_target_length :: NaturalTransformation -> Int
nat_target_length = Functor -> Int
func_reduced_length (Functor -> Int)
-> (NaturalTransformation -> Functor)
-> NaturalTransformation
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NaturalTransformation -> Functor
nat_target

-- | 'is_basic_nt' of a natural transformation is @True@ if the natural transformation is a
-- basic natural transformation, and false otherwise.
is_basic_nt :: NaturalTransformation -> Bool
is_basic_nt :: NaturalTransformation -> Bool
is_basic_nt (NaturalTransformation {}) = Bool
True
is_basic_nt NaturalTransformation
_ = Bool
False

-- | 'is_identity_nt' of a natural transformation is @True@ if the natural transformation
-- is the identity of some functor, and @False@ otherwise.
is_identity_nt :: NaturalTransformation -> Bool
is_identity_nt :: NaturalTransformation -> Bool
is_identity_nt (NatTransVerticalComposite OneGlobelet
_ []) = Bool
True
is_identity_nt NaturalTransformation
_ = Bool
False