{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Bicategory.Op where

import Proarrow.Category.Bicategory (Adjunction_ (..), Bicategory (..), Bimodule (..), Comonad (..), Monad (..), Adj (..))
import Proarrow.Category.Bicategory.Kan
  ( LeftKanExtension (..)
  , LeftKanLift (..)
  , RightKanExtension (..)
  , RightKanLift (..)
  )
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)

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 :: 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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 :: 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)
  withOb2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k)
       (b :: OPK kk i j) r.
(Ob a, Ob b, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k) =>
(Ob (O a b) => r) -> r
withOb2 @(OP a) @(OP b) Ob (O a b) => r
r = forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @kk @b @a r
Ob (O (UN 'OP b) (UN 'OP a)) => r
Ob (O a b) => r
r
  withOb0s :: forall {j :: s} {k :: s} (a :: OPK kk j k) r.
Ob a =>
((Ob0 (OPK kk) j, Ob0 (OPK kk) k) => r) -> r
withOb0s @(OP a) (Ob0 (OPK kk) j, Ob0 (OPK kk) k) => r
r = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @a r
(Ob0 kk k, Ob0 kk j) => r
(Ob0 (OPK kk) j, Ob0 (OPK kk) k) => r
r
  (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: s) (j :: s) (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 :: 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
  Op a ~> b
f o :: forall {i :: s} (j :: s) (k :: s) (a :: OPK kk j k)
       (b :: OPK kk j k) (c :: OPK kk i j) (d :: OPK kk i j).
(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 {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
f)
  leftUnitor :: forall {i :: s} {j :: s} (a :: OPK kk i j).
(Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) =>
O I a ~> a
leftUnitor = (O (UN 'OP a) I ~> UN 'OP a)
-> Op ('OP (O (UN 'OP a) I)) ('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 O (UN 'OP a) I ~> UN 'OP 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
  leftUnitorInv :: forall {i :: s} {j :: s} (a :: OPK kk i j).
(Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN 'OP a ~> O (UN 'OP a) I)
-> Op ('OP (UN 'OP a)) ('OP (O (UN 'OP a) 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 UN 'OP a ~> O (UN 'OP 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
  rightUnitor :: forall {i :: s} {j :: s} (a :: OPK kk i j).
(Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) =>
O a I ~> a
rightUnitor = (O I (UN 'OP a) ~> UN 'OP a)
-> Op ('OP (O I (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 O I (UN 'OP a) ~> UN 'OP 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
  rightUnitorInv :: forall {i :: s} {j :: s} (a :: OPK kk i j).
(Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN 'OP a ~> O I (UN 'OP a))
-> Op ('OP (UN 'OP a)) ('OP (O I (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 ~> O I (UN 'OP 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
  associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: OPK kk j k)
       (b :: OPK kk i j) (c :: OPK kk h i).
(Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k,
 Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @(OP p) @(OP q) @(OP r) = (O (UN 'OP c) (O (UN 'OP b) (UN 'OP a))
 ~> O (O (UN 'OP c) (UN 'OP b)) (UN 'OP a))
-> Op
     ('OP (O (UN 'OP c) (O (UN 'OP b) (UN 'OP a))))
     ('OP (O (O (UN 'OP c) (UN 'OP b)) (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 (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 @r @q @p)
  associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: OPK kk j k)
       (b :: OPK kk i j) (c :: OPK kk h i).
(Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k,
 Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @(OP p) @(OP q) @(OP r) = (O (O (UN 'OP c) (UN 'OP b)) (UN 'OP a)
 ~> O (UN 'OP c) (O (UN 'OP b) (UN 'OP a)))
-> Op
     ('OP (O (O (UN 'OP c) (UN 'OP b)) (UN 'OP a)))
     ('OP (O (UN 'OP c) (O (UN 'OP b) (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 (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 @r @q @p)

type instance IsOb Tight p = IsOb Cotight (UN OP p)
type instance IsOb Cotight p = IsOb Tight (UN OP p)
type instance TightAdjoint p = OP (CotightAdjoint (UN OP p))
type instance CotightAdjoint p = OP (TightAdjoint (UN OP p))
instance (WithObO2 Cotight kk) => WithObO2 Tight (OPK kk) where
  withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k)
       (b :: OPK kk i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 @p @q (IsOb Tight (O a b), Ob (O a b)) => r
r = forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Cotight @kk @(UN OP q) @(UN OP p) r
(IsOb Cotight (O (UN 'OP b) (UN 'OP a)),
 Ob (O (UN 'OP b) (UN 'OP a))) =>
r
(IsOb Tight (O a b), Ob (O a b)) => r
r
instance (WithObO2 Tight kk) => WithObO2 Cotight (OPK kk) where
  withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k)
       (b :: OPK kk i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 @p @q (IsOb Cotight (O a b), Ob (O a b)) => r
r = forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @Tight @kk @(UN OP q) @(UN OP p) r
(IsOb Tight (O (UN 'OP b) (UN 'OP a)),
 Ob (O (UN 'OP b) (UN 'OP a))) =>
r
(IsOb Cotight (O a b), Ob (O a b)) => r
r
instance (Equipment kk) => Equipment (OPK kk) where
  withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @(OP f) (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r = forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
forall (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsTight f) =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @kk @f r
(Adjunction_ (UN 'OP f) (CotightAdjoint (UN 'OP f)),
 IsCotight (CotightAdjoint (UN 'OP f))) =>
r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r
  withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @(OP f) (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r = forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @kk @f r
(Adjunction_ (TightAdjoint (UN 'OP f)) (UN 'OP f),
 IsTight (TightAdjoint (UN 'OP f))) =>
r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r


-- instance (Equipment hk vk) => HasCompanions (OPK hk) (COK vk) where
--   type Companion (OPK hk) f = OP (Conjoint hk (UN CO f))
--   mapCompanion (Co f) = Op (mapConjoint f)
--   withObCompanion @(CO f) r = withObConjoint @hk @vk @f r
--   compToId = Op conjToId
--   compFromId = Op conjFromId
--   compToCompose (Co f) (Co g) = Op (conjToCompose f g)
--   compFromCompose (Co f) (Co g) = Op (conjFromCompose f g)

-- instance (Equipment hk vk) => Equipment (OPK hk) (COK vk) where
--   type Conjoint (OPK hk) f = OP (Companion hk (UN CO f))
--   mapConjoint (Co f) = Op (mapCompanion f)
--   withObConjoint @(CO f) r = withObCompanion @hk @vk @f r
--   conjToId = Op compToId
--   conjFromId = Op compFromId
--   conjToCompose (Co f) (Co g) = Op (compToCompose f g)
--   conjFromCompose (Co f) (Co g) = Op (compFromCompose f g)
--   comConUnit (Co f) = Op (comConUnit f)
--   comConCounit (Co f) = Op (comConCounit f)

-- instance (Equipment hk vk) => HasCompanions (COK hk) (OPK vk) where
--   type Companion (COK hk) f = CO (Conjoint hk (UN OP f))
--   mapCompanion (Op f) = Co (mapConjoint f)
--   withObCompanion @(OP f) r = withObConjoint @hk @vk @f r
--   compToId = Co conjFromId
--   compFromId = Co conjToId
--   compToCompose (Op f) (Op g) = Co (conjFromCompose g f)
--   compFromCompose (Op f) (Op g) = Co (conjToCompose g f)

-- instance (Equipment hk vk) => Equipment (COK hk) (OPK vk) where
--   type Conjoint (COK hk) f = CO (Companion hk (UN OP f))
--   mapConjoint (Op f) = Co (mapCompanion f)
--   withObConjoint @(OP f) r = withObCompanion @hk @vk @f r
--   conjToId = Co compFromId
--   conjFromId = Co compToId
--   conjToCompose (Op f) (Op g) = Co (compFromCompose g f)
--   conjFromCompose (Op f) (Op g) = Co (compToCompose g f)
--   comConUnit (Op f) = Co (comConCounit f)
--   comConCounit (Op f) = Co (comConUnit f)

-- flipSq :: Sq '(CO p, OP f) '(CO q, OP g) -> Sq '(OP q, CO g) '(OP p, CO f)
-- flipSq (Sq (Co sq)) = Sq (Op sq)

-- flipRetroSq :: RetroSq '(CO p, OP f) '(CO q, OP g) -> RetroSq '(OP q, CO g) '(OP p, CO f)
-- flipRetroSq (RetroSq (Co sq)) = RetroSq (Op sq)

instance (RightKanExtension j f) => RightKanLift (OP j) (OP f) where
  type Rift (OP j) (OP f) = OP (Ran j f)
  rift :: O ('OP j) (Rift ('OP j) ('OP f)) ~> 'OP f
rift = (O (Ran j f) j ~> f) -> Op ('OP (O (Ran 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 k d) (f :: kk k 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)
  riftUniv :: forall (g :: OPK kk e d).
Ob g =>
(O ('OP j) g ~> '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 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 a ~> b
O (UN 'OP g) j ~> 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 ('OP j) (Lift ('OP j) ('OP f))
lift = (f ~> O (Lan j f) j) -> Op ('OP f) ('OP (O (Lan 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 k d) (f :: kk k 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)
  liftUniv :: forall (g :: OPK kk e d).
Ob g =>
('OP f ~> O ('OP j) g) -> 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 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 'OP g) j
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 (Ran ('OP j) ('OP f)) ('OP j) ~> 'OP f
ran = (O j (Rift j f) ~> f) -> Op ('OP (O j (Rift 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 d j) (f :: kk e j).
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)
  ranUniv :: forall (g :: OPK kk d e).
Ob g =>
(O g ('OP j) ~> '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 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 a ~> b
O j (UN 'OP g) ~> 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 (Lan ('OP j) ('OP f)) ('OP j)
lan = (f ~> O j (Lift j f)) -> Op ('OP f) ('OP (O j (Lift 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).
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)
  lanUniv :: forall (g :: OPK kk d e).
Ob g =>
('OP f ~> O g ('OP j)) -> 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 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 'OP g)
a ~> b
n)

instance (Adjunction_ f g) => Adjunction_ (OP g) (OP f) where
  adj :: Adj ('OP g) ('OP f)
adj = case forall (l :: kk k j) (r :: kk j k). Adjunction_ l r => Adj l r
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction_ l r =>
Adj l r
adj @f @g of Adj I ~> O g f
un O f g ~> I
coun -> Adj { adjUnit :: I ~> O ('OP f) ('OP g)
adjUnit = (I ~> O g f) -> Op ('OP I) ('OP (O g 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 I ~> O g f
un, adjCounit :: O ('OP g) ('OP f) ~> I
adjCounit = (O f g ~> I) -> Op ('OP (O f g)) ('OP 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 O f g ~> I
coun }

instance (Monad t) => Monad (OP t) where
  eta :: I ~> 'OP t
eta = (I ~> t) -> Op ('OP I) ('OP t)
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 I ~> t
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  mu :: O ('OP t) ('OP t) ~> 'OP t
mu = (O t t ~> t) -> Op ('OP (O t t)) ('OP t)
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 O t t ~> t
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

instance (Comonad t) => Comonad (OP t) where
  epsilon :: 'OP t ~> I
epsilon = (t ~> I) -> Op ('OP t) ('OP 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 t ~> I
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> I
epsilon
  delta :: 'OP t ~> O ('OP t) ('OP t)
delta = (t ~> O t t) -> Op ('OP t) ('OP (O t t))
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 t ~> O t t
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Comonad t =>
t ~> O t t
delta

instance (Bimodule s t p) => Bimodule (OP t) (OP s) (OP p) where
  leftAction :: O ('OP t) ('OP p) ~> 'OP p
leftAction = (O p t ~> p) -> Op ('OP (O p t)) ('OP p)
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 (s :: kk j j) (t :: kk k k) (p :: kk k j).
Bimodule s t p =>
O p t ~> p
forall {k} {kk :: k -> k -> Type} {a :: k} {b :: k} (s :: kk a a)
       (t :: kk b b) (p :: kk b a).
Bimodule s t p =>
O p t ~> p
rightAction @s @t @p)
  rightAction :: O ('OP p) ('OP s) ~> 'OP p
rightAction = (O s p ~> p) -> Op ('OP (O s p)) ('OP p)
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 (s :: kk j j) (t :: kk k k) (p :: kk k j).
Bimodule s t p =>
O s p ~> p
forall {k} {kk :: k -> k -> Type} {a :: k} {b :: k} (s :: kk a a)
       (t :: kk b b) (p :: kk b a).
Bimodule s t p =>
O s p ~> p
leftAction @s @t @p)