{-# 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 (DiscreteTwoOb -> DiscreteTwoOb -> Bool
(DiscreteTwoOb -> DiscreteTwoOb -> Bool)
-> (DiscreteTwoOb -> DiscreteTwoOb -> Bool) -> Eq DiscreteTwoOb
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiscreteTwoOb -> DiscreteTwoOb -> Bool
== :: DiscreteTwoOb -> DiscreteTwoOb -> Bool
$c/= :: DiscreteTwoOb -> DiscreteTwoOb -> Bool
/= :: DiscreteTwoOb -> DiscreteTwoOb -> Bool
Eq, Int -> DiscreteTwoOb -> ShowS
[DiscreteTwoOb] -> ShowS
DiscreteTwoOb -> String
(Int -> DiscreteTwoOb -> ShowS)
-> (DiscreteTwoOb -> String)
-> ([DiscreteTwoOb] -> ShowS)
-> Show DiscreteTwoOb
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiscreteTwoOb -> ShowS
showsPrec :: Int -> DiscreteTwoOb -> ShowS
$cshow :: DiscreteTwoOb -> String
show :: DiscreteTwoOb -> String
$cshowList :: [DiscreteTwoOb] -> ShowS
showList :: [DiscreteTwoOb] -> ShowS
Show, (forall x. DiscreteTwoOb -> Rep DiscreteTwoOb x)
-> (forall x. Rep DiscreteTwoOb x -> DiscreteTwoOb)
-> Generic DiscreteTwoOb
forall x. Rep DiscreteTwoOb x -> DiscreteTwoOb
forall x. DiscreteTwoOb -> Rep DiscreteTwoOb x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DiscreteTwoOb -> Rep DiscreteTwoOb x
from :: forall x. DiscreteTwoOb -> Rep DiscreteTwoOb x
$cto :: forall x. Rep DiscreteTwoOb x -> DiscreteTwoOb
to :: forall x. Rep DiscreteTwoOb x -> DiscreteTwoOb
Generic, Int -> Int -> String -> DiscreteTwoOb -> String
Int -> DiscreteTwoOb -> String
(Int -> DiscreteTwoOb -> String)
-> (Int -> Int -> String -> DiscreteTwoOb -> String)
-> (Int -> DiscreteTwoOb -> String)
-> PrettyPrint DiscreteTwoOb
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: Int -> DiscreteTwoOb -> String
pprint :: Int -> DiscreteTwoOb -> String
$cpprintWithIndentations :: Int -> Int -> String -> DiscreteTwoOb -> String
pprintWithIndentations :: Int -> Int -> String -> DiscreteTwoOb -> String
$cpprintIndent :: Int -> DiscreteTwoOb -> String
pprintIndent :: Int -> DiscreteTwoOb -> String
PrettyPrint, DiscreteTwoOb -> DiscreteTwoOb
(DiscreteTwoOb -> DiscreteTwoOb) -> Simplifiable DiscreteTwoOb
forall a. (a -> a) -> Simplifiable a
$csimplify :: DiscreteTwoOb -> DiscreteTwoOb
simplify :: DiscreteTwoOb -> DiscreteTwoOb
Simplifiable)
    
    -- | There are two identities corresponding to 'A' and 'B'.

    type DiscreteTwoAr = DiscreteTwoOb
    
    instance Morphism DiscreteTwoOb DiscreteTwoOb where
        source :: DiscreteTwoOb -> DiscreteTwoOb
source DiscreteTwoOb
A = DiscreteTwoOb
A
        source DiscreteTwoOb
B = DiscreteTwoOb
B
        target :: DiscreteTwoOb -> DiscreteTwoOb
target DiscreteTwoOb
A = DiscreteTwoOb
A
        target DiscreteTwoOb
B = DiscreteTwoOb
B
        @ :: DiscreteTwoOb -> DiscreteTwoOb -> DiscreteTwoOb
(@) DiscreteTwoOb
A DiscreteTwoOb
A = DiscreteTwoOb
A
        (@) DiscreteTwoOb
B DiscreteTwoOb
B = DiscreteTwoOb
B
        (@) DiscreteTwoOb
_ DiscreteTwoOb
_ = String -> DiscreteTwoOb
forall a. HasCallStack => String -> a
error String
"Incompatible composition of DiscreteTwo morphisms."
    
    -- | 'DiscreteTwo' is a datatype used as category type.

    data DiscreteTwo = DiscreteTwo deriving (DiscreteTwo -> DiscreteTwo -> Bool
(DiscreteTwo -> DiscreteTwo -> Bool)
-> (DiscreteTwo -> DiscreteTwo -> Bool) -> Eq DiscreteTwo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiscreteTwo -> DiscreteTwo -> Bool
== :: DiscreteTwo -> DiscreteTwo -> Bool
$c/= :: DiscreteTwo -> DiscreteTwo -> Bool
/= :: DiscreteTwo -> DiscreteTwo -> Bool
Eq, Int -> DiscreteTwo -> ShowS
[DiscreteTwo] -> ShowS
DiscreteTwo -> String
(Int -> DiscreteTwo -> ShowS)
-> (DiscreteTwo -> String)
-> ([DiscreteTwo] -> ShowS)
-> Show DiscreteTwo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiscreteTwo -> ShowS
showsPrec :: Int -> DiscreteTwo -> ShowS
$cshow :: DiscreteTwo -> String
show :: DiscreteTwo -> String
$cshowList :: [DiscreteTwo] -> ShowS
showList :: [DiscreteTwo] -> ShowS
Show, (forall x. DiscreteTwo -> Rep DiscreteTwo x)
-> (forall x. Rep DiscreteTwo x -> DiscreteTwo)
-> Generic DiscreteTwo
forall x. Rep DiscreteTwo x -> DiscreteTwo
forall x. DiscreteTwo -> Rep DiscreteTwo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DiscreteTwo -> Rep DiscreteTwo x
from :: forall x. DiscreteTwo -> Rep DiscreteTwo x
$cto :: forall x. Rep DiscreteTwo x -> DiscreteTwo
to :: forall x. Rep DiscreteTwo x -> DiscreteTwo
Generic, Int -> Int -> String -> DiscreteTwo -> String
Int -> DiscreteTwo -> String
(Int -> DiscreteTwo -> String)
-> (Int -> Int -> String -> DiscreteTwo -> String)
-> (Int -> DiscreteTwo -> String)
-> PrettyPrint DiscreteTwo
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: Int -> DiscreteTwo -> String
pprint :: Int -> DiscreteTwo -> String
$cpprintWithIndentations :: Int -> Int -> String -> DiscreteTwo -> String
pprintWithIndentations :: Int -> Int -> String -> DiscreteTwo -> String
$cpprintIndent :: Int -> DiscreteTwo -> String
pprintIndent :: Int -> DiscreteTwo -> String
PrettyPrint, DiscreteTwo -> DiscreteTwo
(DiscreteTwo -> DiscreteTwo) -> Simplifiable DiscreteTwo
forall a. (a -> a) -> Simplifiable a
$csimplify :: DiscreteTwo -> DiscreteTwo
simplify :: DiscreteTwo -> DiscreteTwo
Simplifiable)
    
    instance Category DiscreteTwo DiscreteTwoOb DiscreteTwoOb where
        identity :: Morphism DiscreteTwoOb DiscreteTwoOb =>
DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb
identity DiscreteTwo
DiscreteTwo DiscreteTwoOb
A = DiscreteTwoOb
A
        identity DiscreteTwo
DiscreteTwo DiscreteTwoOb
B = DiscreteTwoOb
B
        ar :: Morphism DiscreteTwoOb DiscreteTwoOb =>
DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb -> Set DiscreteTwoOb
ar DiscreteTwo
DiscreteTwo DiscreteTwoOb
A DiscreteTwoOb
A = [DiscreteTwoOb] -> Set DiscreteTwoOb
forall a. [a] -> Set a
set [DiscreteTwoOb
A]
        ar DiscreteTwo
DiscreteTwo DiscreteTwoOb
A DiscreteTwoOb
B = [DiscreteTwoOb] -> Set DiscreteTwoOb
forall a. [a] -> Set a
set []
        ar DiscreteTwo
DiscreteTwo DiscreteTwoOb
B DiscreteTwoOb
A = [DiscreteTwoOb] -> Set DiscreteTwoOb
forall a. [a] -> Set a
set []
        ar DiscreteTwo
DiscreteTwo DiscreteTwoOb
B DiscreteTwoOb
B = [DiscreteTwoOb] -> Set DiscreteTwoOb
forall a. [a] -> Set a
set [DiscreteTwoOb
B]
    
    instance FiniteCategory DiscreteTwo DiscreteTwoOb DiscreteTwoOb where
        ob :: DiscreteTwo -> Set DiscreteTwoOb
ob DiscreteTwo
DiscreteTwo = [DiscreteTwoOb] -> Set DiscreteTwoOb
forall a. [a] -> Set a
set [DiscreteTwoOb
A,DiscreteTwoOb
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 :: forall c m o.
(Category c m o, Morphism m o) =>
c
-> o -> o -> Diagram DiscreteTwo DiscreteTwoOb DiscreteTwoOb c m o
twoDiagram c
c o
a o
b = Diagram{src :: DiscreteTwo
src = DiscreteTwo
DiscreteTwo, tgt :: c
tgt = c
c, omap :: Map DiscreteTwoOb o
omap = AssociationList DiscreteTwoOb o -> Map DiscreteTwoOb o
forall k v. AssociationList k v -> Map k v
weakMap [(DiscreteTwoOb
A,o
a),(DiscreteTwoOb
B,o
b)], mmap :: Map DiscreteTwoOb m
mmap = AssociationList DiscreteTwoOb m -> Map DiscreteTwoOb m
forall k v. AssociationList k v -> Map k v
weakMap [(DiscreteTwoOb
A,c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
a),(DiscreteTwoOb
B, c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
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 :: forall t.
Eq t =>
DiscreteCategory t
-> t
-> t
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory t)
     (DiscreteMorphism t)
     t
insertionDiscreteTwoInDiscreteCategory DiscreteCategory t
dc t
imA t
imB = Diagram
  DiscreteTwo
  DiscreteTwoOb
  DiscreteTwoOb
  (DiscreteCategory t)
  (DiscreteMorphism t)
  t
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory t)
     (DiscreteMorphism t)
     t
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram (Diagram
   DiscreteTwo
   DiscreteTwoOb
   DiscreteTwoOb
   (DiscreteCategory t)
   (DiscreteMorphism t)
   t
 -> Diagram
      DiscreteTwo
      DiscreteTwoOb
      DiscreteTwoOb
      (DiscreteCategory t)
      (DiscreteMorphism t)
      t)
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory t)
     (DiscreteMorphism t)
     t
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory t)
     (DiscreteMorphism t)
     t
forall a b. (a -> b) -> a -> b
$ Diagram{src :: DiscreteTwo
src = DiscreteTwo
DiscreteTwo, tgt :: DiscreteCategory t
tgt = DiscreteCategory t
dc, omap :: Map DiscreteTwoOb t
omap = AssociationList DiscreteTwoOb t -> Map DiscreteTwoOb t
forall k v. AssociationList k v -> Map k v
weakMap [(DiscreteTwoOb
A,t
imA),(DiscreteTwoOb
B,t
imB)], mmap :: Map DiscreteTwoOb (DiscreteMorphism t)
mmap = AssociationList DiscreteTwoOb (DiscreteMorphism t)
-> Map DiscreteTwoOb (DiscreteMorphism t)
forall k v. AssociationList k v -> Map k v
weakMap []}