{-# LANGUAGE MonadComprehensions, MultiParamTypeClasses  #-}
{-| Module  : FiniteCategories
Description : Kan extensions for arbitrary functors.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Kan extensions for arbitrary functors. See 'Math.Functors.SetValued' for Kan extensions for set-valued functors.
-}

module Math.Functors.KanExtension 
(
    leftKan,
    rightKan,
)
where
    import              Data.WeakSet        (Set)
    import qualified    Data.WeakSet    as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap        (Map)
    import qualified    Data.WeakMap    as  Map
    import              Data.WeakMap.Safe

    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.CommaCategory
    
    
    -- | KanObject is either a functor X : A -> C or a functor to be precomposed called RL : B -> C (R or L).

    data KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 = X (Diagram c1 m1 o1 c3 m3 o3) | RL (Diagram c2 m2 o2 c3 m3 o3) deriving (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
[KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
[KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
    
    -- | RightKanMorphism is a natural transformation Delta between functors to be precomposed or a natural transformation Mu to X.

    data RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 = Delta (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c2 m2 o2) | Mu (NaturalTransformation c1 m1 o1 c3 m3 o3) deriving (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
[RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
[RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
              Morphism (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        @? :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
(@?) (Delta NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 Diagram c1 m1 o1 c2 m2 o2
diag1) (Delta NaturalTransformation c2 m2 o2 c3 m3 o3
nat2 Diagram c1 m1 o1 c2 m2 o2
diag2)
            | Diagram c1 m1 o1 c2 m2 o2
diag1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram c1 m1 o1 c2 m2 o2
diag2 = (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Delta NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
diag1) (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Maybe (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? NaturalTransformation c2 m2 o2 c3 m3 o3
nat2)
            | Bool
otherwise = Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Maybe a
Nothing
        (@?) (Mu NaturalTransformation c1 m1 o1 c3 m3 o3
nat2) (Delta NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 Diagram c1 m1 o1 c2 m2 o2
diag) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Mu (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c1 m1 o1 c3 m3 o3
nat2 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? (NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2,
 Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<=@<- Diagram c1 m1 o1 c2 m2 o2
diag))
        (@?) (Mu NaturalTransformation c1 m1 o1 c3 m3 o3
nat1) (Mu NaturalTransformation c1 m1 o1 c3 m3 o3
nat2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Mu (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c1 m1 o1 c3 m3 o3
nat1 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? NaturalTransformation c1 m1 o1 c3 m3 o3
nat2)
        (@?) RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
_ RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
_ = Maybe (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Maybe a
Nothing
    
        source :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
source (Delta NaturalTransformation c2 m2 o2 c3 m3 o3
nat Diagram c1 m1 o1 c2 m2 o2
_) = Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
source NaturalTransformation c2 m2 o2 c3 m3 o3
nat)
        source (Mu NaturalTransformation c1 m1 o1 c3 m3 o3
nat) = Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X (NaturalTransformation c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c3 m3 o3
nat)
        
        target :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
target (Delta NaturalTransformation c2 m2 o2 c3 m3 o3
nat Diagram c1 m1 o1 c2 m2 o2
_) = Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
target NaturalTransformation c2 m2 o2 c3 m3 o3
nat)
        target (Mu NaturalTransformation c1 m1 o1 c3 m3 o3
nat) = Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X (NaturalTransformation c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c3 m3 o3
nat)
        
    -- | RightKanCategory is the category in which we want to take a comma category to find the terminal object.

    data RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = RightKanCategory (Diagram c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c3 m3 o3) deriving (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
[RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
[RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
            identity :: Morphism
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
identity (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
_ Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
diag) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Mu (FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag)) Diagram c1 m1 o1 c3 m3 o3
diag)
            identity (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
diag) = NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Delta (FunctorCategory c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
diag) (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag)) Diagram c2 m2 o2 c3 m3 o3
diag) Diagram c1 m1 o1 c2 m2 o2
f
            
            ar :: Morphism
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
ar (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
_ Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
diag1) (X Diagram c1 m1 o1 c3 m3 o3
diag2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Mu (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Set (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag1) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag1)) Diagram c1 m1 o1 c3 m3 o3
diag1 Diagram c1 m1 o1 c3 m3 o3
diag2
            ar (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
diag1) (RL Diagram c2 m2 o2 c3 m3 o3
diag2) = (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Delta NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
f) (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Set (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
diag1) (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag1)) Diagram c2 m2 o2 c3 m3 o3
diag1 Diagram c2 m2 o2 c3 m3 o3
diag2
            ar (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
diag1) (X Diagram c1 m1 o1 c3 m3 o3
diag2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Mu (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Set (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag2) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag2)) (Diagram c2 m2 o2 c3 m3 o3
diag1 Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
f) Diagram c1 m1 o1 c3 m3 o3
diag2
            ar (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
_ Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
_) = [RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3]
-> Set (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. [a] -> Set a
set []
            
    instance (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,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        
            ob :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
ob (RightKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x) = KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. a -> Set a -> Set a
Set.insert (Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X Diagram c1 m1 o1 c3 m3 o3
x) (Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (Diagram c2 m2 o2 c3 m3 o3)
forall c m o. FiniteCategory c m o => c -> Set o
ob (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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
f) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
x)))
    
    
    -- | Right Kan extension for two arbitrary functors.

    
    -- rightKan f x is the right Kan extension of x along f.

    rightKan ::  (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,
                  FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
                  Diagram c1 m1 o1 c2 m2 o2 -> Diagram  c1 m1 o1 c3 m3 o3 -> Maybe (Diagram c2 m2 o2 c3 m3 o3, NaturalTransformation c1 m1 o1 c3 m3 o3)
    rightKan :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(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,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
rightKan Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x = if Set
  (CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
-> Bool
forall a. Set a -> Bool
Set.null Set
  (CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
terminals then Maybe
  (Diagram c2 m2 o2 c3 m3 o3,
   NaturalTransformation c1 m1 o1 c3 m3 o3)
forall a. Maybe a
Nothing else (Diagram c2 m2 o2 c3 m3 o3,
 NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
forall a. a -> Maybe a
Just (Diagram c2 m2 o2 c3 m3 o3
terminalFunctor, NaturalTransformation c1 m1 o1 c3 m3 o3
terminalNat)
        where
            kanCat :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
RightKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x
            functCat :: FunctorCategory c2 m1 o1 c3 m2 o2
functCat = c2 -> c3 -> FunctorCategory c2 m1 o1 c3 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 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
x)
            t :: Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
t = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> Map o1 o2 -> Map m1 m2 -> Diagram c1 m1 o1 c2 m2 o2
Diagram{src :: FunctorCategory c2 m1 o1 c3 m2 o2
src=FunctorCategory c2 m1 o1 c3 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat, tgt :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
tgt=RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat, omap :: Map
  (Diagram c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
omap=(Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Map
     (Diagram c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (Diagram c2 m2 o2 c3 m3 o3)
forall c m o. FiniteCategory c m o => c -> Set o
ob FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat), mmap :: Map
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
mmap = (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Map
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Delta NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
f) (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat)}
            commaCat :: CommaCategory
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  One
  One
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
commaCat = 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{leftDiagram :: Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
leftDiagram=Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall {m1} {o1} {m2} {o2} {c1} {m1} {o1}.
Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
t, rightDiagram :: Diagram
  One
  One
  One
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
rightDiagram=RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram
     One
     One
     One
     (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
     (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat (Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X Diagram c1 m1 o1 c3 m3 o3
x)}
            terminals :: Set
  (CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
terminals = CommaCategory
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  One
  One
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set
     (CommaObject
        (Diagram c2 m2 o2 c3 m3 o3)
        One
        (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects CommaCategory
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  One
  One
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall {m1} {o1} {m2} {o2}.
CommaCategory
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  One
  One
  (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
commaCat
            aTerminal :: CommaObject
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aTerminal = Set
  (CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
-> CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Set a -> a
anElement Set
  (CommaObject
     (Diagram c2 m2 o2 c3 m3 o3)
     One
     (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
terminals
            terminalFunctor :: Diagram c2 m2 o2 c3 m3 o3
terminalFunctor = CommaObject
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Diagram c2 m2 o2 c3 m3 o3
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aTerminal
            Mu NaturalTransformation c1 m1 o1 c3 m3 o3
terminalNat = CommaObject
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject
  (Diagram c2 m2 o2 c3 m3 o3)
  One
  (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aTerminal
            
            
    
    
    
    
    
    -- | LeftKanMorphism is a natural transformation Sigma between functors to be precomposed or a natural transformation Alpha from X.

    data LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 = Sigma (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c2 m2 o2) | Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3) deriving (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c2, Eq c3, Eq o2, Eq o3, Eq m2, Eq m3, Eq c1, Eq o1, Eq m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
[LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
[LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c2, Show m2, Show o2, Show c3, Show m3, Show o3, Show c1,
 Show o1, Show m1) =>
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
              Morphism (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        @? :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
(@?) (Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 Diagram c1 m1 o1 c2 m2 o2
diag1) (Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
nat2 Diagram c1 m1 o1 c2 m2 o2
diag2)
            | Diagram c1 m1 o1 c2 m2 o2
diag1 Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram c1 m1 o1 c2 m2 o2
diag2 = (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
diag1) (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Maybe (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? NaturalTransformation c2 m2 o2 c3 m3 o3
nat2)
            | Bool
otherwise = Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Maybe a
Nothing
        (@?) (Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 Diagram c1 m1 o1 c2 m2 o2
diag) (Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
nat2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NaturalTransformation c2 m2 o2 c3 m3 o3
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m1 o1 c2 m2 o2 m3 o3 c3 c1.
(Morphism m1 o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2,
 Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<=@<- Diagram c1 m1 o1 c2 m2 o2
diag) NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? NaturalTransformation c1 m1 o1 c3 m3 o3
nat2)
        (@?) (Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
nat1) (Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
nat2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c1 m1 o1 c3 m3 o3
nat1 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> Maybe (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall m o. Morphism m o => m -> m -> Maybe m
@? NaturalTransformation c1 m1 o1 c3 m3 o3
nat2)
        (@?) LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
_ LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
_ = Maybe (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Maybe a
Nothing
    
        source :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
source (Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
nat Diagram c1 m1 o1 c2 m2 o2
_) = Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
source NaturalTransformation c2 m2 o2 c3 m3 o3
nat)
        source (Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
nat) = Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X (NaturalTransformation c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c3 m3 o3
nat)
        
        target :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
target (Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
nat Diagram c1 m1 o1 c2 m2 o2
_) = Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> o
target NaturalTransformation c2 m2 o2 c3 m3 o3
nat)
        target (Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
nat) = Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X (NaturalTransformation c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c3 m3 o3
nat)
        
    -- | LeftKanCategory is the category in which we want to take a comma category to find the initial object.

    data LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = LeftKanCategory (Diagram c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c3 m3 o3) deriving (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2, Eq c3, Eq o3, Eq m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
[LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
[LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2, Show c3,
 Show o3, Show m3) =>
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
            identity :: Morphism
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
identity (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
_ Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
diag) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Alpha (FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag)) Diagram c1 m1 o1 c3 m3 o3
diag)
            identity (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
diag) = NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Sigma (FunctorCategory c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
diag) (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag)) Diagram c2 m2 o2 c3 m3 o3
diag) Diagram c1 m1 o1 c2 m2 o2
f
            
            ar :: Morphism
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
ar (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
_ Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
diag1) (X Diagram c1 m1 o1 c3 m3 o3
diag2) = NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Set (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag1) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag1)) Diagram c1 m1 o1 c3 m3 o3
diag1 Diagram c1 m1 o1 c3 m3 o3
diag2
            ar (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (RL Diagram c2 m2 o2 c3 m3 o3
diag1) (RL Diagram c2 m2 o2 c3 m3 o3
diag2) = (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
f) (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Set (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
diag1) (Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag1)) Diagram c2 m2 o2 c3 m3 o3
diag1 Diagram c2 m2 o2 c3 m3 o3
diag2
            ar (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
_) (X Diagram c1 m1 o1 c3 m3 o3
diag2) (RL Diagram c2 m2 o2 c3 m3 o3
diag1)= NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Set (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
-> Set (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (c1 -> c3 -> FunctorCategory c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
diag2) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
diag2)) Diagram c1 m1 o1 c3 m3 o3
diag2 (Diagram c2 m2 o2 c3 m3 o3
diag1 Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
forall o2 m2 c2 c3 m3 o3 c1 m1 o1.
(Eq o2, Eq m2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
f)
            ar LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
_ KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
_ KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
_ = [LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3]
-> Set (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. [a] -> Set a
set []
            
    instance (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,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        
            ob :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
ob (LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x) = KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. a -> Set a -> Set a
Set.insert (Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X Diagram c1 m1 o1 c3 m3 o3
x) (Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Set (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (Diagram c2 m2 o2 c3 m3 o3)
forall c m o. FiniteCategory c m o => c -> Set o
ob (c2 -> c3 -> FunctorCategory c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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
f) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
x)))
    
    
    -- | Left Kan extension for two arbitrary functors.

    
    -- leftKan f x is the left Kan extension of x along f.

    leftKan ::  (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,
                  FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
                  Diagram c1 m1 o1 c2 m2 o2 -> Diagram  c1 m1 o1 c3 m3 o3 -> Maybe (Diagram c2 m2 o2 c3 m3 o3, NaturalTransformation c1 m1 o1 c3 m3 o3)
    leftKan :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(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,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
leftKan Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x = if Set
  (CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
-> Bool
forall a. Set a -> Bool
Set.null Set
  (CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
initials then Maybe
  (Diagram c2 m2 o2 c3 m3 o3,
   NaturalTransformation c1 m1 o1 c3 m3 o3)
forall a. Maybe a
Nothing else (Diagram c2 m2 o2 c3 m3 o3,
 NaturalTransformation c1 m1 o1 c3 m3 o3)
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
forall a. a -> Maybe a
Just (Diagram c2 m2 o2 c3 m3 o3
initialFunctor, NaturalTransformation c1 m1 o1 c3 m3 o3
initialNat)
        where
            kanCat :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
LeftKanCategory Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c3 m3 o3
x
            functCat :: FunctorCategory c2 m1 o1 c3 m2 o2
functCat = c2 -> c3 -> FunctorCategory c2 m1 o1 c3 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 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
x)
            t :: Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
t = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> Map o1 o2 -> Map m1 m2 -> Diagram c1 m1 o1 c2 m2 o2
Diagram{src :: FunctorCategory c2 m1 o1 c3 m2 o2
src=FunctorCategory c2 m1 o1 c3 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat, tgt :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
tgt=LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat, omap :: Map
  (Diagram c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
omap=(Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (Diagram c2 m2 o2 c3 m3 o3)
-> Map
     (Diagram c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c2 m2 o2 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
RL (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (Diagram c2 m2 o2 c3 m3 o3)
forall c m o. FiniteCategory c m o => c -> Set o
ob FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat), mmap :: Map
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
mmap = (NaturalTransformation c2 m2 o2 c3 m3 o3
 -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
-> Map
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\NaturalTransformation c2 m2 o2 c3 m3 o3
x -> NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Sigma NaturalTransformation c2 m2 o2 c3 m3 o3
x Diagram c1 m1 o1 c2 m2 o2
f) (FunctorCategory c2 m2 o2 c3 m3 o3
-> Set (NaturalTransformation c2 m2 o2 c3 m3 o3)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows FunctorCategory c2 m2 o2 c3 m3 o3
forall {m1} {o1} {m2} {o2}. FunctorCategory c2 m1 o1 c3 m2 o2
functCat)}
            commaCat :: CommaCategory
  One
  One
  One
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
commaCat = 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{leftDiagram :: Diagram
  One
  One
  One
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
leftDiagram=LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram
     One
     One
     One
     (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
     (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
kanCat (Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3 -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
X Diagram c1 m1 o1 c3 m3 o3
x), rightDiagram :: Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
rightDiagram=Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall {m1} {o1} {m2} {o2} {c1} {m1} {o1}.
Diagram
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
t}
            initials :: Set
  (CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
initials = CommaCategory
  One
  One
  One
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Set
     (CommaObject
        One
        (Diagram c2 m2 o2 c3 m3 o3)
        (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
initialObjects CommaCategory
  One
  One
  One
  (FunctorCategory c2 m2 o2 c3 m3 o3)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall {m1} {o1} {m2} {o2}.
CommaCategory
  One
  One
  One
  (FunctorCategory c2 m1 o1 c3 m2 o2)
  (NaturalTransformation c2 m2 o2 c3 m3 o3)
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
  (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
commaCat
            aInitial :: CommaObject
  One
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aInitial = Set
  (CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
-> CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. Set a -> a
anElement Set
  (CommaObject
     One
     (Diagram c2 m2 o2 c3 m3 o3)
     (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3))
initials
            initialFunctor :: Diagram c2 m2 o2 c3 m3 o3
initialFunctor = CommaObject
  One
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Diagram c2 m2 o2 c3 m3 o3
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject
  One
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aInitial
            Alpha NaturalTransformation c1 m1 o1 c3 m3 o3
initialNat = CommaObject
  One
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject
  One
  (Diagram c2 m2 o2 c3 m3 o3)
  (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
aInitial