{-| Module  : FiniteCategories
Description : An example of a 'diagonalFunctor'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An example of 'diagonalFunctor'.


-}
module Math.Functors.DiagonalFunctor.Examples
(
    exampleDiagonalFunctor,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Categories
    import              Math.Functors.DiagonalFunctor

    
    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 
    
    -- | An example of 'diagonalFunctor'.
    exampleDiagonalFunctor :: Diagram (Ens Int) (Function Int) (Set Int) (FunctorCategory (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (NaturalTransformation (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int))
    exampleDiagonalFunctor = diagonalFunctor indexing universe
        where
            universe = ens $ set [set [1], set [3,4]]
            indexing = discreteCategory $ set [0,1]