{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.CatFun where

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Bicategory.Prof
import Proarrow.Category.Enriched (EnrichedProfunctor (..))
import Proarrow.Category.Instance.BiAsCategory (BI (..), Bi (..), Comp)
import Proarrow.Category.Instance.CatProf (Swap)
import Proarrow.Category.Instance.Coproduct (COPRODUCT, Codiag, Lft, Rgt, (:++:))
import Proarrow.Category.Instance.Product (Diag, Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Prof qualified as F
import Proarrow.Category.Instance.Sub qualified as F
import Proarrow.Category.Instance.Zero (Absurd, VOID)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..), distLProd, distRProd)
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, obj, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  )
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Instance.Composition ((:.:))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), withObRep)

instance HasTerminalObject (BI FUNK) where
  type TerminalObject = B ()
  terminate :: forall (a :: BI FUNK). Ob a => a ~> TerminalObject
terminate = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (UN 'B a) ()).
(Ob p, Ob0 FUNK (UN 'B a), Ob0 FUNK ()) =>
Bi ('B (UN 'B a)) ('B ())
Bi @(FUN (Rep (Constant '())))

instance HasInitialObject (BI FUNK) where
  type InitialObject = B VOID
  initiate :: forall (a :: BI FUNK). Ob a => InitialObject ~> a
initiate = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK VOID (UN 'B a)).
(Ob p, Ob0 FUNK VOID, Ob0 FUNK (UN 'B a)) =>
Bi ('B VOID) ('B (UN 'B a))
Bi @(FUN (Rep Absurd))

instance HasBinaryProducts (BI FUNK) where
  type l && r = B (UN B l, UN B r)
  withObProd :: forall (a :: BI FUNK) (b :: BI FUNK) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> a
fst = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (UN 'B a, UN 'B b) (UN 'B a)).
(Ob p, Ob0 FUNK (UN 'B a, UN 'B b), Ob0 FUNK (UN 'B a)) =>
Bi ('B (UN 'B a, UN 'B b)) ('B (UN 'B a))
Bi @(FUN (Rep Fst))
  snd :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> b
snd = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (UN 'B a, UN 'B b) (UN 'B b)).
(Ob p, Ob0 FUNK (UN 'B a, UN 'B b), Ob0 FUNK (UN 'B b)) =>
Bi ('B (UN 'B a, UN 'B b)) ('B (UN 'B b))
Bi @(FUN (Rep Snd))
  Bi @(FUN p) &&& :: forall (a :: BI FUNK) (x :: BI FUNK) (y :: BI FUNK).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Bi @(FUN q) = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK j (k, k)).
(Ob p, Ob0 FUNK j, Ob0 FUNK (k, k)) =>
Bi ('B j) ('B (k, k))
Bi @(FUN ((p :**: q) :.: Rep Diag))

instance HasBinaryCoproducts (BI FUNK) where
  type B l || B r = B (COPRODUCT l r)
  withObCoprod :: forall (a :: BI FUNK) (b :: BI FUNK) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => a ~> (a || b)
lft = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight PROFK (UN 'B a) (COPRODUCT (UN 'B a) (UN 'B b))).
(Ob p, Ob0 FUNK (UN 'B a),
 Ob0 FUNK (COPRODUCT (UN 'B a) (UN 'B b))) =>
Bi ('B (UN 'B a)) ('B (COPRODUCT (UN 'B a) (UN 'B b)))
Bi @(FUN (Rep Lft))
  rgt :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => b ~> (a || b)
rgt = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight PROFK (UN 'B b) (COPRODUCT (UN 'B a) (UN 'B b))).
(Ob p, Ob0 FUNK (UN 'B b),
 Ob0 FUNK (COPRODUCT (UN 'B a) (UN 'B b))) =>
Bi ('B (UN 'B b)) ('B (COPRODUCT (UN 'B a) (UN 'B b)))
Bi @(FUN (Rep Rgt))
  Bi @(FUN p) ||| :: forall (x :: BI FUNK) (a :: BI FUNK) (y :: BI FUNK).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Bi @(FUN q) = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (COPRODUCT j j) k).
(Ob p, Ob0 FUNK (COPRODUCT j j), Ob0 FUNK k) =>
Bi ('B (COPRODUCT j j)) ('B k)
Bi @(FUN (Rep Codiag :.: (p :++: q)))

instance M.MonoidalProfunctor (Bi :: CAT (BI FUNK)) where
  one :: Bi Unit Unit
one = Bi ('B ()) ('B ())
Bi Unit Unit
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: BI FUNK). Ob a => Bi a a
id
  Bi @(FUN f) ** :: forall (x1 :: BI FUNK) (x2 :: BI FUNK) (y1 :: BI FUNK)
       (y2 :: BI FUNK).
Bi x1 x2 -> Bi y1 y2 -> Bi (x1 ** y1) (x2 ** y2)
** Bi @(FUN g) = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (j, j) (k, k)).
(Ob p, Ob0 FUNK (j, j), Ob0 FUNK (k, k)) =>
Bi ('B (j, j)) ('B (k, k))
Bi @(FUN (f :**: g))

instance M.Monoidal (BI FUNK) where
  type Unit = B ()
  type j ** k = B (UN B j, UN B k)
  withOb2 :: forall (a :: BI FUNK) (b :: BI FUNK) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: BI FUNK). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && 'B (UN 'B a)) ~> 'B (UN 'B a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: BI FUNK). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'B (UN 'B a) ~> (TerminalObject && 'B (UN 'B a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: BI FUNK). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('B (UN 'B a) && TerminalObject) ~> 'B (UN 'B a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: BI FUNK). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'B (UN 'B a) ~> ('B (UN 'B a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
(('B (UN 'B a) && 'B (UN 'B b)) && 'B (UN 'B c))
~> ('B (UN 'B a) && ('B (UN 'B b) && 'B (UN '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
  associatorInv :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
('B (UN 'B a) && ('B (UN 'B b) && 'B (UN 'B c)))
~> (('B (UN 'B a) && 'B (UN 'B b)) && 'B (UN '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

instance M.SymMonoidal (BI FUNK) where
  swap :: forall (a :: BI FUNK) (b :: BI FUNK).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight PROFK (UN 'B a, UN 'B b) (UN 'B b, UN 'B a)).
(Ob p, Ob0 FUNK (UN 'B a, UN 'B b), Ob0 FUNK (UN 'B b, UN 'B a)) =>
Bi ('B (UN 'B a, UN 'B b)) ('B (UN 'B b, UN 'B a))
Bi @(FUN (Rep Swap))

data family CurryH :: (i, j) +-> k -> i -> j +-> k
instance (Representable f, Ob (a :: i), CategoryOf i, CategoryOf j) => FunctorForRep (CurryH f a :: j +-> k) where
  type CurryH f a @ b = f % '(a, b)
  fmap :: forall (a :: j) (b :: j).
(a ~> b) -> (CurryH f a @ a) ~> (CurryH f a @ b)
fmap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: (i, j) +-> k) (a :: (i, j)) (b :: (i, j)).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f (forall (a :: i). (CategoryOf i, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> (:**:) (~>) (~>) '(a, a) '(a, b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: a ~> b
f)
data family Curry :: ((i, j) +-> k) -> (i +-> F.FUN j k)
instance (Representable f, CategoryOf i, CategoryOf j) => FunctorForRep (Curry f :: i +-> F.FUN j k) where
  type Curry f @ a = F.SUB (Rep (CurryH f a))
  fmap :: forall (a :: i) (b :: i).
(a ~> b) -> (Curry f @ a) ~> (Curry f @ b)
fmap a ~> b
f = Prof (Rep (CurryH f a)) (Rep (CurryH f b))
-> Sub Prof (SUB (Rep (CurryH f a))) (SUB (Rep (CurryH f b)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
F.Sub ((Rep (CurryH f a) :~> Rep (CurryH f b))
-> Prof (Rep (CurryH f a)) (Rep (CurryH f b))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
F.Prof \(Rep @c a ~> (CurryH f a @ b)
g) -> (a ~> (CurryH f b @ b)) -> Rep (CurryH f b) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: (i, j) +-> k) (a :: (i, j)) (b :: (i, j)).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f (a ~> b
f (a ~> b) -> (b ~> b) -> (:**:) (~>) (~>) '(a, b) '(b, b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) ((f % '(a, b)) ~> (f % '(b, b)))
-> (a ~> (f % '(a, b))) -> a ~> (f % '(b, 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 ~> (CurryH f a @ b)
a ~> (f % '(a, b))
g)) ((Ob a, Ob b) =>
 Sub Prof (SUB (Rep (CurryH f a))) (SUB (Rep (CurryH f b))))
-> (a ~> b)
-> Sub Prof (SUB (Rep (CurryH f a))) (SUB (Rep (CurryH f b)))
forall (a :: i) (b :: i) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
data family Apply :: (F.FUN j k, j) +-> k
instance (CategoryOf j, CategoryOf k) => FunctorForRep (Apply :: (F.FUN j k, j) +-> k) where
  type Apply @ '(f, x) = UN F.SUB f % x
  fmap :: forall (a :: (FUN j k, j)) (b :: (FUN j k, j)).
(a ~> b) -> (Apply @ a) ~> (Apply @ b)
fmap (Sub Prof a1 b1
n :**: a2 ~> b2
f) = a1 ~> b1
Sub Prof a1 b1
n (a1 ~> b1) -> (a2 ~> b2) -> (UN SUB a1 % a2) ~> (UN SUB b1 % b2)
forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
F.! a2 ~> b2
f
instance Closed (BI FUNK) where
  type B j ~~> B k = B (F.FUN j k)
  withObExp :: forall (a :: BI FUNK) (b :: BI FUNK) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Bi @(FUN f)) = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK (UN 'B a) (FUN (UN 'B b) k)).
(Ob p, Ob0 FUNK (UN 'B a), Ob0 FUNK (FUN (UN 'B b) k)) =>
Bi ('B (UN 'B a)) ('B (FUN (UN 'B b) k))
Bi @(FUN (Rep (Curry f)))
  apply :: forall (a :: BI FUNK) (b :: BI FUNK).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight PROFK (FUN (UN 'B a) (UN 'B b), UN 'B a) (UN 'B b)).
(Ob p, Ob0 FUNK (FUN (UN 'B a) (UN 'B b), UN 'B a),
 Ob0 FUNK (UN 'B b)) =>
Bi ('B (FUN (UN 'B a) (UN 'B b), UN 'B a)) ('B (UN 'B b))
Bi @(FUN (Rep Apply))

instance Distributive (BI FUNK) where
  distL :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(BiCCC (BI FUNK), Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c
  distR :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK).
(BiCCC (BI FUNK), Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c
  absorbL :: forall (a :: BI FUNK).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
('B (UN 'B a) && 'B VOID) ~> 'B VOID
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> b
snd
  absorbR :: forall (a :: BI FUNK).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
('B VOID && 'B (UN 'B a)) ~> 'B VOID
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> a
fst

instance (Bicategory kk) => EnrichedProfunctor (BI FUNK) (Bi :: CAT (BI kk)) where
  type ProObj (BI FUNK) (Bi :: CAT (BI kk)) (B j) (B k) = B (kk j k)
  withProObj :: forall (a :: BI kk) (b :: BI kk) r.
(Ob a, Ob b) =>
(Ob (ProObj (BI FUNK) Bi a b) => r) -> r
withProObj Ob (ProObj (BI FUNK) Bi a b) => r
r = r
Ob (ProObj (BI FUNK) Bi a b) => r
r
  underlying :: forall (a :: BI kk) (b :: BI kk).
Bi a b -> Unit ~> ProObj (BI FUNK) Bi a b
underlying (Bi @f) = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT Tight PROFK () (kk j k)).
(Ob p, Ob0 FUNK (), Ob0 FUNK (kk j k)) =>
Bi ('B ()) ('B (kk j k))
Bi @(FUN (Rep (Constant f)))
  enriched :: forall (a :: BI kk) (b :: BI kk).
(Ob a, Ob b) =>
(Unit ~> ProObj (BI FUNK) Bi a b) -> Bi a b
enriched (Bi @(FUN p)) = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @'() (forall (p :: kk (UN 'B a) (UN 'B b)).
(Ob p, Ob0 kk (UN 'B a), Ob0 kk (UN 'B b)) =>
Bi ('B (UN 'B a)) ('B (UN 'B b))
forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
Bi @(p % '()))
  rmap :: forall (a :: BI kk) (b :: BI kk) (c :: BI kk).
(Ob a, Ob b, Ob c) =>
(HomObj (BI FUNK) b c ** ProObj (BI FUNK) Bi a b)
~> ProObj (BI FUNK) Bi a c
rmap = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight
               PROFK
               (kk (UN 'B b) (UN 'B c), kk (UN 'B a) (UN 'B b))
               (kk (UN 'B a) (UN 'B c))).
(Ob p, Ob0 FUNK (kk (UN 'B b) (UN 'B c), kk (UN 'B a) (UN 'B b)),
 Ob0 FUNK (kk (UN 'B a) (UN 'B c))) =>
Bi
  ('B (kk (UN 'B b) (UN 'B c), kk (UN 'B a) (UN 'B b)))
  ('B (kk (UN 'B a) (UN 'B c)))
Bi @(FUN (Rep Comp))
  lmap :: forall (a :: BI kk) (b :: BI kk) (c :: BI kk).
(Ob a, Ob b, Ob c) =>
(HomObj (BI FUNK) c a ** ProObj (BI FUNK) Bi a b)
~> ProObj (BI FUNK) Bi c b
lmap = forall {s} {kk :: CAT s} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall (p :: SUBCAT
               Tight
               PROFK
               (kk (UN 'B c) (UN 'B a), kk (UN 'B a) (UN 'B b))
               (kk (UN 'B c) (UN 'B b))).
(Ob p, Ob0 FUNK (kk (UN 'B c) (UN 'B a), kk (UN 'B a) (UN 'B b)),
 Ob0 FUNK (kk (UN 'B c) (UN 'B b))) =>
Bi
  ('B (kk (UN 'B c) (UN 'B a), kk (UN 'B a) (UN 'B b)))
  ('B (kk (UN 'B c) (UN 'B b)))
Bi @(FUN (Rep Comp :.: Rep Swap))