{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : A discrete category is a full subcategory of __'Galaxy'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A discrete category is a full subcategory of __'Galaxy'__.
-}

module Math.FiniteCategories.DiscreteCategory 
(
    DiscreteMorphism(..),
    DiscreteCategory(..),
    discreteCategory
)
where
    import          Math.FiniteCategory
    import          Math.Categories.Galaxy
    import          Math.FiniteCategories.FullSubcategory
    
    import          Data.WeakSet                        (Set)
    import          Data.WeakSet.Safe
    
    -- | A discrete category is a full subcategory of __'Galaxy'__.
    type DiscreteCategory a = FullSubcategory (Galaxy a) (StarIdentity a) a
    
    -- | A discrete morphism.
    type DiscreteMorphism a = StarIdentity a
    
    -- | Return the 'DiscreteCategory' containing a set of objects.
    discreteCategory :: Set a -> DiscreteCategory a
    discreteCategory s = FullSubcategory Galaxy s