module Proarrow.Category.Instance.Span where

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Hypergraph (ExpHG, Frobenius (..), Hypergraph, applyHG, curryHG, spiderDefault)
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, src)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Pullback (Cone (..), Cosink (..), HasPullbacks (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

newtype SPAN k = SP k
type instance UN SP (SP k) = 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 = case (c ~> a) -> (c ~> a) -> Cosink '[c, c]
forall (o :: k) (a :: k) (b :: k).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
forall k (o :: k) (a :: k) (b :: k).
HasPullbacks k =>
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback c ~> a
c ~> b
i c ~> a
f of Cone (Leg a1 ~> b
l (Leg a1 ~> b
r Cone ('PR a1) (L bs1)
Apex)) -> (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 (c ~> a
h (c ~> a) -> (a ~> c) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> c
a1 ~> b
l) (c ~> b
g (c ~> b) -> (a ~> c) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> c
a1 ~> b
r)
instance (HasPullbacks k) => CategoryOf (SPAN k) where
  type (~>) = Span
  type Ob a = (Is SP a, Ob (UN SP a))

instance (HasPullbacks k) => MonoidalProfunctor (Span :: CAT (SPAN k)) where
  par0 :: Span Unit Unit
par0 = Span Unit Unit
Span ('SP TerminalObject) ('SP TerminalObject)
forall {k} (p :: k +-> 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 par :: forall (x1 :: SPAN k) (x2 :: SPAN k) (y1 :: SPAN k) (y2 :: SPAN k).
Span x1 x2 -> Span y1 y2 -> Span (x1 ** y1) (x2 ** y2)
`par` 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) => 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).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts 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).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c)
instance (HasPullbacks 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, 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 :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (HasPullbacks 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 :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (HasPullbacks k, Ob a) => Frobenius (SP (a :: k)) where
  spider :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
NFold n ('SP a) ~> NFold m ('SP a)
spider @x @y = forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
forall (n :: Nat) (m :: Nat) (a :: SPAN k).
(Monoid a, Comonoid a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
spiderDefault @x @y @(SP a)
instance (HasPullbacks k) => Hypergraph (SPAN k)
instance (HasPullbacks k) => CopyDiscard (SPAN k)

instance (HasPullbacks 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) => StarAutonomous (SPAN k) where
  type Dual a = a
  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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> b
g)
instance (HasPullbacks 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 :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SPAN k). Ob a => Span a a
id

instance (HasPullbacks 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