{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} #if __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE DeriveGeneric #-} #endif #if __GLASGOW_HASKELL__ >= 706 {-# LANGUAGE PolyKinds #-} #endif #if __GLASGOW_HASKELL__ >= 708 {-# LANGUAGE Safe #-} #elif __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-} #endif #include "bifunctors-common.h" module Data.Bifunctor.Sum where import Data.Bifunctor import Data.Bifunctor.Functor import Data.Bifoldable import Data.Bitraversable #if __GLASGOW_HASKELL__ < 710 import Data.Foldable import Data.Functor import Data.Monoid hiding (Sum) import Data.Traversable #endif #if __GLASGOW_HASKELL__ >= 708 import Data.Typeable #endif #if __GLASGOW_HASKELL__ >= 702 import GHC.Generics #endif #if LIFTED_FUNCTOR_CLASSES import Data.Functor.Classes #endif 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 #if __GLASGOW_HASKELL__ >= 702 , 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 #endif #if __GLASGOW_HASKELL__ >= 708 , 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 , Typeable #endif ) 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) #if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 708 data SumMetaData data SumMetaConsL2 data SumMetaConsR2 instance Datatype SumMetaData where datatypeName _ = "Sum" moduleName _ = "Data.Bifunctor.Sum" instance Constructor SumMetaConsL2 where conName _ = "L2" instance Constructor SumMetaConsR2 where conName _ = "R2" instance Generic1 (Sum p q a) where type Rep1 (Sum p q a) = D1 SumMetaData ((:+:) (C1 SumMetaConsL2 (S1 NoSelector (Rec1 (p a)))) (C1 SumMetaConsR2 (S1 NoSelector (Rec1 (q a))))) from1 (L2 p) = M1 (L1 (M1 (M1 (Rec1 p)))) from1 (R2 q) = M1 (R1 (M1 (M1 (Rec1 q)))) to1 (M1 (L1 (M1 (M1 p)))) = L2 (unRec1 p) to1 (M1 (R1 (M1 (M1 q)))) = R2 (unRec1 q) #endif #if LIFTED_FUNCTOR_CLASSES 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 #endif 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