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

{-| Module  : FiniteCategories
Description : The __'FinSet'__ category has finite sets as objects and functions as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'FinSet'__ category has finite sets as objects and functions as morphisms.

Finite sets are represented by weak sets from Data.WeakSet and functions by enriched weak maps from Data.WeakMap.

These structures are homogeneous, meaning you can only have sets containing one type of objects in a given 'FinSet' category.

See the category __'PureSet'__ for the category of sets which can be arbitrarily nested.
-}

module Math.Categories.FinSet
(
    -- * Function

    Function(..),
    (||!||),
    -- * __FinSet__

    FinSet(..),
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.CartesianClosedCategory
    
    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           (nub)
    import              Data.Maybe          (fromJust)
    import              Data.Simplifiable
    
    import              GHC.Generics

    
    -- | A 'Function' (finite function) is a weak map enriched with a codomain.

    --

    -- We have to store the codomain to retrieve the target set of a morphism in __'FinSet'__.

    data Function a = Function 
                            {
                                forall a. Function a -> Map a a
function :: Map a a,
                                forall a. Function a -> Set a
codomain :: Set a
                            }
                        deriving
                            (Function a -> Function a -> Bool
(Function a -> Function a -> Bool)
-> (Function a -> Function a -> Bool) -> Eq (Function a)
forall a. Eq a => Function a -> Function a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Function a -> Function a -> Bool
== :: Function a -> Function a -> Bool
$c/= :: forall a. Eq a => Function a -> Function a -> Bool
/= :: Function a -> Function a -> Bool
Eq, Int -> Function a -> ShowS
[Function a] -> ShowS
Function a -> String
(Int -> Function a -> ShowS)
-> (Function a -> String)
-> ([Function a] -> ShowS)
-> Show (Function a)
forall a. Show a => Int -> Function a -> ShowS
forall a. Show a => [Function a] -> ShowS
forall a. Show a => Function a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Function a -> ShowS
showsPrec :: Int -> Function a -> ShowS
$cshow :: forall a. Show a => Function a -> String
show :: Function a -> String
$cshowList :: forall a. Show a => [Function a] -> ShowS
showList :: [Function a] -> ShowS
Show, (forall x. Function a -> Rep (Function a) x)
-> (forall x. Rep (Function a) x -> Function a)
-> Generic (Function a)
forall x. Rep (Function a) x -> Function a
forall x. Function a -> Rep (Function a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Function a) x -> Function a
forall a x. Function a -> Rep (Function a) x
$cfrom :: forall a x. Function a -> Rep (Function a) x
from :: forall x. Function a -> Rep (Function a) x
$cto :: forall a x. Rep (Function a) x -> Function a
to :: forall x. Rep (Function a) x -> Function a
Generic, Function a -> Function a
(Function a -> Function a) -> Simplifiable (Function a)
forall a. (Simplifiable a, Eq a) => Function a -> Function a
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall a. (Simplifiable a, Eq a) => Function a -> Function a
simplify :: Function a -> Function a
Simplifiable)
    
    instance (PrettyPrint a, Eq a) => PrettyPrint (Function a) where
        pprint :: Int -> Function a -> String
pprint Int
v Function a
a = Int -> Map a a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
a)
        
        -- pprintWithIndentations cv ov indent a = pprintWithIndentations cv ov indent (function a)

        
    instance (Eq a) => Morphism (Function a) (Set a) where
        source :: Function a -> Set a
source = Map a a -> Set a
forall k a. Map k a -> Set k
domain(Map a a -> Set a)
-> (Function a -> Map a a) -> Function a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function a -> Map a a
forall a. Function a -> Map a a
function
        target :: Function a -> Set a
target = Function a -> Set a
forall a. Function a -> Set a
codomain
        @ :: Function a -> Function a -> Function a
(@) Function a
f2 Function a
f1 = Function{function :: Map a a
function = (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f2) Map a a -> Map a a -> Map a a
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f1), codomain :: Set a
codomain = Function a -> Set a
forall a. Function a -> Set a
codomain Function a
f2}
            
    -- | A function to apply a 'Function' to an object in the domain of the 'Function'.

    (||!||) :: (Eq a) => Function a -> a -> a
    ||!|| :: forall a. Eq a => Function a -> a -> a
(||!||) Function a
f a
x = (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
f) Map a a -> a -> a
forall k v. Eq k => Map k v -> k -> v
|!| a
x
    
    -- | __'FinSet'__ is the category of finite sets.

    data FinSet a = FinSet deriving (FinSet a -> FinSet a -> Bool
(FinSet a -> FinSet a -> Bool)
-> (FinSet a -> FinSet a -> Bool) -> Eq (FinSet a)
forall a. FinSet a -> FinSet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. FinSet a -> FinSet a -> Bool
== :: FinSet a -> FinSet a -> Bool
$c/= :: forall a. FinSet a -> FinSet a -> Bool
/= :: FinSet a -> FinSet a -> Bool
Eq, Int -> FinSet a -> ShowS
[FinSet a] -> ShowS
FinSet a -> String
(Int -> FinSet a -> ShowS)
-> (FinSet a -> String) -> ([FinSet a] -> ShowS) -> Show (FinSet a)
forall a. Int -> FinSet a -> ShowS
forall a. [FinSet a] -> ShowS
forall a. FinSet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> FinSet a -> ShowS
showsPrec :: Int -> FinSet a -> ShowS
$cshow :: forall a. FinSet a -> String
show :: FinSet a -> String
$cshowList :: forall a. [FinSet a] -> ShowS
showList :: [FinSet a] -> ShowS
Show, (forall x. FinSet a -> Rep (FinSet a) x)
-> (forall x. Rep (FinSet a) x -> FinSet a) -> Generic (FinSet a)
forall x. Rep (FinSet a) x -> FinSet a
forall x. FinSet a -> Rep (FinSet a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FinSet a) x -> FinSet a
forall a x. FinSet a -> Rep (FinSet a) x
$cfrom :: forall a x. FinSet a -> Rep (FinSet a) x
from :: forall x. FinSet a -> Rep (FinSet a) x
$cto :: forall a x. Rep (FinSet a) x -> FinSet a
to :: forall x. Rep (FinSet a) x -> FinSet a
Generic, Int -> Int -> String -> FinSet a -> String
Int -> FinSet a -> String
(Int -> FinSet a -> String)
-> (Int -> Int -> String -> FinSet a -> String)
-> (Int -> FinSet a -> String)
-> PrettyPrint (FinSet a)
forall a. Int -> Int -> String -> FinSet a -> String
forall a. Int -> FinSet a -> String
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: forall a. Int -> FinSet a -> String
pprint :: Int -> FinSet a -> String
$cpprintWithIndentations :: forall a. Int -> Int -> String -> FinSet a -> String
pprintWithIndentations :: Int -> Int -> String -> FinSet a -> String
$cpprintIndent :: forall a. Int -> FinSet a -> String
pprintIndent :: Int -> FinSet a -> String
PrettyPrint, FinSet a -> FinSet a
(FinSet a -> FinSet a) -> Simplifiable (FinSet a)
forall a. FinSet a -> FinSet a
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall a. FinSet a -> FinSet a
simplify :: FinSet a -> FinSet a
Simplifiable)
    
    instance (Eq a) => Category (FinSet a) (Function a) (Set a) where
        identity :: Morphism (Function a) (Set a) => FinSet a -> Set a -> Function a
identity FinSet a
_ Set a
s = Function {function :: Map a a
function = Set a -> Map a a
forall a. Set a -> Map a a
idFromSet Set a
s, codomain :: Set a
codomain = Set a
s}
        
        ar :: Morphism (Function a) (Set a) =>
FinSet a -> Set a -> Set a -> Set (Function a)
ar FinSet a
_ Set a
s Set a
t
            | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s = [Function a] -> Set (Function a)
forall a. [a] -> Set a
set [Function{function :: Map a a
function = AssociationList a a -> Map a a
forall k v. AssociationList k v -> Map k v
weakMap [], codomain :: Set a
codomain = Set a
t}]
            | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
t = [Function a] -> Set (Function a)
forall a. [a] -> Set a
set []
            | Bool
otherwise = (\Map a a
x -> Function{function :: Map a a
function = Map a a
x, codomain :: Set a
codomain = Set a
t}) (Map a a -> Function a) -> Set (Map a a) -> Set (Function a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Map a a)
functions where
                domain :: [a]
domain = Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList Set a
s
                images :: Set [a]
images = (Set a
t Set a -> Int -> Set [a]
forall a. Eq a => Set a -> Int -> Set [a]
|^| ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
domain))
                functions :: Set (Map a a)
functions = AssociationList a a -> Map a a
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList a a -> Map a a)
-> ([a] -> AssociationList a a) -> [a] -> Map a a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [a] -> AssociationList a a
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
domain ([a] -> Map a a) -> Set [a] -> Set (Map a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set [a]
images
                
    instance (Eq a, Eq oIndex) => HasProducts (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) oIndex where
        product :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
product Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag = Cone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
result
            where
                indexingCat :: DiscreteCategory oIndex
indexingCat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag
                prod :: Set (Limit oIndex a)
prod = (Map oIndex a -> Limit oIndex a
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement)(Map oIndex a -> Limit oIndex a)
-> ([(oIndex, a)] -> Map oIndex a)
-> [(oIndex, a)]
-> Limit oIndex a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(oIndex, a)] -> Map oIndex a
forall k v. AssociationList k v -> Map k v
weakMap ([(oIndex, a)] -> Limit oIndex a)
-> Set [(oIndex, a)] -> Set (Limit oIndex a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (oIndex, a)] -> Set [(oIndex, a)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets (Set (Set (oIndex, a)) -> [Set (oIndex, a)]
forall a. Eq a => Set a -> [a]
setToList [(\a
x -> (oIndex
i,a
x)) (a -> (oIndex, a)) -> Set a -> Set (oIndex, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> oIndex -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat])
                mapping :: oIndex -> Map (Limit oIndex a) (Limit oIndex a)
mapping oIndex
i = (Limit oIndex a -> Limit oIndex a)
-> Set (Limit oIndex a) -> Map (Limit oIndex a) (Limit oIndex a)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\(ProductElement Map oIndex a
tuple) -> a -> Limit oIndex a
forall oIndex t. t -> Limit oIndex t
Projection (Map oIndex a
tuple Map oIndex a -> oIndex -> a
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
i)) Set (Limit oIndex a)
prod
                constDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
constDiag = DiscreteCategory oIndex
-> FinSet (Limit oIndex a)
-> Set (Limit oIndex a)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram DiscreteCategory oIndex
indexingCat FinSet (Limit oIndex a)
forall a. FinSet a
FinSet Set (Limit oIndex a)
prod
                transformObject :: m t -> m (Limit oIndex t)
transformObject m t
x = [t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
e | t
e <- m t
x]
                transformFunction :: Function t -> Function (Limit oIndex t)
transformFunction Function{function :: forall a. Function a -> Map a a
function = Map t t
m, codomain :: forall a. Function a -> Set a
codomain = Set t
cod} = Function{function :: Map (Limit oIndex t) (Limit oIndex t)
function = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
k, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
v) | (t
k,t
v) <- Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
m], codomain :: Set (Limit oIndex t)
codomain = Set t -> Set (Limit oIndex t)
forall {m :: * -> *} {t} {oIndex}.
Monad m =>
m t -> m (Limit oIndex t)
transformObject Set t
cod}
                newDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
newDiag = Diagram{src :: DiscreteCategory oIndex
src = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag, tgt :: FinSet a
tgt = FinSet a
forall a. FinSet a
FinSet, omap :: Map oIndex (Set (Limit oIndex a))
omap = Set a -> Set (Limit oIndex a)
forall {m :: * -> *} {t} {oIndex}.
Monad m =>
m t -> m (Limit oIndex t)
transformObject (Set a -> Set (Limit oIndex a))
-> Map oIndex (Set a) -> Map oIndex (Set (Limit oIndex a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Map oIndex (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag), mmap :: Map (DiscreteMorphism oIndex) (Function (Limit oIndex a))
mmap = Function a -> Function (Limit oIndex a)
forall {t} {oIndex}.
Eq t =>
Function t -> Function (Limit oIndex t)
transformFunction (Function a -> Function (Limit oIndex a))
-> Map (DiscreteMorphism oIndex) (Function a)
-> Map (DiscreteMorphism oIndex) (Function (Limit oIndex a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Map (DiscreteMorphism oIndex) (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag)}
                result :: Cone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
result = Set (Limit oIndex a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone Set (Limit oIndex a)
prod (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
-> Map oIndex (Function (Limit oIndex a))
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
constDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Limit oIndex a))
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
forall {a} {oIndex} {oIndex}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
newDiag (Set (oIndex, Function (Limit oIndex a))
-> Map oIndex (Function (Limit oIndex a))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
i,Function {function :: Map (Limit oIndex a) (Limit oIndex a)
function=oIndex -> Map (Limit oIndex a) (Limit oIndex a)
forall {oIndex}. oIndex -> Map (Limit oIndex a) (Limit oIndex a)
mapping oIndex
i, codomain :: Set (Limit oIndex a)
codomain = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet Any)
  (Function (Limit Any a))
  (Set (Limit oIndex a))
forall {a} {oIndex} {oIndex}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Limit oIndex a))
  (Set (Limit oIndex a))
newDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet Any)
  (Function (Limit Any a))
  (Set (Limit oIndex a))
-> oIndex -> Set (Limit oIndex a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i}) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat]))
                
    instance (Eq a) => HasEqualizers (FinSet a) (Function a) (Set a) where
        equalize :: Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Cone
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
equalize Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag = Cone Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
result
            where
                equalizer :: Set a
equalizer = [a
e | a
e <- Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelOb -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA, (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
e a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelG) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
e]
                mapping :: p -> Map a a
mapping p
i = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id Set a
equalizer
                constDiag :: Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
constDiag = Parallel
-> FinSet a
-> Set a
-> Diagram
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram Parallel
Parallel FinSet a
forall a. FinSet a
FinSet Set a
equalizer
                result :: Cone Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
result = Set a
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Cone
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone Set a
equalizer (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Diagram
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Map ParallelOb (Function a)
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
constDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag (AssociationList ParallelOb (Function a)
-> Map ParallelOb (Function a)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA,Function a
legA), (ParallelOb
ParallelB, (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF) Function a -> Function a -> Function a
forall m o. Morphism m o => m -> m -> m
@ Function a
legA) ]))
                legA :: Function a
legA = Function {function :: Map a a
function=ParallelOb -> Map a a
forall {p}. p -> Map a a
mapping ParallelOb
ParallelA, codomain :: Set a
codomain = Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelOb -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA}
    
    _projectMorphism :: Function t -> Function (Limit oIndex t)
_projectMorphism Function t
m = Function{function :: Map (Limit oIndex t) (Limit oIndex t)
function = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
k, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
v) | (t
k,t
v) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet(Map t t -> Set (t, t))
-> (Function t -> Map t t) -> Function t -> Set (t, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function t -> Map t t
forall a. Function a -> Map a a
function) Function t
m], codomain :: Set (Limit oIndex t)
codomain = t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection (t -> Limit oIndex t) -> Set t -> Set (Limit oIndex t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function t -> Set t
forall a. Function a -> Set a
codomain Function t
m}
    
    instance (Eq a, Eq mIndex, Eq oIndex) => CompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) cIndex mIndex oIndex where
        limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Cone
     cIndex
     mIndex
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
limit = (Function a -> Function (Limit oIndex a))
-> Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Cone
     cIndex
     mIndex
     oIndex
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim,
 HasProducts c m o cLim mLim oLim oIndex,
 HasEqualizers cLim mLim oLim, FiniteCategory cIndex mIndex oIndex,
 Morphism mIndex oIndex, Eq oIndex, Eq mIndex, Eq cIndex) =>
(m -> mLim)
-> Diagram cIndex mIndex oIndex c m o
-> Cone cIndex mIndex oIndex cLim mLim oLim
limitFromProductsAndEqualizers Function a -> Function (Limit oIndex a)
forall {t} {oIndex}.
Eq t =>
Function t -> Function (Limit oIndex t)
_projectMorphism
        
        projectBase :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Diagram
     (FinSet a)
     (Function a)
     (Set a)
     (FinSet (Limit oIndex a))
     (Function (Limit oIndex a))
     (Set (Limit oIndex a))
projectBase Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag = Diagram{src :: FinSet a
src = FinSet a
forall a. FinSet a
FinSet, tgt :: FinSet (Limit oIndex a)
tgt = FinSet (Limit oIndex a)
forall a. FinSet a
FinSet, omap :: Map (Set a) (Set (Limit oIndex a))
omap = (Set a -> Set (Limit oIndex a))
-> Set (Set a) -> Map (Set a) (Set (Limit oIndex a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction ((a -> Limit oIndex a) -> Set a -> Set (Limit oIndex a)
forall a b. (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Limit oIndex a
forall oIndex t. t -> Limit oIndex t
Projection) (Map oIndex (Set a) -> Set (Set a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Map oIndex (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag)), mmap :: Map (Function a) (Function (Limit oIndex a))
mmap = (Function a -> Function (Limit oIndex a))
-> Set (Function a) -> Map (Function a) (Function (Limit oIndex a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Function a -> Function (Limit oIndex a)
forall {t} {oIndex}.
Eq t =>
Function t -> Function (Limit oIndex t)
_projectMorphism (Map mIndex (Function a) -> Set (Function a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Map mIndex (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag))}
        
    
    instance (Eq a, Eq oIndex) => HasCoproducts (FinSet a) (Function a) (Set a) (FinSet (Colimit oIndex a)) (Function (Colimit oIndex a)) (Set (Colimit oIndex a)) oIndex where
        coproduct :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
coproduct Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag = Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
result
            where
                indexingCat :: DiscreteCategory oIndex
indexingCat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag
                coprod :: Set (Colimit oIndex a)
coprod = [Set (Colimit oIndex a)] -> Set (Colimit oIndex a)
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions (Set (Set (Colimit oIndex a)) -> [Set (Colimit oIndex a)]
forall a. Eq a => Set a -> [a]
setToList [oIndex -> a -> Colimit oIndex a
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i (a -> Colimit oIndex a) -> Set a -> Set (Colimit oIndex a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> oIndex -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat])
                constDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
constDiag = DiscreteCategory oIndex
-> FinSet (Colimit oIndex a)
-> Set (Colimit oIndex a)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram DiscreteCategory oIndex
indexingCat FinSet (Colimit oIndex a)
forall a. FinSet a
FinSet Set (Colimit oIndex a)
coprod
                transformObject :: m t -> m (Colimit i t)
transformObject m t
x = [t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
e | t
e <- m t
x]
                transformFunction :: Function t -> Function (Colimit i t)
transformFunction Function{function :: forall a. Function a -> Map a a
function = Map t t
m, codomain :: forall a. Function a -> Set a
codomain = Set t
cod} = Function{function :: Map (Colimit i t) (Colimit i t)
function = Set (Colimit i t, Colimit i t) -> Map (Colimit i t) (Colimit i t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
k, t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
v) | (t
k,t
v) <- Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
m], codomain :: Set (Colimit i t)
codomain = Set t -> Set (Colimit i t)
forall {m :: * -> *} {t} {i}. Monad m => m t -> m (Colimit i t)
transformObject Set t
cod}
                newDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Colimit i a))
  (Set (Colimit i a))
newDiag = Diagram{src :: DiscreteCategory oIndex
src = DiscreteCategory oIndex
indexingCat, tgt :: FinSet a
tgt = FinSet a
forall a. FinSet a
FinSet, omap :: Map oIndex (Set (Colimit i a))
omap = Set a -> Set (Colimit i a)
forall {m :: * -> *} {t} {i}. Monad m => m t -> m (Colimit i t)
transformObject (Set a -> Set (Colimit i a))
-> Map oIndex (Set a) -> Map oIndex (Set (Colimit i a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Map oIndex (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag), mmap :: Map (DiscreteMorphism oIndex) (Function (Colimit i a))
mmap = Function a -> Function (Colimit i a)
forall {t} {i}. Eq t => Function t -> Function (Colimit i t)
transformFunction (Function a -> Function (Colimit i a))
-> Map (DiscreteMorphism oIndex) (Function a)
-> Map (DiscreteMorphism oIndex) (Function (Colimit i a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
-> Map (DiscreteMorphism oIndex) (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function a)
  (Set a)
discreteDiag)}
                mapping :: oIndex -> Map (Colimit i a) (Colimit oIndex a)
mapping oIndex
i = (Colimit i a -> Colimit oIndex a)
-> Set (Colimit i a) -> Map (Colimit i a) (Colimit oIndex a)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\(Coprojection a
x) -> oIndex -> a -> Colimit oIndex a
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i a
x) (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet Any)
  (Function (Colimit Any a))
  (Set (Colimit i a))
forall {a} {i} {i}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Colimit i a))
  (Set (Colimit i a))
newDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet Any)
  (Function (Colimit Any a))
  (Set (Colimit i a))
-> oIndex -> Set (Colimit i a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i)
                result :: Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
result = Set (Colimit oIndex a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone Set (Colimit oIndex a)
coprod (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
-> Map oIndex (Function (Colimit oIndex a))
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
forall {a} {i} {i}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet a)
  (Function (Colimit i a))
  (Set (Colimit i a))
newDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinSet (Colimit oIndex a))
  (Function (Colimit oIndex a))
  (Set (Colimit oIndex a))
constDiag (Set (oIndex, Function (Colimit oIndex a))
-> Map oIndex (Function (Colimit oIndex a))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
i,Function {function :: Map (Colimit oIndex a) (Colimit oIndex a)
function=oIndex -> Map (Colimit oIndex a) (Colimit oIndex a)
forall {i}. oIndex -> Map (Colimit i a) (Colimit oIndex a)
mapping oIndex
i, codomain :: Set (Colimit oIndex a)
codomain = Set (Colimit oIndex a)
coprod}) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat]))
                
    instance (Eq a) => HasCoequalizers (FinSet a) (Function a) (Set a) where
        coequalize :: Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Cocone
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
coequalize Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag = Cocone
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
result
            where
                glue :: a -> (Set a, Map a a) -> (Set a, Map a a)
glue a
x (Set a
s,Map a a
mapping)
                    | (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelG) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
x = (Set a
s,Map a a
mapping)
                    | Bool
otherwise = (a -> Set a -> Set a
forall a. Eq a => a -> Set a -> Set a
Set.delete ((Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
x) Set a
s, (a -> a) -> a -> Map a a -> Map a a
forall k a. Eq k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (a -> a -> a
forall a b. a -> b -> a
const (a -> a -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$ (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelG) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
x) ((Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| a
x) Map a a
mapping)
                (Set a
coequalizer,Map a a
mapping) = (a -> (Set a, Map a a) -> (Set a, Map a a))
-> (Set a, Map a a) -> Set a -> (Set a, Map a a)
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr a -> (Set a, Map a a) -> (Set a, Map a a)
glue ((Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelOb -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB),(a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelOb -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB)) (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelOb -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA) 
                constDiag :: Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
constDiag = Parallel
-> FinSet a
-> Set a
-> Diagram
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram Parallel
Parallel FinSet a
forall a. FinSet a
FinSet Set a
coequalizer
                result :: Cocone
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
result = Set a
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Cocone
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone Set a
coequalizer (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Diagram
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> Map ParallelOb (Function a)
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
constDiag (AssociationList ParallelOb (Function a)
-> Map ParallelOb (Function a)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA,Function {function :: Map a a
function=Map a a
mapping, codomain :: Set a
codomain = Set a
coequalizer} Function a -> Function a -> Function a
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (FinSet a) (Function a) (Set a)
-> ParallelAr -> Function a
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
->£ ParallelAr
ParallelF)), (ParallelOb
ParallelB, Function {function :: Map a a
function=Map a a
mapping, codomain :: Set a
codomain = Set a
coequalizer}) ]))
                
    
    instance (Eq a, Eq mIndex, Eq oIndex) => CocompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Colimit oIndex a)) (Function (Colimit oIndex a)) (Set (Colimit oIndex a)) cIndex mIndex oIndex where
        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
colimit = (Function a -> Function (Colimit oIndex a))
-> Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,
 HasCoequalizers cLim mLim oLim,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq oIndex, Eq mIndex, Eq cIndex) =>
(m -> mLim)
-> Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimitFromCoproductsAndCoequalizers Function a -> Function (Colimit oIndex a)
forall {t} {i}. Eq t => Function t -> Function (Colimit i t)
transformMorphismIntoColimMorphism
            where   
                transformMorphismIntoColimMorphism :: Function t -> Function (Colimit i t)
transformMorphismIntoColimMorphism Function t
m = Function{function :: Map (Colimit i t) (Colimit i t)
function = Set (Colimit i t, Colimit i t) -> Map (Colimit i t) (Colimit i t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
k, t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
v) | (t
k,t
v) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet(Map t t -> Set (t, t))
-> (Function t -> Map t t) -> Function t -> Set (t, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function t -> Map t t
forall a. Function a -> Map a a
function) Function t
m], codomain :: Set (Colimit i t)
codomain = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> Set t -> Set (Colimit i t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function t -> Set t
forall a. Function a -> Set a
codomain Function t
m}
                
        coprojectBase :: Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Diagram
     (FinSet a)
     (Function a)
     (Set a)
     (FinSet (Colimit oIndex a))
     (Function (Colimit oIndex a))
     (Set (Colimit oIndex a))
coprojectBase Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag = Diagram{src :: FinSet a
src = FinSet a
forall a. FinSet a
FinSet, tgt :: FinSet (Colimit oIndex a)
tgt = FinSet (Colimit oIndex a)
forall a. FinSet a
FinSet, omap :: Map (Set a) (Set (Colimit oIndex a))
omap = (Set a -> Set (Colimit oIndex a))
-> Set (Set a) -> Map (Set a) (Set (Colimit oIndex a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction ((a -> Colimit oIndex a) -> Set a -> Set (Colimit oIndex a)
forall a b. (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Colimit oIndex a
forall i t. t -> Colimit i t
Coprojection) (Map oIndex (Set a) -> Set (Set a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Map oIndex (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag)), mmap :: Map (Function a) (Function (Colimit oIndex a))
mmap = (Function a -> Function (Colimit oIndex a))
-> Set (Function a)
-> Map (Function a) (Function (Colimit oIndex a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Function a -> Function (Colimit oIndex a)
forall {t} {i}. Eq t => Function t -> Function (Colimit i t)
transformMorphismIntoColimMorphism (Map mIndex (Function a) -> Set (Function a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
-> Map mIndex (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram cIndex mIndex oIndex (FinSet a) (Function a) (Set a)
diag))}
            where
                transformMorphismIntoColimMorphism :: Function t -> Function (Colimit i t)
transformMorphismIntoColimMorphism Function t
m = Function{function :: Map (Colimit i t) (Colimit i t)
function = Set (Colimit i t, Colimit i t) -> Map (Colimit i t) (Colimit i t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
k, t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
v) | (t
k,t
v) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet(Map t t -> Set (t, t))
-> (Function t -> Map t t) -> Function t -> Set (t, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Function t -> Map t t
forall a. Function a -> Map a a
function) Function t
m], codomain :: Set (Colimit i t)
codomain = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> Set t -> Set (Colimit i t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function t -> Set t
forall a. Function a -> Set a
codomain Function t
m}
                
    instance (Eq a) => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))  where
        internalHom :: CompleteCategory
  (FinSet a)
  (Function a)
  (Set a)
  (FinSet (TwoProduct a))
  (Function (TwoProduct a))
  (Set (TwoProduct a))
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr =>
TwoBase (FinSet a) (Function a) (Set a)
-> Tripod
     (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))
internalHom TwoBase (FinSet a) (Function a) (Set a)
twoBase = Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Cartesian a))
  (Function (Cartesian a))
  (Set (Cartesian a))
-> Function (Cartesian a)
-> Tripod
     (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))
forall c m o.
Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> m -> Tripod c m o
unsafeTripod Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Cartesian a))
  (Function (Cartesian a))
  (Set (Cartesian a))
twoLimit Function (Cartesian a)
evalMap_
            where
                powerObject :: Set (Exponential a)
powerObject = [Map a a -> Exponential a
forall t. Map t t -> Exponential t
ExponentialElement (Function a -> Map a a
forall a. Function a -> Map a a
function Function a
m) | Function a
m <- FinSet a -> Set a -> Set a -> Set (Function a)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar FinSet a
forall a. FinSet a
FinSet (TwoBase (FinSet a) (Function a) (Set a)
twoBase TwoBase (FinSet a) (Function a) (Set a) -> DiscreteTwoAr -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A) (TwoBase (FinSet a) (Function a) (Set a)
twoBase TwoBase (FinSet a) (Function a) (Set a) -> DiscreteTwoAr -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B)]
                newInternalDomain :: Set (Exponential a)
newInternalDomain = a -> Exponential a
forall t. t -> Exponential t
Exprojection (a -> Exponential a) -> Set a -> Set (Exponential a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TwoBase (FinSet a) (Function a) (Set a)
twoBase TwoBase (FinSet a) (Function a) (Set a) -> DiscreteTwoAr -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A
                baseTwoCone :: Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Exponential a))
  (Function (Exponential a))
  (Set (Exponential a))
baseTwoCone = Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Exponential a))
  (Function (Exponential a))
  (Set (Exponential a))
-> Diagram
     DiscreteTwo
     DiscreteTwoAr
     DiscreteTwoAr
     (FinSet (Exponential a))
     (Function (Exponential a))
     (Set (Exponential a))
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: DiscreteTwo
src = DiscreteTwo
DiscreteTwo, tgt :: FinSet (Exponential a)
tgt = FinSet (Exponential a)
forall a. FinSet a
FinSet, omap :: Map DiscreteTwoAr (Set (Exponential a))
omap = AssociationList DiscreteTwoAr (Set (Exponential a))
-> Map DiscreteTwoAr (Set (Exponential a))
forall k v. AssociationList k v -> Map k v
weakMap [(DiscreteTwoAr
A,Set (Exponential a)
powerObject),(DiscreteTwoAr
B,Set (Exponential a)
newInternalDomain)], mmap :: Map DiscreteTwoAr (Function (Exponential a))
mmap = AssociationList DiscreteTwoAr (Function (Exponential a))
-> Map DiscreteTwoAr (Function (Exponential a))
forall k v. AssociationList k v -> Map k v
weakMap []}
                twoLimit :: Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Cartesian a))
  (Function (Cartesian a))
  (Set (Cartesian a))
twoLimit = Diagram
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Exponential a))
  (Function (Exponential a))
  (Set (Exponential a))
-> Cone
     DiscreteTwo
     DiscreteTwoAr
     DiscreteTwoAr
     (FinSet (Cartesian a))
     (Function (Cartesian a))
     (Set (Cartesian a))
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
  (FinSet (Exponential a))
  (Function (Exponential a))
  (Set (Exponential a))
baseTwoCone
                eval :: Map DiscreteTwoAr (Exponential t) -> Limit oIndex (Exponential t)
eval Map DiscreteTwoAr (Exponential t)
tuple = (Exponential t -> Limit oIndex (Exponential t)
forall oIndex t. t -> Limit oIndex t
Projection (t -> Exponential t
forall t. t -> Exponential t
Exprojection (t -> Exponential t) -> t -> Exponential t
forall a b. (a -> b) -> a -> b
$ Map t t
m Map t t -> t -> t
forall k v. Eq k => Map k v -> k -> v
|!| t
x))
                    where
                        (ExponentialElement Map t t
m) = Map DiscreteTwoAr (Exponential t)
tuple Map DiscreteTwoAr (Exponential t) -> DiscreteTwoAr -> Exponential t
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
A
                        (Exprojection t
x)  = Map DiscreteTwoAr (Exponential t)
tuple Map DiscreteTwoAr (Exponential t) -> DiscreteTwoAr -> Exponential t
forall k v. Eq k => Map k v -> k -> v
|!| DiscreteTwoAr
B
                finalInternalCodomain :: Set (Limit oIndex (Exponential a))
finalInternalCodomain = Exponential a -> Limit oIndex (Exponential a)
forall oIndex t. t -> Limit oIndex t
Projection (Exponential a -> Limit oIndex (Exponential a))
-> Set (Exponential a) -> Set (Limit oIndex (Exponential a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Exponential a
forall t. t -> Exponential t
Exprojection (a -> Exponential a) -> Set a -> Set (Exponential a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TwoBase (FinSet a) (Function a) (Set a)
twoBase TwoBase (FinSet a) (Function a) (Set a) -> DiscreteTwoAr -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A)
                evalMap_ :: Function (Cartesian a)
evalMap_ = Function{function :: Map (Cartesian a) (Cartesian a)
function = Set (Cartesian a, Cartesian a) -> Map (Cartesian a) (Cartesian a)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Map DiscreteTwoAr (Exponential a) -> Cartesian a
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement Map DiscreteTwoAr (Exponential a)
tuple, Map DiscreteTwoAr (Exponential a) -> Cartesian a
forall {t} {oIndex}.
Eq t =>
Map DiscreteTwoAr (Exponential t) -> Limit oIndex (Exponential t)
eval Map DiscreteTwoAr (Exponential a)
tuple) | (ProductElement Map DiscreteTwoAr (Exponential a)
tuple) <- Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Cartesian a))
  (Function (Cartesian a))
  (Set (Cartesian a))
-> Set (Cartesian a)
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  DiscreteTwo
  DiscreteTwoAr
  DiscreteTwoAr
  (FinSet (Cartesian a))
  (Function (Cartesian a))
  (Set (Cartesian a))
twoLimit], codomain :: Set (Cartesian a)
codomain = Set (Cartesian a)
forall {oIndex}. Set (Limit oIndex (Exponential a))
finalInternalCodomain}