{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Duploid where

import Data.Kind (Constraint)
import Prelude (($))

import Proarrow.Adjunction (Adjunction)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , StrongMonoidalRep
  , SymMonoidal (..)
  , unparRep
  )
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , dimapDefault
  , lmap
  , rmap
  , (//)
  , type (+->)
  )
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep, withCorepOb)
import Proarrow.Profunctor.Representable (Representable (..), trivialRep, withRepOb)

type DUPLOID :: forall {n} {p}. p +-> n -> Kind
type data DUPLOID (adj :: p +-> n) = N n | P p

data SDuploidObj x where
  SN :: (Ob x) => SDuploidObj (N x)
  SP :: (Ob x) => SDuploidObj (P x)

type IsPN :: forall {n} {p} {adj}. DUPLOID (adj :: p +-> n) -> Constraint
class IsPN x where
  pn :: SDuploidObj x
  withPosOb :: ((Ob (Pos x)) => r) -> r
  withNegOb :: ((Ob (Neg x)) => r) -> r
instance (Ob x, Representable adj) => IsPN (P x :: DUPLOID adj) where
  pn :: SDuploidObj (P x)
pn = SDuploidObj (P x)
forall {p} {n} {adj :: p +-> n} (x :: p). Ob x => SDuploidObj (P x)
SP
  withPosOb :: forall r. (Ob (Pos (P x)) => r) -> r
withPosOb Ob (Pos (P x)) => r
r = r
Ob (Pos (P x)) => r
r
  withNegOb :: forall r. (Ob (Neg (P x)) => r) -> r
withNegOb Ob (Neg (P x)) => r
r = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: p +-> n) (a :: p) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @adj @x r
Ob (adj % x) => r
Ob (Neg (P x)) => r
r
instance (Ob x, Corepresentable adj) => IsPN (N x :: DUPLOID adj) where
  pn :: SDuploidObj (N x)
pn = SDuploidObj (N x)
forall {n} {p} {adj :: p +-> n} (x :: n). Ob x => SDuploidObj (N x)
SN
  withPosOb :: forall r. (Ob (Pos (N x)) => r) -> r
withPosOb Ob (Pos (N x)) => r
r = forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: p +-> n) (a :: n) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepOb @adj @x r
Ob (adj %% x) => r
Ob (Pos (N x)) => r
r
  withNegOb :: forall r. (Ob (Neg (N x)) => r) -> r
withNegOb Ob (Neg (N x)) => r
r = r
Ob (Neg (N x)) => r
r

type family Pos (x :: DUPLOID (adj :: p +-> n)) :: p where
  Pos (P a) = a
  Pos (N a :: DUPLOID adj) = adj %% a

type family Neg (x :: DUPLOID (adj :: p +-> n)) :: n where
  Neg (P a :: DUPLOID adj) = adj % a
  Neg (N a) = a

type Duploid :: CAT (DUPLOID adj)
data Duploid x y where
  Duploid :: forall {adj} (x :: DUPLOID adj) y. (Ob x, Ob y) => adj (Neg x) (Pos y) -> Duploid x y

instance (Adjunction adj) => Profunctor (Duploid :: CAT (DUPLOID adj)) where
  dimap :: forall (c :: DUPLOID adj) (a :: DUPLOID adj) (b :: DUPLOID adj)
       (d :: DUPLOID adj).
(c ~> a) -> (b ~> d) -> Duploid a b -> Duploid c d
dimap = (c ~> a) -> (b ~> d) -> Duploid a b -> Duploid c d
Duploid c a -> Duploid b d -> Duploid a b -> Duploid 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 :: DUPLOID adj) (b :: DUPLOID adj) r.
((Ob a, Ob b) => r) -> Duploid a b -> r
\\ Duploid{} = r
(Ob a, Ob b) => r
r

-- | ATTENTION: a duploid is not associative, so not really a promonad/category!
instance (Adjunction adj) => Promonad (Duploid :: CAT (DUPLOID adj)) where
  id :: forall (a :: DUPLOID adj). Ob a => Duploid a a
id @x = adj (Neg a) (Pos a) -> Duploid a a
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (adj (Neg a) (Pos a) -> Duploid a a)
-> adj (Neg a) (Pos a) -> Duploid a a
forall a b. (a -> b) -> a -> b
$ case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of
    SDuploidObj a
SP -> adj (adj % x) x
adj (Neg a) (Pos a)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep
    SDuploidObj a
SN -> adj x (adj %% x)
adj (Neg a) (Pos a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep
  g :: Duploid b c
g@(Duploid @y adj (Neg b) (Pos c)
_) . :: forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj).
Duploid b c -> Duploid a b -> Duploid a c
. Duploid a b
f = case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @y of
    SDuploidObj b
SP -> P x ~> c
Duploid b c
g (P x ~> c) -> (a ~> P x) -> a ~> c
forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: j)
       (z :: DUPLOID adj).
Representable adj =>
(P y ~> z) -> (x ~> P y) -> x ~> z
◦ a ~> P x
Duploid a b
f
    SDuploidObj b
SN -> N x ~> c
Duploid b c
g (N x ~> c) -> (a ~> N x) -> a ~> c
forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: k)
       (z :: DUPLOID adj).
Corepresentable adj =>
(N y ~> z) -> (x ~> N y) -> x ~> z
• a ~> N x
Duploid a b
f

instance (Adjunction adj) => CategoryOf (DUPLOID adj) where
  type (~>) = Duploid
  type Ob x = IsPN x

(•) :: forall {adj} (x :: DUPLOID adj) y z. (Corepresentable adj) => N y ~> z -> x ~> N y -> x ~> z
Duploid adj (Neg (N y)) (Pos z)
g • :: forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: k)
       (z :: DUPLOID adj).
Corepresentable adj =>
(N y ~> z) -> (x ~> N y) -> x ~> z
• Duploid adj (Neg x) (Pos (N y))
f = adj (Neg x) (Pos z) -> Duploid x z
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj %% y) ~> Pos z)
-> adj (Neg x) (adj %% y) -> adj (Neg x) (Pos z)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (adj y (Pos z) -> (adj %% y) ~> Pos z
forall (a :: k) (b :: j). adj a b -> (adj %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex adj y (Pos z)
adj (Neg (N y)) (Pos z)
g) adj (Neg x) (adj %% y)
adj (Neg x) (Pos (N y))
f)

(◦) :: forall {adj} (x :: DUPLOID adj) y z. (Representable adj) => P y ~> z -> x ~> P y -> x ~> z
Duploid adj (Neg (P y)) (Pos z)
g ◦ :: forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: j)
       (z :: DUPLOID adj).
Representable adj =>
(P y ~> z) -> (x ~> P y) -> x ~> z
◦ Duploid adj (Neg x) (Pos (P y))
f = adj (Neg x) (Pos z) -> Duploid x z
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid ((Neg x ~> (adj % y))
-> adj (adj % y) (Pos z) -> adj (Neg x) (Pos z)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (adj (Neg x) y -> Neg x ~> (adj % y)
forall (a :: k) (b :: j). adj a b -> a ~> (adj % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index adj (Neg x) y
adj (Neg x) (Pos (P y))
f) adj (adj % y) (Pos z)
adj (Neg (P y)) (Pos z)
g)

fromThunkable :: forall {adj} x y. (Adjunction adj) => x ~> y -> P x ~> (P y :: DUPLOID adj)
fromThunkable :: forall {p} {n} {adj :: p +-> n} (x :: p) (y :: p).
Adjunction adj =>
(x ~> y) -> P x ~> P y
fromThunkable x ~> y
f = adj (Neg (P x)) (Pos (P y)) -> Duploid (P x) (P y)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % x) ~> (adj % y)) -> adj (adj % x) y
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj x ~> y
f)) ((Ob x, Ob y) => Duploid (P x) (P y))
-> (x ~> y) -> Duploid (P x) (P y)
forall (a :: p) (b :: p) 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
\\ x ~> y
f

fromLinear :: forall {adj} x y. (Adjunction adj) => x ~> y -> N x ~> (N y :: DUPLOID adj)
fromLinear :: forall {p} {n} {adj :: p +-> n} (x :: n) (y :: n).
Adjunction adj =>
(x ~> y) -> N x ~> N y
fromLinear x ~> y
f = adj (Neg (N x)) (Pos (N y)) -> Duploid (N x) (N y)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj %% x) ~> (adj %% y)) -> adj x (adj %% y)
forall (a :: n) (b :: p). Ob a => ((adj %% a) ~> b) -> adj a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: p +-> n) (a :: n) (b :: n).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @adj x ~> y
f)) ((Ob x, Ob y) => Duploid (N x) (N y))
-> (x ~> y) -> Duploid (N x) (N y)
forall (a :: n) (b :: n) 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
\\ x ~> y
f

type Up x = P (Pos x)

shiftPosObj :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => x ~> Up x
shiftPosObj :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Up x
shiftPosObj = case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of
  SDuploidObj x
SP -> x ~> Up x
Duploid (P x) (P x)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DUPLOID adj). Ob a => Duploid a a
id
  SDuploidObj x
SN -> let f :: adj (Neg (N x)) (adj %% Neg (N x))
f = adj (Neg (N x)) (adj %% Neg (N x))
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep in adj (Neg (N x)) (Pos (P (adj %% x)))
-> Duploid (N x) (P (adj %% x))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid adj (Neg (N x)) (adj %% Neg (N x))
adj (Neg (N x)) (Pos (P (adj %% x)))
f ((Ob (Neg (N x)), Ob (adj %% Neg (N x))) =>
 Duploid (N x) (P (adj %% x)))
-> adj (Neg (N x)) (adj %% Neg (N x))
-> Duploid (N x) (P (adj %% x))
forall (a :: n) (b :: p) r. ((Ob a, Ob b) => r) -> adj 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
\\ adj (Neg (N x)) (adj %% Neg (N x))
f

shiftPosLift :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> Up x ~> y
shiftPosLift :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> y
shiftPosLift (Duploid adj (Neg x) (Pos y)
f) = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @x ((Ob (Pos x) => Up x ~> y) -> Up x ~> y)
-> (Ob (Pos x) => Up x ~> y) -> Up x ~> y
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @y ((Ob (Pos y) => Up x ~> y) -> Up x ~> y)
-> (Ob (Pos y) => Up x ~> y) -> Up x ~> y
forall a b. (a -> b) -> a -> b
$ adj (Neg (Up x)) (Pos y) -> Duploid (Up x) y
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of SDuploidObj x
SP -> adj (Neg x) (Pos y)
adj (Neg (Up x)) (Pos y)
f; SDuploidObj x
SN -> ((adj % (adj %% x)) ~> (adj % Pos y))
-> adj (adj % (adj %% x)) (Pos y)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (adj x (Pos y) -> (adj %% x) ~> Pos y
forall (a :: n) (b :: p). adj a b -> (adj %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex adj x (Pos y)
adj (Neg x) (Pos y)
f)))

shiftPos :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> Up x ~> (Up y :: DUPLOID adj)
shiftPos :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> Up y
shiftPos x ~> y
f = (x ~> P (Pos y)) -> P (Pos x) ~> P (Pos y)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> y
shiftPosLift (y ~> P (Pos y)
Duploid y (P (Pos y))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Up x
shiftPosObj Duploid y (P (Pos y)) -> Duploid x y -> Duploid x (P (Pos y))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj).
Duploid b c -> Duploid a b -> Duploid a c
. x ~> y
Duploid x y
f) ((Ob x, Ob y) => Duploid (P (Pos x)) (P (Pos y)))
-> Duploid x y -> Duploid (P (Pos x)) (P (Pos y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: DUPLOID adj) (b :: DUPLOID adj) r.
((Ob a, Ob b) => r) -> Duploid a b -> r
\\ x ~> y
Duploid x y
f

type Dn x = N (Neg x)

shiftNegObj :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => Dn x ~> x
shiftNegObj :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Dn x ~> x
shiftNegObj = case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of
  SDuploidObj x
SN -> Dn x ~> x
Duploid (N x) (N x)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DUPLOID adj). Ob a => Duploid a a
id
  SDuploidObj x
SP -> let f :: adj (adj % Pos (P x)) (Pos (P x))
f = adj (adj % Pos (P x)) (Pos (P x))
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep in adj (Neg (N (adj % x))) (Pos (P x)) -> Duploid (N (adj % x)) (P x)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid adj (adj % Pos (P x)) (Pos (P x))
adj (Neg (N (adj % x))) (Pos (P x))
f ((Ob (adj % Pos (P x)), Ob (Pos (P x))) =>
 Duploid (N (adj % x)) (P x))
-> adj (adj % Pos (P x)) (Pos (P x)) -> Duploid (N (adj % x)) (P x)
forall (a :: n) (b :: p) r. ((Ob a, Ob b) => r) -> adj 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
\\ adj (adj % Pos (P x)) (Pos (P x))
f

shiftNegLift :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> x ~> Dn y
shiftNegLift :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> x ~> Dn y
shiftNegLift (Duploid adj (Neg x) (Pos y)
f) = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @x ((Ob (Neg x) => x ~> Dn y) -> x ~> Dn y)
-> (Ob (Neg x) => x ~> Dn y) -> x ~> Dn y
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @y ((Ob (Neg y) => x ~> Dn y) -> x ~> Dn y)
-> (Ob (Neg y) => x ~> Dn y) -> x ~> Dn y
forall a b. (a -> b) -> a -> b
$ adj (Neg x) (Pos (Dn y)) -> Duploid x (Dn y)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @y of SDuploidObj y
SP -> ((adj %% Neg x) ~> (adj %% (adj % x)))
-> adj (Neg x) (adj %% (adj % x))
forall (a :: n) (b :: p). Ob a => ((adj %% a) ~> b) -> adj a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: p +-> n) (a :: n) (b :: n).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @adj (adj (Neg x) x -> Neg x ~> (adj % x)
forall (a :: n) (b :: p). adj a b -> a ~> (adj % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index adj (Neg x) x
adj (Neg x) (Pos y)
f)); SDuploidObj y
SN -> adj (Neg x) (Pos y)
adj (Neg x) (Pos (Dn y))
f)

shiftNeg :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> Dn x ~> (Dn y :: DUPLOID adj)
shiftNeg :: forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Dn x ~> Dn y
shiftNeg x ~> y
f = (N (Neg x) ~> y) -> N (Neg x) ~> N (Neg y)
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> x ~> Dn y
shiftNegLift (x ~> y
Duploid x y
f Duploid x y -> Duploid (N (Neg x)) x -> Duploid (N (Neg x)) y
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: DUPLOID adj) (c :: DUPLOID adj) (a :: DUPLOID adj).
Duploid b c -> Duploid a b -> Duploid a c
. N (Neg x) ~> x
Duploid (N (Neg x)) x
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Dn x ~> x
shiftNegObj) ((Ob x, Ob y) => Duploid (N (Neg x)) (N (Neg y)))
-> Duploid x y -> Duploid (N (Neg x)) (N (Neg y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: DUPLOID adj) (b :: DUPLOID adj) r.
((Ob a, Ob b) => r) -> Duploid a b -> r
\\ x ~> y
Duploid x y
f

instance (Adjunction adj, StrongMonoidalRep adj) => MonoidalProfunctor (Duploid :: CAT (DUPLOID adj)) where
  par0 :: Duploid Unit Unit
par0 = Duploid Unit Unit
Duploid (P Unit) (P Unit)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DUPLOID adj). Ob a => Duploid a a
id
  par :: forall (x1 :: DUPLOID adj) (x2 :: DUPLOID adj) (y1 :: DUPLOID adj)
       (y2 :: DUPLOID adj).
Duploid x1 x2 -> Duploid y1 y2 -> Duploid (x1 ** y1) (x2 ** y2)
par @x1 @_ @y1 Duploid x1 x2
f Duploid y1 y2
g = case ((x1 ~> x2) -> P (Pos x1) ~> x2
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> y
shiftPosLift x1 ~> x2
Duploid x1 x2
f, (y1 ~> y2) -> P (Pos y1) ~> y2
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> y
shiftPosLift y1 ~> y2
Duploid y1 y2
g) of
    (Duploid @(P l) adj (Neg (P (Pos x1))) (Pos x2)
fp, Duploid @(P r) adj (Neg (P (Pos y1))) (Pos y2)
gp) ->
      let fg :: adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
fg = adj (adj % Pos x1) (Pos x2)
adj (Neg (P (Pos x1))) (Pos x2)
fp adj (adj % Pos x1) (Pos x2)
-> adj (adj % Pos y1) (Pos y2)
-> adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
forall (x1 :: n) (x2 :: p) (y1 :: n) (y2 :: p).
adj x1 x2 -> adj y1 y2 -> adj (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` adj (adj % Pos y1) (Pos y2)
adj (Neg (P (Pos y1))) (Pos y2)
gp
      in Duploid x1 x2
f Duploid x1 x2
-> ((Ob x1, Ob x2) =>
    Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
           Duploid y1 y2
g Duploid y1 y2
-> ((Ob y1, Ob y2) =>
    Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
             forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @x1 ((Ob (Pos x1) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos x1) =>
    Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall a b. (a -> b) -> a -> b
$
               forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @y1 ((Ob (Pos y1) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos y1) =>
    Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall a b. (a -> b) -> a -> b
$
                 forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos x1) @(Pos y1) ((Ob (Pos x1 ** Pos y1) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos x1 ** Pos y1) =>
    Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall a b. (a -> b) -> a -> b
$
                   adj (Neg (P (Pos x1 ** Pos y1))) (Pos (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % (Pos x1 ** Pos y1)) ~> ((adj % Pos x1) ** (adj % Pos y1)))
-> adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
-> adj (adj % (Pos x1 ** Pos y1)) (Pos x2 ** Pos y2)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall {j} {k} (p :: j +-> k) (x :: j) (y :: j).
(StrongMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
forall (p :: p +-> n) (x :: p) (y :: p).
(StrongMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
unparRep @adj @l @r) adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
fg) ((Ob ((adj % Pos x1) ** (adj % Pos y1)), Ob (Pos x2 ** Pos y2)) =>
 Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall (a :: n) (b :: p) r. ((Ob a, Ob b) => r) -> adj 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
\\ adj ((adj % Pos x1) ** (adj % Pos y1)) (Pos x2 ** Pos y2)
fg

instance (Adjunction adj, StrongMonoidalRep adj) => Monoidal (DUPLOID adj) where
  type x ** y = P (Pos x ** Pos y)
  type Unit = P Unit
  withOb2 :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b Ob (a ** b) => r
r = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => r) -> r) -> (Ob (Pos a) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @b ((Ob (Pos b) => r) -> r) -> (Ob (Pos b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b) r
Ob (Pos a ** Pos b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: DUPLOID adj). Ob a => (Unit ** a) ~> a
leftUnitor @a = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => (Unit ** a) ~> a) -> (Unit ** a) ~> a)
-> (Ob (Pos a) => (Unit ** a) ~> a) -> (Unit ** a) ~> a
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @(Pos a) ((Ob (Unit ** Pos a) => (Unit ** a) ~> a) -> (Unit ** a) ~> a)
-> (Ob (Unit ** Pos a) => (Unit ** a) ~> a) -> (Unit ** a) ~> a
forall a b. (a -> b) -> a -> b
$ adj (Neg (P (Unit ** Pos a))) (Pos a)
-> Duploid (P (Unit ** Pos a)) a
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % (Unit ** Pos a)) ~> (adj % Pos a))
-> adj (adj % (Unit ** Pos a)) (Pos a)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @(Pos a))))
  leftUnitorInv :: forall (a :: DUPLOID adj). Ob a => a ~> (Unit ** a)
leftUnitorInv @a = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => a ~> (Unit ** a)) -> a ~> (Unit ** a))
-> (Ob (Pos a) => a ~> (Unit ** a)) -> a ~> (Unit ** a)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @(Pos a) ((Ob (Unit ** Pos a) => a ~> (Unit ** a)) -> a ~> (Unit ** a))
-> (Ob (Unit ** Pos a) => a ~> (Unit ** a)) -> a ~> (Unit ** a)
forall a b. (a -> b) -> a -> b
$
      adj (Neg a) (Pos (P (Unit ** Pos a)))
-> Duploid a (P (Unit ** Pos a))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (adj (Neg a) (Pos (P (Unit ** Pos a)))
 -> Duploid a (P (Unit ** Pos a)))
-> adj (Neg a) (Pos (P (Unit ** Pos a)))
-> Duploid a (P (Unit ** Pos a))
forall a b. (a -> b) -> a -> b
$
        case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @a of
          SDuploidObj a
SP -> ((adj % x) ~> (adj % (Unit ** x))) -> adj (adj % x) (Unit ** x)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @(Pos a)))
          SDuploidObj a
SN -> ((adj %% x) ~> (Unit ** (adj %% x))) -> adj x (Unit ** (adj %% x))
forall (a :: n) (b :: p). Ob a => ((adj %% a) ~> b) -> adj a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @(adj %% Neg a))
  rightUnitor :: forall (a :: DUPLOID adj). Ob a => (a ** Unit) ~> a
rightUnitor @a = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => (a ** Unit) ~> a) -> (a ** Unit) ~> a)
-> (Ob (Pos a) => (a ** Unit) ~> a) -> (a ** Unit) ~> a
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @Unit ((Ob (Pos a ** Unit) => (a ** Unit) ~> a) -> (a ** Unit) ~> a)
-> (Ob (Pos a ** Unit) => (a ** Unit) ~> a) -> (a ** Unit) ~> a
forall a b. (a -> b) -> a -> b
$ adj (Neg (P (Pos a ** Unit))) (Pos a)
-> Duploid (P (Pos a ** Unit)) a
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % (Pos a ** Unit)) ~> (adj % Pos a))
-> adj (adj % (Pos a ** Unit)) (Pos a)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @(Pos a))))
  rightUnitorInv :: forall (a :: DUPLOID adj). Ob a => a ~> (a ** Unit)
rightUnitorInv @a = forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => a ~> (a ** Unit)) -> a ~> (a ** Unit))
-> (Ob (Pos a) => a ~> (a ** Unit)) -> a ~> (a ** Unit)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @Unit ((Ob (Pos a ** Unit) => a ~> (a ** Unit)) -> a ~> (a ** Unit))
-> (Ob (Pos a ** Unit) => a ~> (a ** Unit)) -> a ~> (a ** Unit)
forall a b. (a -> b) -> a -> b
$
      adj (Neg a) (Pos (P (Pos a ** Unit)))
-> Duploid a (P (Pos a ** Unit))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (adj (Neg a) (Pos (P (Pos a ** Unit)))
 -> Duploid a (P (Pos a ** Unit)))
-> adj (Neg a) (Pos (P (Pos a ** Unit)))
-> Duploid a (P (Pos a ** Unit))
forall a b. (a -> b) -> a -> b
$
        case forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @a of
          SDuploidObj a
SP -> ((adj % x) ~> (adj % (x ** Unit))) -> adj (adj % x) (x ** Unit)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @(Pos a)))
          SDuploidObj a
SN -> ((adj %% x) ~> ((adj %% x) ** Unit)) -> adj x ((adj %% x) ** Unit)
forall (a :: n) (b :: p). Ob a => ((adj %% a) ~> b) -> adj a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @(adj %% Neg a))
  associator :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (c :: DUPLOID adj).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c =
    forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos a) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
      forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @b ((Ob (Pos b) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos b) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
        forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @c ((Ob (Pos c) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos c) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b) ((Ob (Pos a ** Pos b) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos a ** Pos b) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a ** Pos b) @(Pos c) ((Ob ((Pos a ** Pos b) ** Pos c) =>
  ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob ((Pos a ** Pos b) ** Pos c) =>
    ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos b) @(Pos c) ((Ob (Pos b ** Pos c) => ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos b ** Pos c) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b ** Pos c) ((Ob (Pos a ** (Pos b ** Pos c)) =>
  ((a ** b) ** c) ~> (a ** (b ** c)))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> (Ob (Pos a ** (Pos b ** Pos c)) =>
    ((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$
                  adj
  (Neg (P ((Pos a ** Pos b) ** Pos c)))
  (Pos (P (Pos a ** (Pos b ** Pos c))))
-> Duploid
     (P ((Pos a ** Pos b) ** Pos c)) (P (Pos a ** (Pos b ** Pos c)))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % ((Pos a ** Pos b) ** Pos c))
 ~> (adj % (Pos a ** (Pos b ** Pos c))))
-> adj
     (adj % ((Pos a ** Pos b) ** Pos c)) (Pos a ** (Pos b ** Pos c))
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @(Pos a) @(Pos b) @(Pos c))))
  associatorInv :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) (c :: DUPLOID adj).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c =
    forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos a) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
      forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @b ((Ob (Pos b) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos b) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
        forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @c ((Ob (Pos c) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos c) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b) ((Ob (Pos a ** Pos b) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos a ** Pos b) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a ** Pos b) @(Pos c) ((Ob ((Pos a ** Pos b) ** Pos c) =>
  (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob ((Pos a ** Pos b) ** Pos c) =>
    (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos b) @(Pos c) ((Ob (Pos b ** Pos c) => (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos b ** Pos c) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b ** Pos c) ((Ob (Pos a ** (Pos b ** Pos c)) =>
  (a ** (b ** c)) ~> ((a ** b) ** c))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> (Ob (Pos a ** (Pos b ** Pos c)) =>
    (a ** (b ** c)) ~> ((a ** b) ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$
                  adj
  (Neg (P (Pos a ** (Pos b ** Pos c))))
  (Pos (P ((Pos a ** Pos b) ** Pos c)))
-> Duploid
     (P (Pos a ** (Pos b ** Pos c))) (P ((Pos a ** Pos b) ** Pos c))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % (Pos a ** (Pos b ** Pos c)))
 ~> (adj % ((Pos a ** Pos b) ** Pos c)))
-> adj
     (adj % (Pos a ** (Pos b ** Pos c))) ((Pos a ** Pos b) ** Pos c)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @(Pos a) @(Pos b) @(Pos c))))

type StrongSymMonAdj (adj :: p +-> n) = (Adjunction adj, StrongMonoidalRep adj, SymMonoidal p)

instance (StrongSymMonAdj adj) => SymMonoidal (DUPLOID adj) where
  swap :: forall (a :: DUPLOID adj) (b :: DUPLOID adj).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b =
    forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @a ((Ob (Pos a) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a))
-> (Ob (Pos a) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
      forall {n} {p} {adj :: p +-> n} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @b ((Ob (Pos b) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a))
-> (Ob (Pos b) => (a ** b) ~> (b ** a)) -> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos a) @(Pos b) ((Ob (Pos a ** Pos b) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (Ob (Pos a ** Pos b) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Pos b) @(Pos a) ((Ob (Pos b ** Pos a) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (Ob (Pos b ** Pos a) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
            adj (Neg (P (Pos a ** Pos b))) (Pos (P (Pos b ** Pos a)))
-> Duploid (P (Pos a ** Pos b)) (P (Pos b ** Pos a))
forall {p} {n} {adj :: p +-> n} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Neg x) (Pos y) -> Duploid x y
Duploid (((adj % (Pos a ** Pos b)) ~> (adj % (Pos b ** Pos a)))
-> adj (adj % (Pos a ** Pos b)) (Pos b ** Pos a)
forall (b :: p) (a :: n). Ob b => (a ~> (adj % b)) -> adj a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: p +-> n) (a :: p) (b :: p).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(Pos a) @(Pos b))))