{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Bicategory.Op where

import Proarrow.Category.Bicategory (Adjunction (..), Bicategory (..), Bimodule (..), Comonad (..), Monad (..))
import Proarrow.Category.Bicategory.Co (COK (..), Co (..))
import Proarrow.Category.Bicategory.Kan
  ( LeftKanExtension (..)
  , LeftKanLift (..)
  , RightKanExtension (..)
  , RightKanLift (..)
  )
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), RetroSq (..), Sq (..))
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 :: 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 :: 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
  iObj :: forall (i :: s). Ob0 (OPK kk) i => Obj I
iObj = (I ~> I) -> Op ('OP I) ('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 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
  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)

instance (Equipment hk vk) => HasCompanions (OPK hk) (COK vk) where
  type Companion (OPK hk) f = OP (Conjoint hk (UN CO f))
  mapCompanion :: forall {j :: k} {k :: k} (f :: COK vk j k) (g :: COK vk j k).
(f ~> g) -> Companion (OPK hk) f ~> Companion (OPK hk) g
mapCompanion (Co b1 ~> a1
f) = (Conjoint hk a1 ~> Conjoint hk b1)
-> Op ('OP (Conjoint hk a1)) ('OP (Conjoint hk b1))
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 ((b1 ~> a1) -> Conjoint hk a1 ~> Conjoint hk b1
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint b1 ~> a1
f)
  compToId :: forall (k :: k). Ob0 (COK vk) k => Companion (OPK hk) I ~> I
compToId = (Conjoint hk I ~> I) -> Op ('OP (Conjoint hk I)) ('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 Conjoint hk I ~> I
forall (k :: k). Ob0 vk k => Conjoint hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
Conjoint hk I ~> I
conjToId
  compFromId :: forall (k :: k). Ob0 (COK vk) k => I ~> Companion (OPK hk) I
compFromId = (I ~> Conjoint hk I) -> Op ('OP I) ('OP (Conjoint hk 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 I ~> Conjoint hk I
forall (k :: k). Ob0 vk k => I ~> Conjoint hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
I ~> Conjoint hk I
conjFromId
  compToCompose :: forall {i :: k} {j :: k} {k :: k} (f :: COK vk j k)
       (g :: COK vk i j).
Obj f
-> Obj g
-> Companion (OPK hk) (O f g)
   ~> O (Companion (OPK hk) f) (Companion (OPK hk) g)
compToCompose (Co b1 ~> a1
f) (Co b1 ~> a1
g) = (Conjoint hk (O b1 b1) ~> O (Conjoint hk b1) (Conjoint hk b1))
-> Op
     ('OP (Conjoint hk (O b1 b1)))
     ('OP (O (Conjoint hk b1) (Conjoint hk b1)))
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 b1
-> Obj b1
-> Conjoint hk (O b1 b1) ~> O (Conjoint hk b1) (Conjoint hk b1)
forall {k1 :: k} {j :: k} {k2 :: k} (f :: vk j k2) (g :: vk k1 j).
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {k1 :: c} {j :: c} {k2 :: c}
       (f :: vk j k2) (g :: vk k1 j).
Equipment hk vk =>
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
conjToCompose Obj b1
b1 ~> a1
f Obj b1
b1 ~> a1
g)
  compFromCompose :: forall {j1 :: k} {j2 :: k} {k :: k} (f :: COK vk j2 k)
       (g :: COK vk j1 j2).
Obj f
-> Obj g
-> O (Companion (OPK hk) f) (Companion (OPK hk) g)
   ~> Companion (OPK hk) (O f g)
compFromCompose (Co b1 ~> a1
f) (Co b1 ~> a1
g) = (O (Conjoint hk b1) (Conjoint hk b1) ~> Conjoint hk (O b1 b1))
-> Op
     ('OP (O (Conjoint hk b1) (Conjoint hk b1)))
     ('OP (Conjoint hk (O b1 b1)))
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 b1
-> Obj b1
-> O (Conjoint hk b1) (Conjoint hk b1) ~> Conjoint hk (O b1 b1)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
Equipment hk vk =>
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
conjFromCompose Obj b1
b1 ~> a1
f Obj b1
b1 ~> a1
g)

instance (Equipment hk vk) => Equipment (OPK hk) (COK vk) where
  type Conjoint (OPK hk) f = OP (Companion hk (UN CO f))
  mapConjoint :: forall {j :: k} {k :: k} (f :: COK vk j k) (g :: COK vk j k).
(f ~> g) -> Conjoint (OPK hk) g ~> Conjoint (OPK hk) f
mapConjoint (Co b1 ~> a1
f) = (Companion hk b1 ~> Companion hk a1)
-> Op ('OP (Companion hk b1)) ('OP (Companion hk a1))
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 ((b1 ~> a1) -> Companion hk b1 ~> Companion hk a1
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion b1 ~> a1
f)
  conjToId :: forall (k :: k). Ob0 (COK vk) k => Conjoint (OPK hk) I ~> I
conjToId = (Companion hk I ~> I) -> Op ('OP (Companion hk I)) ('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 Companion hk I ~> I
forall (k :: k). Ob0 vk k => Companion hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId
  conjFromId :: forall (k :: k). Ob0 (COK vk) k => I ~> Conjoint (OPK hk) I
conjFromId = (I ~> Companion hk I) -> Op ('OP I) ('OP (Companion hk 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 I ~> Companion hk I
forall (k :: k). Ob0 vk k => I ~> Companion hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId
  conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: COK vk j k2)
       (g :: COK vk k1 j).
Obj f
-> Obj g
-> Conjoint (OPK hk) (O f g)
   ~> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f)
conjToCompose (Co b1 ~> a1
f) (Co b1 ~> a1
g) = (Companion hk (O b1 b1) ~> O (Companion hk b1) (Companion hk b1))
-> Op
     ('OP (Companion hk (O b1 b1)))
     ('OP (O (Companion hk b1) (Companion hk b1)))
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 b1
-> Obj b1
-> Companion hk (O b1 b1) ~> O (Companion hk b1) (Companion hk b1)
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose Obj b1
b1 ~> a1
f Obj b1
b1 ~> a1
g)
  conjFromCompose :: forall {j1 :: k} {j2 :: k} {k :: k} (f :: COK vk j2 k)
       (g :: COK vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f)
   ~> Conjoint (OPK hk) (O f g)
conjFromCompose (Co b1 ~> a1
f) (Co b1 ~> a1
g) = (O (Companion hk b1) (Companion hk b1) ~> Companion hk (O b1 b1))
-> Op
     ('OP (O (Companion hk b1) (Companion hk b1)))
     ('OP (Companion hk (O b1 b1)))
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 b1
-> Obj b1
-> O (Companion hk b1) (Companion hk b1) ~> Companion hk (O b1 b1)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Obj b1
b1 ~> a1
f Obj b1
b1 ~> a1
g)
  comConUnit :: forall {j :: k} {k :: k} (f :: COK vk j k).
Obj f -> I ~> O (Conjoint (OPK hk) f) (Companion (OPK hk) f)
comConUnit (Co b1 ~> a1
f) = (I ~> O (Conjoint hk b1) (Companion hk b1))
-> Op ('OP I) ('OP (O (Conjoint hk b1) (Companion hk b1)))
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 b1 -> I ~> O (Conjoint hk b1) (Companion hk b1)
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj b1
b1 ~> a1
f)
  comConCounit :: forall {j :: k} {k :: k} (f :: COK vk j k).
Obj f -> O (Companion (OPK hk) f) (Conjoint (OPK hk) f) ~> I
comConCounit (Co b1 ~> a1
f) = (O (Companion hk b1) (Conjoint hk b1) ~> I)
-> Op ('OP (O (Companion hk b1) (Conjoint hk b1))) ('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 (Obj b1 -> O (Companion hk b1) (Conjoint hk b1) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit Obj b1
b1 ~> a1
f)

instance (Equipment hk vk) => HasCompanions (COK hk) (OPK vk) where
  type Companion (COK hk) f = CO (Conjoint hk (UN OP f))
  mapCompanion :: forall {j :: k} {k :: k} (f :: OPK vk j k) (g :: OPK vk j k).
(f ~> g) -> Companion (COK hk) f ~> Companion (COK hk) g
mapCompanion (Op a ~> b
f) = (Conjoint hk b ~> Conjoint hk a)
-> Co ('CO (Conjoint hk a)) ('CO (Conjoint hk b))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co ((a ~> b) -> Conjoint hk b ~> Conjoint hk a
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint a ~> b
f)
  compToId :: forall (k :: k). Ob0 (OPK vk) k => Companion (COK hk) I ~> I
compToId = (I ~> Conjoint hk I) -> Co ('CO (Conjoint hk I)) ('CO I)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co I ~> Conjoint hk I
forall (k :: k). Ob0 vk k => I ~> Conjoint hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
I ~> Conjoint hk I
conjFromId
  compFromId :: forall (k :: k). Ob0 (OPK vk) k => I ~> Companion (COK hk) I
compFromId = (Conjoint hk I ~> I) -> Co ('CO I) ('CO (Conjoint hk I))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co Conjoint hk I ~> I
forall (k :: k). Ob0 vk k => Conjoint hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(Equipment hk vk, Ob0 vk k) =>
Conjoint hk I ~> I
conjToId
  compToCompose :: forall {i :: k} {j :: k} {k :: k} (f :: OPK vk j k)
       (g :: OPK vk i j).
Obj f
-> Obj g
-> Companion (COK hk) (O f g)
   ~> O (Companion (COK hk) f) (Companion (COK hk) g)
compToCompose (Op a ~> b
f) (Op a ~> b
g) = (O (Conjoint hk b) (Conjoint hk b) ~> Conjoint hk (O b b))
-> Co
     ('CO (Conjoint hk (O b b)))
     ('CO (O (Conjoint hk b) (Conjoint hk b)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b
-> Obj b
-> O (Conjoint hk b) (Conjoint hk b) ~> Conjoint hk (O b b)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
Equipment hk vk =>
Obj f
-> Obj g
-> O (Conjoint hk g) (Conjoint hk f) ~> Conjoint hk (O f g)
conjFromCompose a ~> b
Obj b
g a ~> b
Obj b
f)
  compFromCompose :: forall {j1 :: k} {j2 :: k} {k :: k} (f :: OPK vk j2 k)
       (g :: OPK vk j1 j2).
Obj f
-> Obj g
-> O (Companion (COK hk) f) (Companion (COK hk) g)
   ~> Companion (COK hk) (O f g)
compFromCompose (Op a ~> b
f) (Op a ~> b
g) = (Conjoint hk (O b b) ~> O (Conjoint hk b) (Conjoint hk b))
-> Co
     ('CO (O (Conjoint hk b) (Conjoint hk b)))
     ('CO (Conjoint hk (O b b)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b
-> Obj b
-> Conjoint hk (O b b) ~> O (Conjoint hk b) (Conjoint hk b)
forall {k1 :: k} {j :: k} {k2 :: k} (f :: vk j k2) (g :: vk k1 j).
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {k1 :: c} {j :: c} {k2 :: c}
       (f :: vk j k2) (g :: vk k1 j).
Equipment hk vk =>
Obj f
-> Obj g
-> Conjoint hk (O f g) ~> O (Conjoint hk g) (Conjoint hk f)
conjToCompose a ~> b
Obj b
g a ~> b
Obj b
f)

instance (Equipment hk vk) => Equipment (COK hk) (OPK vk) where
  type Conjoint (COK hk) f = CO (Companion hk (UN OP f))
  mapConjoint :: forall {j :: k} {k :: k} (f :: OPK vk j k) (g :: OPK vk j k).
(f ~> g) -> Conjoint (COK hk) g ~> Conjoint (COK hk) f
mapConjoint (Op a ~> b
f) = (Companion hk a ~> Companion hk b)
-> Co ('CO (Companion hk b)) ('CO (Companion hk a))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co ((a ~> b) -> Companion hk a ~> Companion hk b
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion a ~> b
f)
  conjToId :: forall (k :: k). Ob0 (OPK vk) k => Conjoint (COK hk) I ~> I
conjToId = (I ~> Companion hk I) -> Co ('CO (Companion hk I)) ('CO I)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co I ~> Companion hk I
forall (k :: k). Ob0 vk k => I ~> Companion hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId
  conjFromId :: forall (k :: k). Ob0 (OPK vk) k => I ~> Conjoint (COK hk) I
conjFromId = (Companion hk I ~> I) -> Co ('CO I) ('CO (Companion hk I))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co Companion hk I ~> I
forall (k :: k). Ob0 vk k => Companion hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId
  conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: OPK vk j k2)
       (g :: OPK vk k1 j).
Obj f
-> Obj g
-> Conjoint (COK hk) (O f g)
   ~> O (Conjoint (COK hk) g) (Conjoint (COK hk) f)
conjToCompose (Op a ~> b
f) (Op a ~> b
g) = (O (Companion hk b) (Companion hk b) ~> Companion hk (O b b))
-> Co
     ('CO (Companion hk (O b b)))
     ('CO (O (Companion hk b) (Companion hk b)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b
-> Obj b
-> O (Companion hk b) (Companion hk b) ~> Companion hk (O b b)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose a ~> b
Obj b
g a ~> b
Obj b
f)
  conjFromCompose :: forall {j1 :: k} {j2 :: k} {k :: k} (f :: OPK vk j2 k)
       (g :: OPK vk j1 j2).
Obj f
-> Obj g
-> O (Conjoint (COK hk) g) (Conjoint (COK hk) f)
   ~> Conjoint (COK hk) (O f g)
conjFromCompose (Op a ~> b
f) (Op a ~> b
g) = (Companion hk (O b b) ~> O (Companion hk b) (Companion hk b))
-> Co
     ('CO (O (Companion hk b) (Companion hk b)))
     ('CO (Companion hk (O b b)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b
-> Obj b
-> Companion hk (O b b) ~> O (Companion hk b) (Companion hk b)
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose a ~> b
Obj b
g a ~> b
Obj b
f)
  comConUnit :: forall {j :: k} {k :: k} (f :: OPK vk j k).
Obj f -> I ~> O (Conjoint (COK hk) f) (Companion (COK hk) f)
comConUnit (Op a ~> b
f) = (O (Companion hk b) (Conjoint hk b) ~> I)
-> Co ('CO I) ('CO (O (Companion hk b) (Conjoint hk b)))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b -> O (Companion hk b) (Conjoint hk b) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit a ~> b
Obj b
f)
  comConCounit :: forall {j :: k} {k :: k} (f :: OPK vk j k).
Obj f -> O (Companion (COK hk) f) (Conjoint (COK hk) f) ~> I
comConCounit (Op a ~> b
f) = (I ~> O (Conjoint hk b) (Companion hk b))
-> Co ('CO (O (Conjoint hk b) (Companion hk b))) ('CO I)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1)
       (a1 :: kk j k1).
(b1 ~> a1) -> Co ('CO a1) ('CO b1)
Co (Obj b -> I ~> O (Conjoint hk b) (Companion hk b)
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit a ~> b
Obj b
f)

flipSq :: Sq '(CO p, OP f) '(CO q, OP g) -> Sq '(OP q, CO g) '(OP p, CO f)
flipSq :: forall {k} {kk :: CAT k} {k :: k} {k :: k} {kk :: CAT k} {j :: k}
       {h :: k} (p :: kk k k) (f :: kk j k) (q :: kk h j) (g :: kk h k).
Sq '( 'CO p, 'OP f) '( 'CO q, 'OP g)
-> Sq '( 'OP q, 'CO g) '( 'OP p, 'CO f)
flipSq (Sq (Co b1 ~> a1
sq)) = (O (Companion (OPK kk) ('CO g)) ('OP q)
 ~> O ('OP p) (Companion (OPK kk) ('CO f)))
-> Sq '( 'OP q, 'CO g) '( 'OP p, 'CO f)
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 ((b1 ~> a1) -> Op ('OP b1) ('OP a1)
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 b1 ~> a1
sq)

flipRetroSq :: RetroSq '(CO p, OP f) '(CO q, OP g) -> RetroSq '(OP q, CO g) '(OP p, CO f)
flipRetroSq :: forall {k} {kk :: CAT k} {h :: k} {j :: k} {kk :: CAT k} {k1 :: k}
       {k :: k} (p :: kk h j) (f :: kk h k1) (q :: kk k1 k) (g :: kk j k).
RetroSq '( 'CO p, 'OP f) '( 'CO q, 'OP g)
-> RetroSq '( 'OP q, 'CO g) '( 'OP p, 'CO f)
flipRetroSq (RetroSq (Co b1 ~> a1
sq)) = (O ('OP q) (Companion (OPK kk) ('CO g))
 ~> O (Companion (OPK kk) ('CO f)) ('OP p))
-> RetroSq '( 'OP q, 'CO g) '( 'OP p, 'CO f)
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 q (Companion hk g) ~> O (Companion hk f) p)
-> RetroSq '(q, g) '(p, f)
RetroSq ((b1 ~> a1) -> Op ('OP b1) ('OP a1)
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 b1 ~> a1
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
  unit :: I ~> O ('OP f) ('OP g)
unit = (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 (forall (l :: kk k j) (r :: kk j k). 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)
  counit :: O ('OP g) ('OP f) ~> I
counit = (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 (forall (l :: kk k j) (r :: kk j k). 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)

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)