module Proarrow.Category.Bicategory.Sub where

import Data.Kind (Type, Constraint)
import Prelude (($))

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

type family IsOb (tag :: Type) (a :: k) :: Constraint

type SUBCAT :: forall {k}. Type -> CAT k -> CAT k
type data SUBCAT tag kk i j = SUB (kk i j)
type instance UN SUB (SUB p) = p

type Sub :: CAT (SUBCAT ob kk i j)
data Sub a b where
  Sub :: (IsOb tag a, IsOb tag b) => a ~> b -> Sub (SUB a :: SUBCAT tag kk i j) (SUB b)

instance (Profunctor ((~>) :: CAT (kk i j))) => Profunctor (Sub :: CAT (SUBCAT tag kk i j)) where
  dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j)
       (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j).
(c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
dimap = (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
Sub c a -> Sub b d -> Sub a b -> Sub 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 :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Sub a ~> b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
p

instance (Promonad ((~>) :: CAT (kk i j))) => Promonad (Sub :: CAT (SUBCAT tag kk i j)) where
  id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a
id = (UN SUB a ~> UN SUB a) -> Sub (SUB (UN SUB a)) (SUB (UN SUB a))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub UN SUB a ~> UN SUB a
forall (a :: kk i j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Sub a ~> b
f . :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j)
       (a :: SUBCAT tag kk i j).
Sub b c -> Sub a b -> Sub a c
. Sub a ~> b
g = (a ~> b) -> Sub (SUB a) (SUB b)
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (a ~> b
f (a ~> b) -> (a ~> a) -> 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
. a ~> a
a ~> b
g)

-- | The subcategory with objects with instances of the given constraint `IsOb tag`.
instance (CategoryOf (kk i j)) => CategoryOf (SUBCAT tag kk i j) where
  type (~>) = Sub
  type Ob (a :: SUBCAT tag kk i j) = (Is SUB a, Ob (UN SUB a), IsOb tag (UN SUB a))

class (IsOb tag (a `O` b)) => IsObO tag kk i j k (a :: kk j k) (b :: kk i j)
instance (IsOb tag (a `O` b)) => IsObO tag kk i j k (a :: kk j k) (b :: kk i j)

class (IsOb tag (I :: kk i i)) => IsObI tag kk i
instance (IsOb tag (I :: kk i i)) => IsObI tag kk i

instance
  ( Bicategory kk
  , forall i. (Ob0 kk i) => IsObI tag kk i
  , forall i j k (a :: kk j k) (b :: kk i j). (IsOb tag a, IsOb tag b) => IsObO tag kk i j k a b
  )
  => Bicategory (SUBCAT tag kk)
  where
  type Ob0 (SUBCAT tag kk) k = Ob0 kk k
  type I = SUB I
  type p `O` q = SUB (UN SUB p `O` UN SUB q)
  iObj :: forall (i :: s). Ob0 (SUBCAT tag kk) i => Obj I
iObj = (I ~> I) -> Sub (SUB I) (SUB I)
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub I ~> I
forall (i :: s). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  Sub a ~> b
m o :: forall {i :: s} (j :: s) (k :: s) (a :: SUBCAT tag kk j k)
       (b :: SUBCAT tag kk j k) (c :: SUBCAT tag kk i j)
       (d :: SUBCAT tag kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Sub a ~> b
n = (O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub ((O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b)))
-> (O a a ~> O b b) -> Sub (SUB (O a a)) (SUB (O b b))
forall a b. (a -> b) -> a -> b
$ a ~> b
m (a ~> b) -> (a ~> b) -> O a a ~> O b 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
n
  (Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: s) (j :: s) (ps :: SUBCAT tag kk i j)
       (qs :: SUBCAT tag kk i j) r.
((Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Sub a ~> b
f = r
(Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r
r ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r) -> (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
\\\ a ~> b
f
  leftUnitor :: forall {i :: s} {j :: s} (a :: SUBCAT tag kk i j).
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob a) =>
O I a ~> a
leftUnitor = (O I (UN SUB a) ~> UN SUB a)
-> Sub (SUB (O I (UN SUB a))) (SUB (UN SUB a))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub O I (UN SUB a) ~> UN SUB 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
  leftUnitorInv :: forall {i :: s} {j :: s} (a :: SUBCAT tag kk i j).
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN SUB a ~> O I (UN SUB a))
-> Sub (SUB (UN SUB a)) (SUB (O I (UN SUB a)))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub UN SUB a ~> O I (UN SUB 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
  rightUnitor :: forall {i :: s} {j :: s} (a :: SUBCAT tag kk i j).
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob a) =>
O a I ~> a
rightUnitor = (O (UN SUB a) I ~> UN SUB a)
-> Sub (SUB (O (UN SUB a) I)) (SUB (UN SUB a))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub O (UN SUB a) I ~> UN SUB 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
  rightUnitorInv :: forall {i :: s} {j :: s} (a :: SUBCAT tag kk i j).
(Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN SUB a ~> O (UN SUB a) I)
-> Sub (SUB (UN SUB a)) (SUB (O (UN SUB a) I))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub UN SUB a ~> O (UN SUB 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
  associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: SUBCAT tag kk j k)
       (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i).
(Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i,
 Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag kk) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @(SUB p) @(SUB q) @(SUB r) = (O (O (UN SUB a) (UN SUB b)) (UN SUB c)
 ~> O (UN SUB a) (O (UN SUB b) (UN SUB c)))
-> Sub
     (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c)))
     (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c))))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub ((O (O (UN SUB a) (UN SUB b)) (UN SUB c)
  ~> O (UN SUB a) (O (UN SUB b) (UN SUB c)))
 -> Sub
      (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c)))
      (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c)))))
-> (O (O (UN SUB a) (UN SUB b)) (UN SUB c)
    ~> O (UN SUB a) (O (UN SUB b) (UN SUB c)))
-> Sub
     (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c)))
     (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c))))
forall a b. (a -> b) -> a -> b
$ 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 @p @q @r
  associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: SUBCAT tag kk j k)
       (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i).
(Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i,
 Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag kk) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @(SUB p) @(SUB q) @(SUB r) = (O (UN SUB a) (O (UN SUB b) (UN SUB c))
 ~> O (O (UN SUB a) (UN SUB b)) (UN SUB c))
-> Sub
     (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c))))
     (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c)))
forall {k} tag (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j).
(IsOb tag a, IsOb tag b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub ((O (UN SUB a) (O (UN SUB b) (UN SUB c))
  ~> O (O (UN SUB a) (UN SUB b)) (UN SUB c))
 -> Sub
      (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c))))
      (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c))))
-> (O (UN SUB a) (O (UN SUB b) (UN SUB c))
    ~> O (O (UN SUB a) (UN SUB b)) (UN SUB c))
-> Sub
     (SUB (O (UN SUB a) (O (UN SUB b) (UN SUB c))))
     (SUB (O (O (UN SUB a) (UN SUB b)) (UN SUB c)))
forall a b. (a -> b) -> a -> b
$ 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 @p @q @r