-- | The category of __spans__ in @k@: objects are those of @k@ (wrapped in 'SP'), and a morphism
-- @a '~>' b@ is a span @a <- x -> b@, composed by pullback. With the product of @k@ as tensor every
-- object is a Frobenius monoid, giving the hypergraph\/dagger structure dual to
-- "Proarrow.Category.Instance.Cospan".
module Proarrow.Category.Instance.Span where

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
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.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), WrappedOb, dimapDefault, src)
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , HasProducts
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))

type data SPAN k = SP k

type Span :: CAT (SPAN k)
data Span a b where
  Span :: forall c a b. c ~> a -> c ~> b -> Span (SP a) (SP b)

arr :: (CategoryOf k) => (a :: k) ~> b -> Span (SP a) (SP b)
arr :: forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr a ~> b
f = (a ~> a) -> (a ~> b) -> Span (SP a) (SP b)
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span ((a ~> b) -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a ~> b
f) a ~> b
f

coarr :: (CategoryOf k) => (a :: k) ~> b -> Span (SP b) (SP a)
coarr :: forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP b) (SP a)
coarr a ~> b
f = (a ~> b) -> (a ~> a) -> Span (SP b) (SP a)
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span a ~> b
f ((a ~> b) -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a ~> b
f)

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

-- | The category of spans in @k@: an arrow @'SP' a '~>' 'SP' b@ is a pair of arrows @x '~>' a@
-- and @x '~>' b@ out of a common object, and composition glues along a pullback.
instance (HasPullbacks k) => CategoryOf (SPAN k) where
  type (~>) = Span
  type Ob a = WrappedOb SP a

instance (HasPullbacks k, HasProducts k) => MonoidalProfunctor (Span :: CAT (SPAN k)) where
  one :: Span Unit Unit
one = Span Unit Unit
Span (SP TerminalObject) (SP TerminalObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id
  Span c ~> a
l1 c ~> b
l2 ** :: forall (x1 :: SPAN k) (x2 :: SPAN k) (y1 :: SPAN k) (y2 :: SPAN k).
Span x1 x2 -> Span y1 y2 -> Span (x1 ** y1) (x2 ** y2)
** Span c ~> a
r1 c ~> b
r2 = ((c && c) ~> (a && a))
-> ((c && c) ~> (b && b)) -> Span (SP (a && a)) (SP (b && b))
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span (c ~> a
l1 (c ~> a) -> (c ~> a) -> (c && c) ~> (a && a)
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).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** c ~> a
r1) (c ~> b
l2 (c ~> b) -> (c ~> b) -> (c && c) ~> (b && b)
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).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** c ~> b
r2)
instance (HasPullbacks k, HasProducts k) => Monoidal (SPAN k) where
  type SP a ** SP b = SP (a && b)
  type Unit = SP TerminalObject
  withOb2 :: forall (a :: SPAN k) (b :: SPAN k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(SP a) @(SP b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN SP a && UN SP b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: SPAN k). Ob a => (Unit ** a) ~> a
leftUnitor = ((TerminalObject && UN SP a) ~> UN SP a)
-> Span (SP (TerminalObject && UN SP a)) (SP (UN SP a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr (TerminalObject && UN SP a) ~> UN SP a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: SPAN k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN SP a ~> (TerminalObject && UN SP a))
-> Span (SP (UN SP a)) (SP (TerminalObject && UN SP a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr UN SP a ~> (TerminalObject && UN SP a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: SPAN k). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN SP a && TerminalObject) ~> UN SP a)
-> Span (SP (UN SP a && TerminalObject)) (SP (UN SP a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr (UN SP a && TerminalObject) ~> UN SP a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: SPAN k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN SP a ~> (UN SP a && TerminalObject))
-> Span (SP (UN SP a)) (SP (UN SP a && TerminalObject))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr UN SP a ~> (UN SP a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: SPAN k) (b :: SPAN k) (c :: SPAN k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(SP a) @(SP b) @(SP c) = (((UN SP a && UN SP b) && UN SP c)
 ~> (UN SP a && (UN SP b && UN SP c)))
-> Span
     (SP ((UN SP a && UN SP b) && UN SP c))
     (SP (UN SP a && (UN SP b && UN SP c)))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr (forall (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c)
  associatorInv :: forall (a :: SPAN k) (b :: SPAN k) (c :: SPAN k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(SP a) @(SP b) @(SP c) = ((UN SP a && (UN SP b && UN SP c))
 ~> ((UN SP a && UN SP b) && UN SP c))
-> Span
     (SP (UN SP a && (UN SP b && UN SP c)))
     (SP ((UN SP a && UN SP b) && UN SP c))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr (forall (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c)
instance (HasPullbacks k, HasProducts k) => SymMonoidal (SPAN k) where
  swap :: forall (a :: SPAN k) (b :: SPAN k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(SP a) @(SP b) = ((UN SP a && UN SP b) ~> (UN SP b && UN SP a))
-> Span (SP (UN SP a && UN SP b)) (SP (UN SP b && UN SP a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr (forall (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b)

instance (HasPullbacks k, HasProducts k, Ob a) => Monoid (SP (a :: k)) where
  mempty :: Unit ~> SP a
mempty = (a ~> TerminalObject) -> Span (SP TerminalObject) (SP a)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP b) (SP a)
coarr a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  mappend :: (SP a ** SP a) ~> SP a
mappend = (a ~> (a && a)) -> Span (SP (a && a)) (SP a)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP b) (SP 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 (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& 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 (HasPullbacks k, HasProducts k, Ob a) => CommutativeMonoid (SP (a :: k))
instance (HasPullbacks k, HasProducts k, Ob a) => Comonoid (SP (a :: k)) where
  counit :: SP a ~> Unit
counit = (a ~> TerminalObject) -> Span (SP a) (SP TerminalObject)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP b)
arr a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  comult :: SP a ~> (SP a ** SP a)
comult = (a ~> (a && a)) -> Span (SP a) (SP (a && a))
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Span (SP a) (SP 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 (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& 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 (HasPullbacks k, HasProducts k, Ob a) => CocommutativeComonoid (SP (a :: k))
instance (HasPullbacks k, HasProducts k, Ob a) => Frobenius (SP (a :: k))
instance (HasPullbacks k, HasProducts k) => Hypergraph (SPAN k)
instance (HasPullbacks k, HasProducts k) => CopyDiscard (SPAN k)

instance (HasPullbacks k, HasProducts k) => Closed (SPAN k) where
  type a ~~> b = ExpHG a b
  withObExp :: forall (a :: SPAN k) (b :: SPAN k) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(SP a) @(SP b) Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN SP a && UN SP b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: SPAN k) (b :: SPAN k) (c :: SPAN 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 :: SPAN k) (b :: SPAN k) (c :: SPAN k).
(Hypergraph (SPAN k), Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
curryHG @a @b
  apply :: forall (a :: SPAN k) (b :: SPAN 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 :: SPAN k) (c :: SPAN k).
(Hypergraph (SPAN k), Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG @b @c

instance (HasPullbacks k, HasProducts k) => StarAutonomous (SPAN k) where
  type Dual a = a
  withObDual :: forall (a :: SPAN k) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: SPAN k) (b :: SPAN k). (a ~> b) -> Dual b ~> Dual a
dual (Span c ~> a
f c ~> b
g) = (c ~> b) -> (c ~> a) -> Span (SP b) (SP a)
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span c ~> b
g c ~> a
f
  dualInv :: forall (a :: SPAN k) (b :: SPAN k).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (Span c ~> a
f c ~> b
g) = (c ~> UN SP b)
-> (c ~> UN SP a) -> Span (SP (UN SP b)) (SP (UN SP a))
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span c ~> b
c ~> UN SP b
g c ~> a
c ~> UN SP a
f
  linDist :: forall (a :: SPAN k) (b :: SPAN k) (c :: SPAN k).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(SP a) @(SP b) (Span c ~> a
f c ~> b
g) = (c ~> UN SP a)
-> (c ~> (UN SP b && UN SP c))
-> Span (SP (UN SP a)) (SP (UN SP b && UN SP c))
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b (a ~> UN SP a) -> (c ~> a) -> c ~> UN SP a
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
. c ~> a
f) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b (a ~> UN SP b) -> (c ~> a) -> c ~> UN SP b
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
. c ~> a
f (c ~> UN SP b) -> (c ~> UN SP c) -> c ~> (UN SP b && UN SP c)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& c ~> b
c ~> UN SP c
g)
  linDistInv :: forall (a :: SPAN k) (b :: SPAN k) (c :: SPAN k).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @(SP b) @(SP c) (Span c ~> a
f c ~> b
g) = (c ~> (UN SP a && UN SP b))
-> (c ~> UN SP c) -> Span (SP (UN SP a && UN SP b)) (SP (UN SP c))
forall {k} (c :: k) (a :: k) (b :: k).
(c ~> a) -> (c ~> b) -> Span (SP a) (SP b)
Span (c ~> a
c ~> UN SP a
f (c ~> UN SP a) -> (c ~> UN SP b) -> c ~> (UN SP a && UN SP b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @b @c (b ~> UN SP b) -> (c ~> b) -> c ~> UN SP b
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
. c ~> b
g) (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @b @c (b ~> UN SP c) -> (c ~> b) -> c ~> UN SP 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
. c ~> b
g)
  doubleNeg :: forall (a :: SPAN k). Ob a => Dual (Dual a) ~> a
doubleNeg = Dual (Dual a) ~> a
Span (SP (UN SP a)) (SP (UN SP a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id
  doubleNegInv :: forall (a :: SPAN k). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
Span (SP (UN SP a)) (SP (UN SP a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id
instance (HasPullbacks k, HasProducts k) => CompactClosed (SPAN k) where
  distribDual :: forall (a :: SPAN k) (b :: SPAN k).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @(SP a) @(SP b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b Span (SP (UN SP a && UN SP b)) (SP (UN SP a && UN SP b))
Ob (UN SP a && UN SP b) =>
Span (SP (UN SP a && UN SP b)) (SP (UN SP a && UN SP b))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Span (SP TerminalObject) (SP TerminalObject)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id
  dualityUnit :: forall (a :: SPAN k). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
forall (a :: SPAN k). Frobenius a => Unit ~> (a ** a)
cup @a
  dualityCounit :: forall (a :: SPAN k). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
forall (a :: SPAN k). Frobenius a => (a ** a) ~> Unit
cap @a

instance (HasPullbacks k, HasProducts k) => DaggerProfunctor (Span :: CAT (SPAN k)) where
  dagger :: forall (a :: SPAN k) (b :: SPAN k). Span a b -> Span b a
dagger = (a ~> b) -> Dual b ~> Dual a
Span a b -> Span b a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
forall (a :: SPAN k) (b :: SPAN k). (a ~> b) -> Dual b ~> Dual a
dual

-- Spans over @k@ do /not/ inherit binary products, coproducts or biproducts from @k@'s
-- coproducts alone. That construction is valid only when @k@ is extensive (its coproducts
-- disjoint and stable under pullback), which 'HasPullbacks' plus 'HasBinaryCoproducts' does not
-- imply. Over BOOL, which satisfies both, @snd . (s &&& t)@ collapses to @s@ where the product
-- law demands @t@. The instances are therefore omitted; the monoidal, compact-closed and
-- hypergraph structure above needs no such condition and is unaffected.