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


import Proarrow.Category.Bicategory (Bicategory (..), Monad(..), Comonad(..), Fold, type (+++), Path (..), SPath (..), singPath, asObj)
import Proarrow.Category.Bicategory.Kan (RightKanExtension(..), LeftKanExtension(..), RightKanLift(..), LeftKanLift(..))
import Proarrow.Core (CategoryOf(..), Profunctor(..), CAT, Promonad (..), dimapDefault, UN, Is)
import Proarrow.Object (obj)


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 :: k) (j :: k) (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 :: 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
\\\ b ~> a
f
  Co b ~> a
f o :: forall {k1 :: k} (i :: k) (j :: k) (a :: COK kk i j)
       (b :: COK kk i j) (c :: COK kk j k1) (d :: COK kk j k1).
(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 {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` b ~> a
g)
  leftUnitor :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> O I a ~> a
leftUnitor (Co b ~> a
p) = (b ~> O I b) -> Co ('CO (O I b)) ('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 (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 Obj b
b ~> a
p)
  leftUnitorInv :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> a ~> O I a
leftUnitorInv (Co b ~> a
p) = (O I b ~> b) -> Co ('CO b) ('CO (O I 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 (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 Obj b
b ~> a
p)
  rightUnitor :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> O a I ~> a
rightUnitor (Co b ~> a
p) = (b ~> O b I) -> Co ('CO (O b I)) ('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 (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 Obj b
b ~> a
p)
  rightUnitorInv :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> a ~> O a I
rightUnitorInv (Co b ~> a
p) = (O b I ~> b) -> Co ('CO b) ('CO (O b 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 (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 Obj b
b ~> a
p)
  associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: COK kk i j2)
       (b :: COK kk j2 j1) (c :: COK kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Co b ~> a
p) (Co b ~> a
q) (Co b ~> a
r) = (O b (O b b) ~> O (O b b) b)
-> Co ('CO (O (O b b) b)) ('CO (O b (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 (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 Obj b
b ~> a
p Obj b
b ~> a
q Obj b
b ~> a
r)
  associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: COK kk i j2)
       (b :: COK kk j2 j1) (c :: COK kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Co b ~> a
p) (Co b ~> a
q) (Co b ~> a
r) = (O (O b b) b ~> O b (O b b))
-> Co ('CO (O b (O b b))) ('CO (O (O b 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 (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 Obj b
b ~> a
p Obj b
b ~> a
q Obj b
b ~> a
r)

concatFoldCo
  :: forall {kk} {i} {j} {k} {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k)
   . (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => SPath ps -> UN CO (Fold ps) `O` UN CO (Fold qs) ~> UN CO (Fold (ps +++ qs))
concatFoldCo :: forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
   ~> UN 'CO (Fold (ps +++ qs))
concatFoldCo SPath ps
SNil = Obj (UN 'CO (Fold qs))
-> O I (UN 'CO (Fold qs)) ~> UN 'CO (Fold qs)
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 (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs)))
concatFoldCo (SCons @_ @ps1 (Co b ~> a
p) SPath ps1
SNil) = case forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (COK kk) j k). IsPath ps => SPath ps
singPath @qs of
  SPath qs
SNil -> 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 Obj b
b ~> a
p
  SCons{} -> Obj b
b ~> a
p Obj b
-> (UN 'CO (Fold qs) ~> UN 'CO (Fold qs))
-> O b (UN 'CO (Fold qs)) ~> O b (UN 'CO (Fold qs))
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` forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs))
concatFoldCo (SCons @_ @ps1 (Co b ~> a
p) ps :: SPath ps1
ps@SCons{})
  = (b ~> b
b ~> a
p (b ~> b)
-> (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs))
    ~> UN 'CO (Fold (p ::: (ps1 +++ qs))))
-> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
   ~> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
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` forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
   ~> UN 'CO (Fold (ps +++ qs))
forall (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk k2, Ob0 kk j, Ob0 kk k) =>
SPath ps1
-> O (UN 'CO (Fold ps1)) (UN 'CO (Fold qs))
   ~> UN 'CO (Fold (ps1 +++ qs))
concatFoldCo @qs SPath ps1
ps)
  (O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
 ~> O b (UN 'CO (Fold (p ::: (ps1 +++ qs)))))
-> (O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
    ~> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs))))
-> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
   ~> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
forall (b :: kk i k) (c :: kk i k) (a :: kk i 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 ~> b)
-> Obj (UN 'CO (Fold (p ::: ps1)))
-> Obj (UN 'CO (Fold qs))
-> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
   ~> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
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 b ~> b
b ~> a
p (forall (a :: kk k2 j). (CategoryOf (kk k2 j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold ps1))) (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs)))
  ((Ob (p ::: ps1), Ob (p ::: ps1)) =>
 O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
 ~> O b (UN 'CO (Fold (p ::: (ps1 +++ qs)))))
-> Strictified (p ::: ps1) (p ::: ps1)
-> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
   ~> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path (COK kk) k2 j) (b :: Path (COK kk) k2 j) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath ps1 -> Obj ps1
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps1
ps

splitFoldCo
  :: forall {kk} {i} {j} {k} {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k)
   . (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => SPath ps -> UN CO (Fold (ps +++ qs)) ~> UN CO (Fold ps) `O` UN CO (Fold qs)
splitFoldCo :: forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> UN 'CO (Fold (ps +++ qs))
   ~> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
splitFoldCo SPath ps
SNil = Obj (UN 'CO (Fold qs))
-> UN 'CO (Fold qs) ~> O I (UN 'CO (Fold qs))
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 (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs)))
splitFoldCo (SCons @_ @ps1 (Co b ~> a
p) SPath ps1
SNil) = case forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (COK kk) j k). IsPath ps => SPath ps
singPath @qs of
  SPath qs
SNil -> 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 Obj b
b ~> a
p
  SCons{} -> b ~> b
b ~> a
p (b ~> b)
-> (UN 'CO (Fold qs) ~> UN 'CO (Fold qs))
-> O b (UN 'CO (Fold qs)) ~> O b (UN 'CO (Fold qs))
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` forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs))
splitFoldCo (SCons @_ @ps1 (Co b ~> a
p) ps :: SPath ps1
ps@SCons{})
  = Obj b
-> Obj (UN 'CO (Fold (p ::: ps1)))
-> Obj (UN 'CO (Fold qs))
-> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
   ~> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
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 Obj b
b ~> a
p (forall (a :: kk k2 j). (CategoryOf (kk k2 j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold ps1))) (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold qs)))
  (O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
 ~> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs)))
-> (O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
    ~> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs))))
-> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
   ~> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
forall (b :: kk i k) (c :: kk i k) (a :: kk i 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
. (Obj b
b ~> a
p Obj b
-> (UN 'CO (Fold (p ::: (ps1 +++ qs)))
    ~> O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
-> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
   ~> O b (O (UN 'CO (Fold (p ::: ps1))) (UN 'CO (Fold qs)))
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` forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> UN 'CO (Fold (ps +++ qs))
   ~> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
forall (qs :: Path (COK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk k2, Ob0 kk j, Ob0 kk k) =>
SPath ps1
-> UN 'CO (Fold (ps1 +++ qs))
   ~> O (UN 'CO (Fold ps1)) (UN 'CO (Fold qs))
splitFoldCo @qs SPath ps1
ps)
  ((Ob (p ::: ps1), Ob (p ::: ps1)) =>
 O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
 ~> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs)))
-> Strictified (p ::: ps1) (p ::: ps1)
-> O b (UN 'CO (Fold (p ::: (ps1 +++ qs))))
   ~> O (O b (UN 'CO (Fold (p ::: ps1)))) (UN 'CO (Fold qs))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path (COK kk) k2 j) (b :: Path (COK kk) k2 j) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath ps1 -> Obj ps1
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps1
ps



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 ('CO j) (Lan ('CO j) ('CO f))
lan = (O j (Ran j f) ~> f) -> Co ('CO f) ('CO (O j (Ran 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).
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)
  lanUniv :: forall (g :: COK kk d e).
Ob g =>
('CO f ~> O ('CO j) g) -> 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 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 b ~> a
O j (UN 'CO g) ~> f
n)

instance LeftKanExtension j f => RightKanExtension (CO j) (CO f) where
  type Ran (CO j) (CO f) = CO (Lan j f)
  ran :: O ('CO j) (Ran ('CO j) ('CO f)) ~> 'CO f
ran = (f ~> O j (Lan j f)) -> Co ('CO (O j (Lan 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 j d) (f :: kk j 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)
  ranUniv :: forall (g :: COK kk d e).
Ob g =>
(O ('CO j) g ~> '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 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 'CO g)
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 (Lift ('CO j) ('CO f)) ('CO j)
lift = (O (Rift j f) j ~> f) -> Co ('CO f) ('CO (O (Rift 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 d k) (f :: kk e k).
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)
  liftUniv :: forall (g :: COK kk e d).
Ob g =>
('CO f ~> O g ('CO j)) -> 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 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 b ~> a
O (UN 'CO g) j ~> f
n)

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