{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
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 Data.Simplifiable
import Math.FiniteCategory
import Math.Categories.FunctorCategory
import Math.Categories.CommaCategory
import Math.IO.PrettyPrint
import GHC.Generics
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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
Morphism m2 o2) =>
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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
Morphism m2 o2) =>
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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
Morphism m2 o2) =>
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, 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
$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
showsPrec :: Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$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
show :: KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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
showList :: [KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show, (forall x.
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int -> String -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
-> Int -> String -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int
-> Int -> String -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int
-> Int -> String -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintWithIndentations :: Int
-> Int -> String -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, KanObject 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
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c1, Simplifiable c3, Simplifiable o1,
Simplifiable o3, Simplifiable m1, Simplifiable m3, Simplifiable c2,
Simplifiable o2, Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c1, Simplifiable c3, Simplifiable o1,
Simplifiable o3, Simplifiable m1, Simplifiable m3, Simplifiable c2,
Simplifiable o2, Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
-> KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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, 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
$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
showsPrec :: Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$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
show :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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
showList :: [RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show, (forall x.
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
-> Int
-> String
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String)
-> (Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int
-> Int
-> String
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int
-> Int
-> String
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
(RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c2, Simplifiable c3, Simplifiable o2,
Simplifiable o3, Simplifiable m2, Simplifiable m3, Simplifiable c1,
Simplifiable o1, Simplifiable m1, Eq o2, Eq m2, Eq o1, Eq m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c2, Simplifiable c3, Simplifiable o2,
Simplifiable o3, Simplifiable m2, Simplifiable m3, Simplifiable c1,
Simplifiable o1, Simplifiable m1, Eq o2, Eq m2, Eq o1, Eq m1) =>
RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
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
-> 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) = 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
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> m -> m
@ NaturalTransformation c2 m2 o2 c3 m3 o3
nat2) Diagram c1 m1 o1 c2 m2 o2
diag1
(@) (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)
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation c1 m1 o1 c3 m3 o3
nat2 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> m -> 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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, 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)
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation c1 m1 o1 c3 m3 o3
nat1 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> m -> 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
_ = String -> RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a. HasCallStack => String -> a
error String
"Incompatible composition of RightKanMorphisms."
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)
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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, 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
$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
showsPrec :: Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$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
show :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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
showList :: [RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show, (forall x.
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
-> Int
-> String
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String)
-> (Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int
-> Int
-> String
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int
-> Int
-> String
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
(RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
Simplifiable o2, Simplifiable m1, Simplifiable m2, Simplifiable c3,
Simplifiable o3, Simplifiable m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
Simplifiable o2, Simplifiable m1, Simplifiable m2, Simplifiable c3,
Simplifiable o3, Simplifiable m3) =>
RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
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)))
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{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{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
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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 m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, FiniteCategory c1 m1 o1, Morphism m2 o2,
Morphism m1 o1) =>
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, 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
$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
showsPrec :: Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$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
show :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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
showList :: [LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show, (forall x.
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
-> Int
-> String
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String)
-> (Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int
-> Int
-> String
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int
-> Int
-> String
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c2, PrettyPrint c3, PrettyPrint o2, PrettyPrint o3,
PrettyPrint m2, PrettyPrint m3, PrettyPrint c1, PrettyPrint o1,
PrettyPrint m1, Eq o2, Eq o3, Eq m2, Eq m3, Eq o1, Eq m1) =>
Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, LeftKanMorphism c1 m1 o1 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
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c2, Simplifiable c3, Simplifiable o2,
Simplifiable o3, Simplifiable m2, Simplifiable m3, Simplifiable c1,
Simplifiable o1, Simplifiable m1, Eq o2, Eq m2, Eq o1, Eq m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c2, Simplifiable c3, Simplifiable o2,
Simplifiable o3, Simplifiable m2, Simplifiable m3, Simplifiable c1,
Simplifiable o1, Simplifiable m1, Eq o2, Eq m2, Eq o1, Eq m1) =>
LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
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
-> 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) = 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
nat1 NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
-> NaturalTransformation c2 m2 o2 c3 m3 o3
forall m o. Morphism m o => m -> m -> m
@ NaturalTransformation c2 m2 o2 c3 m3 o3
nat2) Diagram c1 m1 o1 c2 m2 o2
diag1
(@) (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)
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a b. (a -> b) -> a -> 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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, 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
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> m -> 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)
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a b. (a -> b) -> a -> b
$ (NaturalTransformation c1 m1 o1 c3 m3 o3
nat1 NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall m o. Morphism m o => m -> m -> 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
_ = String -> LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3
forall a. HasCallStack => String -> a
error String
"Incompatible composition of LeftKanMorphisms."
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)
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3) =>
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, 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
$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
showsPrec :: Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$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
show :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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
showList :: [LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
Show, (forall x.
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
-> Int
-> String
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String)
-> (Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int
-> Int
-> String
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int
-> Int
-> String
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c2, PrettyPrint o1, PrettyPrint o2,
PrettyPrint m1, PrettyPrint m2, PrettyPrint c3, PrettyPrint o3,
PrettyPrint m3, Eq o1, Eq o2, Eq m1, Eq m2, Eq o3, Eq m3) =>
Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
(LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
Simplifiable o2, Simplifiable m1, Simplifiable m2, Simplifiable c3,
Simplifiable o3, Simplifiable m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq o1, Eq m1, Simplifiable c1, Simplifiable c2, Simplifiable o1,
Simplifiable o2, Simplifiable m1, Simplifiable m2, Simplifiable c3,
Simplifiable o3, Simplifiable m3) =>
LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
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 c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
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)))
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{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{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