module Proarrow.Category.Bicategory.CategoryAsBi where

import Prelude (Maybe (..), liftA2, (>>), type (~))

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)

type PLAINK :: forall k -> CAT k
data PLAINK k i j = PLAIN -- should be @PLAIN (i ~> j)@ storing a value at type level, but that needs dependent types

type Category :: CAT (PLAINK k i j)
data Category as bs where
  Id :: forall {k} a b. (Ob a, Ob b) => Maybe (a ~> b) -> Category (PLAIN :: PLAINK k (a :: k) (b :: k)) PLAIN

instance (CategoryOf k, Ob i, Ob j) => Profunctor (Category :: CAT (PLAINK k i j)) where
  dimap :: forall (c :: PLAINK k i j) (a :: PLAINK k i j) (b :: PLAINK k i j)
       (d :: PLAINK k i j).
(c ~> a) -> (b ~> d) -> Category a b -> Category c d
dimap = (c ~> a) -> (b ~> d) -> Category a b -> Category c d
Category c a -> Category b d -> Category a b -> Category c d
forall {k} (p :: PRO 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 :: PLAINK k i j) (b :: PLAINK k i j) r.
((Ob a, Ob b) => r) -> Category a b -> r
\\ Id{} = r
(Ob a, Ob b) => r
r
instance (CategoryOf k, Ob i, Ob j) => Promonad (Category :: CAT (PLAINK k i j)) where
  id :: forall (a :: PLAINK k i j). Ob a => Category a a
id = Maybe (i ~> j) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id Maybe (i ~> j)
forall a. Maybe a
Nothing
  Id Maybe (i ~> j)
f . :: forall (b :: PLAINK k i j) (c :: PLAINK k i j) (a :: PLAINK k i j).
Category b c -> Category a b -> Category a c
. Id Maybe (i ~> j)
g = Maybe (i ~> j) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id (Maybe (i ~> j)
f Maybe (i ~> j) -> Maybe (i ~> j) -> Maybe (i ~> j)
forall a b. Maybe a -> Maybe b -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Maybe (i ~> j)
g) -- f and g should be the same, but this isn't checked by the type system
instance (CategoryOf k, Ob i, Ob j) => CategoryOf (PLAINK k i j) where
  type (~>) = Category
  type Ob a = (a ~ PLAIN)

instance (CategoryOf k) => Bicategory (PLAINK k) where
  type Ob0 (PLAINK k) a = Ob a
  type I = PLAIN
  type O PLAIN PLAIN = PLAIN
  (Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: k) (j :: k) (ps :: PLAINK k i j) (qs :: PLAINK k i j)
       r.
((Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Id{} = r
(Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob ps, Ob qs) => r
r
  Id Maybe (j ~> k)
f o :: forall {i :: k} (j :: k) (k :: k) (a :: PLAINK k j k)
       (b :: PLAINK k j k) (c :: PLAINK k i j) (d :: PLAINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Id Maybe (i ~> j)
g = Maybe (i ~> k) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id (((j ~> k) -> (i ~> j) -> i ~> k)
-> Maybe (j ~> k) -> Maybe (i ~> j) -> Maybe (i ~> k)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (j ~> k) -> (i ~> j) -> i ~> k
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
(.) Maybe (j ~> k)
f Maybe (i ~> j)
g)
  leftUnitor :: forall {i :: k} {j :: k} (a :: PLAINK k i j).
(Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) =>
O I a ~> a
leftUnitor = O I a ~> a
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k i j). Ob a => Category a a
id
  leftUnitorInv :: forall {i :: k} {j :: k} (a :: PLAINK k i j).
(Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) =>
a ~> O I a
leftUnitorInv = a ~> O I a
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k i j). Ob a => Category a a
id
  rightUnitor :: forall {i :: k} {j :: k} (a :: PLAINK k i j).
(Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) =>
O a I ~> a
rightUnitor = O a I ~> a
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k i j). Ob a => Category a a
id
  rightUnitorInv :: forall {i :: k} {j :: k} (a :: PLAINK k i j).
(Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) =>
a ~> O a I
rightUnitorInv = a ~> O a I
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k i j). Ob a => Category a a
id
  associator :: forall {h :: k} {i :: k} {j :: k} {k :: k} (a :: PLAINK k j k)
       (b :: PLAINK k i j) (c :: PLAINK k h i).
(Ob0 (PLAINK k) h, Ob0 (PLAINK k) i, Ob0 (PLAINK k) j,
 Ob0 (PLAINK k) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator = O (O a b) c ~> O a (O b c)
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k h k). Ob a => Category a a
id
  associatorInv :: forall {h :: k} {i :: k} {j :: k} {k :: k} (a :: PLAINK k j k)
       (b :: PLAINK k i j) (c :: PLAINK k h i).
(Ob0 (PLAINK k) h, Ob0 (PLAINK k) i, Ob0 (PLAINK k) j,
 Ob0 (PLAINK k) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv = O a (O b c) ~> O (O a b) c
Category 'PLAIN 'PLAIN
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: PLAINK k h k). Ob a => Category a a
id