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

{-| Module  : FiniteCategories
Description : The __'Hat'__ category contains two arrows coming from the same object. It is the opposite of __'V'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'Hat'__ category contains two arrows coming from the same object.

The shape of __'Hat'__ is the following : @`B` <-`F`- `A` -`G`-> `C`@
-}

module Math.FiniteCategories.Hat
(
    HatOb(..),
    HatAr(..),
    Hat(..)
)
where
    import          Math.FiniteCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    import          Data.Simplifiable
    
    import          GHC.Generics
    
    -- | Objects of the __'Hat'__ category.
    data HatOb = HatA | HatB | HatC deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    -- | Morphisms of the __'Hat'__ category.
    data HatAr = HatIdA | HatIdB | HatIdC | HatF | HatG deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    -- | The Hat category.
    data Hat = Hat deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance Morphism HatAr HatOb where
        source HatIdA = HatA
        source HatIdB = HatB
        source HatIdC = HatC
        source _ = HatA
        target HatIdA = HatA
        target HatIdB = HatB
        target HatIdC = HatC
        target HatF = HatB
        target HatG = HatC
        (@) HatIdA HatIdA = HatIdA
        (@) HatF HatIdA = HatF
        (@) HatG HatIdA = HatG
        (@) HatIdB HatIdB = HatIdB
        (@) HatIdC HatIdC = HatIdC
        (@) HatIdB HatF = HatF
        (@) HatIdC HatG = HatG
        (@) _ _ = error "Incompatible composition of Hat morphisms."
    
    instance Category Hat HatAr HatOb where
        identity _ HatA = HatIdA
        identity _ HatB = HatIdB
        identity _ HatC = HatIdC
        ar _ HatA HatA = set [HatIdA]
        ar _ HatB HatB = set [HatIdB]
        ar _ HatC HatC = set [HatIdC]
        ar _ HatA HatB = set [HatF]
        ar _ HatA HatC = set [HatG]
        ar _ _ _ = set []
    
    instance FiniteCategory Hat HatAr HatOb where
        ob _ = set [HatA, HatB, HatC]