{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Strictified where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Bicategory
  ( Adjunction (..)
  , Bicategory (..)
  , Comonad (..)
  , Monad (..)
  , associator'
  , associatorInv'
  , (||)
  )
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, id, src, tgt)
import Proarrow.Object (Obj, obj)
import Prelude (($), type (~))

infixr 5 :::
infixl 5 +++

-- | The type of 2-parameter kind constructors.
type Path :: CAT k -> CAT k

-- | A type-level kind-threaded list. Used to strictify the bicategory and double category definitions.
-- @kk@ is a kind constructor, which creates a kind given two other kinds. (Each kind representing a 0-cell.)
type data Path kk j k where
  Nil :: Path kk k k
  (:::) :: kk i j -> Path kk j k -> Path kk i k

type family (+++) (ps :: Path kk a b) (qs :: Path kk b c) :: Path kk a c
type instance Nil +++ qs = qs
type instance (p ::: ps) +++ qs = p ::: (ps +++ qs)

type SPath :: Path kk j k -> Type
data SPath ps where
  SNil :: (Ob0 kk k) => SPath (Nil :: Path kk k k)
  SCons :: forall {kk} {i} {j} {k} (p :: kk i j) (ps :: Path kk j k). (Ob0 kk i) => Obj p -> SPath ps -> SPath (p ::: ps)

class ((as +++ bs) +++ cs ~ as +++ (bs +++ cs)) => Assoc as bs cs
instance (as +++ (bs +++ cs) ~ (as +++ bs) +++ cs) => Assoc as bs cs

type IsPath :: forall {kk} {j} {k}. Path kk j k -> Constraint
class
  (Bicategory kk, Ob0 kk j, Ob0 kk k, ps +++ Nil ~ ps, forall i h (qs :: Path kk k h) (rs :: Path kk h i). Assoc ps qs rs) =>
  IsPath (ps :: Path kk j k)
  where
  singPath :: SPath ps
instance (Bicategory kk, Ob0 kk k) => IsPath (Nil :: Path kk k k) where
  singPath :: SPath Nil
singPath = SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil
instance (Ob0 kk i, Ob (p :: kk i j), IsPath (ps :: Path kk j k)) => IsPath (p ::: ps) where
  singPath :: SPath (p ::: ps)
singPath = let p :: Obj p
p = forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p in Obj p -> SPath ps -> SPath (p ::: ps)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj p
p SPath ps
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
singPath

withIsPath :: (Bicategory kk) => SPath (ps :: Path kk j k) -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath :: forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
SNil (IsPath ps, Ob0 kk j, Ob0 kk k) => r
r = r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
r
withIsPath (SCons Obj p
p SPath ps
ps) (IsPath ps, Ob0 kk j, Ob0 kk k) => r
r = SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
ps r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
r ((Ob0 kk j, Ob0 kk j, Ob p, Ob p) => r) -> Obj p -> 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 {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
\\\ Obj p
p

append :: SPath ps -> SPath qs -> SPath (ps +++ qs)
append :: forall {k} {kk :: CAT k} {j :: k} {b :: k} {k :: k}
       (ps :: Path kk j b) (qs :: Path kk b k).
SPath ps -> SPath qs -> SPath (ps +++ qs)
append SPath ps
SNil SPath qs
qs = SPath (ps +++ qs)
SPath qs
qs
append (SCons Obj p
p SPath ps
ps) SPath qs
qs = Obj p -> SPath (ps +++ qs) -> SPath (p ::: (ps +++ qs))
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj p
p (SPath ps -> SPath qs -> SPath (ps +++ qs)
forall {k} {kk :: CAT k} {j :: k} {b :: k} {k :: k}
       (ps :: Path kk j b) (qs :: Path kk b k).
SPath ps -> SPath qs -> SPath (ps +++ qs)
append SPath ps
ps SPath qs
qs)

singleton :: (Bicategory kk) => (p :: kk i j) ~> q -> (p ::: Nil) ~> (q ::: Nil)
singleton :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton p ~> q
f = SPath (p ::: Nil)
-> SPath (q ::: Nil)
-> (Fold (p ::: Nil) ~> Fold (q ::: Nil))
-> Strictified (p ::: Nil) (q ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (Obj p -> SPath Nil -> SPath (p ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons ((p ~> q) -> Obj p
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p ~> q
f) SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) (Obj q -> SPath Nil -> SPath (q ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons ((p ~> q) -> Obj q
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p ~> q
f) SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) p ~> q
Fold (p ::: Nil) ~> Fold (q ::: Nil)
f ((Ob0 kk i, Ob0 kk j, Ob p, Ob q) =>
 Strictified (p ::: Nil) (q ::: Nil))
-> (p ~> q) -> Strictified (p ::: Nil) (q ::: Nil)
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 {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
\\\ p ~> q
f

obj1 :: forall {kk} {i} {j} p. (Bicategory kk, Ob (p :: kk i j), Ob0 kk i, Ob0 kk j) => Obj (p ::: Nil)
obj1 :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 = (p ~> p) -> (p ::: Nil) ~> (p ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton (forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p)

asObj :: (Bicategory kk) => SPath (ps :: Path kk i j) -> Obj ps
asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps
SNil = Obj Nil
ps ~> ps
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
asObj (SCons Obj p
p SPath ps
SNil) = (p ~> p) -> (p ::: Nil) ~> (p ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton p ~> p
Obj p
p
asObj (SCons Obj p
p ps :: SPath ps
ps@SCons{}) = SPath ps -> Obj ps
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps
ps ((p ::: ps) ~> (p ::: ps))
-> ((p ::: Nil) ~> (p ::: Nil))
-> O (p ::: ps) (p ::: Nil) ~> O (p ::: ps) (p ::: Nil)
forall {i :: k} (j :: k) (k :: k) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path 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` Obj p -> (p ::: Nil) ~> (p ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton Obj p
p ((Ob p, Ob p) => Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps)))
-> Obj p -> Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps))
forall (a :: kk i j) (b :: kk i 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
\\ Obj p
p

asSPath :: (Bicategory kk) => Obj (ps :: Path kk i j) -> SPath ps
asSPath :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath (Str SPath ps
p SPath ps
_ Fold ps ~> Fold ps
_) = SPath ps
p

withAssoc
  :: forall {kk} {h} {i} {j} {k} (a :: Path kk h i) (b :: Path kk i j) (c :: Path kk j k) r
   . (Bicategory kk)
  => Obj a
  -> Obj b
  -> Obj c
  -> (((a +++ b) +++ c ~ a +++ (b +++ c)) => r)
  -> r
withAssoc :: forall {k} {kk :: CAT k} {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: Path kk h i) (b :: Path kk i j) (c :: Path kk j k) r.
Bicategory kk =>
Obj a
-> Obj b
-> Obj c
-> ((((a +++ b) +++ c) ~ (a +++ (b +++ c))) => r)
-> r
withAssoc as :: Obj a
as@Str{} Str{} Str{} = SPath a -> ((((a +++ b) +++ c) ~ (a +++ (b +++ c))) => r) -> r
forall {a :: k} (a' :: Path kk a i).
SPath a' -> ((((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r) -> r
go (Obj a -> SPath a
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath Obj a
as)
  where
    go :: forall a'. SPath a' -> (((a' +++ b) +++ c ~ a' +++ (b +++ c)) => r) -> r
    go :: forall {a :: k} (a' :: Path kk a i).
SPath a' -> ((((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r) -> r
go SPath a'
SNil (((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r
r = r
(((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r
r
    go (SCons Obj p
_ SPath ps
a) (((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r
r = SPath ps -> ((((ps +++ b) +++ c) ~ (ps +++ (b +++ c))) => r) -> r
forall {a :: k} (a' :: Path kk a i).
SPath a' -> ((((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r) -> r
go SPath ps
a r
(((a' +++ b) +++ c) ~ (a' +++ (b +++ c))) => r
(((ps +++ b) +++ c) ~ (ps +++ (b +++ c))) => r
r

concatFold
  :: forall {kk} {i} {j} {k} (as :: Path kk i j) (bs :: Path kk j k)
   . (Bicategory kk)
  => SPath as
  -> SPath bs
  -> Fold bs `O` Fold as ~> Fold (as +++ bs)
concatFold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       (as :: Path kk i j) (bs :: Path kk j k).
Bicategory kk =>
SPath as -> SPath bs -> O (Fold bs) (Fold as) ~> Fold (as +++ bs)
concatFold SPath as
as SPath bs
bs =
  let fbs :: Fold bs ~> Fold bs
fbs = SPath bs -> Fold bs ~> Fold bs
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath bs
bs
      h :: forall cs. (Ob0 kk k) => SPath cs -> (Fold bs `O` Fold cs) ~> Fold (cs +++ bs)
      h :: forall {j :: k} (cs :: Path kk j j).
Ob0 kk k =>
SPath cs -> O (Fold bs) (Fold cs) ~> Fold (cs +++ bs)
h SPath cs
SNil = O (Fold bs) I ~> Fold bs
(Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
O (Fold bs) I ~> Fold bs
forall {i :: k} {j :: k} (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 ((Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
 O (Fold bs) I ~> Fold bs)
-> (Fold bs ~> Fold bs) -> O (Fold bs) I ~> Fold bs
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 {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
\\\ Fold bs ~> Fold bs
fbs
      h (SCons Obj p
c SPath ps
SNil) = case SPath bs
bs of
        SPath bs
SNil -> O I p ~> p
O I p ~> p
(Ob0 kk j, Ob0 kk j, Ob p, Ob p) => O I p ~> p
forall {i :: k} {j :: k} (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 ((Ob0 kk j, Ob0 kk j, Ob p, Ob p) => O I p ~> p)
-> Obj p -> O I p ~> p
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 {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
\\\ Obj p
c
        SCons{} -> Fold bs ~> Fold bs
Fold (p ::: ps) ~> Fold (p ::: ps)
fbs (Fold (p ::: ps) ~> Fold (p ::: ps))
-> (p ~> p) -> O (Fold (p ::: ps)) p ~> O (Fold (p ::: ps)) p
forall {i :: k} (j :: k) (k :: k) (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` p ~> p
Obj p
c
      h (SCons Obj p
c cs :: SPath ps
cs@SCons{}) = (SPath ps -> O (Fold bs) (Fold ps) ~> Fold (ps +++ bs)
forall {j :: k} (cs :: Path kk j j).
Ob0 kk k =>
SPath cs -> O (Fold bs) (Fold cs) ~> Fold (cs +++ bs)
h SPath ps
cs (O (Fold bs) (Fold (p ::: ps)) ~> Fold (p ::: (ps +++ bs)))
-> Obj p
-> O (O (Fold bs) (Fold (p ::: ps))) p
   ~> O (Fold (p ::: (ps +++ bs))) p
forall {i :: k} (j :: k) (k :: k) (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` Obj p
c) (O (O (Fold bs) (Fold (p ::: ps))) p
 ~> O (Fold (p ::: (ps +++ bs))) p)
-> (O (Fold bs) (O (Fold (p ::: ps)) p)
    ~> O (O (Fold bs) (Fold (p ::: ps))) p)
-> O (Fold bs) (O (Fold (p ::: ps)) p)
   ~> O (Fold (p ::: (ps +++ bs))) p
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
. (Fold bs ~> Fold bs)
-> Obj (Fold (p ::: ps))
-> Obj p
-> O (Fold bs) (O (Fold (p ::: ps)) p)
   ~> O (O (Fold bs) (Fold (p ::: ps))) p
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
       {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv' Fold bs ~> Fold bs
fbs (SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
cs) Obj p
c
  in SPath as -> O (Fold bs) (Fold as) ~> Fold (as +++ bs)
forall {j :: k} (cs :: Path kk j j).
Ob0 kk k =>
SPath cs -> O (Fold bs) (Fold cs) ~> Fold (cs +++ bs)
h SPath as
as ((Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
 O (Fold bs) (Fold as) ~> Fold (as +++ bs))
-> (Fold bs ~> Fold bs)
-> O (Fold bs) (Fold as) ~> Fold (as +++ bs)
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 {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
\\\ Fold bs ~> Fold bs
fbs

splitFold
  :: forall {kk} {i} {j} {k} (as :: Path kk i j) (bs :: Path kk j k)
   . (Bicategory kk)
  => SPath as
  -> SPath bs
  -> Fold (as +++ bs) ~> Fold bs `O` Fold as
splitFold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       (as :: Path kk i j) (bs :: Path kk j k).
Bicategory kk =>
SPath as -> SPath bs -> Fold (as +++ bs) ~> O (Fold bs) (Fold as)
splitFold SPath as
as SPath bs
bs =
  let fbs :: Fold bs ~> Fold bs
fbs = SPath bs -> Fold bs ~> Fold bs
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath bs
bs
      h :: forall cs. (Ob0 kk k) => SPath cs -> Fold (cs +++ bs) ~> Fold bs `O` Fold cs
      h :: forall {i :: k} (cs :: Path kk i j).
Ob0 kk k =>
SPath cs -> Fold (cs +++ bs) ~> O (Fold bs) (Fold cs)
h SPath cs
SNil = Fold bs ~> O (Fold bs) I
(Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
Fold bs ~> O (Fold bs) I
forall {i :: k} {j :: k} (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 ((Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
 Fold bs ~> O (Fold bs) I)
-> (Fold bs ~> Fold bs) -> Fold bs ~> O (Fold bs) I
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 {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
\\\ Fold bs ~> Fold bs
fbs
      h (SCons Obj p
c SPath ps
SNil) = case SPath bs
bs of
        SPath bs
SNil -> p ~> O I p
(Ob0 kk i, Ob0 kk j, Ob p, Ob p) => p ~> O I p
forall {i :: k} {j :: k} (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 ((Ob0 kk i, Ob0 kk j, Ob p, Ob p) => p ~> O I p)
-> Obj p -> p ~> O I p
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 {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
\\\ Obj p
c
        SCons{} -> Fold bs ~> Fold bs
Fold (p ::: ps) ~> Fold (p ::: ps)
fbs (Fold (p ::: ps) ~> Fold (p ::: ps))
-> (p ~> p) -> O (Fold (p ::: ps)) p ~> O (Fold (p ::: ps)) p
forall {i :: k} (j :: k) (k :: k) (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` p ~> p
Obj p
c
      h (SCons Obj p
c cs :: SPath ps
cs@SCons{}) = (Fold bs ~> Fold bs)
-> Obj (Fold (p ::: ps))
-> Obj p
-> O (O (Fold bs) (Fold (p ::: ps))) p
   ~> O (Fold bs) (O (Fold (p ::: ps)) p)
forall {s} {j1 :: s} {i1 :: s} (kk :: s -> s -> Type) {i2 :: s}
       {j2 :: s} (a :: kk i2 j2) (b :: kk j1 i2) (c :: kk i1 j1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator' Fold bs ~> Fold bs
fbs (SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
cs) Obj p
c (O (O (Fold bs) (Fold (p ::: ps))) p
 ~> O (Fold bs) (O (Fold (p ::: ps)) p))
-> (O (Fold (p ::: (ps +++ bs))) p
    ~> O (O (Fold bs) (Fold (p ::: ps))) p)
-> O (Fold (p ::: (ps +++ bs))) p
   ~> O (Fold bs) (O (Fold (p ::: ps)) p)
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
. (SPath ps -> Fold (ps +++ bs) ~> O (Fold bs) (Fold ps)
forall {i :: k} (cs :: Path kk i j).
Ob0 kk k =>
SPath cs -> Fold (cs +++ bs) ~> O (Fold bs) (Fold cs)
h SPath ps
cs (Fold (p ::: (ps +++ bs)) ~> O (Fold bs) (Fold (p ::: ps)))
-> Obj p
-> O (Fold (p ::: (ps +++ bs))) p
   ~> O (O (Fold bs) (Fold (p ::: ps))) p
forall {i :: k} (j :: k) (k :: k) (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` Obj p
c)
  in SPath as -> Fold (as +++ bs) ~> O (Fold bs) (Fold as)
forall {i :: k} (cs :: Path kk i j).
Ob0 kk k =>
SPath cs -> Fold (cs +++ bs) ~> O (Fold bs) (Fold cs)
h SPath as
as ((Ob0 kk j, Ob0 kk k, Ob (Fold bs), Ob (Fold bs)) =>
 Fold (as +++ bs) ~> O (Fold bs) (Fold as))
-> (Fold bs ~> Fold bs)
-> Fold (as +++ bs) ~> O (Fold bs) (Fold as)
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 {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
\\\ Fold bs ~> Fold bs
fbs

type family Fold (as :: Path kk j k) :: kk j k
type instance Fold (Nil :: Path kk j j) = (I :: kk j j)
type instance Fold (p ::: Nil) = p
type instance Fold (p ::: (q ::: ps)) = Fold (q ::: ps) `O` p

fold :: forall {kk} {i} {j} (as :: Path kk i j). (Bicategory kk) => SPath as -> Fold as ~> Fold as
fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath as
SNil = Obj I
Fold as ~> Fold as
forall (i :: k). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
fold (SCons Obj p
p SPath ps
SNil) = Fold as ~> Fold as
Obj p
p
fold (SCons Obj p
p fs :: SPath ps
fs@SCons{}) = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
fs (Fold (p ::: ps) ~> Fold (p ::: ps))
-> Obj p -> O (Fold (p ::: ps)) p ~> O (Fold (p ::: ps)) p
forall {i :: k} (j :: k) (k :: k) (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` Obj p
p

type Strictified :: CAT (Path kk j k)
data Strictified ps qs where
  Str
    :: forall {kk} {j} {k} (ps :: Path kk j k) qs
     . (Ob0 kk j, Ob0 kk k)
    => SPath ps
    -> SPath qs
    -> Fold ps ~> Fold qs
    -> Strictified ps qs

str :: (Bicategory kk) => Obj (ps :: Path kk j k) -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str :: forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj ps
ps Obj qs
qs Fold ps ~> Fold qs
f = SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (Obj ps -> SPath ps
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath Obj ps
ps) (Obj qs -> SPath qs
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath Obj qs
qs) Fold ps ~> Fold qs
f ((Ob0 kk j, Ob0 kk k, Ob (Fold ps), Ob (Fold qs)) =>
 Strictified ps qs)
-> (Fold ps ~> Fold qs) -> Strictified ps qs
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 {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
\\\ Fold ps ~> Fold qs
f

unStr :: Strictified ps qs -> Fold ps ~> Fold qs
unStr :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
Strictified ps qs -> Fold ps ~> Fold qs
unStr (Str SPath ps
_ SPath qs
_ Fold ps ~> Fold qs
f) = Fold ps ~> Fold qs
f

instance (CategoryOf (kk j k), Bicategory kk) => Profunctor (Strictified :: CAT (Path kk j k)) where
  dimap :: forall (c :: Path kk j k) (a :: Path kk j k) (b :: Path kk j k)
       (d :: Path kk j k).
(c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d
dimap = (c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d
Strictified c a
-> Strictified b d -> Strictified a b -> Strictified 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 :: Path kk j k) (b :: Path kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ Str SPath a
ps SPath b
qs Fold a ~> Fold b
_ = SPath a -> ((IsPath a, Ob0 kk j, Ob0 kk k) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath a
ps (SPath b -> ((IsPath b, Ob0 kk j, Ob0 kk k) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath b
qs r
(Ob a, Ob b) => r
(IsPath b, Ob0 kk j, Ob0 kk k) => r
r)
instance (CategoryOf (kk j k), Bicategory kk) => Promonad (Strictified :: CAT (Path kk j k)) where
  id :: forall (a :: Path kk j k). (Ob a) => Strictified a a
  id :: forall (a :: Path kk j k). Ob a => Strictified a a
id = let a :: SPath a
a = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk j k). IsPath ps => SPath ps
singPath @a in SPath a -> SPath a -> (Fold a ~> Fold a) -> Strictified a a
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath a
a SPath a
a (SPath a -> Fold a ~> Fold a
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath a
a)
  Str SPath b
_ SPath c
r Fold b ~> Fold c
m . :: forall (b :: Path kk j k) (c :: Path kk j k) (a :: Path kk j k).
Strictified b c -> Strictified a b -> Strictified a c
. Str SPath a
p SPath b
_ Fold a ~> Fold b
n = SPath a -> SPath c -> (Fold a ~> Fold c) -> Strictified a c
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath a
p SPath c
r (Fold b ~> Fold c
m (Fold b ~> Fold c) -> (Fold a ~> Fold b) -> Fold a ~> Fold c
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
. Fold a ~> Fold b
n)
instance (CategoryOf (kk j k), Bicategory kk) => CategoryOf (Path kk j k) where
  type (~>) = Strictified
  type Ob (ps :: Path kk j k) = (IsPath ps, Ob0 kk j, Ob0 kk k)

introI :: forall {kk} {j}. (Ob0 kk j, Bicategory kk) => (Nil :: Path kk j j) ~> (I ::: Nil)
introI :: forall {k} {kk :: CAT k} {j :: k}.
(Ob0 kk j, Bicategory kk) =>
Nil ~> (I ::: Nil)
introI = SPath Nil
-> SPath (I ::: Nil)
-> (Fold Nil ~> Fold (I ::: Nil))
-> Strictified Nil (I ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil (Obj I -> SPath Nil -> SPath (I ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj I
forall (i :: k). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) Obj I
Fold Nil ~> Fold (I ::: Nil)
forall (i :: k). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj

elimI :: forall {kk} {j}. (Ob0 kk j, Bicategory kk) => (I ::: Nil) ~> (Nil :: Path kk j j)
elimI :: forall {s} {kk :: CAT s} {j :: s}.
(Ob0 kk j, Bicategory kk) =>
(I ::: Nil) ~> Nil
elimI = SPath (I ::: Nil)
-> SPath Nil
-> (Fold (I ::: Nil) ~> Fold Nil)
-> Strictified (I ::: Nil) Nil
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (Obj I -> SPath Nil -> SPath (I ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj I
forall (i :: s). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil Obj I
Fold (I ::: Nil) ~> Fold Nil
forall (i :: s). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj

introO
  :: forall {kk} {i} {j} {k} (p :: kk i j) (q :: kk j k)
   . (Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q)
  => (p ::: q ::: Nil) ~> (q `O` p ::: Nil)
introO :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (q :: kk j k).
(Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q) =>
(p ::: (q ::: Nil)) ~> (O q p ::: Nil)
introO = let p :: Obj p
p = forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p; q :: Obj q
q = forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @q; pq :: O q p ~> O q p
pq = Obj q
q Obj q -> Obj p -> O q p ~> O q p
forall {i :: k} (j :: k) (k :: k) (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` Obj p
p in SPath (p ::: (q ::: Nil))
-> SPath (O q p ::: Nil)
-> (Fold (p ::: (q ::: Nil)) ~> Fold (O q p ::: Nil))
-> Strictified (p ::: (q ::: Nil)) (O q p ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (Obj p -> SPath (q ::: Nil) -> SPath (p ::: (q ::: Nil))
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj p
p (Obj q -> SPath Nil -> SPath (q ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj q
q SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil)) ((O q p ~> O q p) -> SPath Nil -> SPath (O q p ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons O q p ~> O q p
pq SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) O q p ~> O q p
Fold (p ::: (q ::: Nil)) ~> Fold (O q p ::: Nil)
pq

elimO
  :: forall {kk} {i} {j} {k} (p :: kk i j) (q :: kk j k)
   . (Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q)
  => (q `O` p ::: Nil) ~> (p ::: q ::: Nil)
elimO :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (q :: kk j k).
(Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q) =>
(O q p ::: Nil) ~> (p ::: (q ::: Nil))
elimO = let p :: Obj p
p = forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p; q :: Obj q
q = forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @q; pq :: O q p ~> O q p
pq = Obj q
q Obj q -> Obj p -> O q p ~> O q p
forall {i :: k} (j :: k) (k :: k) (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` Obj p
p in SPath (O q p ::: Nil)
-> SPath (p ::: (q ::: Nil))
-> (Fold (O q p ::: Nil) ~> Fold (p ::: (q ::: Nil)))
-> Strictified (O q p ::: Nil) (p ::: (q ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str ((O q p ~> O q p) -> SPath Nil -> SPath (O q p ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons O q p ~> O q p
pq SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) (Obj p -> SPath (q ::: Nil) -> SPath (p ::: (q ::: Nil))
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj p
p (Obj q -> SPath Nil -> SPath (q ::: Nil)
forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (ps :: Path kk j k).
Ob0 kk i =>
Obj p -> SPath ps -> SPath (p ::: ps)
SCons Obj q
q SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil)) O q p ~> O q p
Fold (O q p ::: Nil) ~> Fold (p ::: (q ::: Nil))
pq

instance (Bicategory kk) => Bicategory (Path kk) where
  type Ob0 (Path kk) j = Ob0 kk j
  type I = Nil
  type O ps qs = qs +++ ps
  (Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: s) (j :: s) (ps :: Path kk i j) (qs :: Path kk i j) r.
((Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Str SPath ps
ps SPath qs
qs Fold ps ~> Fold qs
_ = SPath ps -> ((IsPath ps, Ob0 kk i, Ob0 kk j) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
ps (((IsPath ps, Ob0 kk i, Ob0 kk j) => r) -> r)
-> ((IsPath ps, Ob0 kk i, Ob0 kk j) => r) -> r
forall a b. (a -> b) -> a -> b
$ SPath qs -> ((IsPath qs, Ob0 kk i, Ob0 kk j) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath qs
qs r
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob qs) => r
(IsPath qs, Ob0 kk i, Ob0 kk j) => r
r
  Str SPath a
cs SPath b
ds Fold a ~> Fold b
qs o :: forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Str SPath c
as SPath d
bs Fold c ~> Fold d
ps = SPath (c +++ a)
-> SPath (d +++ b)
-> (Fold (c +++ a) ~> Fold (d +++ b))
-> Strictified (c +++ a) (d +++ b)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (SPath c -> SPath a -> SPath (c +++ a)
forall {k} {kk :: CAT k} {j :: k} {b :: k} {k :: k}
       (ps :: Path kk j b) (qs :: Path kk b k).
SPath ps -> SPath qs -> SPath (ps +++ qs)
append SPath c
as SPath a
cs) (SPath d -> SPath b -> SPath (d +++ b)
forall {k} {kk :: CAT k} {j :: k} {b :: k} {k :: k}
       (ps :: Path kk j b) (qs :: Path kk b k).
SPath ps -> SPath qs -> SPath (ps +++ qs)
append SPath d
bs SPath b
ds) (SPath d -> SPath b -> O (Fold b) (Fold d) ~> Fold (d +++ b)
forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       (as :: Path kk i j) (bs :: Path kk j k).
Bicategory kk =>
SPath as -> SPath bs -> O (Fold bs) (Fold as) ~> Fold (as +++ bs)
concatFold SPath d
bs SPath b
ds (O (Fold b) (Fold d) ~> Fold (d +++ b))
-> (Fold (c +++ a) ~> O (Fold b) (Fold d))
-> Fold (c +++ a) ~> Fold (d +++ b)
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
. (Fold a ~> Fold b
qs (Fold a ~> Fold b)
-> (Fold c ~> Fold d) -> O (Fold a) (Fold c) ~> O (Fold b) (Fold d)
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` Fold c ~> Fold d
ps) (O (Fold a) (Fold c) ~> O (Fold b) (Fold d))
-> (Fold (c +++ a) ~> O (Fold a) (Fold c))
-> Fold (c +++ a) ~> O (Fold b) (Fold d)
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
. SPath c -> SPath a -> Fold (c +++ a) ~> O (Fold a) (Fold c)
forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       (as :: Path kk i j) (bs :: Path kk j k).
Bicategory kk =>
SPath as -> SPath bs -> Fold (as +++ bs) ~> O (Fold bs) (Fold as)
splitFold SPath c
as SPath a
cs)
  leftUnitor :: forall {i :: s} {j :: s} (a :: Path kk i j).
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) =>
O I a ~> a
leftUnitor = O I a ~> a
Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk i j). Ob a => Strictified a a
id
  leftUnitorInv :: forall {i :: s} {j :: s} (a :: Path kk i j).
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) =>
a ~> O I a
leftUnitorInv = a ~> O I a
Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk i j). Ob a => Strictified a a
id
  rightUnitor :: forall {i :: s} {j :: s} (a :: Path kk i j).
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) =>
O a I ~> a
rightUnitor = O a I ~> a
Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk i j). Ob a => Strictified a a
id
  rightUnitorInv :: forall {i :: s} {j :: s} (a :: Path kk i j).
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) =>
a ~> O a I
rightUnitorInv = a ~> O a I
Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk i j). Ob a => Strictified a a
id
  associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: Path kk j k)
       (b :: Path kk i j) (c :: Path kk h i).
(Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j,
 Ob0 (Path kk) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @p @q @r = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk j k).
(CategoryOf (Path kk j k), Ob a) =>
Obj a
obj @p Obj a -> (b ~> b) -> O a b ~> O a b
forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path 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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk i j).
(CategoryOf (Path kk i j), Ob a) =>
Obj a
obj @q ((b +++ a) ~> (b +++ a))
-> (c ~> c) -> O (b +++ a) c ~> O (b +++ a) c
forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path 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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk h i).
(CategoryOf (Path kk h i), Ob a) =>
Obj a
obj @r
  associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: Path kk j k)
       (b :: Path kk i j) (c :: Path kk h i).
(Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j,
 Ob0 (Path kk) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @p @q @r = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk j k).
(CategoryOf (Path kk j k), Ob a) =>
Obj a
obj @p Obj a -> (b ~> b) -> O a b ~> O a b
forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path 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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk i j).
(CategoryOf (Path kk i j), Ob a) =>
Obj a
obj @q ((b +++ a) ~> (b +++ a))
-> (c ~> c) -> O (b +++ a) c ~> O (b +++ a) c
forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path 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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: Path kk h i).
(CategoryOf (Path kk h i), Ob a) =>
Obj a
obj @r

instance (Bicategory kk, Ob0 kk a) => Monad (Nil :: Path kk a a) where
  eta :: I ~> Nil
eta = Obj I
I ~> Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  mu :: O Nil Nil ~> Nil
mu = Obj I
O Nil Nil ~> Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj

instance (Monad s, Ob s) => Monad (s ::: Nil) where
  eta :: I ~> (s ::: Nil)
eta = Obj Nil
-> Obj (s ::: Nil)
-> (Fold Nil ~> Fold (s ::: Nil))
-> Strictified Nil (s ::: Nil)
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj I
Obj Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (p :: kk a a).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @s) I ~> s
Fold Nil ~> Fold (s ::: Nil)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  mu :: O (s ::: Nil) (s ::: Nil) ~> (s ::: Nil)
mu = Obj (s ::: (s ::: Nil))
-> Obj (s ::: Nil)
-> (Fold (s ::: (s ::: Nil)) ~> Fold (s ::: Nil))
-> Strictified (s ::: (s ::: Nil)) (s ::: Nil)
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (forall (p :: kk a a).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @s Obj (s ::: Nil)
-> Obj (s ::: Nil)
-> O (s ::: Nil) (s ::: Nil) ~> O (s ::: Nil) (s ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall (p :: kk a a).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @s) (forall (p :: kk a a).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @s) O s s ~> s
Fold (s ::: (s ::: Nil)) ~> Fold (s ::: Nil)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

instance (Bicategory kk, Ob0 kk a) => Comonad (Nil :: Path kk a a) where
  epsilon :: Nil ~> I
epsilon = Obj I
Nil ~> I
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  delta :: Nil ~> O Nil Nil
delta = Obj I
Nil ~> O Nil Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj

instance (Adjunction l r, Ob r, Ob l) => Monad (l ::: r ::: Nil) where
  eta :: I ~> (l ::: (r ::: Nil))
eta = Obj Nil
-> Obj (l ::: (r ::: Nil))
-> (Fold Nil ~> Fold (l ::: (r ::: Nil)))
-> Strictified Nil (l ::: (r ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj I
Obj Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (p :: kk i a).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @r Obj (r ::: Nil)
-> ((l ::: Nil) ~> (l ::: Nil))
-> O (r ::: Nil) (l ::: Nil) ~> O (r ::: Nil) (l ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall (p :: kk a i).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk i) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @l) (forall (l :: kk a i) (r :: kk i a). 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 @l @r)
  mu :: O (l ::: (r ::: Nil)) (l ::: (r ::: Nil)) ~> (l ::: (r ::: Nil))
mu = let r :: Obj (r ::: Nil)
r = forall (p :: kk i a).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @r; l :: (l ::: Nil) ~> (l ::: Nil)
l = forall (p :: kk a i).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk i) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @l in Obj (r ::: Nil)
r Obj (r ::: Nil)
-> (((r ::: Nil) +++ (l ::: Nil)) ~> Nil)
-> O (r ::: Nil) ((r ::: Nil) +++ (l ::: Nil)) ~> O (r ::: Nil) Nil
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj ((r ::: Nil) +++ (l ::: Nil))
-> Obj Nil
-> (Fold ((r ::: Nil) +++ (l ::: Nil)) ~> Fold Nil)
-> Strictified ((r ::: Nil) +++ (l ::: Nil)) Nil
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str ((l ::: Nil) ~> (l ::: Nil)
l ((l ::: Nil) ~> (l ::: Nil))
-> Obj (r ::: Nil)
-> O (l ::: Nil) (r ::: Nil) ~> O (l ::: Nil) (r ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (r ::: Nil)
r) Obj I
Obj Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (l :: kk a i) (r :: kk i a). 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 @l @r) ((((r ::: Nil) +++ (l ::: Nil)) +++ (r ::: Nil))
 ~> (Nil +++ (r ::: Nil)))
-> ((l ::: Nil) ~> (l ::: Nil))
-> O (((r ::: Nil) +++ (l ::: Nil)) +++ (r ::: Nil)) (l ::: Nil)
   ~> O (Nil +++ (r ::: Nil)) (l ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| (l ::: Nil) ~> (l ::: Nil)
l

instance (Adjunction l r, Ob r, Ob l) => Comonad (r ::: l ::: Nil) where
  epsilon :: (r ::: (l ::: Nil)) ~> I
epsilon = Obj (r ::: (l ::: Nil))
-> Obj Nil
-> (Fold (r ::: (l ::: Nil)) ~> Fold Nil)
-> Strictified (r ::: (l ::: Nil)) Nil
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (forall (p :: kk i a).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @l Obj (l ::: Nil)
-> ((r ::: Nil) ~> (r ::: Nil))
-> O (l ::: Nil) (r ::: Nil) ~> O (l ::: Nil) (r ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall (p :: kk a i).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk i) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @r) Obj I
Obj Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (l :: kk i a) (r :: kk a i). 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 @l @r)
  delta :: (r ::: (l ::: Nil)) ~> O (r ::: (l ::: Nil)) (r ::: (l ::: Nil))
delta = let r :: (r ::: Nil) ~> (r ::: Nil)
r = forall (p :: kk a i).
(Bicategory kk, Ob p, Ob0 kk a, Ob0 kk i) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @r; l :: Obj (l ::: Nil)
l = forall (p :: kk i a).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk a) =>
Obj (p ::: Nil)
forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j).
(Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) =>
Obj (p ::: Nil)
obj1 @l in Obj (l ::: Nil)
l Obj (l ::: Nil)
-> (Nil ~> ((l ::: Nil) +++ (r ::: Nil)))
-> O (l ::: Nil) Nil ~> O (l ::: Nil) ((l ::: Nil) +++ (r ::: Nil))
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj Nil
-> Obj ((l ::: Nil) +++ (r ::: Nil))
-> (Fold Nil ~> Fold ((l ::: Nil) +++ (r ::: Nil)))
-> Strictified Nil ((l ::: Nil) +++ (r ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj I
Obj Nil
forall (i :: k). Ob0 (Path kk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj ((r ::: Nil) ~> (r ::: Nil)
r ((r ::: Nil) ~> (r ::: Nil))
-> Obj (l ::: Nil)
-> O (r ::: Nil) (l ::: Nil) ~> O (r ::: Nil) (l ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (l ::: Nil)
l) (forall (l :: kk i a) (r :: kk a i). 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 @l @r) ((Nil +++ (l ::: Nil))
 ~> (((l ::: Nil) +++ (r ::: Nil)) +++ (l ::: Nil)))
-> ((r ::: Nil) ~> (r ::: Nil))
-> O (Nil +++ (l ::: Nil)) (r ::: Nil)
   ~> O (((l ::: Nil) +++ (r ::: Nil)) +++ (l ::: Nil)) (r ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| (r ::: Nil) ~> (r ::: Nil)
r