{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Duploid where

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

import Proarrow.Adjunction (AdjMonad, Adjunction)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), StrongMonoidalCorep, SymMonoidal (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , dimapDefault
  , lmap
  , obj
  , rmap
  , (//)
  , type (+->)
  )
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep, withObCorep)
import Proarrow.Profunctor.Representable (CorepStar (..), Representable (..), trivialRep, withObRep)

type DUPLOID :: forall {n} {p}. n +-> p -> Kind
type data DUPLOID (adj :: n +-> p) = 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 :: n +-> p) -> Constraint
class IsPN x where
  pn :: SDuploidObj x
  withPosOb :: ((Ob (Pos x)) => r) -> r
  withNegOb :: ((Ob (Neg x)) => r) -> r
instance (Ob x, Corepresentable adj) => IsPN (P x :: DUPLOID adj) where
  pn :: SDuploidObj (P x)
pn = SDuploidObj (P x)
forall {p} {n} {adj :: n +-> p} (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 {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: n +-> p) (a :: p) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @adj @x r
Ob (adj %% x) => r
Ob (Neg (P x)) => r
r
instance (Ob x, Representable adj) => IsPN (N x :: DUPLOID adj) where
  pn :: SDuploidObj (N x)
pn = SDuploidObj (N x)
forall {n} {p} {adj :: n +-> p} (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 {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: n +-> p) (a :: n) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @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 :: n +-> p)) :: p where
  Pos (P a) = a
  Pos (N a :: DUPLOID adj) = adj % a

type family Neg (x :: DUPLOID (adj :: n +-> p)) :: 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 (Pos x) (Neg 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 (Pos a) (Neg a) -> Duploid a a
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (adj (Pos a) (Neg a) -> Duploid a a)
-> adj (Pos a) (Neg a) -> Duploid a a
forall a b. (a -> b) -> a -> b
$ case forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of
    SDuploidObj a
SP -> adj x (adj %% x)
adj (Pos a) (Neg a)
forall (a :: p). Ob a => adj a (adj %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep
    SDuploidObj a
SN -> adj (adj % x) x
adj (Pos a) (Neg a)
forall (a :: n). Ob a => adj (adj % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep
  g :: Duploid b c
g@(Duploid @y adj (Pos b) (Neg 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 :: n +-> p} (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 :: k)
       (z :: DUPLOID adj).
Corepresentable 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 :: j)
       (z :: DUPLOID adj).
Representable 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) => P y ~> z -> x ~> P y -> x ~> z
Duploid adj (Pos (P y)) (Neg z)
g • :: forall {j} {k} {adj :: j +-> k} (x :: DUPLOID adj) (y :: k)
       (z :: DUPLOID adj).
Corepresentable adj =>
(P y ~> z) -> (x ~> P y) -> x ~> z
• Duploid adj (Pos x) (Neg (P y))
f = adj (Pos x) (Neg z) -> Duploid x z
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (((adj %% y) ~> Neg z)
-> adj (Pos x) (adj %% y) -> adj (Pos x) (Neg z)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> adj a b -> adj a d
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 (Neg z) -> (adj %% y) ~> Neg 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 (Neg z)
adj (Pos (P y)) (Neg z)
g) adj (Pos x) (adj %% y)
adj (Pos x) (Neg (P y))
f)

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

fromThunkable :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj, Ob x, Ob y) => Pos x ~> Pos y -> x ~> y
fromThunkable :: forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable Pos x ~> Pos y
f = adj (Pos x) (Neg y) -> Duploid x y
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (case forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @y of SDuploidObj y
SN -> (Pos x ~> (adj % x)) -> adj (Pos x) x
forall (b :: n) (a :: k). 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 Pos x ~> (adj % x)
Pos x ~> Pos y
f; SDuploidObj y
SP -> ((adj %% Pos x) ~> (adj %% x)) -> adj (Pos x) (adj %% x)
forall (a :: k) (b :: n). 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 :: n +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @adj Pos x ~> x
Pos x ~> Pos y
f)) ((Ob (Pos x), Ob (Pos y)) => Duploid x y)
-> (Pos x ~> Pos y) -> Duploid x y
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
\\ Pos x ~> Pos y
f

fromLinear :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj, Ob x, Ob y) => Neg x ~> Neg y -> x ~> y
fromLinear :: forall {k} {p} {adj :: k +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Neg x ~> Neg y) -> x ~> y
fromLinear Neg x ~> Neg y
f = adj (Pos x) (Neg y) -> Duploid x y
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (case forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
IsPN x =>
SDuploidObj x
forall (x :: DUPLOID adj). IsPN x => SDuploidObj x
pn @x of SDuploidObj x
SN -> ((adj % x) ~> (adj % Neg y)) -> adj (adj % x) (Neg y)
forall (b :: k) (a :: p). 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 :: k +-> p) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @adj x ~> Neg y
Neg x ~> Neg y
f); SDuploidObj x
SP -> ((adj %% x) ~> Neg y) -> adj x (Neg y)
forall (a :: p) (b :: k). 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 (adj %% x) ~> Neg y
Neg x ~> Neg y
f) ((Ob (Neg x), Ob (Neg y)) => Duploid x y)
-> (Neg x ~> Neg y) -> Duploid x y
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
\\ Neg x ~> Neg y
f

type Dn x = P (Pos x)

down :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => x ~> Dn x
down :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Dn x
down = forall {n} {p} {adj :: n +-> p} (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) => x ~> Dn x) -> x ~> Dn x)
-> (Ob (Pos x) => x ~> Dn x) -> x ~> Dn x
forall a b. (a -> b) -> a -> b
$ adj (Pos x) (Neg (Dn x)) -> Duploid x (Dn x)
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid adj (Pos x) (adj %% Pos x)
adj (Pos x) (Neg (Dn x))
forall (a :: p). Ob a => adj a (adj %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep

undown :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => Dn x ~> x
undown :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Dn x ~> x
undown = forall {n} {p} {adj :: n +-> p} (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) => Dn x ~> x) -> Dn x ~> x)
-> (Ob (Pos x) => Dn x ~> x) -> Dn x ~> x
forall a b. (a -> b) -> a -> b
$ (Pos (Dn x) ~> Pos x) -> Dn x ~> x
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall (a :: p). (CategoryOf p, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Pos x))

mapDown :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> Dn x ~> (Dn y :: DUPLOID adj)
mapDown :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Dn x ~> Dn y
mapDown x ~> y
f = y ~> P (Pos y)
Duploid y (P (Pos y))
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Dn x
down Duploid y (P (Pos y))
-> Duploid (P (Pos x)) y -> Duploid (P (Pos 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 Duploid x y -> Duploid (P (Pos x)) x -> Duploid (P (Pos 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
. P (Pos x) ~> x
Duploid (P (Pos x)) x
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Dn x ~> x
undown ((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 Up x = N (Neg x)

unup :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => Up x ~> x
unup :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Up x ~> x
unup = forall {n} {p} {adj :: n +-> p} (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) => Up x ~> x) -> Up x ~> x)
-> (Ob (Neg x) => Up x ~> x) -> Up x ~> x
forall a b. (a -> b) -> a -> b
$ adj (Pos (Up x)) (Neg x) -> Duploid (Up x) x
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid adj (adj % Neg x) (Neg x)
adj (Pos (Up x)) (Neg x)
forall (a :: n). Ob a => adj (adj % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep

up :: forall {adj} (x :: DUPLOID adj). (Adjunction adj, Ob x) => x ~> Up x
up :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Up x
up = forall {n} {p} {adj :: n +-> p} (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 ~> Up x) -> x ~> Up x)
-> (Ob (Neg x) => x ~> Up x) -> x ~> Up x
forall a b. (a -> b) -> a -> b
$ (Neg x ~> Neg (Up x)) -> x ~> Up x
forall {k} {p} {adj :: k +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Neg x ~> Neg y) -> x ~> y
fromLinear (forall (a :: n). (CategoryOf n, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Neg x))

mapUp :: forall {adj} (x :: DUPLOID adj) y. (Adjunction adj) => x ~> y -> Up x ~> (Up y :: DUPLOID adj)
mapUp :: forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
Adjunction adj =>
(x ~> y) -> Up x ~> Up y
mapUp x ~> y
f = y ~> N (Neg y)
Duploid y (N (Neg y))
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Up x
up Duploid y (N (Neg y))
-> Duploid (N (Neg x)) y -> Duploid (N (Neg x)) (N (Neg 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 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 {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
Up x ~> x
unup ((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 :: n +-> p), StrongMonoidalCorep 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 @_ @x2 @_ @y2 Duploid x1 x2
f Duploid y1 y2
g =
    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
// case (x2 ~> Dn x2
Duploid x2 (Dn x2)
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Dn x
down Duploid x2 (Dn x2) -> Duploid x1 x2 -> Duploid x1 (Dn x2)
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
. Duploid x1 x2
f, y2 ~> Dn y2
Duploid y2 (Dn y2)
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj).
(Adjunction adj, Ob x) =>
x ~> Dn x
down Duploid y2 (Dn y2) -> Duploid y1 y2 -> Duploid y1 (Dn y2)
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
. Duploid y1 y2
g) of
      (Duploid adj (Pos x1) (Neg (Dn x2))
fp, Duploid adj (Pos y1) (Neg (Dn y2))
gp) ->
        forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @x2 ((Ob (Pos x2) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos x2) =>
    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 :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Pos x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Pos x) => r) -> r
withPosOb @y2 ((Ob (Pos y2) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos y2) =>
    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 x2) @(Pos y2) ((Ob (Pos x2 ** Pos y2) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (Pos x2 ** Pos y2) =>
    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 {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: n +-> p) (a :: p) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @adj @(Pos x2 ** Pos y2) ((Ob (adj %% (Pos x2 ** Pos y2)) =>
  Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
 -> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> (Ob (adj %% (Pos x2 ** Pos y2)) =>
    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
$
                case (Pos x1 ~> (adj % (adj %% Pos x2)))
-> (:.:) adj (CorepStar adj) (adj % (adj %% Pos x2)) (Pos x2)
-> (:.:) adj (CorepStar adj) (Pos x1) (Pos x2)
forall (c :: p) (a :: p) (b :: p).
(c ~> a)
-> (:.:) adj (CorepStar adj) a b -> (:.:) adj (CorepStar adj) c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (adj (Pos x1) (adj %% Pos x2) -> Pos x1 ~> (adj % (adj %% Pos x2))
forall (a :: p) (b :: n). 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 (Pos x1) (adj %% Pos x2)
adj (Pos x1) (Neg (Dn x2))
fp) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: p +-> p) (a :: p).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @(AdjMonad adj) @(Pos x2))
                  (:.:) adj (CorepStar adj) (Pos x1) (Pos x2)
-> (:.:) adj (CorepStar adj) (Pos y1) (Pos y2)
-> (:.:) adj (CorepStar adj) (Pos x1 ** Pos y1) (Pos x2 ** Pos y2)
forall (x1 :: p) (x2 :: p) (y1 :: p) (y2 :: p).
(:.:) adj (CorepStar adj) x1 x2
-> (:.:) adj (CorepStar adj) y1 y2
-> (:.:) adj (CorepStar 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` (Pos y1 ~> (adj % (adj %% Pos y2)))
-> (:.:) adj (CorepStar adj) (adj % (adj %% Pos y2)) (Pos y2)
-> (:.:) adj (CorepStar adj) (Pos y1) (Pos y2)
forall (c :: p) (a :: p) (b :: p).
(c ~> a)
-> (:.:) adj (CorepStar adj) a b -> (:.:) adj (CorepStar adj) c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (adj (Pos y1) (adj %% Pos y2) -> Pos y1 ~> (adj % (adj %% Pos y2))
forall (a :: p) (b :: n). 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 (Pos y1) (adj %% Pos y2)
adj (Pos y1) (Neg (Dn y2))
gp) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: p +-> p) (a :: p).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @(AdjMonad adj) @(Pos y2)) of
                  adj (Pos x1 ** Pos y1) b
fg :.: CorepStar b ~> (adj %% (Pos x2 ** Pos y2))
h -> adj (Pos (P (Pos x1 ** Pos y1))) (Neg (P (Pos x2 ** Pos y2)))
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid ((b ~> (adj %% (Pos x2 ** Pos y2)))
-> adj (Pos x1 ** Pos y1) b
-> adj (Pos x1 ** Pos y1) (adj %% (Pos x2 ** Pos y2))
forall (b :: n) (d :: n) (a :: p). (b ~> d) -> adj a b -> adj a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> (adj %% (Pos x2 ** Pos y2))
h adj (Pos x1 ** Pos y1) b
fg) ((Ob (Pos x1 ** Pos y1), Ob b) =>
 Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2)))
-> adj (Pos x1 ** Pos y1) b
-> Duploid (P (Pos x1 ** Pos y1)) (P (Pos x2 ** Pos y2))
forall (a :: p) (b :: n) 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 (Pos x1 ** Pos y1) b
fg

instance (Adjunction (adj :: n +-> p), StrongMonoidalCorep 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 :: n +-> p} (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 :: n +-> p} (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 :: n +-> p} (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
$ (Pos (P (Unit ** Pos a)) ~> Pos a) -> P (Unit ** Pos a) ~> a
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (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 :: n +-> p} (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
$ (Pos a ~> Pos (P (Unit ** Pos a))) -> a ~> P (Unit ** Pos a)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @(Pos a))
  rightUnitor :: forall (a :: DUPLOID adj). Ob a => (a ** Unit) ~> a
rightUnitor @a = forall {n} {p} {adj :: n +-> p} (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
$ (Pos (P (Pos a ** Unit)) ~> Pos a) -> P (Pos a ** Unit) ~> a
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (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 :: n +-> p} (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
$ (Pos a ~> Pos (P (Pos a ** Unit))) -> a ~> P (Pos a ** Unit)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @(Pos 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 :: n +-> p} (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 :: n +-> p} (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 :: n +-> p} (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
$
                  (Pos (P ((Pos a ** Pos b) ** Pos c))
 ~> Pos (P (Pos a ** (Pos b ** Pos c))))
-> P ((Pos a ** Pos b) ** Pos c) ~> P (Pos a ** (Pos b ** Pos c))
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (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 :: n +-> p} (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 :: n +-> p} (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 :: n +-> p} (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
$
                  (Pos (P (Pos a ** (Pos b ** Pos c)))
 ~> Pos (P ((Pos a ** Pos b) ** Pos c)))
-> P (Pos a ** (Pos b ** Pos c)) ~> P ((Pos a ** Pos b) ** Pos c)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (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 :: n +-> p) = (Adjunction adj, StrongMonoidalCorep 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 :: n +-> p} (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 :: n +-> p} (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
$
            (Pos (P (Pos a ** Pos b)) ~> Pos (P (Pos b ** Pos a)))
-> P (Pos a ** Pos b) ~> P (Pos b ** Pos a)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(Pos a) @(Pos b))

instance (HasBinaryCoproducts p, Adjunction adj) => HasBinaryCoproducts (DUPLOID (adj :: n +-> p)) where
  type a || b = P (Pos a || Pos b)
  withObCoprod :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = forall {n} {p} {adj :: n +-> p} (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 :: n +-> p} (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.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @p @(Pos a) @(Pos b) r
Ob (Pos a || Pos b) => r
Ob (a || b) => r
r
  lft :: forall (a :: DUPLOID adj) (b :: DUPLOID adj).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = forall {n} {p} {adj :: n +-> p} (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 || b)) -> a ~> (a || b))
-> (Ob (Pos a) => a ~> (a || b)) -> a ~> (a || b)
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: n +-> p} (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 ~> (a || b)) -> a ~> (a || b))
-> (Ob (Pos b) => a ~> (a || b)) -> a ~> (a || b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @p @(Pos a) @(Pos b) ((Ob (Pos a || Pos b) => a ~> (a || b)) -> a ~> (a || b))
-> (Ob (Pos a || Pos b) => a ~> (a || b)) -> a ~> (a || b)
forall a b. (a -> b) -> a -> b
$ (Pos a ~> Pos (P (Pos a || Pos b))) -> a ~> P (Pos a || Pos b)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @p @(Pos a) @(Pos b))
  rgt :: forall (a :: DUPLOID adj) (b :: DUPLOID adj).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = forall {n} {p} {adj :: n +-> p} (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) => b ~> (a || b)) -> b ~> (a || b))
-> (Ob (Pos a) => b ~> (a || b)) -> b ~> (a || b)
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: n +-> p} (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) => b ~> (a || b)) -> b ~> (a || b))
-> (Ob (Pos b) => b ~> (a || b)) -> b ~> (a || b)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @p @(Pos a) @(Pos b) ((Ob (Pos a || Pos b) => b ~> (a || b)) -> b ~> (a || b))
-> (Ob (Pos a || Pos b) => b ~> (a || b)) -> b ~> (a || b)
forall a b. (a -> b) -> a -> b
$ (Pos b ~> Pos (P (Pos a || Pos b))) -> b ~> P (Pos a || Pos b)
forall {n} {k} {adj :: n +-> k} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Pos x ~> Pos y) -> x ~> y
fromThunkable (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @p @(Pos a) @(Pos b))
  Duploid @x @a adj (Pos x) (Neg a)
f ||| :: forall (x :: DUPLOID adj) (a :: DUPLOID adj) (y :: DUPLOID adj).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Duploid @y adj (Pos y) (Neg a)
g =
    forall {n} {p} {adj :: n +-> p} (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) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (Pos x) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$
      forall {n} {p} {adj :: n +-> p} (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) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (Pos y) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @p @(Pos x) @(Pos y) ((Ob (Pos x || Pos y) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (Pos x || Pos y) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$
          forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @a ((Ob (Neg a) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (Neg a) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$
            adj (Pos (P (Pos x || Pos y))) (Neg a)
-> Duploid (P (Pos x || Pos y)) a
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (adj (Pos (P (Pos x || Pos y))) (Neg a)
 -> Duploid (P (Pos x || Pos y)) a)
-> adj (Pos (P (Pos x || Pos y))) (Neg a)
-> Duploid (P (Pos x || Pos y)) a
forall a b. (a -> b) -> a -> b
$
              (Pos (P (Pos x || Pos y)) ~> (adj % Neg a))
-> adj (Pos (P (Pos x || Pos y))) (Neg a)
forall (b :: n) (a :: p). 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 (adj (Pos x) (Neg a) -> Pos x ~> (adj % Neg a)
forall (a :: p) (b :: n). 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 (Pos x) (Neg a)
f (Pos x ~> (adj % Neg a))
-> (Pos y ~> (adj % Neg a)) -> (Pos x || Pos y) ~> (adj % Neg a)
forall (x :: p) (a :: p) (y :: p).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| adj (Pos y) (Neg a) -> Pos y ~> (adj % Neg a)
forall (a :: p) (b :: n). 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 (Pos y) (Neg a)
g)

instance (HasBinaryProducts n, Adjunction adj) => HasBinaryProducts (DUPLOID (adj :: n +-> p)) where
  type a && b = N (Neg a && Neg b)
  withObProd :: forall (a :: DUPLOID adj) (b :: DUPLOID adj) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @a ((Ob (Neg a) => r) -> r) -> (Ob (Neg a) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @b ((Ob (Neg b) => r) -> r) -> (Ob (Neg b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @n @(Neg a) @(Neg b) r
Ob (Neg a && Neg b) => r
Ob (a && b) => r
r
  fst :: forall (a :: DUPLOID adj) (b :: DUPLOID adj).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @a ((Ob (Neg a) => (a && b) ~> a) -> (a && b) ~> a)
-> (Ob (Neg a) => (a && b) ~> a) -> (a && b) ~> a
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @b ((Ob (Neg b) => (a && b) ~> a) -> (a && b) ~> a)
-> (Ob (Neg b) => (a && b) ~> a) -> (a && b) ~> a
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @n @(Neg a) @(Neg b) ((Ob (Neg a && Neg b) => (a && b) ~> a) -> (a && b) ~> a)
-> (Ob (Neg a && Neg b) => (a && b) ~> a) -> (a && b) ~> a
forall a b. (a -> b) -> a -> b
$ (Neg (N (Neg a && Neg b)) ~> Neg a) -> N (Neg a && Neg b) ~> a
forall {k} {p} {adj :: k +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Neg x ~> Neg y) -> x ~> y
fromLinear (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @n @(Neg a) @(Neg b))
  snd :: forall (a :: DUPLOID adj) (b :: DUPLOID adj).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @a ((Ob (Neg a) => (a && b) ~> b) -> (a && b) ~> b)
-> (Ob (Neg a) => (a && b) ~> b) -> (a && b) ~> b
forall a b. (a -> b) -> a -> b
$ forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj) r.
IsPN x =>
(Ob (Neg x) => r) -> r
forall (x :: DUPLOID adj) r. IsPN x => (Ob (Neg x) => r) -> r
withNegOb @b ((Ob (Neg b) => (a && b) ~> b) -> (a && b) ~> b)
-> (Ob (Neg b) => (a && b) ~> b) -> (a && b) ~> b
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @n @(Neg a) @(Neg b) ((Ob (Neg a && Neg b) => (a && b) ~> b) -> (a && b) ~> b)
-> (Ob (Neg a && Neg b) => (a && b) ~> b) -> (a && b) ~> b
forall a b. (a -> b) -> a -> b
$ (Neg (N (Neg a && Neg b)) ~> Neg b) -> N (Neg a && Neg b) ~> b
forall {k} {p} {adj :: k +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Adjunction adj, Ob x, Ob y) =>
(Neg x ~> Neg y) -> x ~> y
fromLinear (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @n @(Neg a) @(Neg b))
  Duploid @a @x adj (Pos a) (Neg x)
f &&& :: forall (a :: DUPLOID adj) (x :: DUPLOID adj) (y :: DUPLOID adj).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Duploid @_ @y adj (Pos a) (Neg y)
g =
    forall {n} {p} {adj :: n +-> p} (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) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (Neg x) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$
      forall {n} {p} {adj :: n +-> p} (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) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (Neg y) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @n @(Neg x) @(Neg y) ((Ob (Neg x && Neg y) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (Neg x && Neg y) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$
          forall {n} {p} {adj :: n +-> p} (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 ~> (x && y)) -> a ~> (x && y))
-> (Ob (Pos a) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$
            adj (Pos a) (Neg (N (Neg x && Neg y)))
-> Duploid a (N (Neg x && Neg y))
forall {n} {p} {adj :: n +-> p} (x :: DUPLOID adj)
       (y :: DUPLOID adj).
(Ob x, Ob y) =>
adj (Pos x) (Neg y) -> Duploid x y
Duploid (((adj %% Pos a) ~> (Neg x && Neg y))
-> adj (Pos a) (Neg x && Neg y)
forall (a :: p) (b :: n). 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 (adj (Pos a) (Neg x) -> (adj %% Pos a) ~> Neg x
forall (a :: p) (b :: n). 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 (Pos a) (Neg x)
f ((adj %% Pos a) ~> Neg x)
-> ((adj %% Pos a) ~> Neg y) -> (adj %% Pos a) ~> (Neg x && Neg y)
forall (a :: n) (x :: n) (y :: n).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& adj (Pos a) (Neg y) -> (adj %% Pos a) ~> Neg y
forall (a :: p) (b :: n). 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 (Pos a) (Neg y)
g))