module Proarrow.Category.Equipment.BiAsEquipment where

import Proarrow.Category.Bicategory (Bicategory (..), Ob0', leftUnitor', leftUnitorInv')
import Proarrow.Category.Bicategory.Bidiscrete (Bidiscrete (..), DiscreteK (..))
import Proarrow.Category.Equipment
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)

type data WKK kk i j = WK (kk i j)
type instance UN WK (WK p) = p

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

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

-- | A bicategory as a proarrow equipment with only identity arrows vertically.
instance (Bicategory kk) => HasCompanions (WKK kk) (DiscreteK (Ob0' kk)) where
  type Companion (WKK kk) DK = WK I
  mapCompanion :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j k)
       (g :: DiscreteK (Ob0' kk) j k).
(f ~> g) -> Companion (WKK kk) f ~> Companion (WKK kk) g
mapCompanion f ~> g
Bidiscrete f g
Bidiscrete = Obj I
Companion (WKK kk) f ~> Companion (WKK kk) g
forall (i :: s). Ob0 (WKK kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  compToId :: forall (k :: s).
Ob0 (DiscreteK (Ob0' kk)) k =>
Companion (WKK kk) I ~> I
compToId = (I ~> I) -> W (WK I) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W 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
  compFromId :: forall (k :: s).
Ob0 (DiscreteK (Ob0' kk)) k =>
I ~> Companion (WKK kk) I
compFromId = (I ~> I) -> W (WK I) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W 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
  compToCompose :: forall {i :: s} {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j k)
       (g :: DiscreteK (Ob0' kk) i j).
Obj f
-> Obj g
-> Companion (WKK kk) (O f g)
   ~> O (Companion (WKK kk) f) (Companion (WKK kk) g)
compToCompose Obj f
Bidiscrete f f
Bidiscrete Obj g
Bidiscrete g g
Bidiscrete = (I ~> O I I) -> W (WK I) (WK (O I I))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> I ~> O I I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> a ~> O I b
leftUnitorInv' 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)
  compFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j2 k)
       (g :: DiscreteK (Ob0' kk) j1 j2).
Obj f
-> Obj g
-> O (Companion (WKK kk) f) (Companion (WKK kk) g)
   ~> Companion (WKK kk) (O f g)
compFromCompose Obj f
Bidiscrete f f
Bidiscrete Obj g
Bidiscrete g g
Bidiscrete = (O I I ~> I) -> W (WK (O I I)) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> O I I ~> I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> O I a ~> b
leftUnitor' 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)

instance (Bicategory kk) => Equipment (WKK kk) (DiscreteK (Ob0' kk)) where
  type Conjoint (WKK kk) DK = WK I
  mapConjoint :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j k)
       (g :: DiscreteK (Ob0' kk) j k).
(f ~> g) -> Conjoint (WKK kk) g ~> Conjoint (WKK kk) f
mapConjoint f ~> g
Bidiscrete f g
Bidiscrete = Obj I
Conjoint (WKK kk) g ~> Conjoint (WKK kk) f
forall (i :: s). Ob0 (WKK kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  conjToId :: forall (k :: s).
Ob0 (DiscreteK (Ob0' kk)) k =>
Conjoint (WKK kk) I ~> I
conjToId = (I ~> I) -> W (WK I) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W 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
  conjFromId :: forall (k :: s).
Ob0 (DiscreteK (Ob0' kk)) k =>
I ~> Conjoint (WKK kk) I
conjFromId = (I ~> I) -> W (WK I) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W 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
  conjToCompose :: forall {k1 :: s} {j :: s} {k2 :: s} (f :: DiscreteK (Ob0' kk) j k2)
       (g :: DiscreteK (Ob0' kk) k1 j).
Obj f
-> Obj g
-> Conjoint (WKK kk) (O f g)
   ~> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f)
conjToCompose Obj f
Bidiscrete f f
Bidiscrete Obj g
Bidiscrete g g
Bidiscrete = (I ~> O I I) -> W (WK I) (WK (O I I))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> I ~> O I I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> a ~> O I b
leftUnitorInv' 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)
  conjFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j2 k)
       (g :: DiscreteK (Ob0' kk) j1 j2).
Obj f
-> Obj g
-> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f)
   ~> Conjoint (WKK kk) (O f g)
conjFromCompose Obj f
Bidiscrete f f
Bidiscrete Obj g
Bidiscrete g g
Bidiscrete = (O I I ~> I) -> W (WK (O I I)) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> O I I ~> I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> O I a ~> b
leftUnitor' 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)
  comConUnit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j k).
Obj f -> I ~> O (Conjoint (WKK kk) f) (Companion (WKK kk) f)
comConUnit Obj f
Bidiscrete f f
Bidiscrete = (I ~> O I I) -> W (WK I) (WK (O I I))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> I ~> O I I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> a ~> O I b
leftUnitorInv' 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)
  comConCounit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk) j k).
Obj f -> O (Companion (WKK kk) f) (Conjoint (WKK kk) f) ~> I
comConCounit Obj f
Bidiscrete f f
Bidiscrete = (O I I ~> I) -> W (WK (O I I)) (WK I)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> W (WK a) (WK b)
W ((I ~> I) -> O I I ~> I
forall {s} (kk :: CAT s) (i :: s) (j :: s) (a :: kk i j)
       (b :: kk i j).
Bicategory kk =>
(a ~> b) -> O I a ~> b
leftUnitor' 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)