module Proarrow.Category.Equipment.Quintet where

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Bicategory.MonoidalAsBi (Mon2 (..), MonK (..))
import Proarrow.Category.Equipment (HasCompanions (..), Sq (..), vArr)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)

type data QKK kk i j = QK (kk i j)
type instance UN QK (QK p) = p

type QuintetSq (f :: kk a b) (g :: kk a c) (h :: kk b d) (k :: kk c d) = Sq '(QK f, h) '(QK k, g)

type Q2 :: CAT (QKK kk i j)
data Q2 a b where
  Q2 :: a ~> b -> Q2 (QK a) (QK b)
instance (CategoryOf (kk i j)) => Profunctor (Q2 :: CAT (QKK kk i j)) where
  dimap :: forall (c :: QKK kk i j) (a :: QKK kk i j) (b :: QKK kk i j)
       (d :: QKK kk i j).
(c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d
dimap = (c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d
Q2 c a -> Q2 b d -> Q2 a b -> Q2 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 :: QKK kk i j) (b :: QKK kk i j) r.
((Ob a, Ob b) => r) -> Q2 a b -> r
\\ Q2 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 (CategoryOf (kk i j)) => Promonad (Q2 :: CAT (QKK kk i j)) where
  id :: forall (a :: QKK kk i j). Ob a => Q2 a a
id = (UN QK a ~> UN QK a) -> Q2 (QK (UN QK a)) (QK (UN QK a))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 UN QK a ~> UN QK 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
  Q2 a ~> b
f . :: forall (b :: QKK kk i j) (c :: QKK kk i j) (a :: QKK kk i j).
Q2 b c -> Q2 a b -> Q2 a c
. Q2 a ~> b
g = (a ~> b) -> Q2 (QK a) (QK b)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (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)
instance (CategoryOf (kk i j)) => CategoryOf (QKK kk i j) where
  type (~>) = Q2
  type Ob (a :: QKK kk i j) = (Is QK a, Ob (UN QK a))

instance (Bicategory kk) => Bicategory (QKK kk) where
  type Ob0 (QKK kk) k = Ob0 kk k
  type I = QK I
  type O a b = QK (UN QK a `O` UN QK b)
  (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: s) (j :: s) (ps :: QKK kk i j) (qs :: QKK kk i j) r.
((Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Q2 a ~> b
f = r
(Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r
(Ob0 (QKK kk) i, Ob0 (QKK 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
  iObj :: forall (i :: s). Ob0 (QKK kk) i => Obj I
iObj = (I ~> I) -> Q2 (QK I) (QK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 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
  Q2 a ~> b
f o :: forall {i :: s} (j :: s) (k :: s) (a :: QKK kk j k)
       (b :: QKK kk j k) (c :: QKK kk i j) (d :: QKK kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Q2 a ~> b
g = (O a a ~> O b b) -> Q2 (QK (O a a)) (QK (O b b))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (a ~> b
f (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
g)
  leftUnitor :: forall {i :: s} {j :: s} (a :: QKK kk i j).
(Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) =>
O I a ~> a
leftUnitor = (O I (UN QK a) ~> UN QK a)
-> Q2 (QK (O I (UN QK a))) (QK (UN QK a))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 O I (UN QK a) ~> UN QK 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 :: QKK kk i j).
(Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN QK a ~> O I (UN QK a))
-> Q2 (QK (UN QK a)) (QK (O I (UN QK a)))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 UN QK a ~> O I (UN QK 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 :: QKK kk i j).
(Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) =>
O a I ~> a
rightUnitor = (O (UN QK a) I ~> UN QK a)
-> Q2 (QK (O (UN QK a) I)) (QK (UN QK a))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 O (UN QK a) I ~> UN QK 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 :: QKK kk i j).
(Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN QK a ~> O (UN QK a) I)
-> Q2 (QK (UN QK a)) (QK (O (UN QK a) I))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 UN QK a ~> O (UN QK 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 :: QKK kk j k)
       (b :: QKK kk i j) (c :: QKK kk h i).
(Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK kk) k,
 Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @(QK p) @(QK q) @(QK r) = (O (O (UN QK a) (UN QK b)) (UN QK c)
 ~> O (UN QK a) (O (UN QK b) (UN QK c)))
-> Q2
     (QK (O (O (UN QK a) (UN QK b)) (UN QK c)))
     (QK (O (UN QK a) (O (UN QK b) (UN QK c))))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (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 :: QKK kk j k)
       (b :: QKK kk i j) (c :: QKK kk h i).
(Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK kk) k,
 Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @(QK p) @(QK q) @(QK r) = (O (UN QK a) (O (UN QK b) (UN QK c))
 ~> O (O (UN QK a) (UN QK b)) (UN QK c))
-> Q2
     (QK (O (UN QK a) (O (UN QK b) (UN QK c))))
     (QK (O (O (UN QK a) (UN QK b)) (UN QK c)))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (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)

instance (Bicategory kk) => HasCompanions (QKK kk) kk where
  type Companion (QKK kk) f = QK f
  mapCompanion :: forall {j :: c} {k :: c} (f :: kk j k) (g :: kk j k).
(f ~> g) -> Companion (QKK kk) f ~> Companion (QKK kk) g
mapCompanion f ~> g
f = (f ~> g) -> Q2 (QK f) (QK g)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 f ~> g
f
  compToId :: forall (k :: c). Ob0 kk k => Companion (QKK kk) I ~> I
compToId = (I ~> I) -> Q2 (QK I) (QK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 I ~> I
forall (i :: c). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  compFromId :: forall (k :: c). Ob0 kk k => I ~> Companion (QKK kk) I
compFromId = (I ~> I) -> Q2 (QK I) (QK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 I ~> I
forall (i :: c). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  compToCompose :: forall {i :: c} {j :: c} {k :: c} (f :: kk j k) (g :: kk i j).
Obj f
-> Obj g
-> Companion (QKK kk) (O f g)
   ~> O (Companion (QKK kk) f) (Companion (QKK kk) g)
compToCompose Obj f
f Obj g
g = (O f g ~> O f g) -> Q2 (QK (O f g)) (QK (O f g))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj f
f Obj f -> Obj g -> O f g ~> O f g
forall {i :: c} (j :: c) (k :: c) (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` Obj g
g)
  compFromCompose :: forall {j1 :: c} {j2 :: c} {k :: c} (f :: kk j2 k) (g :: kk j1 j2).
Obj f
-> Obj g
-> O (Companion (QKK kk) f) (Companion (QKK kk) g)
   ~> Companion (QKK kk) (O f g)
compFromCompose Obj f
f Obj g
g = (O f g ~> O f g) -> Q2 (QK (O f g)) (QK (O f g))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj f
f Obj f -> Obj g -> O f g ~> O f g
forall {i :: c} (j :: c) (k :: c) (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` Obj g
g)

-- | BiPara as a quintet construction.
type BiParaSq (a :: k) b p q = QuintetSq (MK p :: MonK k '() '()) (MK b) (MK a) (MK q :: MonK k '() '())

bipara :: (Ob p, Ob q, Ob a, Ob b) => a M.** p ~> q M.** b -> BiParaSq a b p q
bipara :: forall {k} (p :: k) (q :: k) (a :: k) (b :: k).
(Ob p, Ob q, Ob a, Ob b) =>
((a ** p) ~> (q ** b)) -> BiParaSq a b p q
bipara (a ** p) ~> (q ** b)
n = (O (Companion (QKK (MonK k)) ('MK a)) (QK ('MK p))
 ~> O (QK ('MK q)) (Companion (QKK (MonK k)) ('MK b)))
-> Sq '(QK ('MK p), 'MK a) '(QK ('MK q), 'MK b)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (('MK (a ** p) ~> 'MK (q ** b))
-> Q2 (QK ('MK (a ** p))) (QK ('MK (q ** b)))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (((a ** p) ~> (q ** b)) -> Mon2 ('MK (a ** p)) ('MK (q ** b))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 (a ** p) ~> (q ** b)
n))

reparam :: forall {k} (a :: k) (b :: k). (M.Monoidal k) => a ~> b -> BiParaSq a b M.Unit M.Unit
reparam :: forall {k} (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> BiParaSq a b Unit Unit
reparam a ~> b
f = ('MK a ~> 'MK b) -> Sq '(I, 'MK a) '(I, 'MK b)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
vArr ((a ~> b) -> Mon2 ('MK a) ('MK b)
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 a ~> b
f)