{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.Coproduct (COPRODUCT, COLLAGE(..), (:++:), pattern InjL, pattern InjR) where

import Prelude (type (~))

import Proarrow.Core (CAT, CategoryOf (..))
import Proarrow.Profunctor.Initial (InitialProfunctor)
import Proarrow.Category.Instance.Collage (COLLAGE(..), Collage(..))
import Proarrow.Category.Dagger (DaggerProfunctor (..), Dagger)

type COPRODUCT j k = COLLAGE (InitialProfunctor @j @k)

type (:++:) :: CAT j -> CAT k -> CAT (COPRODUCT j k)
type (:++:) c d = Collage :: CAT (COPRODUCT j k)

pattern InjL :: () => (a' ~ L a, b' ~ L b) => a ~> b -> ((~>) :++: (~>)) a' b'
pattern $mInjL :: forall {r} {k} {j} {a' :: COLLAGE InitialProfunctor}
       {b' :: COLLAGE InitialProfunctor}.
(:++:) (~>) (~>) a' b'
-> (forall {a :: k} {b :: k}.
    (a' ~ L a, b' ~ L b) =>
    (a ~> b) -> r)
-> ((# #) -> r)
-> r
$bInjL :: forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: k) (b :: k).
(a' ~ L a, b' ~ L b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjL f = InL f

pattern InjR :: () => (a' ~ R a, b' ~ R b) => a ~> b -> ((~>) :++: (~>)) a' b'
pattern $mInjR :: forall {r} {k} {j} {a' :: COLLAGE InitialProfunctor}
       {b' :: COLLAGE InitialProfunctor}.
(:++:) (~>) (~>) a' b'
-> (forall {a :: j} {b :: j}.
    (a' ~ R a, b' ~ R b) =>
    (a ~> b) -> r)
-> ((# #) -> r)
-> r
$bInjR :: forall {k} {j} (a' :: COLLAGE InitialProfunctor)
       (b' :: COLLAGE InitialProfunctor) (a :: j) (b :: j).
(a' ~ R a, b' ~ R b) =>
(a ~> b) -> (:++:) (~>) (~>) a' b'
InjR f = InR f

{-# COMPLETE InjL, InjR #-}

instance (Dagger j, Dagger k) => DaggerProfunctor ((~>) :++: (~>) :: CAT (COPRODUCT j k)) where
  dagger :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k).
(:++:) (~>) (~>) a b -> (:++:) (~>) (~>) b a
dagger = \case
    InL a1 ~> b1
f -> (b1 ~> a1) -> Collage (L b1) (L a1)
forall {j} {k} (a1 :: j) (b1 :: j) (p :: k +-> j).
(a1 ~> b1) -> Collage (L a1) (L b1)
InL ((a1 ~> b1) -> b1 ~> a1
forall (a :: k) (b :: k). (a ~> b) -> b ~> a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger a1 ~> b1
f)
    InR a1 ~> b1
f -> (b1 ~> a1) -> Collage (R b1) (R a1)
forall {k} {j} (a1 :: k) (b1 :: k) (p :: k +-> j).
(a1 ~> b1) -> Collage (R a1) (R b1)
InR ((a1 ~> b1) -> b1 ~> a1
forall (a :: j) (b :: j). (a ~> b) -> b ~> a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger a1 ~> b1
f)