module Proarrow.Category.Bicategory.CategoryAsBi where

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

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

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 (i ~> j)
f o :: forall {k1 :: k} (i :: k) (j :: k) (a :: PLAINK k i j)
       (b :: PLAINK k i j) (c :: PLAINK k j k1) (d :: PLAINK k j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Id Maybe (j ~> k1)
g = Maybe (i ~> k1) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id (((j ~> k1) -> (i ~> j) -> i ~> k1)
-> Maybe (j ~> k1) -> Maybe (i ~> j) -> Maybe (i ~> k1)
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 ~> k1) -> (i ~> j) -> i ~> k1
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 ~> k1)
g Maybe (i ~> j)
f)
  leftUnitor :: forall (i :: k) (j :: k) (a :: PLAINK k i j). Obj a -> O I a ~> a
leftUnitor (Id Maybe (i ~> j)
p) = 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)
p
  leftUnitorInv :: forall (i :: k) (j :: k) (a :: PLAINK k i j). Obj a -> a ~> O I a
leftUnitorInv (Id Maybe (i ~> j)
p) = 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)
p
  rightUnitor :: forall (i :: k) (j :: k) (a :: PLAINK k i j). Obj a -> O a I ~> a
rightUnitor (Id Maybe (i ~> j)
p) = 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)
p
  rightUnitorInv :: forall (i :: k) (j :: k) (a :: PLAINK k i j). Obj a -> a ~> O a I
rightUnitorInv (Id Maybe (i ~> j)
p) = 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)
p
  associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: PLAINK k i j2)
       (b :: PLAINK k j2 j1) (c :: PLAINK k j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Id Maybe (i ~> j2)
p) (Id Maybe (j2 ~> j1)
q) (Id Maybe (j1 ~> k1)
r) = Maybe (i ~> k1) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id (((j1 ~> k1) -> (i ~> j1) -> i ~> k1)
-> Maybe (j1 ~> k1) -> Maybe (i ~> j1) -> Maybe (i ~> k1)
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 (j1 ~> k1) -> (i ~> j1) -> i ~> k1
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 (j1 ~> k1)
r (((j2 ~> j1) -> (i ~> j2) -> i ~> j1)
-> Maybe (j2 ~> j1) -> Maybe (i ~> j2) -> Maybe (i ~> j1)
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 (j2 ~> j1) -> (i ~> j2) -> i ~> j1
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 (j2 ~> j1)
q Maybe (i ~> j2)
p))
  associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: PLAINK k i j2)
       (b :: PLAINK k j2 j1) (c :: PLAINK k j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Id Maybe (i ~> j2)
p) (Id Maybe (j2 ~> j1)
q) (Id Maybe (j1 ~> k1)
r) = Maybe (i ~> k1) -> Category 'PLAIN 'PLAIN
forall {k} (a :: k) (b :: k).
(Ob a, Ob b) =>
Maybe (a ~> b) -> Category 'PLAIN 'PLAIN
Id (((j1 ~> k1) -> (i ~> j1) -> i ~> k1)
-> Maybe (j1 ~> k1) -> Maybe (i ~> j1) -> Maybe (i ~> k1)
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 (j1 ~> k1) -> (i ~> j1) -> i ~> k1
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 (j1 ~> k1)
r (((j2 ~> j1) -> (i ~> j2) -> i ~> j1)
-> Maybe (j2 ~> j1) -> Maybe (i ~> j2) -> Maybe (i ~> j1)
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 (j2 ~> j1) -> (i ~> j2) -> i ~> j1
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 (j2 ~> j1)
q Maybe (i ~> j2)
p))