{-# LANGUAGE GADTs, EmptyDataDecls #-} module Data.Semigroupoid.Coproduct ( L, R, Coproduct(..), distributeDualCoproduct, factorDualCoproduct) where import Data.Semigroupoid import Data.Semigroupoid.Dual import Data.Groupoid data L a data R a data Coproduct j k a b where L :: j a b -> Coproduct j k (L a) (L b) R :: k a b -> Coproduct j k (R a) (R b) instance (Semigroupoid j, Semigroupoid k) => Semigroupoid (Coproduct j k) where L f `o` L g = L (f `o` g) R f `o` R g = R (f `o` g) _ `o` _ = error "GADT fail" instance (Groupoid j, Groupoid k) => Groupoid (Coproduct j k) where inv (L f) = L (inv f) inv (R f) = R (inv f) distributeDualCoproduct :: Dual (Coproduct j k) a b -> Coproduct (Dual j) (Dual k) a b distributeDualCoproduct (Dual (L l)) = L (Dual l) distributeDualCoproduct (Dual (R r)) = R (Dual r) factorDualCoproduct :: Coproduct (Dual j) (Dual k) a b -> Dual (Coproduct j k) a b factorDualCoproduct (L (Dual l)) = Dual (L l) factorDualCoproduct (R (Dual r)) = Dual (R r)