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

{-| Module  : FiniteCategories
Description : The 'DiscreteTwo' category contains two objects and their identities.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The 'DiscreteTwo' category contains two objects and their identities.

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

module Math.FiniteCategories.DiscreteTwo
(
    DiscreteTwoOb(..),
    DiscreteTwoAr(..),
    DiscreteTwo(..),
    twoDiagram,
    insertionDiscreteTwoInDiscreteCategory,
)
where
    import          Math.FiniteCategory
    import          Math.Categories.FunctorCategory
    import          Math.FiniteCategories.DiscreteCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    import          Data.WeakMap.Safe
    import          Data.Simplifiable
    
    import          GHC.Generics
    
    -- | 'DiscreteTwoOb' is a datatype used as the object type and the morphism type.
    --
    -- It has two constructors 'A' and 'B'.
    data DiscreteTwoOb = A | B  deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    -- | There are two identities corresponding to 'A' and 'B'.
    type DiscreteTwoAr = DiscreteTwoOb
    
    instance Morphism DiscreteTwoOb DiscreteTwoOb where
        source A = A
        source B = B
        target A = A
        target B = B
        (@) A A = A
        (@) B B = B
        (@) _ _ = error "Incompatible composition of DiscreteTwo morphisms."
    
    -- | 'DiscreteTwo' is a datatype used as category type.
    data DiscreteTwo = DiscreteTwo deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance Category DiscreteTwo DiscreteTwoOb DiscreteTwoOb where
        identity DiscreteTwo A = A
        identity DiscreteTwo B = B
        ar DiscreteTwo A A = set [A]
        ar DiscreteTwo A B = set []
        ar DiscreteTwo B A = set []
        ar DiscreteTwo B B = set [B]
    
    instance FiniteCategory DiscreteTwo DiscreteTwoOb DiscreteTwoOb where
        ob DiscreteTwo = set [A,B]
    
    -- | Constructs a diagram from 'DiscreteTwo' to another category.
    twoDiagram :: (Category c m o, Morphism m o) => c -> o -> o -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
    twoDiagram c a b = Diagram{src = DiscreteTwo, tgt = c, omap = weakMap [(A,a),(B,b)], mmap = weakMap [(A,identity c a),(B, identity c b)]}
    
    -- | Return an insertion functor from 'DiscreteTwo' to a 'DiscreteCategory' given a 'DiscreteCategory' and the image of 'A' and 'B'.
    insertionDiscreteTwoInDiscreteCategory :: (Eq t) => (DiscreteCategory t) -> t -> t -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb (DiscreteCategory t) (DiscreteMorphism t) t
    insertionDiscreteTwoInDiscreteCategory dc imA imB = completeDiagram $ Diagram{src = DiscreteTwo, tgt = dc, omap = weakMap [(A,imA),(B,imB)], mmap = weakMap []}