-- | __Decorated cospans__ in @k@: a morphism @a '~>' b@ is a cospan @a -> x <- b@ together with a
-- decoration of its apex, a value of @f x@. Composition glues along a pushout and joins the two
-- decorations on the glued apex, using the 'Alternative' structure of @f@, which takes decorations
-- on two objects to one on their coproduct. As for "Proarrow.Category.Instance.Cospan", the
-- coproduct of @k@ is the tensor and every object is a Frobenius monoid, so this is a
-- 'Hypergraph' category.
--
-- With labelled boxes as the decoration, a morphism is an open hypergraph: see
-- "Proarrow.Category.Instance.OpenHypergraph".
module Proarrow.Category.Instance.DecoratedCospan where

import Data.Kind (Type)

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction)
import Proarrow.Category.Monoidal.Applicative (Alternative (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..), coactCC)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Dialogue (Dialogue (..))
import Proarrow.Category.Monoidal.Hypergraph (ExpHG, Frobenius, Hypergraph, Sized (..), applyHG, cap, cup, curryHG)
import Proarrow.Category.Monoidal.IsoMix (IsoMix (..))
import Proarrow.Category.Monoidal.StarAutonomous (StarAutonomous (..))
import Proarrow.Category.Monoidal.Strength (Costrong (..))
import Proarrow.Colimit.BinaryCoproduct
  ( HasBinaryCoproducts (..)
  , HasCoproducts
  , associatorCoprod
  , associatorCoprodInv
  , leftUnitorCoprod
  , leftUnitorCoprodInv
  , rightUnitorCoprod
  , rightUnitorCoprodInv
  , swapCoprod
  )
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), WrappedOb, dimapDefault, tgt, type (+->))
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))

type data DECCOSPAN (f :: k -> Type) = DC k

type DecCospan :: CAT (DECCOSPAN f)
data DecCospan a b where
  DecCospan :: forall {k} {f :: k -> Type} c a b. a ~> c -> b ~> c -> f c -> DecCospan (DC a :: DECCOSPAN f) (DC b)

-- | A morphism of @k@ as a cospan with the empty decoration.
arr :: forall {k} (f :: k -> Type) a b. (Alternative f) => a ~> b -> DecCospan (DC a :: DECCOSPAN f) (DC b)
arr :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr a ~> b
f = (a ~> b) -> (b ~> b) -> f b -> DecCospan (DC a) (DC b)
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan a ~> b
f ((a ~> b) -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a ~> b
f) (Unit ~> f b
() -> f b
forall (a :: k). Ob a => Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
(Alternative f, Ob a) =>
Unit ~> f a
empty ()) ((Ob a, Ob b) => DecCospan (DC a) (DC b))
-> (a ~> b) -> DecCospan (DC a) (DC b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

-- | A morphism of @k@ as a cospan the other way round, with the empty decoration.
coarr :: forall {k} (f :: k -> Type) a b. (Alternative f) => a ~> b -> DecCospan (DC b :: DECCOSPAN f) (DC a)
coarr :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC b) (DC a)
coarr a ~> b
f = (b ~> b) -> (a ~> b) -> f b -> DecCospan (DC b) (DC a)
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan ((a ~> b) -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a ~> b
f) a ~> b
f (Unit ~> f b
() -> f b
forall (a :: k). Ob a => Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
(Alternative f, Ob a) =>
Unit ~> f a
empty ()) ((Ob a, Ob b) => DecCospan (DC b) (DC a))
-> (a ~> b) -> DecCospan (DC b) (DC a)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance (HasPushouts k, Alternative f) => Profunctor (DecCospan :: CAT (DECCOSPAN (f :: k -> Type))) where
  dimap :: forall (c :: DECCOSPAN f) (a :: DECCOSPAN f) (b :: DECCOSPAN f)
       (d :: DECCOSPAN f).
(c ~> a) -> (b ~> d) -> DecCospan a b -> DecCospan c d
dimap = (c ~> a) -> (b ~> d) -> DecCospan a b -> DecCospan c d
DecCospan c a -> DecCospan b d -> DecCospan a b -> DecCospan c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) r.
((Ob a, Ob b) => r) -> DecCospan a b -> r
\\ DecCospan a ~> c
f b ~> c
g f c
_ = r
(Ob a, Ob c) => r
(Ob a, Ob b) => r
r ((Ob a, Ob c) => r) -> (a ~> c) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> c
f ((Ob b, Ob c) => r) -> (b ~> c) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> c
g
instance (HasPushouts k, Alternative f) => Promonad (DecCospan :: CAT (DECCOSPAN (f :: k -> Type))) where
  id :: forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id = (UN DC a ~> UN DC a) -> DecCospan (DC (UN DC a)) (DC (UN DC a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr UN DC a ~> UN DC a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  DecCospan a ~> c
f b ~> c
g f c
s . :: forall (b :: DECCOSPAN f) (c :: DECCOSPAN f) (a :: DECCOSPAN f).
DecCospan b c -> DecCospan a b -> DecCospan a c
. DecCospan a ~> c
h b ~> c
i f c
t = (a ~> c)
-> (a ~> c)
-> (forall (p :: k). (c ~> p) -> (c ~> p) -> DecCospan a c)
-> DecCospan a c
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushout a ~> c
b ~> c
i a ~> c
f \c ~> p
l c ~> p
r -> (a ~> p) -> (b ~> p) -> f p -> DecCospan (DC a) (DC b)
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan (c ~> p
l (c ~> p) -> (a ~> c) -> a ~> p
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> c
h) (c ~> p
r (c ~> p) -> (b ~> c) -> b ~> p
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> c
g) (((c || c) ~> p) -> (f c ** f c) ~> f p
forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Alternative f, Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
alt (c ~> p
l (c ~> p) -> (c ~> p) -> (c || c) ~> p
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| c ~> p
r) (f c
t, f c
s)) ((Ob a, Ob c) => DecCospan a c) -> (a ~> c) -> DecCospan a c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> c
b ~> c
i ((Ob a, Ob c) => DecCospan a c) -> (a ~> c) -> DecCospan a c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> c
f

-- | The category of decorated cospans in @k@: an arrow @'DC' a '~>' 'DC' b@ is a pair of arrows
-- @a '~>' x@ and @b '~>' x@ into a common object, with a decoration of @x@.
instance (HasPushouts k, Alternative f) => CategoryOf (DECCOSPAN (f :: k -> Type)) where
  type (~>) = DecCospan
  type Ob a = WrappedOb DC a

instance (HasPushouts k, HasCoproducts k, Alternative f) => MonoidalProfunctor (DecCospan :: CAT (DECCOSPAN (f :: k -> Type))) where
  one :: DecCospan Unit Unit
one = DecCospan Unit Unit
DecCospan (DC InitialObject) (DC InitialObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id
  DecCospan @c1 a ~> c
l1 b ~> c
l2 f c
s ** :: forall (x1 :: DECCOSPAN f) (x2 :: DECCOSPAN f) (y1 :: DECCOSPAN f)
       (y2 :: DECCOSPAN f).
DecCospan x1 x2
-> DecCospan y1 y2 -> DecCospan (x1 ** y1) (x2 ** y2)
** DecCospan @c2 a ~> c
r1 b ~> c
r2 f c
t =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @c1 @c2 (((a || a) ~> (c || c))
-> ((b || b) ~> (c || c))
-> f (c || c)
-> DecCospan (DC (a || a)) (DC (b || b))
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan (a ~> c
l1 (a ~> c) -> (a ~> c) -> (a || a) ~> (c || c)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ a ~> c
r1) (b ~> c
l2 (b ~> c) -> (b ~> c) -> (b || b) ~> (c || c)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ b ~> c
r2) (((c || c) ~> (c || c)) -> (f c ** f c) ~> f (c || c)
forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Alternative f, Ob a, Ob b) =>
((a || b) ~> c) -> (f a ** f b) ~> f c
alt (c || c) ~> (c || c)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (f c
s, f c
t))) ((Ob a, Ob c) => DecCospan (DC (a || a)) (DC (b || b)))
-> (a ~> c) -> DecCospan (DC (a || a)) (DC (b || b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> c
l1 ((Ob a, Ob c) => DecCospan (DC (a || a)) (DC (b || b)))
-> (a ~> c) -> DecCospan (DC (a || a)) (DC (b || b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> c
r1
instance (HasPushouts k, HasCoproducts k, Alternative f) => Monoidal (DECCOSPAN (f :: k -> Type)) where
  type DC a ** DC b = DC (a || b)
  type Unit = DC InitialObject
  withOb2 :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(DC a) @(DC b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN DC a || UN DC b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: DECCOSPAN f). Ob a => (Unit ** a) ~> a
leftUnitor = ((InitialObject || UN DC a) ~> UN DC a)
-> DecCospan (DC (InitialObject || UN DC a)) (DC (UN DC a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (InitialObject || UN DC a) ~> UN DC a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(InitialObject || a) ~> a
leftUnitorCoprod
  leftUnitorInv :: forall (a :: DECCOSPAN f). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN DC a ~> (InitialObject || UN DC a))
-> DecCospan (DC (UN DC a)) (DC (InitialObject || UN DC a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr UN DC a ~> (InitialObject || UN DC a)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (InitialObject || a)
leftUnitorCoprodInv
  rightUnitor :: forall (a :: DECCOSPAN f). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN DC a || InitialObject) ~> UN DC a)
-> DecCospan (DC (UN DC a || InitialObject)) (DC (UN DC a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (UN DC a || InitialObject) ~> UN DC a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(a || InitialObject) ~> a
rightUnitorCoprod
  rightUnitorInv :: forall (a :: DECCOSPAN f). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN DC a ~> (UN DC a || InitialObject))
-> DecCospan (DC (UN DC a)) (DC (UN DC a || InitialObject))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr UN DC a ~> (UN DC a || InitialObject)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (a || InitialObject)
rightUnitorCoprodInv
  associator :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(DC a) @(DC b) @(DC c) = (((UN DC a || UN DC b) || UN DC c)
 ~> (UN DC a || (UN DC b || UN DC c)))
-> DecCospan
     (DC ((UN DC a || UN DC b) || UN DC c))
     (DC (UN DC a || (UN DC b || UN DC c)))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
associatorCoprod @a @b @c)
  associatorInv :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(DC a) @(DC b) @(DC c) = ((UN DC a || (UN DC b || UN DC c))
 ~> ((UN DC a || UN DC b) || UN DC c))
-> DecCospan
     (DC (UN DC a || (UN DC b || UN DC c)))
     (DC ((UN DC a || UN DC b) || UN DC c))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
associatorCoprodInv @a @b @c)
instance (HasPushouts k, HasCoproducts k, Alternative f) => SymMonoidal (DECCOSPAN (f :: k -> Type)) where
  swap :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(DC a) @(DC b) = ((UN DC a || UN DC b) ~> (UN DC b || UN DC a))
-> DecCospan (DC (UN DC a || UN DC b)) (DC (UN DC b || UN DC a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @a @b)

instance (HasPushouts k, HasCoproducts k, Alternative f, Ob a) => Monoid (DC a :: DECCOSPAN (f :: k -> Type)) where
  mempty :: Unit ~> DC a
mempty = (InitialObject ~> a) -> DecCospan (DC InitialObject) (DC a)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  mappend :: (DC a ** DC a) ~> DC a
mappend = ((a || a) ~> a) -> DecCospan (DC (a || a)) (DC a)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC a) (DC b)
arr (a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (a ~> a) -> (a || a) ~> a
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (HasPushouts k, HasCoproducts k, Alternative f, Ob a) => CommutativeMonoid (DC a :: DECCOSPAN (f :: k -> Type))
instance (HasPushouts k, HasCoproducts k, Alternative f, Ob a) => Comonoid (DC a :: DECCOSPAN (f :: k -> Type)) where
  counit :: DC a ~> Unit
counit = (InitialObject ~> a) -> DecCospan (DC a) (DC InitialObject)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC b) (DC a)
coarr InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  comult :: DC a ~> (DC a ** DC a)
comult = ((a || a) ~> a) -> DecCospan (DC a) (DC (a || a))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
Alternative f =>
(a ~> b) -> DecCospan (DC b) (DC a)
coarr (a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (a ~> a) -> (a ~> a) -> (a || a) ~> a
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (HasPushouts k, HasCoproducts k, Alternative f, Ob a) => CocommutativeComonoid (DC a :: DECCOSPAN (f :: k -> Type))
instance (HasPushouts k, HasCoproducts k, Alternative f, Ob a) => Frobenius (DC a :: DECCOSPAN (f :: k -> Type))
instance (HasPushouts k, HasCoproducts k, Alternative f) => Hypergraph (DECCOSPAN (f :: k -> Type))
instance (HasPushouts k, HasCoproducts k, Alternative f) => CopyDiscard (DECCOSPAN (f :: k -> Type))
instance (HasPushouts k, Alternative f) => Sized (DECCOSPAN (f :: k -> Type)) where
  sizeOf :: forall (a :: DECCOSPAN f). Ob a => Int
sizeOf = Int
2

instance (HasPushouts k, HasCoproducts k, Alternative f) => Closed (DECCOSPAN (f :: k -> Type)) where
  type a ~~> b = ExpHG a b
  withObExp :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(DC a) @(DC b) Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN DC a || UN DC b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b = forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Hypergraph (DECCOSPAN f), Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
curryHG @a @b
  apply :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @b @c = forall {k} (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
forall (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Hypergraph (DECCOSPAN f), Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG @b @c

instance (HasPushouts k, HasCoproducts k, Alternative f) => Dialogue (DECCOSPAN (f :: k -> Type)) where
  type Dual a = a
  withObDual :: forall (a :: DECCOSPAN f) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
(a ~> b) -> Dual b ~> Dual a
dual = (a ~> b) -> Dual b ~> Dual a
DecCospan a b -> DecCospan b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
DecCospan a b -> DecCospan b a
dagger
  linDist :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(DC a) @(DC b) (DecCospan a ~> c
f b ~> c
g f c
s) = (UN DC a ~> c)
-> ((UN DC b || UN DC c) ~> c)
-> f c
-> DecCospan (DC (UN DC a)) (DC (UN DC b || UN DC c))
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan (a ~> c
f (a ~> c) -> (UN DC a ~> a) -> UN DC a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) (a ~> c
f (a ~> c) -> (UN DC b ~> a) -> UN DC b ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b (UN DC b ~> c) -> (UN DC c ~> c) -> (UN DC b || UN DC c) ~> c
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> c
UN DC c ~> c
g) f c
s
  linDistInv :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f) (c :: DECCOSPAN f).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @(DC b) @(DC c) (DecCospan a ~> c
f b ~> c
g f c
s) = ((UN DC a || UN DC b) ~> c)
-> (UN DC c ~> c)
-> f c
-> DecCospan (DC (UN DC a || UN DC b)) (DC (UN DC c))
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan (a ~> c
UN DC a ~> c
f (UN DC a ~> c) -> (UN DC b ~> c) -> (UN DC a || UN DC b) ~> c
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> c
g (b ~> c) -> (UN DC b ~> b) -> UN DC b ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @b @c) (b ~> c
g (b ~> c) -> (UN DC c ~> b) -> UN DC c ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @c) f c
s
  doubleNegInv :: forall (a :: DECCOSPAN f). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
DecCospan (DC (UN DC a)) (DC (UN DC a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id

instance (HasPushouts k, HasCoproducts k, Alternative f) => StarAutonomous (DECCOSPAN (f :: k -> Type)) where
  dualInv :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (Dual a ~> Dual b) -> b ~> a
DecCospan (DC (UN DC a)) (DC (UN DC b))
-> DecCospan (DC (UN DC b)) (DC (UN DC a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
DecCospan a b -> DecCospan b a
dagger
  doubleNeg :: forall (a :: DECCOSPAN f). Ob a => Dual (Dual a) ~> a
doubleNeg = Dual (Dual a) ~> a
DecCospan (DC (UN DC a)) (DC (UN DC a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id
instance (HasPushouts k, HasCoproducts k, Alternative f) => IsoMix (DECCOSPAN (f :: k -> Type)) where
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
DecCospan (DC InitialObject) (DC InitialObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id
  dualUnitInv :: Unit ~> Dual Unit
dualUnitInv = Unit ~> Dual Unit
DecCospan (DC InitialObject) (DC InitialObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id
  dualityCounit :: forall (a :: DECCOSPAN f). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
forall (a :: DECCOSPAN f). Frobenius a => (a ** a) ~> Unit
cap @a

instance (HasPushouts k, HasCoproducts k, Alternative f) => CompactClosed (DECCOSPAN (f :: k -> Type)) where
  distribDual :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @(DC a) @(DC b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b DecCospan (DC (UN DC a || UN DC b)) (DC (UN DC a || UN DC b))
Ob (UN DC a || UN DC b) =>
DecCospan (DC (UN DC a || UN DC b)) (DC (UN DC a || UN DC b))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DECCOSPAN f). Ob a => DecCospan a a
id
  dualityUnit :: forall (a :: DECCOSPAN f). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
forall (a :: DECCOSPAN f). Frobenius a => Unit ~> (a ** a)
cup @a

instance
  ( HasPushouts k
  , HasCoproducts k
  , Alternative f
  , MonoidalAction (t :: (DECCOSPAN f, DECCOSPAN f) +-> DECCOSPAN f)
  )
  => Costrong t (DecCospan :: CAT (DECCOSPAN (f :: k -> Type)))
  where
  coact :: forall (a :: DECCOSPAN f) (x :: DECCOSPAN f) (y :: DECCOSPAN f).
(Ob a, Ob x, Ob y) =>
DecCospan (Act t a x) (Act t a y) -> DecCospan x y
coact @a = forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) =>
(Act t u x ~> Act t u y) -> x ~> y
forall (t :: (DECCOSPAN f, DECCOSPAN f) +-> DECCOSPAN f)
       (u :: DECCOSPAN f) (x :: DECCOSPAN f) (y :: DECCOSPAN f).
(CompactClosed (DECCOSPAN f), MonoidalAction t, Ob x, Ob y,
 Ob u) =>
(Act t u x ~> Act t u y) -> x ~> y
coactCC @t @a

instance (HasPushouts k, Alternative f) => DaggerProfunctor (DecCospan :: CAT (DECCOSPAN (f :: k -> Type))) where
  dagger :: forall (a :: DECCOSPAN f) (b :: DECCOSPAN f).
DecCospan a b -> DecCospan b a
dagger (DecCospan a ~> c
f b ~> c
g f c
s) = (b ~> c) -> (a ~> c) -> f c -> DecCospan (DC b) (DC a)
forall {k} {f :: k -> Type} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> f c -> DecCospan (DC a) (DC b)
DecCospan b ~> c
g a ~> c
f f c
s