{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.Op where

import Proarrow.Category.Bicategory (Bicategory(..))
import Proarrow.Category.Bicategory.Kan (RightKanExtension(..), LeftKanExtension(..), RightKanLift(..), LeftKanLift(..))
import Proarrow.Core (CategoryOf(..), Profunctor(..), CAT, Promonad (..), dimapDefault, UN, Is)


type OPK :: CAT k -> CAT k
newtype OPK kk j k = OP (kk k j)
type instance UN OP (OP k) = k

type Op :: CAT (OPK kk k j)
data Op a b where
  Op :: a ~> b -> Op (OP a) (OP b)

instance (CategoryOf (kk k j)) => Profunctor (Op :: CAT (OPK kk j k)) where
  dimap :: forall (c :: OPK kk j k) (a :: OPK kk j k) (b :: OPK kk j k)
       (d :: OPK kk j k).
(c ~> a) -> (b ~> d) -> Op a b -> Op c d
dimap = (c ~> a) -> (b ~> d) -> Op a b -> Op c d
Op c a -> Op b d -> Op a b -> Op 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 :: OPK kk j k) (b :: OPK kk j k) r.
((Ob a, Ob b) => r) -> Op a b -> r
\\ Op a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: kk k j) (b :: kk k 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
f
instance (CategoryOf (kk k j)) => Promonad (Op :: CAT (OPK kk j k)) where
  id :: forall (a :: OPK kk j k). Ob a => Op a a
id = (UN 'OP a ~> UN 'OP a) -> Op ('OP (UN 'OP a)) ('OP (UN 'OP a))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op UN 'OP a ~> UN 'OP a
forall (a :: kk k j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Op a ~> b
f . :: forall (b :: OPK kk j k) (c :: OPK kk j k) (a :: OPK kk j k).
Op b c -> Op a b -> Op a c
. Op a ~> b
g = (a ~> b) -> Op ('OP a) ('OP b)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: kk k j) (c :: kk k j) (a :: kk k 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 k j)) => CategoryOf (OPK kk j k) where
  type (~>) = Op
  type Ob a = (Is OP a, Ob (UN OP a))

-- | Create a dual of a bicategory by reversing the 1-cells.
instance Bicategory kk => Bicategory (OPK kk) where
  type Ob0 (OPK kk) k = Ob0 kk k
  type I = OP I
  type O a b = OP (UN OP b `O` UN OP a)
  (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: k) (j :: k) (ps :: OPK kk i j) (qs :: OPK kk i j) r.
((Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Op a ~> b
f = r
(Ob0 kk j, Ob0 kk i, Ob a, Ob b) => r
(Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob ps, Ob qs) => r
r ((Ob0 kk j, Ob0 kk i, Ob a, Ob b) => r) -> (a ~> b) -> r
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall k (kk :: CAT k) (i :: k) (j :: k) (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
  Op a ~> b
f o :: forall {k1 :: k} (i :: k) (j :: k) (a :: OPK kk i j)
       (b :: OPK kk i j) (c :: OPK kk j k1) (d :: OPK kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Op a ~> b
g = (O a a ~> O b b) -> Op ('OP (O a a)) ('OP (O b b))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (a ~> b
g (a ~> b) -> (a ~> b) -> O a a ~> O b b
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
f)
  leftUnitor :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> O I a ~> a
leftUnitor (Op a ~> b
p) = (O b I ~> b) -> Op ('OP (O b I)) ('OP b)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> O b I ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
rightUnitor a ~> b
Obj b
p)
  leftUnitorInv :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> a ~> O I a
leftUnitorInv (Op a ~> b
p) = (b ~> O b I) -> Op ('OP b) ('OP (O b I))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> b ~> O b I
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
rightUnitorInv a ~> b
Obj b
p)
  rightUnitor :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> O a I ~> a
rightUnitor (Op a ~> b
p) = (O I b ~> b) -> Op ('OP (O I b)) ('OP b)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> O I b ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
leftUnitor a ~> b
Obj b
p)
  rightUnitorInv :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> a ~> O a I
rightUnitorInv (Op a ~> b
p) = (b ~> O I b) -> Op ('OP b) ('OP (O I b))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> b ~> O I b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
leftUnitorInv a ~> b
Obj b
p)
  associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: OPK kk i j2)
       (b :: OPK kk j2 j1) (c :: OPK kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Op a ~> b
p) (Op a ~> b
q) (Op a ~> b
r) = (O b (O b b) ~> O (O b b) b)
-> Op ('OP (O b (O b b))) ('OP (O (O b b) b))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> Obj b -> Obj b -> O b (O b b) ~> O (O b b) b
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv a ~> b
Obj b
r a ~> b
Obj b
q a ~> b
Obj b
p)
  associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: OPK kk i j2)
       (b :: OPK kk j2 j1) (c :: OPK kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Op a ~> b
p) (Op a ~> b
q) (Op a ~> b
r) = (O (O b b) b ~> O b (O b b))
-> Op ('OP (O (O b b) b)) ('OP (O b (O b b)))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (Obj b -> Obj b -> Obj b -> O (O b b) b ~> O b (O b b)
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator a ~> b
Obj b
r a ~> b
Obj b
q a ~> b
Obj b
p)

instance RightKanExtension j f => RightKanLift (OP j) (OP f) where
  type Rift (OP j) (OP f) = OP (Ran j f)
  rift :: O (Rift ('OP j) ('OP f)) ('OP j) ~> 'OP f
rift = (O j (Ran j f) ~> f) -> Op ('OP (O j (Ran j f))) ('OP f)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk k d) (f :: kk k e).
RightKanExtension j f =>
O j (Ran j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O j (Ran j f) ~> f
ran @j @f)
  riftUniv :: forall (g :: OPK kk e d).
Ob g =>
(O g ('OP j) ~> 'OP f) -> g ~> Rift ('OP j) ('OP f)
riftUniv (Op a ~> b
n) = (UN 'OP g ~> Ran j f) -> Op ('OP (UN 'OP g)) ('OP (Ran j f))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk k d) (f :: kk k e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O j g ~> f) -> g ~> Ran j f
ranUniv @j @f a ~> b
O j (UN 'OP g) ~> f
n)

instance LeftKanExtension j f => LeftKanLift (OP j) (OP f) where
  type Lift (OP j) (OP f) = OP (Lan j f)
  lift :: 'OP f ~> O (Lift ('OP j) ('OP f)) ('OP j)
lift = (f ~> O j (Lan j f)) -> Op ('OP f) ('OP (O j (Lan j f)))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk k d) (f :: kk k e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O j (Lan j f)
lan @j @f)
  liftUniv :: forall (g :: OPK kk e d).
Ob g =>
('OP f ~> O g ('OP j)) -> Lift ('OP j) ('OP f) ~> g
liftUniv (Op a ~> b
n) = (Lan j f ~> UN 'OP g) -> Op ('OP (Lan j f)) ('OP (UN 'OP g))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk k d) (f :: kk k e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O j g) -> Lan j f ~> g
lanUniv @j @f f ~> O j (UN 'OP g)
a ~> b
n)

instance RightKanLift j f => RightKanExtension (OP j) (OP f) where
  type Ran (OP j) (OP f) = OP (Rift j f)
  ran :: O ('OP j) (Ran ('OP j) ('OP f)) ~> 'OP f
ran = (O (Rift j f) j ~> f) -> Op ('OP (O (Rift j f) j)) ('OP f)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk d j) (f :: kk e j).
RightKanLift j f =>
O (Rift j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O (Rift j f) j ~> f
rift @j @f)
  ranUniv :: forall (g :: OPK kk d e).
Ob g =>
(O ('OP j) g ~> 'OP f) -> g ~> Ran ('OP j) ('OP f)
ranUniv (Op a ~> b
n) = (UN 'OP g ~> Rift j f) -> Op ('OP (UN 'OP g)) ('OP (Rift j f))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk d j) (f :: kk e j) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O g j ~> f) -> g ~> Rift j f
riftUniv @j @f a ~> b
O (UN 'OP g) j ~> f
n)

instance LeftKanLift j f => LeftKanExtension (OP j) (OP f) where
  type Lan (OP j) (OP f) = OP (Lift j f)
  lan :: 'OP f ~> O ('OP j) (Lan ('OP j) ('OP f))
lan = (f ~> O (Lift j f) j) -> Op ('OP f) ('OP (O (Lift j f) j))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk d j) (f :: kk e j).
LeftKanLift j f =>
f ~> O (Lift j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O (Lift j f) j
lift @j @f)
  lanUniv :: forall (g :: OPK kk d e).
Ob g =>
('OP f ~> O ('OP j) g) -> Lan ('OP j) ('OP f) ~> g
lanUniv (Op a ~> b
n) = (Lift j f ~> UN 'OP g) -> Op ('OP (Lift j f)) ('OP (UN 'OP g))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk j k).
(a ~> b) -> Op ('OP a) ('OP b)
Op (forall (j :: kk d j) (f :: kk e j) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O g j) -> Lift j f ~> g
liftUniv @j @f f ~> O (UN 'OP g) j
a ~> b
n)