-- | The category of __cospans__ in @k@: objects are those of @k@ (wrapped in 'CS'), and a morphism
-- @a '~>' b@ is a cospan @a -> x <- b@, composed by pushout. With the coproduct of @k@ as tensor
-- every object is a Frobenius monoid, giving a 'Proarrow.Category.Monoidal.Hypergraph.Hypergraph',
-- compact closed, dagger category. This is the archetypal setting for undirected wiring diagrams.
module Proarrow.Category.Instance.Cospan where

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.Span (SPAN (..), Span (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Hypergraph (ExpHG, Frobenius, Hypergraph, applyHG, cap, cup, curryHG)
import Proarrow.Category.Monoidal.StarAutonomous (StarAutonomous (..))
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.Functor (FunctorForRep (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))

type data COSPAN k = CS k

type Cospan :: CAT (COSPAN k)
data Cospan a b where
  Cospan :: forall c a b. a ~> c -> b ~> c -> Cospan (CS a) (CS b)

arr :: (CategoryOf k) => (a :: k) ~> b -> Cospan (CS a) (CS b)
arr :: forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr a ~> b
f = (a ~> b) -> (b ~> b) -> Cospan (CS a) (CS b)
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan 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)

coarr :: (CategoryOf k) => (a :: k) ~> b -> Cospan (CS b) (CS a)
coarr :: forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS b) (CS a)
coarr a ~> b
f = (b ~> b) -> (a ~> b) -> Cospan (CS b) (CS a)
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan ((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

instance (HasPushouts k) => Profunctor (Cospan :: CAT (COSPAN k)) where
  dimap :: forall (c :: COSPAN k) (a :: COSPAN k) (b :: COSPAN k)
       (d :: COSPAN k).
(c ~> a) -> (b ~> d) -> Cospan a b -> Cospan c d
dimap = (c ~> a) -> (b ~> d) -> Cospan a b -> Cospan c d
Cospan c a -> Cospan b d -> Cospan a b -> Cospan 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 :: COSPAN k) (b :: COSPAN k) r.
((Ob a, Ob b) => r) -> Cospan a b -> r
\\ Cospan a ~> c
f b ~> c
g = 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) => Promonad (Cospan :: CAT (COSPAN k)) where
  id :: forall (a :: COSPAN k). Ob a => Cospan a a
id = (UN CS a ~> UN CS a)
-> (UN CS a ~> UN CS a) -> Cospan (CS (UN CS a)) (CS (UN CS a))
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan UN CS a ~> UN CS a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id UN CS a ~> UN CS a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Cospan a ~> c
f b ~> c
g . :: forall (b :: COSPAN k) (c :: COSPAN k) (a :: COSPAN k).
Cospan b c -> Cospan a b -> Cospan a c
. Cospan a ~> c
h b ~> c
i = (a ~> c)
-> (a ~> c)
-> (forall (p :: k). (c ~> p) -> (c ~> p) -> Cospan a c)
-> Cospan 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) -> Cospan (CS a) (CS b)
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan (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)

-- | The category of cospans in @k@: an arrow @'CS' a '~>' 'CS' b@ is a pair of arrows
-- @a '~>' x@ and @b '~>' x@ into a common object, and composition glues along a pushout.
instance (HasPushouts k) => CategoryOf (COSPAN k) where
  type (~>) = Cospan
  type Ob a = WrappedOb CS a

instance (HasPushouts k, HasCoproducts k) => MonoidalProfunctor (Cospan :: CAT (COSPAN k)) where
  one :: Cospan Unit Unit
one = Cospan Unit Unit
Cospan (CS InitialObject) (CS InitialObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COSPAN k). Ob a => Cospan a a
id
  Cospan a ~> c
l1 b ~> c
l2 ** :: forall (x1 :: COSPAN k) (x2 :: COSPAN k) (y1 :: COSPAN k)
       (y2 :: COSPAN k).
Cospan x1 x2 -> Cospan y1 y2 -> Cospan (x1 ** y1) (x2 ** y2)
** Cospan a ~> c
r1 b ~> c
r2 = ((a || a) ~> (c || c))
-> ((b || b) ~> (c || c)) -> Cospan (CS (a || a)) (CS (b || b))
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan (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)
instance (HasPushouts k, HasCoproducts k) => Monoidal (COSPAN k) where
  type CS a ** CS b = CS (a || b)
  type Unit = CS InitialObject
  withOb2 :: forall (a :: COSPAN k) (b :: COSPAN k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(CS a) @(CS 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 CS a || UN CS b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: COSPAN k). Ob a => (Unit ** a) ~> a
leftUnitor = ((InitialObject || UN CS a) ~> UN CS a)
-> Cospan (CS (InitialObject || UN CS a)) (CS (UN CS a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr (InitialObject || UN CS a) ~> UN CS a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(InitialObject || a) ~> a
leftUnitorCoprod
  leftUnitorInv :: forall (a :: COSPAN k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN CS a ~> (InitialObject || UN CS a))
-> Cospan (CS (UN CS a)) (CS (InitialObject || UN CS a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr UN CS a ~> (InitialObject || UN CS a)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (InitialObject || a)
leftUnitorCoprodInv
  rightUnitor :: forall (a :: COSPAN k). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN CS a || InitialObject) ~> UN CS a)
-> Cospan (CS (UN CS a || InitialObject)) (CS (UN CS a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr (UN CS a || InitialObject) ~> UN CS a
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(a || InitialObject) ~> a
rightUnitorCoprod
  rightUnitorInv :: forall (a :: COSPAN k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN CS a ~> (UN CS a || InitialObject))
-> Cospan (CS (UN CS a)) (CS (UN CS a || InitialObject))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr UN CS a ~> (UN CS a || InitialObject)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (a || InitialObject)
rightUnitorCoprodInv
  associator :: forall (a :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(CS a) @(CS b) @(CS c) = (((UN CS a || UN CS b) || UN CS c)
 ~> (UN CS a || (UN CS b || UN CS c)))
-> Cospan
     (CS ((UN CS a || UN CS b) || UN CS c))
     (CS (UN CS a || (UN CS b || UN CS c)))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS 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 :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(CS a) @(CS b) @(CS c) = ((UN CS a || (UN CS b || UN CS c))
 ~> ((UN CS a || UN CS b) || UN CS c))
-> Cospan
     (CS (UN CS a || (UN CS b || UN CS c)))
     (CS ((UN CS a || UN CS b) || UN CS c))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS 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) => SymMonoidal (COSPAN k) where
  swap :: forall (a :: COSPAN k) (b :: COSPAN k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(CS a) @(CS b) = ((UN CS a || UN CS b) ~> (UN CS b || UN CS a))
-> Cospan (CS (UN CS a || UN CS b)) (CS (UN CS b || UN CS a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS 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, Ob a) => Monoid (CS (a :: k)) where
  mempty :: Unit ~> CS a
mempty = (InitialObject ~> a) -> Cospan (CS InitialObject) (CS a)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS b)
arr InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  mappend :: (CS a ** CS a) ~> CS a
mappend = ((a || a) ~> a) -> Cospan (CS (a || a)) (CS a)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS a) (CS 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, Ob a) => CommutativeMonoid (CS (a :: k))
instance (HasPushouts k, HasCoproducts k, Ob a) => Comonoid (CS (a :: k)) where
  counit :: CS a ~> Unit
counit = (InitialObject ~> a) -> Cospan (CS a) (CS InitialObject)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS b) (CS a)
coarr InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  comult :: CS a ~> (CS a ** CS a)
comult = ((a || a) ~> a) -> Cospan (CS a) (CS (a || a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Cospan (CS b) (CS 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, Ob a) => CocommutativeComonoid (CS (a :: k))
instance (HasPushouts k, HasCoproducts k, Ob a) => Frobenius (CS (a :: k))
instance (HasPushouts k, HasCoproducts k) => Hypergraph (COSPAN k)
instance (HasPushouts k, HasCoproducts k) => CopyDiscard (COSPAN k)

instance (HasPushouts k, HasCoproducts k) => Closed (COSPAN k) where
  type a ~~> b = ExpHG a b
  withObExp :: forall (a :: COSPAN k) (b :: COSPAN k) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(CS a) @(CS 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 CS a || UN CS b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(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 :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(Hypergraph (COSPAN k), Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
curryHG @a @b
  apply :: forall (a :: COSPAN k) (b :: COSPAN k).
(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 :: COSPAN k) (c :: COSPAN k).
(Hypergraph (COSPAN k), Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG @b @c

instance (HasPushouts k, HasCoproducts k) => StarAutonomous (COSPAN k) where
  type Dual a = a
  withObDual :: forall (a :: COSPAN k) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: COSPAN k) (b :: COSPAN k).
(a ~> b) -> Dual b ~> Dual a
dual = (a ~> b) -> Dual b ~> Dual a
Cospan a b -> Cospan b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: COSPAN k) (b :: COSPAN k). Cospan a b -> Cospan b a
dagger
  dualInv :: forall (a :: COSPAN k) (b :: COSPAN k).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (Dual a ~> Dual b) -> b ~> a
Cospan (CS (UN CS a)) (CS (UN CS b))
-> Cospan (CS (UN CS b)) (CS (UN CS a))
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
forall (a :: COSPAN k) (b :: COSPAN k). Cospan a b -> Cospan b a
dagger
  linDist :: forall (a :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(CS a) @(CS b) (Cospan a ~> c
f b ~> c
g) = (UN CS a ~> c)
-> ((UN CS b || UN CS c) ~> c)
-> Cospan (CS (UN CS a)) (CS (UN CS b || UN CS c))
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan (a ~> c
f (a ~> c) -> (UN CS a ~> a) -> UN CS 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 CS b ~> a) -> UN CS 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 CS b ~> c) -> (UN CS c ~> c) -> (UN CS b || UN CS 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 CS c ~> c
g)
  linDistInv :: forall (a :: COSPAN k) (b :: COSPAN k) (c :: COSPAN k).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @(CS b) @(CS c) (Cospan a ~> c
f b ~> c
g) = ((UN CS a || UN CS b) ~> c)
-> (UN CS c ~> c)
-> Cospan (CS (UN CS a || UN CS b)) (CS (UN CS c))
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan (a ~> c
UN CS a ~> c
f (UN CS a ~> c) -> (UN CS b ~> c) -> (UN CS a || UN CS 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 CS b ~> b) -> UN CS 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 CS c ~> b) -> UN CS 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)
  doubleNeg :: forall (a :: COSPAN k). Ob a => Dual (Dual a) ~> a
doubleNeg = Dual (Dual a) ~> a
Cospan (CS (UN CS a)) (CS (UN CS a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COSPAN k). Ob a => Cospan a a
id
  doubleNegInv :: forall (a :: COSPAN k). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
Cospan (CS (UN CS a)) (CS (UN CS a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COSPAN k). Ob a => Cospan a a
id
instance (HasPushouts k, HasCoproducts k) => CompactClosed (COSPAN k) where
  distribDual :: forall (a :: COSPAN k) (b :: COSPAN k).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @(CS a) @(CS b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b Cospan (CS (UN CS a || UN CS b)) (CS (UN CS a || UN CS b))
Ob (UN CS a || UN CS b) =>
Cospan (CS (UN CS a || UN CS b)) (CS (UN CS a || UN CS b))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COSPAN k). Ob a => Cospan a a
id
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Cospan (CS InitialObject) (CS InitialObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COSPAN k). Ob a => Cospan a a
id
  dualityUnit :: forall (a :: COSPAN k). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
forall (a :: COSPAN k). Frobenius a => Unit ~> (a ** a)
cup @a
  dualityCounit :: forall (a :: COSPAN k). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
forall (a :: COSPAN k). Frobenius a => (a ** a) ~> Unit
cap @a

instance (HasPushouts k) => DaggerProfunctor (Cospan :: CAT (COSPAN k)) where
  dagger :: forall (a :: COSPAN k) (b :: COSPAN k). Cospan a b -> Cospan b a
dagger (Cospan a ~> c
f b ~> c
g) = (b ~> c) -> (a ~> c) -> Cospan (CS b) (CS a)
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan b ~> c
g a ~> c
f

data family Pushout :: SPAN k +-> COSPAN k
instance (HasPushouts k, HasPullbacks k) => FunctorForRep (Pushout :: SPAN k +-> COSPAN k) where
  type Pushout @ (SP a) = CS a
  fmap :: forall (a :: SPAN k) (b :: SPAN k).
(a ~> b) -> (Pushout @ a) ~> (Pushout @ b)
fmap (Span c ~> a1
l c ~> b1
r) = (c ~> a1)
-> (c ~> b1)
-> (forall (p :: k).
    (a1 ~> p) -> (b1 ~> p) -> Cospan (CS a1) (CS b1))
-> Cospan (CS a1) (CS b1)
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 c ~> a1
l c ~> b1
r (a1 ~> p) -> (b1 ~> p) -> Cospan (CS a1) (CS b1)
forall (p :: k). (a1 ~> p) -> (b1 ~> p) -> Cospan (CS a1) (CS b1)
forall {k} (c :: k) (a :: k) (b :: k).
(a ~> c) -> (b ~> c) -> Cospan (CS a) (CS b)
Cospan

data family Pullback :: COSPAN k +-> SPAN k
instance (HasPushouts k, HasPullbacks k) => FunctorForRep (Pullback :: COSPAN k +-> SPAN k) where
  type Pullback @ (CS a) = SP a
  fmap :: forall (a :: COSPAN k) (b :: COSPAN k).
(a ~> b) -> (Pullback @ a) ~> (Pullback @ b)
fmap (Cospan a ~> c
l b ~> c
r) = (a ~> c)
-> (b ~> c)
-> (forall (p :: k). (p ~> a) -> (p ~> b) -> Span (SP a) (SP b))
-> Span (SP a) (SP b)
forall (o :: k) (a :: k) (b :: k) r.
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPullbacks k =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
pullback a ~> c
l b ~> c
r (p ~> a) -> (p ~> b) -> Span (SP a) (SP b)
forall (p :: k). (p ~> a) -> (p ~> b) -> Span (SP a) (SP b)
forall {k} (c :: k) (a1 :: k) (b1 :: k).
(c ~> a1) -> (c ~> b1) -> Span (SP a1) (SP b1)
Span