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

{-| Module  : FiniteCategories
Description : The __1__ category contains one object and its identity.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __1__ category contains one object and its identity.

You can construct it using 'NumberCategory', it is defined as a standalone category because it is often used unlike other number categories.
-}

module Math.FiniteCategories.One
(
    One(..)
)
where
    import          Math.FiniteCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    import          Data.Simplifiable
    
    import          GHC.Generics
    
    -- | 'One' is a datatype used as the object type, the morphism type and the category type of __1__.
    data One = One deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance Morphism One One where
        source One = One
        target One = One
        (@) One One = One
    
    instance Category One One One where
        identity One One = One
        ar One One One = set [One]
    
    instance FiniteCategory One One One where
        ob One = set [One]