{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.BiAsCategory where

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
import Proarrow.Functor (FunctorForRep (..))

newtype BI (kk :: CAT s) = B s

type Bi :: CAT (BI kk)
data Bi a b where
  Bi :: forall {kk} {j} {k} p. (Ob (p :: kk j k), Ob0 kk j, Ob0 kk k) => Bi (B j :: BI kk) (B k)

-- | The category of 0-cells and 1-cells of a bicategory, forgetting 2-cells.
instance (Bicategory kk) => CategoryOf (BI kk) where
  type (~>) = Bi
  type Ob @(BI kk) c = (Is B c, Ob0 kk (UN B c))

instance (Bicategory kk) => Promonad (Bi :: CAT (BI kk)) where
  id :: forall (a :: BI kk). Ob a => Bi a a
id @(B k) = forall (p :: kk (UN 'B a) (UN 'B a)).
(Ob p, Ob0 kk (UN 'B a), Ob0 kk (UN 'B a)) =>
Bi ('B (UN 'B a)) ('B (UN 'B a))
forall {s} {kk :: s -> s -> Type} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
Bi @(I :: kk k k)
  Bi @p . :: forall (b :: BI kk) (c :: BI kk) (a :: BI kk).
Bi b c -> Bi a b -> Bi a c
. Bi @q = forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @p @q (forall (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
forall {s} {kk :: s -> s -> Type} {j :: s} {k :: s} (p :: kk j k).
(Ob p, Ob0 kk j, Ob0 kk k) =>
Bi ('B j) ('B k)
Bi @(p `O` q))

instance (Bicategory kk) => Profunctor (Bi :: CAT (BI kk)) where
  dimap :: forall (c :: BI kk) (a :: BI kk) (b :: BI kk) (d :: BI kk).
(c ~> a) -> (b ~> d) -> Bi a b -> Bi c d
dimap = (c ~> a) -> (b ~> d) -> Bi a b -> Bi c d
Bi c a -> Bi b d -> Bi a b -> Bi 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 :: BI kk) (b :: BI kk) r.
((Ob a, Ob b) => r) -> Bi a b -> r
\\ Bi a b
Bi = r
(Ob a, Ob b) => r
r

data family Comp :: (kk j k, kk i j) +-> kk i k
instance (Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k) => FunctorForRep (Comp :: (kk j k, kk i j) +-> kk i k) where
  type Comp @ '(f, g) = (f `O` g)
  fmap :: forall (a :: (kk j k, kk i j)) (b :: (kk j k, kk i j)).
(a ~> b) -> (Comp @ a) ~> (Comp @ b)
fmap (a1 ~> b1
n :**: a2 ~> b2
m) = a1 ~> b1
n (a1 ~> b1) -> (a2 ~> b2) -> O a1 a2 ~> O b1 b2
forall {i :: k} {j :: k} {k :: k} (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` a2 ~> b2
m ((Ob a1, Ob b1) => O a1 a2 ~> O b1 b2)
-> (a1 ~> b1) -> O a1 a2 ~> O b1 b2
forall (a :: kk j k) (b :: kk j 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
\\ a1 ~> b1
n ((Ob a2, Ob b2) => O a1 a2 ~> O b1 b2)
-> (a2 ~> b2) -> O a1 a2 ~> O b1 b2
forall (a :: kk i j) (b :: kk i j) 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
\\ a2 ~> b2
m