{-# 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 :: forall a. Set a -> DiscreteCategory a
discreteCategory Set a
s = Galaxy a -> Set a -> FullSubcategory (Galaxy a) (StarIdentity a) a
forall c m o. c -> Set o -> FullSubcategory c m o
FullSubcategory Galaxy a
forall a. Galaxy a
Galaxy Set a
s