{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory
  ( -- * Bicategories
    Bicategory (..)
  , (==)
  , (||)
  , appendObj
  , leftUnitor'
  , leftUnitorInv'
  , rightUnitor'
  , rightUnitorInv'
  , associator'
  , associatorInv'
  , leftUnitorWith
  , leftUnitorInvWith
  , rightUnitorWith
  , rightUnitorInvWith
  , Ob0'
  , Ob'

    -- * More
  , Monad (..)
  , Comonad (..)
  , Adjunction (..)
  , leftAdjunct
  , rightAdjunct
  , Bimodule (..)
  )
where

import Data.Kind (Constraint)

import Proarrow.Core (CAT, CategoryOf (..), Promonad (..), id)
import Proarrow.Object (Obj, obj)

infixl 8 ||
infixl 7 ==
infixl 1 \\\

-- | A bicategory is locally "something" if each hom-category is "something".
class (forall j k. (Ob0 kk j, Ob0 kk k) => c (kk j k)) => Locally c kk

instance (forall j k. (Ob0 kk j, Ob0 kk k) => c (kk j k)) => Locally c kk

class (Ob0 kk j) => Ob0' kk j
instance (Ob0 kk j) => Ob0' kk j

class (Ob0 kk j, Ob0 kk k, Ob a) => Ob' (a :: kk j k)
instance (Ob0 kk j, Ob0 kk k, Ob a) => Ob' (a :: kk j k)

-- | Bicategories.
--
-- * 0-cells are kinds @i@, @j@, @k@... satisfying the @Ob0 kk@ constraint.
-- * 1-cells are types of kind @kk j k@ for any 0-cells @j@ and @k@, satisfying the @Ob@ constraint.
-- * 2-cells are values of type @p ~> q@, where @p@ and @q@ are 1-cells.
type Bicategory :: forall {s}. CAT s -> Constraint
class (Locally CategoryOf kk, CategoryOf s) => Bicategory (kk :: CAT s) where
  type Ob0 kk (j :: k) :: Constraint
  type Ob0 kk j = ()
  type I :: kk i i
  type O (p :: kk j k) (q :: kk i j) :: kk i k

  -- | The identity 1-cell (as represented by an identity 2-cell).
  iObj :: (Ob0 kk i) => Obj (I :: kk i i)
  default iObj :: (Ob0 kk i, Ob (I :: kk i i)) => Obj (I :: kk i i)
  iObj = I ~> I
forall (a :: kk i i). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

  -- | Horizontal composition of 2-cells.
  o :: (a :: kk j k) ~> b -> c ~> d -> (a `O` c) ~> (b `O` d)

  -- | Observe constraints from a 2-cell value.
  (\\\) :: ((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps :: kk i j) ~> qs -> r

  leftUnitor :: forall {i} {j} a. (Ob0 kk i, Ob0 kk j, Ob (a :: kk i j)) => (I `O` a) ~> a
  leftUnitorInv :: forall {i} {j} a. (Ob0 kk i, Ob0 kk j, Ob (a :: kk i j)) => a ~> (I `O` a)
  rightUnitor :: forall {i} {j} a. (Ob0 kk i, Ob0 kk j, Ob (a :: kk i j)) => (a `O` I) ~> a
  rightUnitorInv :: forall {i} {j} a. (Ob0 kk i, Ob0 kk j, Ob (a :: kk i j)) => a ~> (a `O` I)
  associator
    :: forall {h} {i} {j} {k} a b c
     . (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob (a :: kk j k), Ob (b :: kk i j), Ob (c :: kk h i))
    => (a `O` b) `O` c ~> a `O` (b `O` c)
  associatorInv
    :: forall {h} {i} {j} {k} a b c
     . (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob (a :: kk j k), Ob (b :: kk i j), Ob (c :: kk h i))
    => a `O` (b `O` c) ~> (a `O` b) `O` c

leftUnitor' :: (Bicategory kk) => (a :: kk i j) ~> b -> (I `O` a) ~> b
leftUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> O I a ~> b
leftUnitor' a ~> b
f = a ~> b
f (a ~> b) -> (O I a ~> a) -> O I a ~> b
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. O I a ~> a
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => O I a ~> b)
-> (a ~> b) -> O I a ~> b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
f

leftUnitorInv' :: (Bicategory kk) => (a :: kk i j) ~> b -> a ~> (I `O` b)
leftUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> a ~> O I b
leftUnitorInv' a ~> b
f = b ~> O I b
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv (b ~> O I b) -> (a ~> b) -> a ~> O I b
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => a ~> O I b)
-> (a ~> b) -> a ~> O I b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
f

rightUnitor' :: (Bicategory kk) => (a :: kk i j) ~> b -> (a `O` I) ~> b
rightUnitor' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> O a I ~> b
rightUnitor' a ~> b
f = a ~> b
f (a ~> b) -> (O a I ~> a) -> O a I ~> b
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. O a I ~> a
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => O a I ~> b)
-> (a ~> b) -> O a I ~> b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
f

rightUnitorInv' :: (Bicategory kk) => (a :: kk i j) ~> b -> a ~> (b `O` I)
rightUnitorInv' :: forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> a ~> O b I
rightUnitorInv' a ~> b
f = b ~> O b I
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
rightUnitorInv (b ~> O b I) -> (a ~> b) -> a ~> O b I
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => a ~> O b I)
-> (a ~> b) -> a ~> O b I
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
f

associator'
  :: forall kk {i} {j} (a :: kk i j) b c. (Bicategory kk) => Obj a -> Obj b -> Obj c -> (a `O` b) `O` c ~> a `O` (b `O` c)
associator' :: forall {s} {j :: s} {i :: s} (kk :: s -> s -> Type) {i :: s}
       {j :: s} (a :: kk i j) (b :: kk j i) (c :: kk i j).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Obj a
a Obj b
b Obj c
c = forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @kk @a @b @c ((Ob0 kk i, Ob0 kk j, Ob a, Ob a) => O (O a b) c ~> O a (O b c))
-> Obj a -> O (O a b) c ~> O a (O b c)
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj a
a ((Ob0 kk j, Ob0 kk i, Ob b, Ob b) => O (O a b) c ~> O a (O b c))
-> Obj b -> O (O a b) c ~> O a (O b c)
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj b
b ((Ob0 kk i, Ob0 kk j, Ob c, Ob c) => O (O a b) c ~> O a (O b c))
-> Obj c -> O (O a b) c ~> O a (O b c)
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj c
c

associatorInv'
  :: forall kk {i} {j} (a :: kk i j) b c. (Bicategory kk) => Obj a -> Obj b -> Obj c -> a `O` (b `O` c) ~> (a `O` b) `O` c
associatorInv' :: forall {s} {j :: s} {i :: s} (kk :: s -> s -> Type) {i :: s}
       {j :: s} (a :: kk i j) (b :: kk j i) (c :: kk i j).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' Obj a
a Obj b
b Obj c
c = forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @kk @a @b @c ((Ob0 kk i, Ob0 kk j, Ob a, Ob a) => O a (O b c) ~> O (O a b) c)
-> Obj a -> O a (O b c) ~> O (O a b) c
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj a
a ((Ob0 kk j, Ob0 kk i, Ob b, Ob b) => O a (O b c) ~> O (O a b) c)
-> Obj b -> O a (O b c) ~> O (O a b) c
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj b
b ((Ob0 kk i, Ob0 kk j, Ob c, Ob c) => O a (O b c) ~> O (O a b) c)
-> Obj c -> O a (O b c) ~> O (O a b) c
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj c
c

leftUnitorWith :: (Bicategory kk) => (c ~> (I :: kk i i)) -> a ~> b -> (c `O` a) ~> b
leftUnitorWith :: forall {s} {i :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i i) (b :: kk i i).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O c a ~> b
leftUnitorWith c ~> I
c a ~> b
ab = (O I b ~> b
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor (O I b ~> b) -> (O c a ~> O I b) -> O c a ~> b
forall (b :: kk i i) (c :: kk i i) (a :: kk i i).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> I
c (c ~> I) -> (a ~> b) -> O c a ~> O I b
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
ab)) ((Ob0 kk i, Ob0 kk i, Ob a, Ob b) => O c a ~> b)
-> (a ~> b) -> O c a ~> b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
ab

leftUnitorInvWith :: (Bicategory kk) => ((I :: kk i i) ~> c) -> a ~> b -> a ~> (c `O` b)
leftUnitorInvWith :: forall {s} {i :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i i) (b :: kk i i).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith I ~> c
c a ~> b
ab = ((I ~> c
c (I ~> c) -> (a ~> b) -> O I a ~> O c b
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
ab) (O I a ~> O c b) -> (a ~> O I a) -> a ~> O c b
forall (b :: kk i i) (c :: kk i i) (a :: kk i i).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> O I a
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv) ((Ob0 kk i, Ob0 kk i, Ob a, Ob b) => a ~> O c b)
-> (a ~> b) -> a ~> O c b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
ab

rightUnitorWith :: (Bicategory kk) => (c ~> (I :: kk i i)) -> a ~> b -> (a `O` c) ~> b
rightUnitorWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith c ~> I
c a ~> b
ab = (O b I ~> b
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O a I ~> a
rightUnitor (O b I ~> b) -> (O a c ~> O b I) -> O a c ~> b
forall (b :: kk i k) (c :: kk i k) (a :: kk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
ab (a ~> b) -> (c ~> I) -> O a c ~> O b I
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` c ~> I
c)) ((Ob0 kk i, Ob0 kk k, Ob a, Ob b) => O a c ~> b)
-> (a ~> b) -> O a c ~> b
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
ab

rightUnitorInvWith :: (Bicategory kk) => ((I :: kk i i) ~> c) -> a ~> b -> a ~> (b `O` c)
rightUnitorInvWith :: forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i k) (b :: kk i k).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O b c
rightUnitorInvWith I ~> c
c a ~> b
ab = ((a ~> b
ab (a ~> b) -> (I ~> c) -> O a I ~> O b c
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` I ~> c
c) (O a I ~> O b c) -> (a ~> O a I) -> a ~> O b c
forall (b :: kk i k) (c :: kk i k) (a :: kk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> O a I
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O a I
rightUnitorInv) ((Ob0 kk i, Ob0 kk k, Ob a, Ob b) => a ~> O b c)
-> (a ~> b) -> a ~> O b c
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ a ~> b
ab

appendObj
  :: forall {kk} {i} {j} {k} (a :: kk j k) (b :: kk i j) r
   . (Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b)
  => ((Ob (a `O` b)) => r)
  -> r
appendObj :: forall {s} {kk :: s -> s -> Type} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj Ob (O a b) => r
r = r
Ob (O a b) => r
(Ob0 kk i, Ob0 kk k, Ob (O a b), Ob (O a b)) => r
r ((Ob0 kk i, Ob0 kk k, Ob (O a b), Ob (O a b)) => r)
-> (O a b ~> O a b) -> r
forall (i :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> O a b ~> O a b
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

(||) :: (Bicategory kk) => ((a :: kk i j) ~> b) -> (c ~> d) -> O a c ~> O b d
|| :: forall {s} {i :: s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j) (c :: kk i i) (d :: kk i i).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
(||) = (a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {i :: s} (j :: s) (k :: s) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
o

(==) :: (CategoryOf k) => ((a :: k) ~> b) -> (b ~> c) -> a ~> c
a ~> b
f == :: forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== b ~> c
g = b ~> c
g (b ~> c) -> (a ~> b) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f

type Monad :: forall {kk} {a}. kk a a -> Constraint
class (Bicategory kk, Ob0 kk a) => Monad (t :: kk a a) where
  eta :: I ~> t
  mu :: t `O` t ~> t

type Comonad :: forall {kk} {a}. kk a a -> Constraint
class (Bicategory kk, Ob0 kk a) => Comonad (t :: kk a a) where
  epsilon :: t ~> I
  delta :: t ~> t `O` t

type Bimodule :: forall {kk} {a} {b}. kk a a -> kk b b -> kk b a -> Constraint
class (Monad s, Monad t) => Bimodule s t p where
  leftAction :: s `O` p ~> p
  rightAction :: p `O` t ~> p

instance {-# OVERLAPPABLE #-} (Monad s) => Bimodule s s s where
  leftAction :: O s s ~> s
leftAction = O s s ~> s
forall k (kk :: k -> k -> Type) (b :: k) (s :: kk b b).
Monad s =>
O s s ~> s
mu
  rightAction :: O s s ~> s
rightAction = O s s ~> s
forall k (kk :: k -> k -> Type) (b :: k) (s :: kk b b).
Monad s =>
O s s ~> s
mu

type Adjunction :: forall {kk} {c} {d}. kk c d -> kk d c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d) => Adjunction (l :: kk c d) (r :: kk d c) where
  unit :: I ~> r `O` l
  counit :: l `O` r ~> I

leftAdjunct
  :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) (a :: kk i c) b
   . (Adjunction l r, Ob a, Ob r, Ob l, Ob0 kk i)
  => l `O` a ~> b
  -> a ~> r `O` b
leftAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a, Ob r, Ob l, Ob0 kk i) =>
(O l a ~> b) -> a ~> O r b
leftAdjunct O l a ~> b
f =
  a ~> O I a
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
a ~> O I a
leftUnitorInv
    (a ~> O I a) -> (O I a ~> O (O r l) a) -> a ~> O (O r l) a
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (l :: kk c d) (r :: kk d c). Adjunction l r => I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @l @r (I ~> O r l) -> (a ~> a) -> O I a ~> O (O r l) a
forall {s} {i :: s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j) (c :: kk i i) (d :: kk i i).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall (a :: kk i c). (CategoryOf (kk i c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a
    (a ~> O (O r l) a)
-> (O (O r l) a ~> O r (O l a)) -> a ~> O r (O l a)
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @r @l @a
    (a ~> O r (O l a)) -> (O r (O l a) ~> O r b) -> a ~> O r b
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: kk d c). (CategoryOf (kk d c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r -> (O l a ~> b) -> O r (O l a) ~> O r b
forall {s} {i :: s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j) (c :: kk i i) (d :: kk i i).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| O l a ~> b
f

rightAdjunct
  :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) (a :: kk i c) b
   . (Adjunction l r, Ob b, Ob r, Ob l, Ob0 kk i)
  => a ~> r `O` b
  -> l `O` a ~> b
rightAdjunct :: forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob b, Ob r, Ob l, Ob0 kk i) =>
(a ~> O r b) -> O l a ~> b
rightAdjunct a ~> O r b
f =
  forall (a :: kk c d). (CategoryOf (kk c d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @l Obj l -> (a ~> O r b) -> O l a ~> O l (O r b)
forall {s} {i :: s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j) (c :: kk i i) (d :: kk i i).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| a ~> O r b
f
    (O l a ~> O l (O r b))
-> (O l (O r b) ~> O (O l r) b) -> O l a ~> O (O l r) b
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @l @r @b
    (O l a ~> O (O l r) b) -> (O (O l r) b ~> O I b) -> O l a ~> O I b
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (l :: kk c d) (r :: kk d c). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @l @r (O l r ~> I) -> (b ~> b) -> O (O l r) b ~> O I b
forall {s} {i :: s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j) (c :: kk i i) (d :: kk i i).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall (a :: kk i d). (CategoryOf (kk i d), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b
    (O l a ~> O I b) -> (O I b ~> b) -> O l a ~> b
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== O I b ~> b
forall {i :: s} {j :: s} (a :: kk i j).
(Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
forall {s} (kk :: CAT s) {i :: s} {j :: s} (a :: kk i j).
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob a) =>
O I a ~> a
leftUnitor