{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : Category of cones and category of cocones of a diagram.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A cone is an object in the comma category (/D/|1_/F/) where /D/ is the diagonal functor and 1_/F/ is the diagram that selects the diagram of interest in the functor category.

A cocone is an object in the comma category (1_/F/|/D/).
-}

module ConeCategory.ConeCategory
(
    -- * Cone related functions and types.

    Cone,
    ConeMorphism,
    ConeCategory,
    apex,
    coneToNaturalTransformation,
    naturalTransformationToCone,
    mkConeCategory,
    conesOfApex,
    terminalObjects,
    limits,
    -- * Cocone related functions and types.

    Cocone,
    CoconeMorphism,
    CoconeCategory,
    nadir,
    coconeToNaturalTransformation,
    naturalTransformationToCocone,
    mkCoconeCategory,
    coconesOfNadir,
    initialObjects,
    colimits
)
where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import DiagonalFunctor.DiagonalFunctor
    import CommaCategory.CommaCategory
    import FunctorCategory.FunctorCategory
    import UsualCategories.One
    import Data.Maybe                                  (fromJust)
    import Utils.AssociationList

    -- --------------------------------

    -- Cone related functions and types.

    -- --------------------------------

        
    -- | A `Cone` is a `CommaObject` in the `CommaCategory` (/D/|1_/F/).

    type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | A `ConeMorphism` is a morphism between cones.

    type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | `ConeCategory` is the type of the cone category, it is a `CommaCategory` (/D/|1_/F/).

    type ConeCategory c1 m1 o1 c2 m2 o2 = CommaCategory c2 m2 o2 One One One (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

    -- | Returns the `apex` of a `Cone`.

    apex :: Cone c1 m1 o1 c2 m2 o2 -> o2
    apex :: forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc

    -- | Returns the `Cone` as a `NaturalTransformation`.

    --

    -- prop> naturalTransformationToCone . coneToNaturalTransformation = id

    -- prop> coneToNaturalTransformation . naturalTransformationToCone = id

    coneToNaturalTransformation :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
    coneToNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coneToNaturalTransformation = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow
    
    -- | Returns a `NaturalTransformation` as a `Cone`.

    --

    -- prop> naturalTransformationToCone . coneToNaturalTransformation = id

    -- prop> coneToNaturalTransformation . naturalTransformationToCone = id

    naturalTransformationToCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                                   ,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
                                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
    naturalTransformationToCone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
naturalTransformationToCone nt :: NaturalTransformation c1 m1 o1 c2 m2 o2
nt@NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
compo}
        | [o1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
s)) = [Char] -> Cone c1 m1 o1 c2 m2 o2
forall a. HasCallStack => [Char] -> a
error [Char]
"Cone of a diagram with empty index category"
        | Bool
otherwise = CommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
CommaObject{indexSrc :: o2
indexSrc=(Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
s) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! ([o1] -> o1
forall a. [a] -> a
head (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
s))),indexTgt :: One
indexTgt=One
One,arrow :: NaturalTransformation c1 m1 o1 c2 m2 o2
arrow=NaturalTransformation c1 m1 o1 c2 m2 o2
nt}

    -- | Constructs the category of cones of a diagram. Objects of the category are `CommaObject` objects with the `apex` of the cone in the `indexSrc` field and the natural transformation in the `arrow` field.

    mkConeCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                       FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
    mkConeCategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
mkConeCategory diag :: Diagram c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap=AssociationList o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m1 m2
fm} =  CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiag :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
leftDiag = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct
                                                                             , rightDiag :: Diagram
  One
  One
  One
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
rightDiag = Maybe
  (Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2))
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe
   (Diagram
      One
      One
      One
      (FunctorCategory c1 m1 o1 c2 m2 o2)
      (NaturalTransformation c1 m1 o1 c2 m2 o2)
      (Diagram c1 m1 o1 c2 m2 o2))
 -> Diagram
      One
      One
      One
      (FunctorCategory c1 m1 o1 c2 m2 o2)
      (NaturalTransformation c1 m1 o1 c2 m2 o2)
      (Diagram c1 m1 o1 c2 m2 o2))
-> Maybe
     (Diagram
        One
        One
        One
        (FunctorCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2)
        (Diagram c1 m1 o1 c2 m2 o2))
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Maybe
     (Diagram
        One
        One
        One
        (FunctorCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2)
        (Diagram c1 m1 o1 c2 m2 o2))
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag}
                                                                where
                                                                    diagonalFunct :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
mkDiagonalFunctor c1
s c2
t

    -- | Returns all cones of a given apex.

    conesOfApex :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                    FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> o2 -> [Cone c1 m1 o1 c2 m2 o2]
    conesOfApex :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> o2 -> [Cone c1 m1 o1 c2 m2 o2]
conesOfApex Diagram c1 m1 o1 c2 m2 o2
diag o2
apx
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o2 -> [o2] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o2
apx (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag)) = [Char] -> [Cone c1 m1 o1 c2 m2 o2]
forall a. HasCallStack => [Char] -> a
error [Char]
"Trying to construct cones from an apex not in the target category."
        | Bool
otherwise = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
naturalTransformationToCone (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2)
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
-> [Cone c1 m1 o1 c2 m2 o2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar FunctorCategory c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c2 m2 o2
functCat Diagram c1 m1 o1 c2 m2 o2
constDiag Diagram c1 m1 o1 c2 m2 o2
diag
        where 
            functCat :: FunctorCategory c1 m1 o1 c2 m2 o2
functCat = c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag)
            Just Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag) o2
apx
            
    -- | Returns limits of a diagram (terminal cones).

    limits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
               FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
               Diagram c1 m1 o1 c2 m2 o2 -> [Cone c1 m1 o1 c2 m2 o2]
    limits :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> [Cone c1 m1 o1 c2 m2 o2]
limits = ConeCategory c1 m1 o1 c2 m2 o2 -> [Cone c1 m1 o1 c2 m2 o2]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
terminalObjects(ConeCategory c1 m1 o1 c2 m2 o2 -> [Cone c1 m1 o1 c2 m2 o2])
-> (Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> [Cone c1 m1 o1 c2 m2 o2]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
mkConeCategory
    
    -- --------------------------------

    -- Cocone related functions and types.

    -- --------------------------------

    

    -- | A `Cocone` is a `CommaObject` in the `CommaCategory` (1_/F/|/D/).

    type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)

    -- | A `CoconeMorphism` is a morphism between cocones.

    type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | `CoconeCategory` is the type of the cocone category, it is a `CommaCategory` (1_/F/|/D/).

    type CoconeCategory c1 m1 o1 c2 m2 o2 = CommaCategory One One One c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
    
    
    -- | Returns the `nadir` of a `Cocone`.

    nadir :: Cocone c1 m1 o1 c2 m2 o2 -> o2
    nadir :: forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt

    -- | Returns the `Cocone` as a `NaturalTransformation`.

    coconeToNaturalTransformation :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
    coconeToNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coconeToNaturalTransformation = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow
    
    -- | Returns a `NaturalTransformation` as a `Cocone`.

    --

    -- prop> naturalTransformationToCocone . coconeToNaturalTransformation = id

    -- prop> coconeToNaturalTransformation . naturalTransformationToCocone = id

    naturalTransformationToCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                                     ,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
                                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
    naturalTransformationToCocone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
naturalTransformationToCocone nt :: NaturalTransformation c1 m1 o1 c2 m2 o2
nt@NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
compo}
        | [o1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
t)) = [Char] -> Cocone c1 m1 o1 c2 m2 o2
forall a. HasCallStack => [Char] -> a
error [Char]
"Diagram with empty index category"
        | Bool
otherwise = CommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
CommaObject{indexSrc :: One
indexSrc=One
One,indexTgt :: o2
indexTgt=(Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
t) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! ([o1] -> o1
forall a. [a] -> a
head (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
t))),arrow :: NaturalTransformation c1 m1 o1 c2 m2 o2
arrow=NaturalTransformation c1 m1 o1 c2 m2 o2
nt}
 
    -- | Constructs the category of cocones of a diagram. Objects of the category are `CommaObject` objects with the nadir of the cone in the `indexTgt` field and the natural transformation in the `arrow` field.

    mkCoconeCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                       FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
    mkCoconeCategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
mkCoconeCategory diag :: Diagram c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap=AssociationList o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m1 m2
fm} =  CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiag :: Diagram
  One
  One
  One
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
leftDiag = Maybe
  (Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2))
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe
   (Diagram
      One
      One
      One
      (FunctorCategory c1 m1 o1 c2 m2 o2)
      (NaturalTransformation c1 m1 o1 c2 m2 o2)
      (Diagram c1 m1 o1 c2 m2 o2))
 -> Diagram
      One
      One
      One
      (FunctorCategory c1 m1 o1 c2 m2 o2)
      (NaturalTransformation c1 m1 o1 c2 m2 o2)
      (Diagram c1 m1 o1 c2 m2 o2))
-> Maybe
     (Diagram
        One
        One
        One
        (FunctorCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2)
        (Diagram c1 m1 o1 c2 m2 o2))
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Maybe
     (Diagram
        One
        One
        One
        (FunctorCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation c1 m1 o1 c2 m2 o2)
        (Diagram c1 m1 o1 c2 m2 o2))
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag
                                                                               , rightDiag :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
rightDiag = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct}
                                                                where
                                                                    diagonalFunct :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
mkDiagonalFunctor c1
s c2
t

    -- | Returns all cocones of a given nadir.

    coconesOfNadir :: ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                        FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> o2 -> [Cocone c1 m1 o1 c2 m2 o2]
    coconesOfNadir :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> o2 -> [Cocone c1 m1 o1 c2 m2 o2]
coconesOfNadir Diagram c1 m1 o1 c2 m2 o2
diag o2
nadr
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o2 -> [o2] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o2
nadr (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag)) = [Char] -> [Cocone c1 m1 o1 c2 m2 o2]
forall a. HasCallStack => [Char] -> a
error [Char]
"Trying to construct cocones to a nadir not in the target category."
        | Bool
otherwise = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
naturalTransformationToCocone (NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Cocone c1 m1 o1 c2 m2 o2)
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
-> [Cocone c1 m1 o1 c2 m2 o2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar FunctorCategory c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c2 m2 o2
functCat Diagram c1 m1 o1 c2 m2 o2
diag Diagram c1 m1 o1 c2 m2 o2
constDiag
        where 
            functCat :: FunctorCategory c1 m1 o1 c2 m2 o2
functCat = c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag)
            Just Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
diag) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
diag) o2
nadr
            
    -- | Returns colimits of a diagram (initial cocones).

    colimits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
               FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
               Diagram c1 m1 o1 c2 m2 o2 -> [Cocone c1 m1 o1 c2 m2 o2]
    colimits :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> [Cocone c1 m1 o1 c2 m2 o2]
colimits = CoconeCategory c1 m1 o1 c2 m2 o2 -> [Cocone c1 m1 o1 c2 m2 o2]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
initialObjects(CoconeCategory c1 m1 o1 c2 m2 o2 -> [Cocone c1 m1 o1 c2 m2 o2])
-> (Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> [Cocone c1 m1 o1 c2 m2 o2]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
mkCoconeCategory