{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : ('FinCat' 'ExponentialCategory') is the category in which live the exponential objects of 'FinCat' with the original categories.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

('FinCat' 'ExponentialCategory') is the category in which live the exponential objects of 'FinCat' with the original categories. To compute exponential objects in a usual category, see Math.CartesianClosedCategory. To compute exponential objects in a custom 'FiniteCategory', see 'exponentialObjects' in Math.CartesianClosedCategory.
-}

module Math.FiniteCategories.ExponentialCategory
(
    -- * Exponential category

    -- ** Object

    ExponentialCategoryObject(..),
    -- ** Morphism

    ExponentialCategoryMorphism(..),
    -- ** Category

    ExponentialCategory(..),
    -- * Cartesian category type

    -- ** Object

    CartesianObject(..),
    -- ** Morphism

    CartesianMorphism(..),
    -- ** Category

    CartesianCategory(..),
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    import              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.LimitCategory
    import              Math.CompleteCategory
    import              Math.CartesianClosedCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | An object in an 'ExponentialCategory'. It is either a 'ExprojectedObject' in an original category or a 'ExponentialElementObject'.

    data ExponentialCategoryObject c m o = ExprojectedObject o -- ^ An 'ExprojectedObject' is an object o.

                                         | ExponentialElementObject (FinFunctor c m o) -- ^ The exponential elemets in Cat are functors.

        deriving (ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
(ExponentialCategoryObject c m o
 -> ExponentialCategoryObject c m o -> Bool)
-> (ExponentialCategoryObject c m o
    -> ExponentialCategoryObject c m o -> Bool)
-> Eq (ExponentialCategoryObject c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq o, Eq c, Eq m, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
$c== :: forall c m o.
(Eq o, Eq c, Eq m, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
== :: ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
$c/= :: forall c m o.
(Eq o, Eq c, Eq m, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
/= :: ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o -> Bool
Eq, Int -> ExponentialCategoryObject c m o -> ShowS
[ExponentialCategoryObject c m o] -> ShowS
ExponentialCategoryObject c m o -> String
(Int -> ExponentialCategoryObject c m o -> ShowS)
-> (ExponentialCategoryObject c m o -> String)
-> ([ExponentialCategoryObject c m o] -> ShowS)
-> Show (ExponentialCategoryObject c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show o, Show c, Show m) =>
Int -> ExponentialCategoryObject c m o -> ShowS
forall c m o.
(Show o, Show c, Show m) =>
[ExponentialCategoryObject c m o] -> ShowS
forall c m o.
(Show o, Show c, Show m) =>
ExponentialCategoryObject c m o -> String
$cshowsPrec :: forall c m o.
(Show o, Show c, Show m) =>
Int -> ExponentialCategoryObject c m o -> ShowS
showsPrec :: Int -> ExponentialCategoryObject c m o -> ShowS
$cshow :: forall c m o.
(Show o, Show c, Show m) =>
ExponentialCategoryObject c m o -> String
show :: ExponentialCategoryObject c m o -> String
$cshowList :: forall c m o.
(Show o, Show c, Show m) =>
[ExponentialCategoryObject c m o] -> ShowS
showList :: [ExponentialCategoryObject c m o] -> ShowS
Show, (forall x.
 ExponentialCategoryObject c m o
 -> Rep (ExponentialCategoryObject c m o) x)
-> (forall x.
    Rep (ExponentialCategoryObject c m o) x
    -> ExponentialCategoryObject c m o)
-> Generic (ExponentialCategoryObject c m o)
forall x.
Rep (ExponentialCategoryObject c m o) x
-> ExponentialCategoryObject c m o
forall x.
ExponentialCategoryObject c m o
-> Rep (ExponentialCategoryObject c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (ExponentialCategoryObject c m o) x
-> ExponentialCategoryObject c m o
forall c m o x.
ExponentialCategoryObject c m o
-> Rep (ExponentialCategoryObject c m o) x
$cfrom :: forall c m o x.
ExponentialCategoryObject c m o
-> Rep (ExponentialCategoryObject c m o) x
from :: forall x.
ExponentialCategoryObject c m o
-> Rep (ExponentialCategoryObject c m o) x
$cto :: forall c m o x.
Rep (ExponentialCategoryObject c m o) x
-> ExponentialCategoryObject c m o
to :: forall x.
Rep (ExponentialCategoryObject c m o) x
-> ExponentialCategoryObject c m o
Generic, ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o
(ExponentialCategoryObject c m o
 -> ExponentialCategoryObject c m o)
-> Simplifiable (ExponentialCategoryObject c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m, Eq o, Eq m) =>
ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o
$csimplify :: forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m, Eq o, Eq m) =>
ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o
simplify :: ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o
Simplifiable, Int -> Int -> String -> ExponentialCategoryObject c m o -> String
Int -> ExponentialCategoryObject c m o -> String
(Int -> ExponentialCategoryObject c m o -> String)
-> (Int
    -> Int -> String -> ExponentialCategoryObject c m o -> String)
-> (Int -> ExponentialCategoryObject c m o -> String)
-> PrettyPrint (ExponentialCategoryObject c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> ExponentialCategoryObject c m o -> String
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> ExponentialCategoryObject c m o -> String
$cpprint :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> ExponentialCategoryObject c m o -> String
pprint :: Int -> ExponentialCategoryObject c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> ExponentialCategoryObject c m o -> String
pprintWithIndentations :: Int -> Int -> String -> ExponentialCategoryObject c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> ExponentialCategoryObject c m o -> String
pprintIndent :: Int -> ExponentialCategoryObject c m o -> String
PrettyPrint)
       
       
    -- | A morphism in an 'ExponentialCategory'. It is either a 'ExprojectedMorphism' in an original category or an 'ExponentialElementMorphism'.

    data ExponentialCategoryMorphism c m o = ExprojectedMorphism m -- ^ An 'ExprojectedMorphism' is a morphism m.

                                           | ExponentialElementMorphism (NaturalTransformation c m o c m o) -- ^ A 'NaturalTransformation' is a morphism in the 'ExponentialCategory'.

        deriving (ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
(ExponentialCategoryMorphism c m o
 -> ExponentialCategoryMorphism c m o -> Bool)
-> (ExponentialCategoryMorphism c m o
    -> ExponentialCategoryMorphism c m o -> Bool)
-> Eq (ExponentialCategoryMorphism c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq m, Eq c, Eq o, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
$c== :: forall c m o.
(Eq m, Eq c, Eq o, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
== :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
$c/= :: forall c m o.
(Eq m, Eq c, Eq o, FiniteCategory c m o, Morphism m o) =>
ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
/= :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o -> Bool
Eq, Int -> ExponentialCategoryMorphism c m o -> ShowS
[ExponentialCategoryMorphism c m o] -> ShowS
ExponentialCategoryMorphism c m o -> String
(Int -> ExponentialCategoryMorphism c m o -> ShowS)
-> (ExponentialCategoryMorphism c m o -> String)
-> ([ExponentialCategoryMorphism c m o] -> ShowS)
-> Show (ExponentialCategoryMorphism c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show m, Show c, Show o) =>
Int -> ExponentialCategoryMorphism c m o -> ShowS
forall c m o.
(Show m, Show c, Show o) =>
[ExponentialCategoryMorphism c m o] -> ShowS
forall c m o.
(Show m, Show c, Show o) =>
ExponentialCategoryMorphism c m o -> String
$cshowsPrec :: forall c m o.
(Show m, Show c, Show o) =>
Int -> ExponentialCategoryMorphism c m o -> ShowS
showsPrec :: Int -> ExponentialCategoryMorphism c m o -> ShowS
$cshow :: forall c m o.
(Show m, Show c, Show o) =>
ExponentialCategoryMorphism c m o -> String
show :: ExponentialCategoryMorphism c m o -> String
$cshowList :: forall c m o.
(Show m, Show c, Show o) =>
[ExponentialCategoryMorphism c m o] -> ShowS
showList :: [ExponentialCategoryMorphism c m o] -> ShowS
Show, (forall x.
 ExponentialCategoryMorphism c m o
 -> Rep (ExponentialCategoryMorphism c m o) x)
-> (forall x.
    Rep (ExponentialCategoryMorphism c m o) x
    -> ExponentialCategoryMorphism c m o)
-> Generic (ExponentialCategoryMorphism c m o)
forall x.
Rep (ExponentialCategoryMorphism c m o) x
-> ExponentialCategoryMorphism c m o
forall x.
ExponentialCategoryMorphism c m o
-> Rep (ExponentialCategoryMorphism c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (ExponentialCategoryMorphism c m o) x
-> ExponentialCategoryMorphism c m o
forall c m o x.
ExponentialCategoryMorphism c m o
-> Rep (ExponentialCategoryMorphism c m o) x
$cfrom :: forall c m o x.
ExponentialCategoryMorphism c m o
-> Rep (ExponentialCategoryMorphism c m o) x
from :: forall x.
ExponentialCategoryMorphism c m o
-> Rep (ExponentialCategoryMorphism c m o) x
$cto :: forall c m o x.
Rep (ExponentialCategoryMorphism c m o) x
-> ExponentialCategoryMorphism c m o
to :: forall x.
Rep (ExponentialCategoryMorphism c m o) x
-> ExponentialCategoryMorphism c m o
Generic, ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
(ExponentialCategoryMorphism c m o
 -> ExponentialCategoryMorphism c m o)
-> Simplifiable (ExponentialCategoryMorphism c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable m, Simplifiable c, Simplifiable o, Eq o, Eq m) =>
ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
$csimplify :: forall c m o.
(Simplifiable m, Simplifiable c, Simplifiable o, Eq o, Eq m) =>
ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
simplify :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
Simplifiable, Int -> Int -> String -> ExponentialCategoryMorphism c m o -> String
Int -> ExponentialCategoryMorphism c m o -> String
(Int -> ExponentialCategoryMorphism c m o -> String)
-> (Int
    -> Int -> String -> ExponentialCategoryMorphism c m o -> String)
-> (Int -> ExponentialCategoryMorphism c m o -> String)
-> PrettyPrint (ExponentialCategoryMorphism c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) =>
Int -> Int -> String -> ExponentialCategoryMorphism c m o -> String
forall c m o.
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) =>
Int -> ExponentialCategoryMorphism c m o -> String
$cpprint :: forall c m o.
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) =>
Int -> ExponentialCategoryMorphism c m o -> String
pprint :: Int -> ExponentialCategoryMorphism c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) =>
Int -> Int -> String -> ExponentialCategoryMorphism c m o -> String
pprintWithIndentations :: Int -> Int -> String -> ExponentialCategoryMorphism c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) =>
Int -> ExponentialCategoryMorphism c m o -> String
pprintIndent :: Int -> ExponentialCategoryMorphism c m o -> String
PrettyPrint)        
        
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Morphism (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        source :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryObject c m o
source (ExprojectedMorphism m
m) = o -> ExponentialCategoryObject c m o
forall c m o. o -> ExponentialCategoryObject c m o
ExprojectedObject (m -> o
forall m o. Morphism m o => m -> o
source m
m)
        source (ExponentialElementMorphism NaturalTransformation c m o c m o
nat) = FinFunctor c m o -> ExponentialCategoryObject c m o
forall c m o. FinFunctor c m o -> ExponentialCategoryObject c m o
ExponentialElementObject (NaturalTransformation c m o c m o -> FinFunctor c m o
forall m o. Morphism m o => m -> o
source NaturalTransformation c m o c m o
nat)
        target :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryObject c m o
target (ExprojectedMorphism m
m) = o -> ExponentialCategoryObject c m o
forall c m o. o -> ExponentialCategoryObject c m o
ExprojectedObject (m -> o
forall m o. Morphism m o => m -> o
target m
m)
        target (ExponentialElementMorphism NaturalTransformation c m o c m o
nat) = FinFunctor c m o -> ExponentialCategoryObject c m o
forall c m o. FinFunctor c m o -> ExponentialCategoryObject c m o
ExponentialElementObject (NaturalTransformation c m o c m o -> FinFunctor c m o
forall m o. Morphism m o => m -> o
target NaturalTransformation c m o c m o
nat)
        (ExprojectedMorphism m
m2) @ :: ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
-> ExponentialCategoryMorphism c m o
@ (ExprojectedMorphism m
m1) = m -> ExponentialCategoryMorphism c m o
forall c m o. m -> ExponentialCategoryMorphism c m o
ExprojectedMorphism (m -> ExponentialCategoryMorphism c m o)
-> m -> ExponentialCategoryMorphism c m o
forall a b. (a -> b) -> a -> b
$ m
m2 m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
m1
        (ExponentialElementMorphism NaturalTransformation c m o c m o
nat2) @ (ExponentialElementMorphism NaturalTransformation c m o c m o
nat1) = NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
forall c m o.
NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
ExponentialElementMorphism (NaturalTransformation c m o c m o
 -> ExponentialCategoryMorphism c m o)
-> NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c m o c m o
nat2 NaturalTransformation c m o c m o
-> NaturalTransformation c m o c m o
-> NaturalTransformation c m o c m o
forall m o. Morphism m o => m -> m -> m
@ NaturalTransformation c m o c m o
nat1
        ExponentialCategoryMorphism c m o
_ @ ExponentialCategoryMorphism c m o
_ = String -> ExponentialCategoryMorphism c m o
forall a. HasCallStack => String -> a
error String
"Incompatible composition of ExponentialCategory morphisms."
    
    
    
    -- | An 'ExponentialCategory' is either an 'ExprojectedCategory' (an original category) or an 'ExponentialCategory'.

    data ExponentialCategory c m o = ExprojectedCategory c -- ^ An original category in 'FinCat'.

                                   | ExponentialCategory (FunctorCategory c m o c m o)     -- ^ The exponential category of a given 2-base is a 'FunctorCategory'.

        deriving (ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
(ExponentialCategory c m o -> ExponentialCategory c m o -> Bool)
-> (ExponentialCategory c m o -> ExponentialCategory c m o -> Bool)
-> Eq (ExponentialCategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
Eq c =>
ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
$c== :: forall c m o.
Eq c =>
ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
== :: ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
$c/= :: forall c m o.
Eq c =>
ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
/= :: ExponentialCategory c m o -> ExponentialCategory c m o -> Bool
Eq, Int -> ExponentialCategory c m o -> ShowS
[ExponentialCategory c m o] -> ShowS
ExponentialCategory c m o -> String
(Int -> ExponentialCategory c m o -> ShowS)
-> (ExponentialCategory c m o -> String)
-> ([ExponentialCategory c m o] -> ShowS)
-> Show (ExponentialCategory c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o. Show c => Int -> ExponentialCategory c m o -> ShowS
forall c m o. Show c => [ExponentialCategory c m o] -> ShowS
forall c m o. Show c => ExponentialCategory c m o -> String
$cshowsPrec :: forall c m o. Show c => Int -> ExponentialCategory c m o -> ShowS
showsPrec :: Int -> ExponentialCategory c m o -> ShowS
$cshow :: forall c m o. Show c => ExponentialCategory c m o -> String
show :: ExponentialCategory c m o -> String
$cshowList :: forall c m o. Show c => [ExponentialCategory c m o] -> ShowS
showList :: [ExponentialCategory c m o] -> ShowS
Show, (forall x.
 ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x)
-> (forall x.
    Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o)
-> Generic (ExponentialCategory c m o)
forall x.
Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o
forall x.
ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o
forall c m o x.
ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x
$cfrom :: forall c m o x.
ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x
from :: forall x.
ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x
$cto :: forall c m o x.
Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o
to :: forall x.
Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o
Generic, ExponentialCategory c m o -> ExponentialCategory c m o
(ExponentialCategory c m o -> ExponentialCategory c m o)
-> Simplifiable (ExponentialCategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
Simplifiable c =>
ExponentialCategory c m o -> ExponentialCategory c m o
$csimplify :: forall c m o.
Simplifiable c =>
ExponentialCategory c m o -> ExponentialCategory c m o
simplify :: ExponentialCategory c m o -> ExponentialCategory c m o
Simplifiable, Int -> Int -> String -> ExponentialCategory c m o -> String
Int -> ExponentialCategory c m o -> String
(Int -> ExponentialCategory c m o -> String)
-> (Int -> Int -> String -> ExponentialCategory c m o -> String)
-> (Int -> ExponentialCategory c m o -> String)
-> PrettyPrint (ExponentialCategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
PrettyPrint c =>
Int -> Int -> String -> ExponentialCategory c m o -> String
forall c m o.
PrettyPrint c =>
Int -> ExponentialCategory c m o -> String
$cpprint :: forall c m o.
PrettyPrint c =>
Int -> ExponentialCategory c m o -> String
pprint :: Int -> ExponentialCategory c m o -> String
$cpprintWithIndentations :: forall c m o.
PrettyPrint c =>
Int -> Int -> String -> ExponentialCategory c m o -> String
pprintWithIndentations :: Int -> Int -> String -> ExponentialCategory c m o -> String
$cpprintIndent :: forall c m o.
PrettyPrint c =>
Int -> ExponentialCategory c m o -> String
pprintIndent :: Int -> ExponentialCategory c m o -> String
PrettyPrint)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        identity :: Morphism
  (ExponentialCategoryMorphism c m o)
  (ExponentialCategoryObject c m o) =>
ExponentialCategory c m o
-> ExponentialCategoryObject c m o
-> ExponentialCategoryMorphism c m o
identity (ExprojectedCategory c
c) (ExprojectedObject o
o) = m -> ExponentialCategoryMorphism c m o
forall c m o. m -> ExponentialCategoryMorphism c m o
ExprojectedMorphism (m -> ExponentialCategoryMorphism c m o)
-> m -> ExponentialCategoryMorphism c m o
forall a b. (a -> b) -> a -> b
$ c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
        identity (ExponentialCategory FunctorCategory c m o c m o
_) (ExprojectedObject o
_) = String -> ExponentialCategoryMorphism c m o
forall a. HasCallStack => String -> a
error String
"Identity in an exponential category on an exprojected object."
        identity (ExprojectedCategory c
_) (ExponentialElementObject FinFunctor c m o
_) = String -> ExponentialCategoryMorphism c m o
forall a. HasCallStack => String -> a
error String
"Identity in an exprojected category on a exponential element."
        identity (ExponentialCategory FunctorCategory c m o c m o
functCat) (ExponentialElementObject FinFunctor c m o
funct) = NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
forall c m o.
NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
ExponentialElementMorphism (NaturalTransformation c m o c m o
 -> ExponentialCategoryMorphism c m o)
-> NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
forall a b. (a -> b) -> a -> b
$ FunctorCategory c m o c m o
-> FinFunctor c m o -> NaturalTransformation c m o c m o
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FunctorCategory c m o c m o
functCat FinFunctor c m o
funct
        ar :: Morphism
  (ExponentialCategoryMorphism c m o)
  (ExponentialCategoryObject c m o) =>
ExponentialCategory c m o
-> ExponentialCategoryObject c m o
-> ExponentialCategoryObject c m o
-> Set (ExponentialCategoryMorphism c m o)
ar (ExprojectedCategory c
functCat) (ExprojectedObject o
s) (ExprojectedObject o
t) = m -> ExponentialCategoryMorphism c m o
forall c m o. m -> ExponentialCategoryMorphism c m o
ExprojectedMorphism (m -> ExponentialCategoryMorphism c m o)
-> Set m -> Set (ExponentialCategoryMorphism c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
functCat o
s o
t
        ar (ExprojectedCategory c
_) (ExprojectedObject o
_) (ExponentialElementObject FinFunctor c m o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exprojected category where the target is an exponential element."
        ar (ExprojectedCategory c
_) (ExponentialElementObject FinFunctor c m o
_) (ExprojectedObject o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exprojected category where the source is an exponential element."
        ar (ExprojectedCategory c
_) (ExponentialElementObject FinFunctor c m o
_) (ExponentialElementObject FinFunctor c m o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exprojected category where the source and the target are exponential elements."
        ar (ExponentialCategory FunctorCategory c m o c m o
_) (ExprojectedObject o
_) (ExprojectedObject o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exponential category where the source and target are exprojected objects."
        ar (ExponentialCategory FunctorCategory c m o c m o
_) (ExprojectedObject o
_) (ExponentialElementObject FinFunctor c m o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exponential category where the source is an exprojected object."
        ar (ExponentialCategory FunctorCategory c m o c m o
_) (ExponentialElementObject FinFunctor c m o
_) (ExprojectedObject o
_) = String -> Set (ExponentialCategoryMorphism c m o)
forall a. HasCallStack => String -> a
error String
"Ar in an exponential category where the target is an exprojected object."
        ar (ExponentialCategory FunctorCategory c m o c m o
functCat) (ExponentialElementObject FinFunctor c m o
s) (ExponentialElementObject FinFunctor c m o
t) = NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
forall c m o.
NaturalTransformation c m o c m o
-> ExponentialCategoryMorphism c m o
ExponentialElementMorphism (NaturalTransformation c m o c m o
 -> ExponentialCategoryMorphism c m o)
-> Set (NaturalTransformation c m o c m o)
-> Set (ExponentialCategoryMorphism c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c m o c m o
-> FinFunctor c m o
-> FinFunctor c m o
-> Set (NaturalTransformation c m o c m o)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar FunctorCategory c m o c m o
functCat FinFunctor c m o
s FinFunctor c m o
t
            
            
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        ob :: ExponentialCategory c m o -> Set (ExponentialCategoryObject c m o)
ob (ExprojectedCategory c
cat) = o -> ExponentialCategoryObject c m o
forall c m o. o -> ExponentialCategoryObject c m o
ExprojectedObject (o -> ExponentialCategoryObject c m o)
-> Set o -> Set (ExponentialCategoryObject c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat
        ob (ExponentialCategory FunctorCategory c m o c m o
functCat) = FinFunctor c m o -> ExponentialCategoryObject c m o
forall c m o. FinFunctor c m o -> ExponentialCategoryObject c m o
ExponentialElementObject (FinFunctor c m o -> ExponentialCategoryObject c m o)
-> Set (FinFunctor c m o) -> Set (ExponentialCategoryObject c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c m o c m o -> Set (FinFunctor c m o)
forall c m o. FiniteCategory c m o => c -> Set o
ob FunctorCategory c m o c m o
functCat
    
    type TwoProductOfCategories c m o = FinCat (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o)
    type TwoProductOfCategoriesMorphism c m o = FinFunctor (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o)
    type TwoProductOfCategoriesObject c m o = LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
    
    -- | The type of the category containing categories and their exponential objects.

    type CartesianCategory c m o = TwoProductOfCategories (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    -- | A morphism in 'CartesianCategory'.

    type CartesianMorphism c m o = TwoProductOfCategoriesMorphism (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    -- | An object in 'CartesianCategory'.

    type CartesianObject c m o = TwoProductOfCategoriesObject (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => CartesianClosedCategory (FinCat c m o) (FinFunctor c m o) c (TwoProductOfCategories c m o) (TwoProductOfCategoriesMorphism c m o) (TwoProductOfCategoriesObject c m o) (CartesianCategory c m o) (CartesianMorphism c m o) (CartesianObject c m o) where
        internalHom :: CompleteCategory
  (FinCat c m o)
  (FinFunctor c m o)
  c
  (TwoProductOfCategories c m o)
  (TwoProductOfCategoriesMorphism c m o)
  (TwoProductOfCategoriesObject c m o)
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr =>
TwoBase (FinCat c m o) (FinFunctor c m o) c
-> Tripod
     (CartesianCategory c m o)
     (CartesianMorphism c m o)
     (CartesianObject c m o)
internalHom TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase = Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
-> CartesianMorphism c m o
-> Tripod
     (CartesianCategory c m o)
     (CartesianMorphism c m o)
     (CartesianObject c m o)
forall c m o.
Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> m -> Tripod c m o
unsafeTripod Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
twoLimit CartesianMorphism c m o
forall {cIndex} {mIndex} {oIndex} {m} {o} {m} {o} {oIndex} {c} {o}
       {oIndex} {c} {m}.
Diagram
  (CartesianObject c m o)
  (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
  (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
  (LimitCategory
     cIndex mIndex oIndex (ExponentialCategory c m o) m o)
  (Limit oIndex (ExponentialCategoryMorphism c m o))
  (Limit oIndex (ExponentialCategoryObject c m o))
evalMap_
            where
                powerObject :: ExponentialCategory c m o
powerObject = FunctorCategory c m o c m o -> ExponentialCategory c m o
forall c m o.
FunctorCategory c m o c m o -> ExponentialCategory c m o
ExponentialCategory (c -> c -> FunctorCategory c m o c m o
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase TwoBase (FinCat c m o) (FinFunctor c m o) c -> DiscreteTwoAr -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A) (TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase TwoBase (FinCat c m o) (FinFunctor c m o) c -> DiscreteTwoAr -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B))
                baseTwoCone :: Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinCat
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (FinFunctor
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (ExponentialCategory c m o)
baseTwoCone = FinCat
  (ExponentialCategory c m o)
  (ExponentialCategoryMorphism c m o)
  (ExponentialCategoryObject c m o)
-> ExponentialCategory c m o
-> ExponentialCategory c m o
-> Diagram
     DiscreteTwo
     DiscreteTwoAr
     DiscreteTwoAr
     (FinCat
        (ExponentialCategory c m o)
        (ExponentialCategoryMorphism c m o)
        (ExponentialCategoryObject c m o))
     (FinFunctor
        (ExponentialCategory c m o)
        (ExponentialCategoryMorphism c m o)
        (ExponentialCategoryObject c m o))
     (ExponentialCategory c m o)
forall c m o.
(Category c m o, Morphism m o) =>
c
-> o -> o -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoDiagram FinCat
  (ExponentialCategory c m o)
  (ExponentialCategoryMorphism c m o)
  (ExponentialCategoryObject c m o)
forall c m o. FinCat c m o
FinCat ExponentialCategory c m o
forall {m} {o}. ExponentialCategory c m o
powerObject (c -> ExponentialCategory c m o
forall c m o. c -> ExponentialCategory c m o
ExprojectedCategory (TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase TwoBase (FinCat c m o) (FinFunctor c m o) c -> DiscreteTwoAr -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A))
                twoLimit :: Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
twoLimit = Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinCat
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (FinFunctor
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (ExponentialCategory c m o)
-> Cone
     DiscreteTwo
     DiscreteTwoAr
     DiscreteTwoAr
     (CartesianCategory c m o)
     (CartesianMorphism c m o)
     (CartesianObject c m o)
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cone cIndex mIndex oIndex cLim mLim oLim
limit Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinCat
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (FinFunctor
     (ExponentialCategory c m o)
     (ExponentialCategoryMorphism c m o)
     (ExponentialCategoryObject c m o))
  (ExponentialCategory c m o)
baseTwoCone
                evalOb :: Limit DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
-> Limit oIndex (ExponentialCategoryObject c m o)
evalOb (ProductElement Map DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
tuple) = ExponentialCategoryObject c m o
-> Limit oIndex (ExponentialCategoryObject c m o)
forall oIndex t. t -> Limit oIndex t
Projection (o -> ExponentialCategoryObject c m o
forall c m o. o -> ExponentialCategoryObject c m o
ExprojectedObject (o -> ExponentialCategoryObject c m o)
-> o -> ExponentialCategoryObject c m o
forall a b. (a -> b) -> a -> b
$ FinFunctor c2 m2 o
funct FinFunctor c2 m2 o -> o -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o
x)
                    where
                        (ExponentialElementObject FinFunctor c2 m2 o
funct) = Map DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
tuple Map DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
-> DiscreteTwoAr -> ExponentialCategoryObject c2 m2 o
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
A
                        (ExprojectedObject o
x)  = Map DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
tuple Map DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
-> DiscreteTwoAr -> ExponentialCategoryObject c2 m2 o
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
B
                evalAr :: Limit DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
-> Limit oIndex (ExponentialCategoryMorphism c m o)
evalAr (ProductElement Map DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
tuple) = ExponentialCategoryMorphism c m o
-> Limit oIndex (ExponentialCategoryMorphism c m o)
forall oIndex t. t -> Limit oIndex t
Projection (m -> ExponentialCategoryMorphism c m o
forall c m o. m -> ExponentialCategoryMorphism c m o
ExprojectedMorphism (m -> ExponentialCategoryMorphism c m o)
-> m -> ExponentialCategoryMorphism c m o
forall a b. (a -> b) -> a -> b
$ ((NaturalTransformation c1 m o2 c1 m o2 -> Diagram c1 m o2 c1 m o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m o2 c1 m o2
nat) Diagram c1 m o2 c1 m o2 -> m -> m
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m
f) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (NaturalTransformation c1 m o2 c1 m o2
nat NaturalTransformation c1 m o2 c1 m o2 -> o2 -> m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (m -> o2
forall m o. Morphism m o => m -> o
source m
f)))
                    where
                        (ExponentialElementMorphism NaturalTransformation c1 m o2 c1 m o2
nat) = Map DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
tuple Map DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
-> DiscreteTwoAr -> ExponentialCategoryMorphism c1 m o2
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
A
                        (ExprojectedMorphism m
f)  = Map DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
tuple Map DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
-> DiscreteTwoAr -> ExponentialCategoryMorphism c1 m o2
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
B
                finalInternalCodomain :: Limit oIndex (Exponential c)
finalInternalCodomain = Exponential c -> Limit oIndex (Exponential c)
forall oIndex t. t -> Limit oIndex t
Projection (Exponential c -> Limit oIndex (Exponential c))
-> Exponential c -> Limit oIndex (Exponential c)
forall a b. (a -> b) -> a -> b
$ (c -> Exponential c
forall t. t -> Exponential t
Exprojection (c -> Exponential c) -> c -> Exponential c
forall a b. (a -> b) -> a -> b
$ TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase TwoBase (FinCat c m o) (FinFunctor c m o) c -> DiscreteTwoAr -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A)
                newInternalCodomain :: LimitCategory cIndex mIndex oIndex (ExponentialCategory c m o) m o
newInternalCodomain = ExponentialCategory c m o
-> LimitCategory
     cIndex mIndex oIndex (ExponentialCategory c m o) m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (ExponentialCategory c m o
 -> LimitCategory
      cIndex mIndex oIndex (ExponentialCategory c m o) m o)
-> ExponentialCategory c m o
-> LimitCategory
     cIndex mIndex oIndex (ExponentialCategory c m o) m o
forall a b. (a -> b) -> a -> b
$ c -> ExponentialCategory c m o
forall c m o. c -> ExponentialCategory c m o
ExprojectedCategory (c -> ExponentialCategory c m o) -> c -> ExponentialCategory c m o
forall a b. (a -> b) -> a -> b
$ (TwoBase (FinCat c m o) (FinFunctor c m o) c
twoBase TwoBase (FinCat c m o) (FinFunctor c m o) c -> DiscreteTwoAr -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B)
                evalMap_ :: Diagram
  (CartesianObject c m o)
  (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
  (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
  (LimitCategory
     cIndex mIndex oIndex (ExponentialCategory c m o) m o)
  (Limit oIndex (ExponentialCategoryMorphism c m o))
  (Limit oIndex (ExponentialCategoryObject c m o))
evalMap_ = Diagram{src :: CartesianObject c m o
src = Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
-> CartesianObject c m o
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
twoLimit, tgt :: LimitCategory cIndex mIndex oIndex (ExponentialCategory c m o) m o
tgt = LimitCategory cIndex mIndex oIndex (ExponentialCategory c m o) m o
forall {cIndex} {mIndex} {oIndex} {m} {o} {m} {o}.
LimitCategory cIndex mIndex oIndex (ExponentialCategory c m o) m o
newInternalCodomain, omap :: Map
  (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
  (Limit oIndex (ExponentialCategoryObject c m o))
omap = (Limit DiscreteTwoAr (ExponentialCategoryObject c m o)
 -> Limit oIndex (ExponentialCategoryObject c m o))
-> Set (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
-> Map
     (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
     (Limit oIndex (ExponentialCategoryObject c m o))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Limit DiscreteTwoAr (ExponentialCategoryObject c m o)
-> Limit oIndex (ExponentialCategoryObject c m o)
forall {o} {c2} {m2} {oIndex} {c} {m}.
Eq o =>
Limit DiscreteTwoAr (ExponentialCategoryObject c2 m2 o)
-> Limit oIndex (ExponentialCategoryObject c m o)
evalOb (CartesianObject c m o
-> Set (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
forall c m o. FiniteCategory c m o => c -> Set o
ob (CartesianObject c m o
 -> Set (Limit DiscreteTwoAr (ExponentialCategoryObject c m o)))
-> CartesianObject c m o
-> Set (Limit DiscreteTwoAr (ExponentialCategoryObject c m o))
forall a b. (a -> b) -> a -> b
$ Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
-> CartesianObject c m o
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
twoLimit), mmap :: Map
  (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
  (Limit oIndex (ExponentialCategoryMorphism c m o))
mmap = (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o)
 -> Limit oIndex (ExponentialCategoryMorphism c m o))
-> Set (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
-> Map
     (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
     (Limit oIndex (ExponentialCategoryMorphism c m o))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o)
-> Limit oIndex (ExponentialCategoryMorphism c m o)
forall {m} {o2} {c1} {oIndex} {c} {o}.
(Morphism m o2, FiniteCategory c1 m o2, Eq m, Eq c1, Eq o2) =>
Limit DiscreteTwoAr (ExponentialCategoryMorphism c1 m o2)
-> Limit oIndex (ExponentialCategoryMorphism c m o)
evalAr (CartesianObject c m o
-> Set (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (CartesianObject c m o
 -> Set (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o)))
-> CartesianObject c m o
-> Set (Limit DiscreteTwoAr (ExponentialCategoryMorphism c m o))
forall a b. (a -> b) -> a -> b
$ Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
-> CartesianObject c m o
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (CartesianCategory c m o)
  (CartesianMorphism c m o)
  (CartesianObject c m o)
twoLimit)}