module Proarrow.Category.Bicategory.Co where

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

type COK :: CAT k -> CAT k
newtype COK kk j k = CO (kk j k)
type instance UN CO (CO k) = k

type Co :: CAT (COK kk j k)
data Co a b where
  Co :: b ~> a -> Co (CO a) (CO b)

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

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

instance Adjunction f g => Adjunction (CO g) (CO f) where
  unit :: I ~> O ('CO f) ('CO g)
unit = (O f g ~> I) -> Co ('CO I) ('CO (O f g))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (l :: kk j k) (r :: kk k j). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @f @g)
  counit :: O ('CO g) ('CO f) ~> I
counit = (I ~> O g f) -> Co ('CO (O g f)) ('CO I)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (l :: kk j k) (r :: kk k j). Adjunction l r => I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @f @g)

instance (Comonad m) => Monad (CO m) where
  eta :: I ~> 'CO m
eta = (m ~> I) -> Co ('CO I) ('CO m)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co m ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon
  mu :: O ('CO m) ('CO m) ~> 'CO m
mu = (m ~> O m m) -> Co ('CO (O m m)) ('CO m)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co m ~> O m m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta

instance (Monad m) => Comonad (CO m) where
  epsilon :: 'CO m ~> I
epsilon = (I ~> m) -> Co ('CO m) ('CO I)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co I ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  delta :: 'CO m ~> O ('CO m) ('CO m)
delta = (O m m ~> m) -> Co ('CO m) ('CO (O m m))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co O m m ~> m
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

instance (RightKanExtension j f) => LeftKanExtension (CO j) (CO f) where
  type Lan (CO j) (CO f) = CO (Ran j f)
  lan :: 'CO f ~> O (Lan ('CO j) ('CO f)) ('CO j)
lan = (O (Ran j f) j ~> f) -> Co ('CO f) ('CO (O (Ran j f) j))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk j d) (f :: kk j e).
RightKanExtension j f =>
O (Ran j f) j ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
RightKanExtension j f =>
O (Ran j f) j ~> f
ran @j @f)
  lanUniv :: forall (g :: COK kk d e).
Ob g =>
('CO f ~> O g ('CO j)) -> Lan ('CO j) ('CO f) ~> g
lanUniv (Co b ~> a
n) = (UN 'CO g ~> Ran j f) -> Co ('CO (Ran j f)) ('CO (UN 'CO g))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk j d) (f :: kk j e) (g :: kk d e).
(RightKanExtension j f, Ob g) =>
(O g j ~> 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 g j ~> f) -> g ~> Ran j f
ranUniv @j @f b ~> a
O (UN 'CO g) j ~> f
n)

instance (LeftKanExtension j f) => RightKanExtension (CO j) (CO f) where
  type Ran (CO j) (CO f) = CO (Lan j f)
  ran :: O (Ran ('CO j) ('CO f)) ('CO j) ~> 'CO f
ran = (f ~> O (Lan j f) j) -> Co ('CO (O (Lan j f) j)) ('CO f)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk j d) (f :: kk j e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk c d)
       (f :: kk c e).
LeftKanExtension j f =>
f ~> O (Lan j f) j
lan @j @f)
  ranUniv :: forall (g :: COK kk d e).
Ob g =>
(O g ('CO j) ~> 'CO f) -> g ~> Ran ('CO j) ('CO f)
ranUniv (Co b ~> a
n) = (Lan j f ~> UN 'CO g) -> Co ('CO (UN 'CO g)) ('CO (Lan j f))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk j d) (f :: kk j e) (g :: kk d e).
(LeftKanExtension j f, Ob g) =>
(f ~> O g j) -> 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 g j) -> Lan j f ~> g
lanUniv @j @f f ~> O (UN 'CO g) j
b ~> a
n)

instance (RightKanLift j f) => LeftKanLift (CO j) (CO f) where
  type Lift (CO j) (CO f) = CO (Rift j f)
  lift :: 'CO f ~> O ('CO j) (Lift ('CO j) ('CO f))
lift = (O j (Rift j f) ~> f) -> Co ('CO f) ('CO (O j (Rift j f)))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk d k) (f :: kk e k).
RightKanLift j f =>
O j (Rift j f) ~> f
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
RightKanLift j f =>
O j (Rift j f) ~> f
rift @j @f)
  liftUniv :: forall (g :: COK kk e d).
Ob g =>
('CO f ~> O ('CO j) g) -> Lift ('CO j) ('CO f) ~> g
liftUniv (Co b ~> a
n) = (UN 'CO g ~> Rift j f) -> Co ('CO (Rift j f)) ('CO (UN 'CO g))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk d k) (f :: kk e k) (g :: kk e d).
(RightKanLift j f, Ob g) =>
(O j g ~> 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 j g ~> f) -> g ~> Rift j f
riftUniv @j @f b ~> a
O j (UN 'CO g) ~> f
n)

instance (LeftKanLift j f) => RightKanLift (CO j) (CO f) where
  type Rift (CO j) (CO f) = CO (Lift j f)
  rift :: O ('CO j) (Rift ('CO j) ('CO f)) ~> 'CO f
rift = (f ~> O j (Lift j f)) -> Co ('CO (O j (Lift j f))) ('CO f)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk d k) (f :: kk e k).
LeftKanLift j f =>
f ~> O j (Lift j f)
forall {k} {kk :: CAT k} {c :: k} {d :: k} {e :: k} (j :: kk d c)
       (f :: kk e c).
LeftKanLift j f =>
f ~> O j (Lift j f)
lift @j @f)
  riftUniv :: forall (g :: COK kk e d).
Ob g =>
(O ('CO j) g ~> 'CO f) -> g ~> Rift ('CO j) ('CO f)
riftUniv (Co b ~> a
n) = (Lift j f ~> UN 'CO g) -> Co ('CO (UN 'CO g)) ('CO (Lift j f))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (b :: kk j k)
       (a :: kk j k).
(b ~> a) -> Co ('CO a) ('CO b)
Co (forall (j :: kk d k) (f :: kk e k) (g :: kk e d).
(LeftKanLift j f, Ob g) =>
(f ~> O j g) -> 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 j g) -> Lift j f ~> g
liftUniv @j @f f ~> O j (UN 'CO g)
b ~> a
n)