{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

module Data.Bifunctor.Sum where

import Data.Bifunctor
import Data.Bifunctor.Functor
import Data.Bifoldable
import Data.Bitraversable
import Data.Functor.Classes
import GHC.Generics

data Sum p q a b = L2 (p a b) | R2 (q a b)
  deriving (Sum p q a b -> Sum p q a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Eq (p a b), Eq (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
/= :: Sum p q a b -> Sum p q a b -> Bool
$c/= :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Eq (p a b), Eq (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
== :: Sum p q a b -> Sum p q a b -> Bool
$c== :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Eq (p a b), Eq (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
Eq, Sum p q a b -> Sum p q a b -> Bool
Sum p q a b -> Sum p q a b -> Ordering
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 {k} {k} {p :: k -> k -> *} {q :: k -> k -> *} {a :: k}
       {b :: k}.
(Ord (p a b), Ord (q a b)) =>
Eq (Sum p q a b)
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Ordering
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Sum p q a b
min :: Sum p q a b -> Sum p q a b -> Sum p q a b
$cmin :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Sum p q a b
max :: Sum p q a b -> Sum p q a b -> Sum p q a b
$cmax :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Sum p q a b
>= :: Sum p q a b -> Sum p q a b -> Bool
$c>= :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
> :: Sum p q a b -> Sum p q a b -> Bool
$c> :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
<= :: Sum p q a b -> Sum p q a b -> Bool
$c<= :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
< :: Sum p q a b -> Sum p q a b -> Bool
$c< :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Bool
compare :: Sum p q a b -> Sum p q a b -> Ordering
$ccompare :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Ord (p a b), Ord (q a b)) =>
Sum p q a b -> Sum p q a b -> Ordering
Ord, Int -> Sum p q a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
Int -> Sum p q a b -> ShowS
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
[Sum p q a b] -> ShowS
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
Sum p q a b -> String
showList :: [Sum p q a b] -> ShowS
$cshowList :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
[Sum p q a b] -> ShowS
show :: Sum p q a b -> String
$cshow :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
Sum p q a b -> String
showsPrec :: Int -> Sum p q a b -> ShowS
$cshowsPrec :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Show (p a b), Show (q a b)) =>
Int -> Sum p q a b -> ShowS
Show, ReadPrec [Sum p q a b]
ReadPrec (Sum p q a b)
ReadS [Sum p q a b]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadPrec [Sum p q a b]
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadPrec (Sum p q a b)
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
Int -> ReadS (Sum p q a b)
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadS [Sum p q a b]
readListPrec :: ReadPrec [Sum p q a b]
$creadListPrec :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadPrec [Sum p q a b]
readPrec :: ReadPrec (Sum p q a b)
$creadPrec :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadPrec (Sum p q a b)
readList :: ReadS [Sum p q a b]
$creadList :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
ReadS [Sum p q a b]
readsPrec :: Int -> ReadS (Sum p q a b)
$creadsPrec :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k).
(Read (p a b), Read (q a b)) =>
Int -> ReadS (Sum p q a b)
Read, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k)
       x.
Rep (Sum p q a b) x -> Sum p q a b
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k)
       x.
Sum p q a b -> Rep (Sum p q a b) x
$cto :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k)
       x.
Rep (Sum p q a b) x -> Sum p q a b
$cfrom :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (b :: k)
       x.
Sum p q a b -> Rep (Sum p q a b) x
Generic, forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (a :: k).
Rep1 (Sum p q a) a -> Sum p q a a
forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (a :: k).
Sum p q a a -> Rep1 (Sum p q a) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (a :: k).
Rep1 (Sum p q a) a -> Sum p q a a
$cfrom1 :: forall k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k) (a :: k).
Sum p q a a -> Rep1 (Sum p q a) a
Generic1)
deriving instance (Functor (f a), Functor (g a)) => Functor (Sum f g a)
deriving instance (Foldable (f a), Foldable (g a)) => Foldable (Sum f g a)
deriving instance (Traversable (f a), Traversable (g a)) => Traversable (Sum f g a)

instance (Eq2 f, Eq2 g, Eq a) => Eq1 (Sum f g a) where
  liftEq :: forall a b. (a -> b -> Bool) -> Sum f g a a -> Sum f g a b -> Bool
liftEq = forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 forall a. Eq a => a -> a -> Bool
(==)
instance (Eq2 f, Eq2 g) => Eq2 (Sum f g) where
  liftEq2 :: forall a b c d.
(a -> b -> Bool)
-> (c -> d -> Bool) -> Sum f g a c -> Sum f g b d -> Bool
liftEq2 a -> b -> Bool
f c -> d -> Bool
g (L2 f a c
x1) (L2 f b d
x2) = forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 a -> b -> Bool
f c -> d -> Bool
g f a c
x1 f b d
x2
  liftEq2 a -> b -> Bool
_ c -> d -> Bool
_ (L2 f a c
_)  (R2 g b d
_)  = Bool
False
  liftEq2 a -> b -> Bool
_ c -> d -> Bool
_ (R2 g a c
_)  (L2 f b d
_)  = Bool
False
  liftEq2 a -> b -> Bool
f c -> d -> Bool
g (R2 g a c
y1) (R2 g b d
y2) = forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 a -> b -> Bool
f c -> d -> Bool
g g a c
y1 g b d
y2

instance (Ord2 f, Ord2 g, Ord a) => Ord1 (Sum f g a) where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> Sum f g a a -> Sum f g a b -> Ordering
liftCompare = forall (f :: * -> * -> *) a b c d.
Ord2 f =>
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
liftCompare2 forall a. Ord a => a -> a -> Ordering
compare
instance (Ord2 f, Ord2 g) => Ord2 (Sum f g) where
  liftCompare2 :: forall a b c d.
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> Sum f g a c -> Sum f g b d -> Ordering
liftCompare2 a -> b -> Ordering
f c -> d -> Ordering
g (L2 f a c
x1) (L2 f b d
x2) = forall (f :: * -> * -> *) a b c d.
Ord2 f =>
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
liftCompare2 a -> b -> Ordering
f c -> d -> Ordering
g f a c
x1 f b d
x2
  liftCompare2 a -> b -> Ordering
_ c -> d -> Ordering
_ (L2 f a c
_)  (R2 g b d
_)  = Ordering
LT
  liftCompare2 a -> b -> Ordering
_ c -> d -> Ordering
_ (R2 g a c
_)  (L2 f b d
_)  = Ordering
GT
  liftCompare2 a -> b -> Ordering
f c -> d -> Ordering
g (R2 g a c
y1) (R2 g b d
y2) = forall (f :: * -> * -> *) a b c d.
Ord2 f =>
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
liftCompare2 a -> b -> Ordering
f c -> d -> Ordering
g g a c
y1 g b d
y2

instance (Read2 f, Read2 g, Read a) => Read1 (Sum f g a) where
  liftReadsPrec :: forall a.
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Sum f g a a)
liftReadsPrec = forall (f :: * -> * -> *) a b.
Read2 f =>
(Int -> ReadS a)
-> ReadS [a]
-> (Int -> ReadS b)
-> ReadS [b]
-> Int
-> ReadS (f a b)
liftReadsPrec2 forall a. Read a => Int -> ReadS a
readsPrec forall a. Read a => ReadS [a]
readList
instance (Read2 f, Read2 g) => Read2 (Sum f g) where
  liftReadsPrec2 :: forall a b.
(Int -> ReadS a)
-> ReadS [a]
-> (Int -> ReadS b)
-> ReadS [b]
-> Int
-> ReadS (Sum f g a b)
liftReadsPrec2 Int -> ReadS a
rp1 ReadS [a]
rl1 Int -> ReadS b
rp2 ReadS [b]
rl2 = forall a. (String -> ReadS a) -> Int -> ReadS a
readsData forall a b. (a -> b) -> a -> b
$
    forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith (forall (f :: * -> * -> *) a b.
Read2 f =>
(Int -> ReadS a)
-> ReadS [a]
-> (Int -> ReadS b)
-> ReadS [b]
-> Int
-> ReadS (f a b)
liftReadsPrec2 Int -> ReadS a
rp1 ReadS [a]
rl1 Int -> ReadS b
rp2 ReadS [b]
rl2) String
"L2" forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 forall a. Monoid a => a -> a -> a
`mappend`
    forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith (forall (f :: * -> * -> *) a b.
Read2 f =>
(Int -> ReadS a)
-> ReadS [a]
-> (Int -> ReadS b)
-> ReadS [b]
-> Int
-> ReadS (f a b)
liftReadsPrec2 Int -> ReadS a
rp1 ReadS [a]
rl1 Int -> ReadS b
rp2 ReadS [b]
rl2) String
"R2" forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2

instance (Show2 f, Show2 g, Show a) => Show1 (Sum f g a) where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> Sum f g a a -> ShowS
liftShowsPrec = forall (f :: * -> * -> *) a b.
Show2 f =>
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> f a b
-> ShowS
liftShowsPrec2 forall a. Show a => Int -> a -> ShowS
showsPrec forall a. Show a => [a] -> ShowS
showList
instance (Show2 f, Show2 g) => Show2 (Sum f g) where
  liftShowsPrec2 :: forall a b.
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> Sum f g a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
sp1 [a] -> ShowS
sl1 Int -> b -> ShowS
sp2 [b] -> ShowS
sl2 Int
p (L2 f a b
x) =
    forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith (forall (f :: * -> * -> *) a b.
Show2 f =>
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> f a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
sp1 [a] -> ShowS
sl1 Int -> b -> ShowS
sp2 [b] -> ShowS
sl2) String
"L2" Int
p f a b
x
  liftShowsPrec2 Int -> a -> ShowS
sp1 [a] -> ShowS
sl1 Int -> b -> ShowS
sp2 [b] -> ShowS
sl2 Int
p (R2 g a b
y) =
    forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith (forall (f :: * -> * -> *) a b.
Show2 f =>
(Int -> a -> ShowS)
-> ([a] -> ShowS)
-> (Int -> b -> ShowS)
-> ([b] -> ShowS)
-> Int
-> f a b
-> ShowS
liftShowsPrec2 Int -> a -> ShowS
sp1 [a] -> ShowS
sl1 Int -> b -> ShowS
sp2 [b] -> ShowS
sl2) String
"R2" Int
p g a b
y

instance (Bifunctor p, Bifunctor q) => Bifunctor (Sum p q) where
  bimap :: forall a b c d. (a -> b) -> (c -> d) -> Sum p q a c -> Sum p q b d
bimap a -> b
f c -> d
g (L2 p a c
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g p a c
p)
  bimap a -> b
f c -> d
g (R2 q a c
q) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g q a c
q)
  first :: forall a b c. (a -> b) -> Sum p q a c -> Sum p q b c
first a -> b
f (L2 p a c
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f p a c
p)
  first a -> b
f (R2 q a c
q) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f q a c
q)
  second :: forall b c a. (b -> c) -> Sum p q a b -> Sum p q a c
second b -> c
f (L2 p a b
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> c
f p a b
p)
  second b -> c
f (R2 q a b
q) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second b -> c
f q a b
q)

instance (Bifoldable p, Bifoldable q) => Bifoldable (Sum p q) where
  bifoldMap :: forall m a b. Monoid m => (a -> m) -> (b -> m) -> Sum p q a b -> m
bifoldMap a -> m
f b -> m
g (L2 p a b
p) = forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f b -> m
g p a b
p
  bifoldMap a -> m
f b -> m
g (R2 q a b
q) = forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f b -> m
g q a b
q

instance (Bitraversable p, Bitraversable q) => Bitraversable (Sum p q) where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> Sum p q a b -> f (Sum p q c d)
bitraverse a -> f c
f b -> f d
g (L2 p a b
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse a -> f c
f b -> f d
g p a b
p
  bitraverse a -> f c
f b -> f d
g (R2 q a b
q) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse a -> f c
f b -> f d
g q a b
q

instance BifunctorFunctor (Sum p) where
  bifmap :: forall (p :: k -> k -> *) (q :: k -> k -> *).
(p :-> q) -> Sum p p :-> Sum p q
bifmap p :-> q
_ (L2 p a b
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 p a b
p
  bifmap p :-> q
f (R2 p a b
q) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2 (p :-> q
f p a b
q)

instance BifunctorMonad (Sum p) where
  bireturn :: forall (p :: k -> k -> *). p :-> Sum p p
bireturn = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
q a b -> Sum p q a b
R2
  bijoin :: forall (p :: k -> k -> *). Sum p (Sum p p) :-> Sum p p
bijoin (L2 p a b
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 p a b
p
  bijoin (R2 Sum p p a b
q) = Sum p p a b
q
  bibind :: forall (p :: k -> k -> *) (q :: k -> k -> *).
(p :-> Sum p q) -> Sum p p :-> Sum p q
bibind p :-> Sum p q
_ (L2 p a b
p) = forall {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
p a b -> Sum p q a b
L2 p a b
p
  bibind p :-> Sum p q
f (R2 p a b
q) = p :-> Sum p q
f p a b
q