{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory (
  -- * Bicategories
  Bicategory(..)
  , BicategoryConstraints
  , IIsOb
  , appendObj

  -- * Paths
  , Path(..)
  , SPath(..)
  , IsPath(..)
  , asObj
  , asSPath
  , type (+++)
  , append
  , withAssoc
  , withUnital
  , Strictified(..)
  , Fold
  , fold
  , obj1
  , concatFold
  , splitFold
  , introI
  , elimI
  , introO
  , elimO

  -- * More
  , Monad(..)
  , Comonad(..)
  , Adjunction(..)
  , Bimodule(..)
)
where

import Data.Kind (Constraint, Type)

import Proarrow.Core (CategoryOf(..), CAT, id, Any, Profunctor(..), Promonad(..), dimapDefault)
import Proarrow.Object (Obj, obj)
import Prelude (($))

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} {j} {k} (p :: kk j k) ps. (Ob0 kk j, Ob0 kk k) => Obj p -> SPath ps -> SPath (p ::: ps)

type IsPath :: forall {kk} {j} {k}. Path kk j k -> Constraint
class IsPath (ps :: Path kk j k) where
  singPath :: SPath ps
instance 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, Ob0 kk j, Ob0 kk k, Ob (p :: kk i j), IsPath (ps :: Path kk j k), Bicategory kk) => 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} {k :: k} {kk :: k -> k -> Type} {j :: k} {k :: k}
       (p :: kk j k) (ps :: Path kk k k).
(Ob0 kk j, Ob0 kk k) =>
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

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} {k :: k} {kk :: k -> k -> Type} {j :: k} {k :: k}
       (p :: kk j k) (ps :: Path kk k k).
(Ob0 kk j, Ob0 kk k) =>
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, Ob0 kk i, Ob0 kk j) => (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, Ob0 kk i, Ob0 kk j) =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton p ~> q
f = (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).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str p ~> q
Fold (p ::: Nil) ~> Fold (q ::: Nil)
f ((Ob p, Ob q) => Strictified (p ::: Nil) (q ::: Nil))
-> (p ~> q) -> Strictified (p ::: Nil) (q ::: Nil)
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
\\ 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, Ob0 kk i, Ob0 kk j) =>
(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, Ob0 kk i, Ob0 kk j) =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton p ~> p
Obj p
p
asObj (SCons Obj p
p ps :: SPath ps
ps@SCons{}) = 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, Ob0 kk i, Ob0 kk j) =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton Obj p
p ((p ::: Nil) ~> (p ::: Nil))
-> ((p ::: ps) ~> (p ::: ps))
-> O (p ::: Nil) (p ::: ps) ~> O (p ::: Nil) (p ::: ps)
forall {k :: k} (i :: k) (j :: k) (a :: Path kk i j)
       (b :: Path kk i j) (c :: Path kk j k) (d :: Path kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` 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 ((Ob p, Ob p) => Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps)))
-> Obj p -> Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps))
forall (a :: kk i k) (b :: kk i 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
\\ 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 Obj ps
p = SPath ps
(Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob ps) => SPath ps
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
singPath ((Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob ps) => SPath ps)
-> Obj ps -> SPath ps
forall (i :: k) (j :: k) (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
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
\\\ Obj 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

withUnital
  :: forall {kk} {j} {k} (a :: Path kk j k) r
   . Bicategory kk
  => Obj a -> (a +++ Nil ~ a => r) -> r
withUnital :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (a :: Path kk j k) r.
Bicategory kk =>
Obj a -> (((a +++ Nil) ~ a) => r) -> r
withUnital Str{} = SPath a -> (((a +++ Nil) ~ a) => r) -> r
forall {k} {kk :: CAT k} {a :: k} {c :: k} (a' :: Path kk a c).
SPath a' -> (((a' +++ Nil) ~ a') => r) -> r
go (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)
  where
    go :: forall a'. SPath a' -> (a' +++ Nil ~ a' => r) -> r
    go :: forall {k} {kk :: CAT k} {a :: k} {c :: k} (a' :: Path kk a c).
SPath a' -> (((a' +++ Nil) ~ a') => r) -> r
go SPath a'
SNil ((a' +++ Nil) ~ a') => r
r = r
((a' +++ Nil) ~ a') => r
r
    go (SCons Obj p
_ SPath ps
a) ((a' +++ Nil) ~ a') => r
r = SPath ps -> (((ps +++ Nil) ~ ps) => r) -> r
forall {k} {kk :: CAT k} {a :: k} {c :: k} (a' :: Path kk a c).
SPath a' -> (((a' +++ Nil) ~ a') => r) -> r
go SPath ps
a r
((a' +++ Nil) ~ a') => r
((ps +++ Nil) ~ ps) => r
r

concatFold
  :: forall {kk} {i} {j} {k} (as :: Path kk i j) (bs :: Path kk j k). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk)
  => Fold as `O` Fold bs ~> 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).
(Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk) =>
O (Fold as) (Fold bs) ~> Fold (as +++ bs)
concatFold =
  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 (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 @bs)
      h :: forall cs. SPath cs -> (Fold cs `O` Fold bs) ~> Fold (cs +++ bs)
      h :: forall {j :: k} (cs :: Path kk j j).
SPath cs -> O (Fold cs) (Fold bs) ~> Fold (cs +++ bs)
h SPath cs
SNil = (Fold bs ~> Fold bs) -> O I (Fold bs) ~> Fold bs
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 Fold bs ~> Fold bs
fbs
      -- h (SCons c cs) = (c `o` h cs) . associator c (fold cs) fbs
      h (SCons Obj p
c SPath ps
SNil) = case 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 @bs of
        SPath bs
SNil -> Obj p -> O p I ~> p
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 p
c
        SCons{} -> Obj p
c Obj p
-> (Fold (p ::: ps) ~> Fold (p ::: ps))
-> O p (Fold (p ::: ps)) ~> O p (Fold (p ::: ps))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Fold bs ~> Fold bs
Fold (p ::: ps) ~> Fold (p ::: ps)
fbs
      h (SCons Obj p
c cs :: SPath ps
cs@SCons{}) = (Obj p
c Obj p
-> (O (Fold (p ::: ps)) (Fold bs) ~> Fold (p ::: (ps +++ bs)))
-> O p (O (Fold (p ::: ps)) (Fold bs))
   ~> O p (Fold (p ::: (ps +++ bs)))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` SPath ps -> O (Fold ps) (Fold bs) ~> Fold (ps +++ bs)
forall {j :: k} (cs :: Path kk j j).
SPath cs -> O (Fold cs) (Fold bs) ~> Fold (cs +++ bs)
h SPath ps
cs) (O p (O (Fold (p ::: ps)) (Fold bs))
 ~> O p (Fold (p ::: (ps +++ bs))))
-> (O (O p (Fold (p ::: ps))) (Fold bs)
    ~> O p (O (Fold (p ::: ps)) (Fold bs)))
-> O (O p (Fold (p ::: ps))) (Fold bs)
   ~> O p (Fold (p ::: (ps +++ bs)))
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
. Obj p
-> Obj (Fold (p ::: ps))
-> (Fold bs ~> Fold bs)
-> O (O p (Fold (p ::: ps))) (Fold bs)
   ~> O p (O (Fold (p ::: ps)) (Fold bs))
forall {j :: k} {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk j j) (c :: kk j k).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j :: k} {k :: k} (i :: k) (j :: k)
       (a :: kk i j) (b :: kk j j) (c :: kk j k).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj p
c (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) Fold bs ~> Fold bs
fbs
  in SPath as -> O (Fold as) (Fold bs) ~> Fold (as +++ bs)
forall {j :: k} (cs :: Path kk j j).
SPath cs -> O (Fold cs) (Fold bs) ~> Fold (cs +++ bs)
h (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk i j). IsPath ps => SPath ps
singPath @as)

splitFold
  :: forall {kk} {i} {j} {k} (as :: Path kk i j) (bs :: Path kk j k). (Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk)
  => Fold (as +++ bs) ~> Fold as `O` Fold bs
splitFold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} {k :: k}
       (as :: Path kk i j) (bs :: Path kk j k).
(Ob as, Ob bs, Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk) =>
Fold (as +++ bs) ~> O (Fold as) (Fold bs)
splitFold =
  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 (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 @bs)
      h :: forall cs. SPath cs -> Fold (cs +++ bs) ~> Fold cs `O` Fold bs
      h :: forall {i :: k} (cs :: Path kk i j).
SPath cs -> Fold (cs +++ bs) ~> O (Fold cs) (Fold bs)
h SPath cs
SNil = (Fold bs ~> Fold bs) -> Fold bs ~> O I (Fold bs)
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 Fold bs ~> Fold bs
fbs
      -- h (SCons c cs) = associatorInv c (fold cs) fbs . (c `o` h cs)
      h (SCons Obj p
c SPath ps
SNil) = case 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 @bs of
        SPath bs
SNil -> Obj p -> p ~> O p 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 p
Obj p
c
        SCons{} -> Obj p
c Obj p
-> (Fold (p ::: ps) ~> Fold (p ::: ps))
-> O p (Fold (p ::: ps)) ~> O p (Fold (p ::: ps))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Fold bs ~> Fold bs
Fold (p ::: ps) ~> Fold (p ::: ps)
fbs
      h (SCons Obj p
c cs :: SPath ps
cs@SCons{}) = Obj p
-> Obj (Fold (p ::: ps))
-> (Fold bs ~> Fold bs)
-> O p (O (Fold (p ::: ps)) (Fold bs))
   ~> O (O p (Fold (p ::: ps))) (Fold bs)
forall {j :: k} {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk j j) (c :: kk j k).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j :: k} {k :: k} (i :: k) (j :: k)
       (a :: kk i j) (b :: kk j j) (c :: kk j k).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj p
c (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) Fold bs ~> Fold bs
fbs (O p (O (Fold (p ::: ps)) (Fold bs))
 ~> O (O p (Fold (p ::: ps))) (Fold bs))
-> (O p (Fold (p ::: (ps +++ bs)))
    ~> O p (O (Fold (p ::: ps)) (Fold bs)))
-> O p (Fold (p ::: (ps +++ bs)))
   ~> O (O p (Fold (p ::: ps))) (Fold bs)
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 p
c Obj p
-> (Fold (p ::: (ps +++ bs)) ~> O (Fold (p ::: ps)) (Fold bs))
-> O p (Fold (p ::: (ps +++ bs)))
   ~> O p (O (Fold (p ::: ps)) (Fold bs))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` SPath ps -> Fold (ps +++ bs) ~> O (Fold ps) (Fold bs)
forall {i :: k} (cs :: Path kk i j).
SPath cs -> Fold (cs +++ bs) ~> O (Fold cs) (Fold bs)
h SPath ps
cs)
  in SPath as -> Fold (as +++ bs) ~> O (Fold as) (Fold bs)
forall {i :: k} (cs :: Path kk i j).
SPath cs -> Fold (cs +++ bs) ~> O (Fold cs) (Fold bs)
h (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk i j). IsPath ps => SPath ps
singPath @as)

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 ::: ps) = p `O` Fold ps
type instance Fold (p ::: Nil) = p
type instance Fold (p ::: (q ::: ps)) = p `O` Fold (q ::: ps)

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 = I ~> I
Fold as ~> Fold as
forall (a :: kk i i). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
-- fold (SCons p ps) = p `o` fold ps
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{}) = Obj p
p Obj p
-> (Fold (p ::: ps) ~> Fold (p ::: ps))
-> O p (Fold (p ::: ps)) ~> O p (Fold (p ::: ps))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` 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


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

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

instance (CategoryOf (kk j k), Ob0 kk j, Ob0 kk 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{} = r
(Ob a, Ob b) => r
r
instance (CategoryOf (kk j k), Ob0 kk j, Ob0 kk 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 = (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).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str (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 (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))
  Str 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 Fold a ~> Fold b
n = (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).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str (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), Ob0 kk j, Ob0 kk k, Bicategory kk) => CategoryOf (Path kk j k) where
  type (~>) = Strictified
  type Ob (ps :: Path kk j k) = (IsPath ps, Ob (Fold ps))

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 = (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).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str Obj I
Fold Nil ~> Fold (I ::: Nil)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj

elimI :: forall {kk} {j}. (Ob0 kk j, Bicategory kk) => (I ::: Nil) ~> (Nil :: Path kk j j)
elimI :: forall {k} {kk :: CAT k} {j :: k}.
(Ob0 kk j, Bicategory kk) =>
(I ::: Nil) ~> Nil
elimI = (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).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str Obj I
Fold (I ::: Nil) ~> Fold Nil
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj

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) ~> (p `O` q ::: 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 p q ::: Nil)
introO = (Fold (p ::: (q ::: Nil)) ~> Fold (O p q ::: Nil))
-> Strictified (p ::: (q ::: Nil)) (O p q ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str O p q ~> O p q
Fold (p ::: (q ::: Nil)) ~> Fold (O p q ::: Nil)
forall (a :: kk i k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (O p q), Ob (O p q)) =>
 Strictified (p ::: (q ::: Nil)) (O p q ::: Nil))
-> (O p q ~> O p q)
-> Strictified (p ::: (q ::: Nil)) (O p q ::: Nil)
forall (a :: kk i k) (b :: kk i 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
\\ (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 Obj p -> (q ~> q) -> O p q ~> O p q
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
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 @q)

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)
  => (p `O` q ::: 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 p q ::: Nil) ~> (p ::: (q ::: Nil))
elimO = (Fold (O p q ::: Nil) ~> Fold (p ::: (q ::: Nil)))
-> Strictified (O p q ::: Nil) (p ::: (q ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str O p q ~> O p q
Fold (O p q ::: Nil) ~> Fold (p ::: (q ::: Nil))
forall (a :: kk i k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (O p q), Ob (O p q)) =>
 Strictified (O p q ::: Nil) (p ::: (q ::: Nil)))
-> (O p q ~> O p q)
-> Strictified (O p q ::: Nil) (p ::: (q ::: Nil))
forall (a :: kk i k) (b :: kk i 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
\\ (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 Obj p -> (q ~> q) -> O p q ~> O p q
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
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 @q)


class Ob (I :: kk i i) => IIsOb kk i
instance Ob (I :: kk i i) => IIsOb kk i

class (forall j k. (Ob0 kk j, Ob0 kk k) => CategoryOf (kk j k), forall i. Ob0 kk i => IIsOb kk i) => BicategoryConstraints kk
instance (forall j k. (Ob0 kk j, Ob0 kk k) => CategoryOf (kk j k), forall i. Ob0 kk i => IIsOb kk i) => BicategoryConstraints kk

-- | Bicategories.
--
-- * 0-cells are kinds @i@, @j@, @k@... satisfying the @Ob0 kk@ constraint.
-- * 1-cells are types of kind @kk j k@ for any 0-cells @j@ and @k@, satisfying the @Ob@ constraint.
-- * 2-cells are values of type @p ~> q@, where @p@ and @q@ are 1-cells.
type Bicategory :: CAT k -> Constraint
class BicategoryConstraints kk => Bicategory kk where
  type Ob0 kk (j :: k) :: Constraint
  type Ob0 kk j = Any j
  type I :: kk i i
  type O (p :: kk i j) (q :: kk j k) :: kk i k
  -- | Horizontal composition of 2-cells.
  o :: (a :: kk i j) ~> b -> c ~> d -> (a `O` c) ~> (b `O` d)
  -- | Observe constraints from a 2-cell value.
  (\\\) :: ((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps :: kk i j) ~> qs -> r
  leftUnitor :: Obj (a :: kk i j) -> (I `O` a) ~> a
  leftUnitorInv :: Obj (a :: kk i j) -> a ~> (I `O` a)
  rightUnitor :: Obj (a :: kk i j) -> (a `O` I) ~> a
  rightUnitorInv :: Obj (a :: kk i j) -> a ~> (a `O` I)
  associator :: Obj (a :: kk i j) -> Obj b -> Obj c -> (a `O` b) `O` c ~> a `O` (b `O` c)
  associatorInv :: Obj (a :: kk i j) -> Obj b -> Obj c -> a `O` (b `O` c) ~> (a `O` b) `O` c

appendObj
  :: forall {kk} {i} {j} {k} (a :: kk i j) (b :: kk j k) r
   . (Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b)
  => (Ob (a `O` b) => r) -> r
appendObj :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (a :: kk i j) (b :: kk j k) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj Ob (O a b) => r
r = r
Ob (O a b) => r
(Ob0 kk i, Ob0 kk k, Ob (O a b), Ob (O a b)) => r
r ((Ob0 kk i, Ob0 kk k, Ob (O a b), Ob (O a b)) => r)
-> (O a b ~> O a b) -> 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
\\\ (forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> O a b ~> O a b
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
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 @b)


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



type Monad :: forall {kk} {a}. kk a a -> Constraint
class (Bicategory kk, Ob0 kk a, Ob t) => Monad (t :: kk a a) where
  eta :: I ~> t
  mu :: t `O` t ~> t

instance (Bicategory (Path kk), Ob0 kk a) => Monad (Nil :: Path kk a a) where
  eta :: I ~> Nil
eta = I ~> Nil
Strictified Nil Nil
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id
  mu :: O Nil Nil ~> Nil
mu = O Nil Nil ~> Nil
Strictified Nil Nil
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id

class (Bicategory kk, Ob0 kk a, Ob t) => Comonad (t :: kk a a) where
  epsilon :: t ~> I
  delta :: t ~> t `O` t

instance (Bicategory (Path kk), Ob0 kk a) => Comonad (Nil :: Path kk a a) where
  epsilon :: Nil ~> I
epsilon = Nil ~> I
Strictified Nil Nil
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id
  delta :: Nil ~> O Nil Nil
delta = Nil ~> O Nil Nil
Strictified Nil Nil
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id

class (Monad s, Monad t) => Bimodule s t (p :: kk a b) where
  leftAction :: s `O` p ~> p
  rightAction :: p `O` t ~> p

instance {-# OVERLAPPABLE #-} Monad s => Bimodule s s s where
  leftAction :: O s s ~> s
leftAction = O s s ~> s
forall k (kk :: k -> k -> Type) (b :: k) (s :: kk b b).
Monad s =>
O s s ~> s
mu
  rightAction :: O s s ~> s
rightAction = O s s ~> s
forall k (kk :: k -> k -> Type) (b :: k) (s :: kk b b).
Monad s =>
O s s ~> s
mu

type Adjunction :: forall {kk} {c} {d}. kk c d -> kk d c -> Constraint
class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob l, Ob r) => Adjunction (l :: kk c d) (r :: kk d c) where
  unit :: I ~> r `O` l
  counit :: l `O` r ~> I

instance (Adjunction l r, Ob (r `O` l)) => Monad (r ::: l ::: Nil) where
  eta :: I ~> (r ::: (l ::: Nil))
eta = (Fold Nil ~> Fold (r ::: (l ::: Nil)))
-> Strictified Nil (r ::: (l ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str (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)
  mu :: O (r ::: (l ::: Nil)) (r ::: (l ::: Nil)) ~> (r ::: (l ::: Nil))
mu = let r :: Obj r
r = forall (a :: kk a i). (CategoryOf (kk a i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r; l :: Obj l
l = forall (a :: kk i a). (CategoryOf (kk i a), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @l in (Fold (r ::: (l ::: (r ::: (l ::: Nil))))
 ~> Fold (r ::: (l ::: Nil)))
-> Strictified
     (r ::: (l ::: (r ::: (l ::: Nil)))) (r ::: (l ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Bicategory kk, IsPath ps, IsPath qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
mkStr (Obj r
r Obj r -> (O l (O r l) ~> l) -> O r (O l (O r l)) ~> O r l
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` (Obj l -> O I l ~> l
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 l
l (O I l ~> l) -> (O l (O r l) ~> O I l) -> O l (O r l) ~> l
forall (b :: kk i a) (c :: kk i a) (a :: kk i a).
(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
. (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 (O l r ~> I) -> Obj l -> O (O l r) l ~> O I l
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj l
l) (O (O l r) l ~> O I l)
-> (O l (O r l) ~> O (O l r) l) -> O l (O r l) ~> O I l
forall (b :: kk i a) (c :: kk i a) (a :: kk i a).
(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 l -> Obj r -> Obj l -> O l (O r l) ~> O (O l r) l
forall {j :: k} {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk j j) (c :: kk j k).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j :: k} {k :: k} (i :: k) (j :: k)
       (a :: kk i j) (b :: kk j j) (c :: kk j k).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj l
l Obj r
r Obj l
l))

instance (Adjunction l r, Ob (l `O` r)) => Comonad (l ::: r ::: Nil) where
  epsilon :: (l ::: (r ::: Nil)) ~> I
epsilon = (Fold (l ::: (r ::: Nil)) ~> Fold Nil)
-> Strictified (l ::: (r ::: Nil)) Nil
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
Str (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)
  delta :: (l ::: (r ::: Nil)) ~> O (l ::: (r ::: Nil)) (l ::: (r ::: Nil))
delta = let r :: Obj r
r = forall (a :: kk i a). (CategoryOf (kk i a), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r; l :: Obj l
l = forall (a :: kk a i). (CategoryOf (kk a i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @l in (Fold (l ::: (r ::: Nil))
 ~> Fold (l ::: (r ::: (l ::: (r ::: Nil)))))
-> Strictified
     (l ::: (r ::: Nil)) (l ::: (r ::: (l ::: (r ::: Nil))))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Bicategory kk, IsPath ps, IsPath qs, Ob0 kk j, Ob0 kk k) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
mkStr (Obj l
l Obj l -> (r ~> O r (O l r)) -> O l r ~> O l (O r (O l r))
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` (Obj r -> Obj l -> Obj r -> O (O r l) r ~> O r (O l r)
forall {j :: k} {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk j j) (c :: kk j k).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j :: k} {k :: k} (i :: k) (j :: k)
       (a :: kk i j) (b :: kk j j) (c :: kk j k).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj r
r Obj l
l Obj r
r (O (O r l) r ~> O r (O l r))
-> (r ~> O (O r l) r) -> r ~> O r (O l r)
forall (b :: kk i a) (c :: kk i a) (a :: kk i a).
(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
. (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 (I ~> O r l) -> Obj r -> O I r ~> O (O r l) r
forall {k :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k) (d :: kk j k).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k) (d :: kk j k).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj r
r) (O I r ~> O (O r l) r) -> (r ~> O I r) -> r ~> O (O r l) r
forall (b :: kk i a) (c :: kk i a) (a :: kk i a).
(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 r -> r ~> O I r
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 r
r))