{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PatternSynonyms #-}
module Data.InternalCategory(
  -- * Path
  Path(.., Path, EmptyPath, NonEmptyPath),
  -- ** Constructing path
  path, emptyPath, singlePath,
  composePath, (>?>),
  concatPath,

  -- ** Partial construction functions
  errPath,
  errComposePath, (>!>),

  -- ** Sum and Product of paths
  injectLeftPath, injectRightPath,
  separateSumPath,
  fstPath, sndPath,
  
  -- ** Unsafe
  unsafePath,

  -- * Internal categories
  ICategory(..),
  dom, cod,
  identity, compose,

  -- * Reexport
  IQuiver(..),
) where

import Data.InternalQuiver
import Data.Void
import GHC.Stack (HasCallStack)
import Data.Maybe (fromMaybe)
import Control.Applicative ((<|>))


-- * Path
data Path v e = UnsafePath v [e] v
    deriving (Path v e -> Path v e -> Bool
(Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool) -> Eq (Path v e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
$c== :: forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
== :: Path v e -> Path v e -> Bool
$c/= :: forall v e. (Eq e, Eq v) => Path v e -> Path v e -> Bool
/= :: Path v e -> Path v e -> Bool
Eq, Eq (Path v e)
Eq (Path v e) =>
(Path v e -> Path v e -> Ordering)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Bool)
-> (Path v e -> Path v e -> Path v e)
-> (Path v e -> Path v e -> Path v e)
-> Ord (Path v e)
Path v e -> Path v e -> Bool
Path v e -> Path v e -> Ordering
Path v e -> Path v e -> Path v e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v e. (Ord e, Ord v) => Eq (Path v e)
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Ordering
forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
$ccompare :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Ordering
compare :: Path v e -> Path v e -> Ordering
$c< :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
< :: Path v e -> Path v e -> Bool
$c<= :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
<= :: Path v e -> Path v e -> Bool
$c> :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
> :: Path v e -> Path v e -> Bool
$c>= :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Bool
>= :: Path v e -> Path v e -> Bool
$cmax :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
max :: Path v e -> Path v e -> Path v e
$cmin :: forall v e. (Ord e, Ord v) => Path v e -> Path v e -> Path v e
min :: Path v e -> Path v e -> Path v e
Ord)

instance IQuiver v (Path v e) where
  src :: Path v e -> v
src (UnsafePath v
v0 [e]
_ v
_) = v
v0
  tgt :: Path v e -> v
tgt (UnsafePath v
_ [e]
_ v
v1) = v
v1

-- Pattern synonyms

pattern Path :: v -> [e] -> v -> Path v e
pattern $mPath :: forall {r} {v} {e}.
Path v e -> (v -> [e] -> v -> r) -> ((# #) -> r) -> r
Path v0 es v1 <- UnsafePath v0 es v1

{-# COMPLETE Path #-}

pattern EmptyPath :: v -> Path v e
pattern $mEmptyPath :: forall {r} {v} {e}. Path v e -> (v -> r) -> ((# #) -> r) -> r
EmptyPath v0 <- UnsafePath v0 [] _

pattern NonEmptyPath :: e -> [e] -> Path v e
pattern $mNonEmptyPath :: forall {r} {e} {v}.
Path v e -> (e -> [e] -> r) -> ((# #) -> r) -> r
NonEmptyPath e es <- UnsafePath _ (e:es) _

{-# COMPLETE EmptyPath, NonEmptyPath #-}

-- Safe constructors

path :: (Eq v, IQuiver v e) => v -> [e] -> v -> Maybe (Path v e)
path :: forall v e.
(Eq v, IQuiver v e) =>
v -> [e] -> v -> Maybe (Path v e)
path v
v0 [e]
edges v
v1
  | Bool
valid     = Path v e -> Maybe (Path v e)
forall a. a -> Maybe a
Just (Path v e -> Maybe (Path v e)) -> Path v e -> Maybe (Path v e)
forall a b. (a -> b) -> a -> b
$ v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 [e]
edges v
v1
  | Bool
otherwise = Maybe (Path v e)
forall a. Maybe a
Nothing
  where
    valid :: Bool
valid = v -> [e] -> Bool
forall {e}. IQuiver v e => v -> [e] -> Bool
go v
v0 [e]
edges
    go :: v -> [e] -> Bool
go v
v []     = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v1
    go v
v (e
e:[e]
es) = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== e -> v
forall v e. IQuiver v e => e -> v
src e
e Bool -> Bool -> Bool
&& v -> [e] -> Bool
go (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e) [e]
es

emptyPath :: v -> Path v e
emptyPath :: forall v e. v -> Path v e
emptyPath v
v = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v [] v
v

singlePath :: IQuiver v e => e -> Path v e
singlePath :: forall v e. IQuiver v e => e -> Path v e
singlePath e
e = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath (e -> v
forall v e. IQuiver v e => e -> v
src e
e) [e
e] (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e)

composePath, (>?>) :: Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath :: forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath (UnsafePath v
v0 [e]
es v
v1) (UnsafePath v
v1' [e]
es' v
v2')
  | v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v1' = Path v e -> Maybe (Path v e)
forall a. a -> Maybe a
Just (Path v e -> Maybe (Path v e)) -> Path v e -> Maybe (Path v e)
forall a b. (a -> b) -> a -> b
$ v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 ([e]
es [e] -> [e] -> [e]
forall a. [a] -> [a] -> [a]
++ [e]
es') v
v2'
  | Bool
otherwise = Maybe (Path v e)
forall a. Maybe a
Nothing

>?> :: forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
(>?>) = Path v e -> Path v e -> Maybe (Path v e)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath

infixr 1 >?>

concatPath :: Path v (Path v e) -> Path v e
concatPath :: forall v e. Path v (Path v e) -> Path v e
concatPath (UnsafePath v
v0 [Path v e]
pathes v
v1) = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath v
v0 [e]
allEdges v
v1
  where
    allEdges :: [e]
allEdges = [Path v e]
pathes [Path v e] -> (Path v e -> [e]) -> [e]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(UnsafePath v
_ [e]
es v
_) -> [e]
es

-- Partial constructors

errPath :: HasCallStack => (Eq v, Show v, IQuiver v e) => v -> [e] -> v -> Path v e
errPath :: forall v e.
(HasCallStack, Eq v, Show v, IQuiver v e) =>
v -> [e] -> v -> Path v e
errPath v
v0 [e]
edges v
v1 = case v -> [e] -> v -> Maybe (Path v e)
forall v e.
(Eq v, IQuiver v e) =>
v -> [e] -> v -> Maybe (Path v e)
path v
v0 [e]
edges v
v1 of
  Maybe (Path v e)
Nothing -> [Char] -> Path v e
forall a. HasCallStack => [Char] -> a
error [Char]
errMsg
  Just Path v e
p -> Path v e
p
  where
    errMsg :: [Char]
errMsg = [Char]
"Unmatched endpoinds in path: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
pathTypeStr
    pathTypeStr :: [Char]
pathTypeStr = v -> [e] -> [Char]
forall {e}. IQuiver v e => v -> [e] -> [Char]
go v
v0 [e]
edges
    showExpect :: a -> a -> [Char]
showExpect a
v a
v'
      | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v'   = a -> [Char]
forall a. Show a => a -> [Char]
show a
v
      | Bool
otherwise = a -> [Char]
forall a. Show a => a -> [Char]
show a
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (!!) " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
v'
    go :: v -> [e] -> [Char]
go v
v []     = v -> v -> [Char]
forall {a}. (Eq a, Show a) => a -> a -> [Char]
showExpect v
v v
v1
    go v
v (e
e:[e]
es) = v -> v -> [Char]
forall {a}. (Eq a, Show a) => a -> a -> [Char]
showExpect v
v (e -> v
forall v e. IQuiver v e => e -> v
src e
e) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ v -> [e] -> [Char]
go (e -> v
forall v e. IQuiver v e => e -> v
tgt e
e) [e]
es

errComposePath, (>!>) :: HasCallStack => (Show v, Eq v) => Path v e -> Path v e -> Path v e
errComposePath :: forall v e.
(HasCallStack, Show v, Eq v) =>
Path v e -> Path v e -> Path v e
errComposePath Path v e
p1 Path v e
p2 = case Path v e -> Path v e -> Maybe (Path v e)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
composePath Path v e
p1 Path v e
p2 of
  Maybe (Path v e)
Nothing -> [Char] -> Path v e
forall a. HasCallStack => [Char] -> a
error [Char]
errMsg
  Just Path v e
p -> Path v e
p
  where
    showType :: e -> [Char]
showType e
p = a -> [Char]
forall a. Show a => a -> [Char]
show (e -> a
forall v e. IQuiver v e => e -> v
src e
p) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"->" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show (e -> a
forall v e. IQuiver v e => e -> v
tgt e
p)
    errMsg :: [Char]
errMsg = [Char]
"Unmatched endpoints of two paths: (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Path v e -> [Char]
forall {a} {e}. (IQuiver a e, Show a) => e -> [Char]
showType Path v e
p1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") >!> (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Path v e -> [Char]
forall {a} {e}. (IQuiver a e, Show a) => e -> [Char]
showType Path v e
p2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

>!> :: forall v e.
(HasCallStack, Show v, Eq v) =>
Path v e -> Path v e -> Path v e
(>!>) = Path v e -> Path v e -> Path v e
forall v e.
(HasCallStack, Show v, Eq v) =>
Path v e -> Path v e -> Path v e
errComposePath

infixr 1 >!>

-- ** Sum and product

injectLeftPath :: Path v e -> Path (Either v w) (Either e f)
injectLeftPath :: forall v e w f. Path v e -> Path (Either v w) (Either e f)
injectLeftPath (UnsafePath v
v0 [e]
es v
v1) = Either v w
-> [Either e f] -> Either v w -> Path (Either v w) (Either e f)
forall v e. v -> [e] -> v -> Path v e
UnsafePath (v -> Either v w
forall a b. a -> Either a b
Left v
v0) (e -> Either e f
forall a b. a -> Either a b
Left (e -> Either e f) -> [e] -> [Either e f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e]
es) (v -> Either v w
forall a b. a -> Either a b
Left v
v1)

injectRightPath :: Path w f -> Path (Either v w) (Either e f)
injectRightPath :: forall w f v e. Path w f -> Path (Either v w) (Either e f)
injectRightPath (UnsafePath w
w0 [f]
fs w
w1) = Either v w
-> [Either e f] -> Either v w -> Path (Either v w) (Either e f)
forall v e. v -> [e] -> v -> Path v e
UnsafePath (w -> Either v w
forall a b. b -> Either a b
Right w
w0) (f -> Either e f
forall a b. b -> Either a b
Right (f -> Either e f) -> [f] -> [Either e f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f]
fs) (w -> Either v w
forall a b. b -> Either a b
Right w
w1)

separateSumPath :: Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath :: forall v w e f.
Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath (UnsafePath Either v w
vw0 [Either e f]
edges Either v w
vw1) = Either (Path v e) (Path w f)
-> Maybe (Either (Path v e) (Path w f))
-> Either (Path v e) (Path w f)
forall a. a -> Maybe a -> a
fromMaybe Either (Path v e) (Path w f)
forall {a}. a
err (Maybe (Either (Path v e) (Path w f))
forall {b}. Maybe (Either (Path v e) b)
leftPath Maybe (Either (Path v e) (Path w f))
-> Maybe (Either (Path v e) (Path w f))
-> Maybe (Either (Path v e) (Path w f))
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe (Either (Path v e) (Path w f))
forall {a}. Maybe (Either a (Path w f))
rightPath)
  where
    err :: a
err = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen for a valid path"
    getLeft :: Either b b -> Maybe b
getLeft Either b b
ab  = do { Left b
a <- Either b b -> Maybe (Either b b)
forall a. a -> Maybe a
Just Either b b
ab; b -> Maybe b
forall a. a -> Maybe a
Just b
a }
    getRight :: Either a b -> Maybe b
getRight Either a b
ab = do { Right b
b <- Either a b -> Maybe (Either a b)
forall a. a -> Maybe a
Just Either a b
ab; b -> Maybe b
forall a. a -> Maybe a
Just b
b }
    leftPath :: Maybe (Either (Path v e) b)
leftPath = Path v e -> Either (Path v e) b
forall a b. a -> Either a b
Left (Path v e -> Either (Path v e) b)
-> Maybe (Path v e) -> Maybe (Either (Path v e) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath (v -> [e] -> v -> Path v e)
-> Maybe v -> Maybe ([e] -> v -> Path v e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either v w -> Maybe v
forall {b} {b}. Either b b -> Maybe b
getLeft Either v w
vw0 Maybe ([e] -> v -> Path v e) -> Maybe [e] -> Maybe (v -> Path v e)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Either e f -> Maybe e) -> [Either e f] -> Maybe [e]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Either e f -> Maybe e
forall {b} {b}. Either b b -> Maybe b
getLeft [Either e f]
edges Maybe (v -> Path v e) -> Maybe v -> Maybe (Path v e)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either v w -> Maybe v
forall {b} {b}. Either b b -> Maybe b
getLeft Either v w
vw1)
    rightPath :: Maybe (Either a (Path w f))
rightPath = Path w f -> Either a (Path w f)
forall a b. b -> Either a b
Right (Path w f -> Either a (Path w f))
-> Maybe (Path w f) -> Maybe (Either a (Path w f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (w -> [f] -> w -> Path w f
forall v e. v -> [e] -> v -> Path v e
UnsafePath (w -> [f] -> w -> Path w f)
-> Maybe w -> Maybe ([f] -> w -> Path w f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either v w -> Maybe w
forall {a} {b}. Either a b -> Maybe b
getRight Either v w
vw0 Maybe ([f] -> w -> Path w f) -> Maybe [f] -> Maybe (w -> Path w f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Either e f -> Maybe f) -> [Either e f] -> Maybe [f]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Either e f -> Maybe f
forall {a} {b}. Either a b -> Maybe b
getRight [Either e f]
edges Maybe (w -> Path w f) -> Maybe w -> Maybe (Path w f)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either v w -> Maybe w
forall {a} {b}. Either a b -> Maybe b
getRight Either v w
vw1)

fstPath :: Path (v,w) (e,f) -> Path v e
fstPath :: forall v w e f. Path (v, w) (e, f) -> Path v e
fstPath (UnsafePath (v, w)
vw0 [(e, f)]
edges (v, w)
vw1) = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath ((v, w) -> v
forall a b. (a, b) -> a
fst (v, w)
vw0) ((e, f) -> e
forall a b. (a, b) -> a
fst ((e, f) -> e) -> [(e, f)] -> [e]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(e, f)]
edges) ((v, w) -> v
forall a b. (a, b) -> a
fst (v, w)
vw1)

sndPath :: Path (v,w) (e,f) -> Path w f
sndPath :: forall v w e f. Path (v, w) (e, f) -> Path w f
sndPath (UnsafePath (v, w)
vw0 [(e, f)]
edges (v, w)
vw1) = w -> [f] -> w -> Path w f
forall v e. v -> [e] -> v -> Path v e
UnsafePath ((v, w) -> w
forall a b. (a, b) -> b
snd (v, w)
vw0) ((e, f) -> f
forall a b. (a, b) -> b
snd ((e, f) -> f) -> [(e, f)] -> [f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(e, f)]
edges) ((v, w) -> w
forall a b. (a, b) -> b
snd (v, w)
vw1)

-- ** Unsafe path construction

unsafePath :: v -> [e] -> v -> Path v e
unsafePath :: forall v e. v -> [e] -> v -> Path v e
unsafePath = v -> [e] -> v -> Path v e
forall v e. v -> [e] -> v -> Path v e
UnsafePath


-- * Internal Category

class IQuiver ob mor => ICategory ob mor | mor -> ob where
  foldPath :: Path ob mor -> mor

dom, cod :: ICategory ob mor => mor -> ob
dom :: forall ob mor. ICategory ob mor => mor -> ob
dom = mor -> ob
forall v e. IQuiver v e => e -> v
src
cod :: forall ob mor. ICategory ob mor => mor -> ob
cod = mor -> ob
forall v e. IQuiver v e => e -> v
tgt

identity :: ICategory ob mor => ob -> mor
identity :: forall ob mor. ICategory ob mor => ob -> mor
identity = Path ob mor -> mor
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path ob mor -> mor) -> (ob -> Path ob mor) -> ob -> mor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ob -> Path ob mor
forall v e. v -> Path v e
emptyPath

compose :: (Eq ob, ICategory ob mor) => mor -> mor -> Maybe mor
compose :: forall ob mor. (Eq ob, ICategory ob mor) => mor -> mor -> Maybe mor
compose mor
f mor
g = Path ob mor -> mor
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path ob mor -> mor) -> Maybe (Path ob mor) -> Maybe mor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (mor -> Path ob mor
forall v e. IQuiver v e => e -> Path v e
singlePath mor
f Path ob mor -> Path ob mor -> Maybe (Path ob mor)
forall v e. Eq v => Path v e -> Path v e -> Maybe (Path v e)
>?> mor -> Path ob mor
forall v e. IQuiver v e => e -> Path v e
singlePath mor
g)

---- Instances

-- | @Path@ is the free category
instance ICategory ob (Path ob mor) where
  foldPath :: Path ob (Path ob mor) -> Path ob mor
foldPath = Path ob (Path ob mor) -> Path ob mor
forall v e. Path v (Path v e) -> Path v e
concatPath

-- | Empty graph
instance ICategory Void Void where
  foldPath :: Path Void Void -> Void
foldPath (Path Void
v [Void]
_ Void
_) = Void -> Void
forall a. Void -> a
absurd Void
v

-- | A graph with one vertex and one loop on it
instance ICategory () () where
  foldPath :: Path () () -> ()
foldPath Path () ()
_ = ()

instance (ICategory v e, ICategory w f) => ICategory (Either v w) (Either e f) where
  foldPath :: Path (Either v w) (Either e f) -> Either e f
foldPath Path (Either v w) (Either e f)
p = case Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
forall v w e f.
Path (Either v w) (Either e f) -> Either (Path v e) (Path w f)
separateSumPath Path (Either v w) (Either e f)
p of
    Left Path v e
leftP   -> e -> Either e f
forall a b. a -> Either a b
Left (Path v e -> e
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath Path v e
leftP)
    Right Path w f
rightP -> f -> Either e f
forall a b. b -> Either a b
Right (Path w f -> f
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath Path w f
rightP)

instance (ICategory v e, ICategory w f) => ICategory (v,w) (e,f) where
  foldPath :: Path (v, w) (e, f) -> (e, f)
foldPath Path (v, w) (e, f)
p = (Path v e -> e
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path (v, w) (e, f) -> Path v e
forall v w e f. Path (v, w) (e, f) -> Path v e
fstPath Path (v, w) (e, f)
p), Path w f -> f
forall ob mor. ICategory ob mor => Path ob mor -> mor
foldPath (Path (v, w) (e, f) -> Path w f
forall v w e f. Path (v, w) (e, f) -> Path w f
sndPath Path (v, w) (e, f)
p))