{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Strictified where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Bicategory
  ( Adjunction (..)
  , Bicategory (..)
  , Comonad (..)
  , Monad (..)
  , associator'
  , associatorInv'
  , leftUnitorInvWith
  , leftUnitorWith
  , rightUnitorWith
  , (||)
  )
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..))
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
  withIsPath2 :: IsPath qs => ((Ob (ps +++ qs)) => r) -> r
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
  withIsPath2 :: forall {c :: k} (qs :: Path kk k c) r.
IsPath qs =>
(Ob (Nil +++ qs) => r) -> r
withIsPath2 Ob (Nil +++ qs) => r
r = r
Ob (Nil +++ qs) => r
r
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
  withIsPath2 :: forall {c :: k} (qs :: Path kk k c) r.
IsPath qs =>
(Ob ((p ::: ps) +++ qs) => r) -> r
withIsPath2 @qs Ob ((p ::: ps) +++ qs) => r
r = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       {c :: k} (qs :: Path kk k c) r.
(IsPath ps, IsPath qs) =>
(Ob (ps +++ qs) => r) -> r
forall (ps :: Path kk j k) {c :: k} (qs :: Path kk k c) r.
(IsPath ps, IsPath qs) =>
(Ob (ps +++ qs) => r) -> r
withIsPath2 @ps @qs r
Ob ((p ::: ps) +++ qs) => r
Ob (ps +++ qs) => r
r

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 {j} {k} (a :: k) (b :: j) (p :: j +-> k).
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 :: k1 +-> k2).
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 :: j +-> k) (a :: k) (b :: j) 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 @_ @_ @_ @ps Obj ps
p = 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 @ps ((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 {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 ps
p

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 :: 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 :: 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 = I ~> I
Fold as ~> Fold as
forall (a :: kk i i). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
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

st :: forall {kk} {i} {j} (ps :: Path kk i j) qs. (Bicategory kk, Ob ps, Ob qs) => (Fold ps ~> Fold qs) -> Strictified ps qs
st :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st = 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 (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 @ps) (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 @qs)

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 :: 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 (as :: Path kk j k). (Ob as) => Strictified as as
  id :: forall (a :: Path kk j k). Ob a => Strictified a a
id = forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk j k) (qs :: Path kk j k).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @as @as (SPath as -> Fold as ~> Fold as
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 @as))
  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 :: 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 (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil) Obj I
Fold Nil ~> Fold (I ::: Nil)
forall (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

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 (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id 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 (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

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
  withOb2 :: forall {i :: s} {j :: s} {k :: s} (a :: Path kk j k)
       (b :: Path kk i j) r.
(Ob a, Ob b, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path kk) k) =>
(Ob (O a b) => r) -> r
withOb2 @ps @qs = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       {c :: k} (qs :: Path kk k c) r.
(IsPath ps, IsPath qs) =>
(Ob (ps +++ qs) => r) -> r
forall (ps :: Path kk i j) {c :: s} (qs :: Path kk j c) r.
(IsPath ps, IsPath qs) =>
(Ob (ps +++ qs) => r) -> r
withIsPath2 @qs @ps
  withOb0s :: forall {j :: s} {k :: s} (a :: Path kk j k) r.
Ob a =>
((Ob0 (Path kk) j, Ob0 (Path kk) k) => r) -> r
withOb0s @ps (Ob0 (Path kk) j, Ob0 (Path kk) k) => r
r = 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 @ps of
    SPath a
SNil -> r
(Ob0 (Path kk) j, Ob0 (Path kk) k) => r
r
    SCons @p Obj p
p SPath ps
ps -> forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p (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
(Ob0 (Path kk) j, Ob0 (Path 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 :: s) (j :: s) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj p
p
  (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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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

companionFold
  :: forall {hk} {vk} {j} {k} (fs :: Path vk j k)
   . (HasCompanions hk vk)
  => SPath fs
  -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath fs
SNil = Companion hk I ~> I
Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
forall (k :: k). Ob0 vk k => Companion hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId
companionFold (SCons Obj p
f SPath ps
SNil) = (p ~> p) -> Companion hk p ~> Companion hk p
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion p ~> p
Obj p
f
companionFold (SCons Obj p
f fs :: SPath ps
fs@SCons{}) = let cfs :: O (Companion hk (Fold (p ::: ps))) (Companion hk p)
~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
cfs = SPath ps -> Companion hk (Fold ps) ~> Fold (Companion (Path hk) ps)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath ps
fs (Companion hk (Fold (p ::: ps))
 ~> Fold (Companion hk p ::: Companion (Path hk) ps))
-> (Companion hk p ~> Companion hk p)
-> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
   ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
        (Companion hk p)
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk 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 {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj p
f in (O (Companion hk (Fold (p ::: ps))) (Companion hk p)
~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
cfs (O (Companion hk (Fold (p ::: ps))) (Companion hk p)
 ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
      (Companion hk p))
-> (Companion hk (O (Fold (p ::: ps)) p)
    ~> O (Companion hk (Fold (p ::: ps))) (Companion hk p))
-> Companion hk (O (Fold (p ::: ps)) p)
   ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
        (Companion hk p)
forall (b :: hk j k) (c :: hk j k) (a :: hk j k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Fold (p ::: ps))
-> Obj p
-> Companion hk (O (Fold (p ::: ps)) p)
   ~> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose (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) Obj p
f) ((Ob0 hk j, Ob0 hk k,
  Ob (O (Companion hk (Fold (p ::: ps))) (Companion hk p)),
  Ob
    (O (Fold (Companion hk p ::: Companion (Path hk) ps))
       (Companion hk p))) =>
 Companion hk (O (Fold (p ::: ps)) p)
 ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
      (Companion hk p))
-> (O (Companion hk (Fold (p ::: ps))) (Companion hk p)
    ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
         (Companion hk p))
-> Companion hk (O (Fold (p ::: ps)) p)
   ~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
        (Companion hk p)
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Companion hk (Fold (p ::: ps))) (Companion hk p)
~> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
cfs

foldCompanion
  :: forall {hk} {vk} {j} {k} (fs :: Path vk j k)
   . (HasCompanions hk vk)
  => SPath fs
  -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath fs
SNil = I ~> Companion hk I
Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
forall (k :: k). Ob0 vk k => I ~> Companion hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId
foldCompanion (SCons Obj p
f SPath ps
SNil) = (p ~> p) -> Companion hk p ~> Companion hk p
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion p ~> p
Obj p
f
foldCompanion (SCons Obj p
f fs :: SPath ps
fs@SCons{}) = let cfs :: O (Fold (Companion hk p ::: Companion (Path hk) ps))
  (Companion hk p)
~> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
cfs = SPath ps -> Fold (Companion (Path hk) ps) ~> Companion hk (Fold ps)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath ps
fs (Fold (Companion hk p ::: Companion (Path hk) ps)
 ~> Companion hk (Fold (p ::: ps)))
-> (Companion hk p ~> Companion hk p)
-> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
   ~> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk 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 {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj p
f in (Obj (Fold (p ::: ps))
-> Obj p
-> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
   ~> Companion hk (O (Fold (p ::: ps)) p)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose (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) Obj p
f (O (Companion hk (Fold (p ::: ps))) (Companion hk p)
 ~> Companion hk (O (Fold (p ::: ps)) p))
-> (O (Fold (Companion hk p ::: Companion (Path hk) ps))
      (Companion hk p)
    ~> O (Companion hk (Fold (p ::: ps))) (Companion hk p))
-> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
   ~> Companion hk (O (Fold (p ::: ps)) p)
forall (b :: hk j k) (c :: hk j k) (a :: hk j k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. O (Fold (Companion hk p ::: Companion (Path hk) ps))
  (Companion hk p)
~> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
cfs) ((Ob0 hk j, Ob0 hk k,
  Ob
    (O (Fold (Companion hk p ::: Companion (Path hk) ps))
       (Companion hk p)),
  Ob (O (Companion hk (Fold (p ::: ps))) (Companion hk p))) =>
 O (Fold (Companion hk p ::: Companion (Path hk) ps))
   (Companion hk p)
 ~> Companion hk (O (Fold (p ::: ps)) p))
-> (O (Fold (Companion hk p ::: Companion (Path hk) ps))
      (Companion hk p)
    ~> O (Companion hk (Fold (p ::: ps))) (Companion hk p))
-> O (Fold (Companion hk p ::: Companion (Path hk) ps))
     (Companion hk p)
   ~> Companion hk (O (Fold (p ::: ps)) p)
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ O (Fold (Companion hk p ::: Companion (Path hk) ps))
  (Companion hk p)
~> O (Companion hk (Fold (p ::: ps))) (Companion hk p)
cfs

mapCompanionSPath
  :: forall hk {vk} {j} {k} (fs :: Path vk j k)
   . (HasCompanions hk vk)
  => SPath fs
  -> SPath (Companion (Path hk) fs)
mapCompanionSPath :: forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath fs
SNil = SPath Nil
SPath (Companion (Path hk) fs)
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil
mapCompanionSPath (SCons Obj p
f SPath ps
fs) = Obj (Companion hk p)
-> SPath (Companion (Path hk) ps)
-> SPath (Companion hk p ::: Companion (Path hk) 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 -> Obj (Companion hk p)
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion Obj p
f) (SPath ps -> SPath (Companion (Path hk) ps)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath ps
fs)

instance (HasCompanions hk vk) => HasCompanions (Path hk) (Path vk) where
  type Companion (Path hk) Nil = Nil
  type Companion (Path hk) (p ::: ps) = Companion hk p ::: Companion (Path hk) ps

  mapCompanion :: forall {j :: k} {k :: k} (f :: Path vk j k) (g :: Path vk j k).
(f ~> g) -> Companion (Path hk) f ~> Companion (Path hk) g
mapCompanion (Str SPath f
fs SPath g
gs Fold f ~> Fold g
n) =
    SPath (Companion (Path hk) f)
-> SPath (Companion (Path hk) g)
-> (Fold (Companion (Path hk) f) ~> Fold (Companion (Path hk) g))
-> Strictified (Companion (Path hk) f) (Companion (Path hk) g)
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 (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath @hk SPath f
fs) (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath @hk SPath g
gs) ((Fold (Companion (Path hk) f) ~> Fold (Companion (Path hk) g))
 -> Strictified (Companion (Path hk) f) (Companion (Path hk) g))
-> (Fold (Companion (Path hk) f) ~> Fold (Companion (Path hk) g))
-> Strictified (Companion (Path hk) f) (Companion (Path hk) g)
forall a b. (a -> b) -> a -> b
$ SPath g -> Companion hk (Fold g) ~> Fold (Companion (Path hk) g)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath g
gs (Companion hk (Fold g) ~> Fold (Companion (Path hk) g))
-> (Fold (Companion (Path hk) f) ~> Companion hk (Fold g))
-> Fold (Companion (Path hk) f) ~> Fold (Companion (Path hk) g)
forall (b :: hk j k) (c :: hk j k) (a :: hk j k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk @vk Fold f ~> Fold g
n (Companion hk (Fold f) ~> Companion hk (Fold g))
-> (Fold (Companion (Path hk) f) ~> Companion hk (Fold f))
-> Fold (Companion (Path hk) f) ~> Companion hk (Fold g)
forall (b :: hk j k) (c :: hk j k) (a :: hk j k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. SPath f -> Fold (Companion (Path hk) f) ~> Companion hk (Fold f)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath f
fs

  withObCompanion :: forall {j :: k} {k :: k} (f :: Path vk j k) r.
Ob f =>
(Ob (Companion (Path hk) f) => r) -> r
withObCompanion @p Ob (Companion (Path hk) f) => r
r = SPath (Companion (Path hk) f)
-> ((IsPath (Companion (Path hk) f), Ob0 hk j, Ob0 hk 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 (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath @hk (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @p)) r
Ob (Companion (Path hk) f) => r
(IsPath (Companion (Path hk) f), Ob0 hk j, Ob0 hk k) => r
r

  compToId :: forall (k :: k). Ob0 (Path vk) k => Companion (Path hk) I ~> I
compToId = SPath Nil
-> SPath Nil -> (Fold Nil ~> Fold Nil) -> Strictified 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 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 I ~> I
Fold Nil ~> Fold Nil
forall (a :: hk k k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  compFromId :: forall (k :: k). Ob0 (Path vk) k => I ~> Companion (Path hk) I
compFromId = SPath Nil
-> SPath Nil -> (Fold Nil ~> Fold Nil) -> Strictified 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 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 I ~> I
Fold Nil ~> Fold Nil
forall (a :: hk k k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  compToCompose :: forall {i :: k} {j :: k} {k :: k} (f :: Path vk j k)
       (g :: Path vk i j).
Obj f
-> Obj g
-> Companion (Path hk) (O f g)
   ~> O (Companion (Path hk) f) (Companion (Path hk) g)
compToCompose (Str SPath f
fs SPath f
_ Fold f ~> Fold f
f) (Str SPath g
gs SPath g
_ Fold g ~> Fold g
g) =
    let cfs :: SPath (Companion (Path hk) f)
cfs = SPath f -> SPath (Companion (Path hk) f)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath f
fs
        cgs :: SPath (Companion (Path hk) g)
cgs = SPath g -> SPath (Companion (Path hk) g)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath g
gs
        fgs :: SPath (g +++ f)
fgs = SPath g -> SPath f -> SPath (g +++ f)
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 g
gs SPath f
fs
    in SPath (Companion (Path hk) (g +++ f))
-> SPath (Companion (Path hk) g +++ Companion (Path hk) f)
-> (Fold (Companion (Path hk) (g +++ f))
    ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f))
-> Strictified
     (Companion (Path hk) (g +++ f))
     (Companion (Path hk) g +++ Companion (Path hk) f)
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 (g +++ f) -> SPath (Companion (Path hk) (g +++ f))
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath (g +++ f)
fgs) (SPath (Companion (Path hk) g)
cgs SPath (Companion (Path hk) g)
-> SPath (Companion (Path hk) f)
-> SPath (Companion (Path hk) g +++ Companion (Path hk) f)
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 (Companion (Path hk) f)
cfs) ((Fold (Companion (Path hk) (g +++ f))
  ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f))
 -> Strictified
      (Companion (Path hk) (g +++ f))
      (Companion (Path hk) g +++ Companion (Path hk) f))
-> (Fold (Companion (Path hk) (g +++ f))
    ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f))
-> Strictified
     (Companion (Path hk) (g +++ f))
     (Companion (Path hk) g +++ Companion (Path hk) f)
forall a b. (a -> b) -> a -> b
$
        SPath (Companion (Path hk) g)
-> SPath (Companion (Path hk) f)
-> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
   ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
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 (Companion (Path hk) g)
cgs SPath (Companion (Path hk) f)
cfs
          (O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
 ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f))
-> (Fold (Companion (Path hk) (g +++ f))
    ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g)))
-> Fold (Companion (Path hk) (g +++ f))
   ~> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
forall (b :: hk i k) (c :: hk i k) (a :: hk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (SPath f -> Companion hk (Fold f) ~> Fold (Companion (Path hk) f)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath f
fs (Companion hk (Fold f) ~> Fold (Companion (Path hk) f))
-> (Companion hk (Fold g) ~> Fold (Companion (Path hk) g))
-> O (Companion hk (Fold f)) (Companion hk (Fold g))
   ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk 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` SPath g -> Companion hk (Fold g) ~> Fold (Companion (Path hk) g)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath g
gs)
          (O (Companion hk (Fold f)) (Companion hk (Fold g))
 ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g)))
-> (Fold (Companion (Path hk) (g +++ f))
    ~> O (Companion hk (Fold f)) (Companion hk (Fold g)))
-> Fold (Companion (Path hk) (g +++ f))
   ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
forall (b :: hk i k) (c :: hk i k) (a :: hk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Fold f ~> Fold f)
-> (Fold g ~> Fold g)
-> Companion hk (O (Fold f) (Fold g))
   ~> O (Companion hk (Fold f)) (Companion hk (Fold g))
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose Fold f ~> Fold f
f Fold g ~> Fold g
g
          (Companion hk (O (Fold f) (Fold g))
 ~> O (Companion hk (Fold f)) (Companion hk (Fold g)))
-> (Fold (Companion (Path hk) (g +++ f))
    ~> Companion hk (O (Fold f) (Fold g)))
-> Fold (Companion (Path hk) (g +++ f))
   ~> O (Companion hk (Fold f)) (Companion hk (Fold g))
forall (b :: hk i k) (c :: hk i k) (a :: hk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Fold (g +++ f) ~> O (Fold f) (Fold g))
-> Companion hk (Fold (g +++ f))
   ~> Companion hk (O (Fold f) (Fold g))
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion (SPath g -> SPath f -> Fold (g +++ f) ~> O (Fold f) (Fold g)
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 g
gs SPath f
fs)
          (Companion hk (Fold (g +++ f))
 ~> Companion hk (O (Fold f) (Fold g)))
-> (Fold (Companion (Path hk) (g +++ f))
    ~> Companion hk (Fold (g +++ f)))
-> Fold (Companion (Path hk) (g +++ f))
   ~> Companion hk (O (Fold f) (Fold g))
forall (b :: hk i k) (c :: hk i k) (a :: hk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. SPath (g +++ f)
-> Fold (Companion (Path hk) (g +++ f))
   ~> Companion hk (Fold (g +++ f))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath (g +++ f)
fgs
  compFromCompose :: forall {j1 :: k} {j2 :: k} {k :: k} (f :: Path vk j2 k)
       (g :: Path vk j1 j2).
Obj f
-> Obj g
-> O (Companion (Path hk) f) (Companion (Path hk) g)
   ~> Companion (Path hk) (O f g)
compFromCompose (Str SPath f
fs SPath f
_ Fold f ~> Fold f
f) (Str SPath g
gs SPath g
_ Fold g ~> Fold g
g) =
    let cfs :: SPath (Companion (Path hk) f)
cfs = SPath f -> SPath (Companion (Path hk) f)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath f
fs
        cgs :: SPath (Companion (Path hk) g)
cgs = SPath g -> SPath (Companion (Path hk) g)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath g
gs
        fgs :: SPath (g +++ f)
fgs = SPath g -> SPath f -> SPath (g +++ f)
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 g
gs SPath f
fs
    in SPath (Companion (Path hk) g +++ Companion (Path hk) f)
-> SPath (Companion (Path hk) (g +++ f))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> Fold (Companion (Path hk) (g +++ f)))
-> Strictified
     (Companion (Path hk) g +++ Companion (Path hk) f)
     (Companion (Path hk) (g +++ f))
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 (Companion (Path hk) g)
cgs SPath (Companion (Path hk) g)
-> SPath (Companion (Path hk) f)
-> SPath (Companion (Path hk) g +++ Companion (Path hk) f)
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 (Companion (Path hk) f)
cfs) (SPath (g +++ f) -> SPath (Companion (Path hk) (g +++ f))
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath (g +++ f)
fgs) ((Fold (Companion (Path hk) g +++ Companion (Path hk) f)
  ~> Fold (Companion (Path hk) (g +++ f)))
 -> Strictified
      (Companion (Path hk) g +++ Companion (Path hk) f)
      (Companion (Path hk) (g +++ f)))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> Fold (Companion (Path hk) (g +++ f)))
-> Strictified
     (Companion (Path hk) g +++ Companion (Path hk) f)
     (Companion (Path hk) (g +++ f))
forall a b. (a -> b) -> a -> b
$
        SPath (g +++ f)
-> Companion hk (Fold (g +++ f))
   ~> Fold (Companion (Path hk) (g +++ f))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath (g +++ f)
fgs
          (Companion hk (Fold (g +++ f))
 ~> Fold (Companion (Path hk) (g +++ f)))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> Companion hk (Fold (g +++ f)))
-> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
   ~> Fold (Companion (Path hk) (g +++ f))
forall (b :: hk j1 k) (c :: hk j1 k) (a :: hk j1 k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (O (Fold f) (Fold g) ~> Fold (g +++ f))
-> Companion hk (O (Fold f) (Fold g))
   ~> Companion hk (Fold (g +++ f))
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion (SPath g -> SPath f -> O (Fold f) (Fold g) ~> Fold (g +++ f)
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 g
gs SPath f
fs)
          (Companion hk (O (Fold f) (Fold g))
 ~> Companion hk (Fold (g +++ f)))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> Companion hk (O (Fold f) (Fold g)))
-> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
   ~> Companion hk (Fold (g +++ f))
forall (b :: hk j1 k) (c :: hk j1 k) (a :: hk j1 k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Fold f ~> Fold f)
-> (Fold g ~> Fold g)
-> O (Companion hk (Fold f)) (Companion hk (Fold g))
   ~> Companion hk (O (Fold f) (Fold g))
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Fold f ~> Fold f
f Fold g ~> Fold g
g
          (O (Companion hk (Fold f)) (Companion hk (Fold g))
 ~> Companion hk (O (Fold f) (Fold g)))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> O (Companion hk (Fold f)) (Companion hk (Fold g)))
-> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
   ~> Companion hk (O (Fold f) (Fold g))
forall (b :: hk j1 k) (c :: hk j1 k) (a :: hk j1 k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (SPath f -> Fold (Companion (Path hk) f) ~> Companion hk (Fold f)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath f
fs (Fold (Companion (Path hk) f) ~> Companion hk (Fold f))
-> (Fold (Companion (Path hk) g) ~> Companion hk (Fold g))
-> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
   ~> O (Companion hk (Fold f)) (Companion hk (Fold g))
forall {i :: k} (j :: k) (k :: k) (a :: hk j k) (b :: hk j k)
       (c :: hk i j) (d :: hk 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` SPath g -> Fold (Companion (Path hk) g) ~> Companion hk (Fold g)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath g
gs)
          (O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
 ~> O (Companion hk (Fold f)) (Companion hk (Fold g)))
-> (Fold (Companion (Path hk) g +++ Companion (Path hk) f)
    ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g)))
-> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
   ~> O (Companion hk (Fold f)) (Companion hk (Fold g))
forall (b :: hk j1 k) (c :: hk j1 k) (a :: hk j1 k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. SPath (Companion (Path hk) g)
-> SPath (Companion (Path hk) f)
-> Fold (Companion (Path hk) g +++ Companion (Path hk) f)
   ~> O (Fold (Companion (Path hk) f)) (Fold (Companion (Path hk) g))
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 (Companion (Path hk) g)
cgs SPath (Companion (Path hk) f)
cfs

mapConjointSPath
  :: forall hk {vk} {j} {k} (fs :: Path vk j k)
   . (Equipment hk vk)
  => SPath fs
  -> SPath (Conjoint (Path hk) fs)
mapConjointSPath :: forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
mapConjointSPath SPath fs
SNil = SPath (Conjoint (Path hk) fs)
SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil
mapConjointSPath (SCons Obj p
f SPath ps
fs) = let fc :: Conjoint hk p ~> Conjoint hk p
fc = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj p
f in SPath ps -> SPath (Conjoint (Path hk) ps)
forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
mapConjointSPath SPath ps
fs SPath (Conjoint (Path hk) ps)
-> SPath (Conjoint hk p ::: Nil)
-> SPath (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
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` (Conjoint hk p ~> Conjoint hk p)
-> SPath Nil -> SPath (Conjoint hk 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 Conjoint hk p ~> Conjoint hk p
fc SPath Nil
forall {k} (kk :: CAT k) (k :: k). Ob0 kk k => SPath Nil
SNil ((Ob0 hk j, Ob0 hk j, Ob (Conjoint hk p), Ob (Conjoint hk p)) =>
 SPath (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))
-> (Conjoint hk p ~> Conjoint hk p)
-> SPath (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ Conjoint hk p ~> Conjoint hk p
fc

instance (Equipment hk vk) => Equipment (Path hk) (Path vk) where
  type Conjoint (Path hk) Nil = Nil
  type Conjoint (Path hk) (p ::: ps) = Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)

  mapConjoint :: forall {j :: k} {k :: k} (f :: Path vk j k) (g :: Path vk j k).
(f ~> g) -> Conjoint (Path hk) g ~> Conjoint (Path hk) f
mapConjoint n :: f ~> g
n@(Str SPath f
fsp SPath g
gsp Fold f ~> Fold g
_) =
    let fs :: Obj f
fs = Strictified f g -> Obj f
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src f ~> g
Strictified f g
n
        gs :: Obj g
gs = Strictified f g -> Obj g
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt f ~> g
Strictified f g
n
        cfs :: Obj (Conjoint (Path hk) f)
cfs = SPath (Conjoint (Path hk) f) -> Obj (Conjoint (Path hk) f)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
mapConjointSPath @hk SPath f
fsp)
        cgs :: Obj (Conjoint (Path hk) g)
cgs = SPath (Conjoint (Path hk) g) -> Obj (Conjoint (Path hk) g)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
mapConjointSPath @hk SPath g
gsp)
        compN :: Companion (Path hk) f ~> Companion (Path hk) g
compN = (f ~> g) -> Companion (Path hk) f ~> Companion (Path hk) g
forall {j :: k} {k :: k} (f :: Path vk j k) (g :: Path vk j k).
(f ~> g) -> Companion (Path hk) f ~> Companion (Path hk) g
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion f ~> g
n
    in ((Conjoint (Path hk) g +++ Companion (Path hk) g) ~> I)
-> Obj (Conjoint (Path hk) f)
-> O (Conjoint (Path hk) f)
     (Conjoint (Path hk) g +++ Companion (Path hk) g)
   ~> Conjoint (Path hk) f
forall {s} {k :: s} (kk :: CAT s) (i :: s) (c :: kk i i)
       (a :: kk i k) (b :: kk i k).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O a c ~> b
rightUnitorWith (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit @(Path hk) Obj g
gs) Obj (Conjoint (Path hk) f)
cfs
        Strictified
  ((Conjoint (Path hk) g +++ Companion (Path hk) g)
   +++ Conjoint (Path hk) f)
  (Conjoint (Path hk) f)
-> Strictified
     (Conjoint (Path hk) g)
     ((Conjoint (Path hk) g +++ Companion (Path hk) g)
      +++ Conjoint (Path hk) f)
-> Strictified (Conjoint (Path hk) g) (Conjoint (Path hk) f)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k j) (c :: Path hk k j) (a :: Path hk k j).
Strictified b c -> Strictified a b -> Strictified a c
. Obj (Conjoint (Path hk) f)
-> Obj (Companion (Path hk) g)
-> Obj (Conjoint (Path hk) g)
-> O (O (Conjoint (Path hk) f) (Companion (Path hk) g))
     (Conjoint (Path hk) g)
   ~> O (Conjoint (Path hk) f)
        (O (Companion (Path hk) g) (Conjoint (Path hk) g))
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' Obj (Conjoint (Path hk) f)
cfs (Strictified (Companion (Path hk) f) (Companion (Path hk) g)
-> Obj (Companion (Path hk) g)
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt Companion (Path hk) f ~> Companion (Path hk) g
Strictified (Companion (Path hk) f) (Companion (Path hk) g)
compN) Obj (Conjoint (Path hk) g)
cgs
        Strictified
  (Conjoint (Path hk) g
   +++ (Companion (Path hk) g +++ Conjoint (Path hk) f))
  ((Conjoint (Path hk) g +++ Companion (Path hk) g)
   +++ Conjoint (Path hk) f)
-> Strictified
     (Conjoint (Path hk) g)
     (Conjoint (Path hk) g
      +++ (Companion (Path hk) g +++ Conjoint (Path hk) f))
-> Strictified
     (Conjoint (Path hk) g)
     ((Conjoint (Path hk) g +++ Companion (Path hk) g)
      +++ Conjoint (Path hk) f)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k j) (c :: Path hk k j) (a :: Path hk k j).
Strictified b c -> Strictified a b -> Strictified a c
. ((Obj (Conjoint (Path hk) f)
cfs Obj (Conjoint (Path hk) f)
-> (Companion (Path hk) f ~> Companion (Path hk) g)
-> O (Conjoint (Path hk) f) (Companion (Path hk) f)
   ~> O (Conjoint (Path hk) f) (Companion (Path hk) g)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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` Companion (Path hk) f ~> Companion (Path hk) g
compN) ((Companion (Path hk) f +++ Conjoint (Path hk) f)
 ~> (Companion (Path hk) g +++ Conjoint (Path hk) f))
-> Obj (Conjoint (Path hk) g)
-> O (Companion (Path hk) f +++ Conjoint (Path hk) f)
     (Conjoint (Path hk) g)
   ~> O (Companion (Path hk) g +++ Conjoint (Path hk) f)
        (Conjoint (Path hk) g)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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 (Conjoint (Path hk) g)
cgs)
        Strictified
  (Conjoint (Path hk) g
   +++ (Companion (Path hk) f +++ Conjoint (Path hk) f))
  (Conjoint (Path hk) g
   +++ (Companion (Path hk) g +++ Conjoint (Path hk) f))
-> Strictified
     (Conjoint (Path hk) g)
     (Conjoint (Path hk) g
      +++ (Companion (Path hk) f +++ Conjoint (Path hk) f))
-> Strictified
     (Conjoint (Path hk) g)
     (Conjoint (Path hk) g
      +++ (Companion (Path hk) g +++ Conjoint (Path hk) f))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k j) (c :: Path hk k j) (a :: Path hk k j).
Strictified b c -> Strictified a b -> Strictified a c
. (I ~> (Companion (Path hk) f +++ Conjoint (Path hk) f))
-> Obj (Conjoint (Path hk) g)
-> Conjoint (Path hk) g
   ~> O (Companion (Path hk) f +++ Conjoint (Path hk) f)
        (Conjoint (Path hk) g)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
       (a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(I ~> c) -> (a ~> b) -> a ~> O c b
leftUnitorInvWith (Obj f -> I ~> O (Conjoint (Path hk) f) (Companion (Path hk) f)
forall {j :: k} {k :: k} (f :: Path vk j k).
Obj f -> I ~> O (Conjoint (Path hk) f) (Companion (Path hk) f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj f
fs) Obj (Conjoint (Path hk) g)
cgs

  withObConjoint :: forall {j :: k} {k :: k} (f :: Path vk j k) r.
Ob f =>
(Ob (Conjoint (Path hk) f) => r) -> r
withObConjoint @p Ob (Conjoint (Path hk) f) => r
r = SPath (Conjoint (Path hk) f)
-> ((IsPath (Conjoint (Path hk) f), Ob0 hk k, Ob0 hk 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 (forall {k} (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k :: k}
       (fs :: Path vk j k).
Equipment hk vk =>
SPath fs -> SPath (Conjoint (Path hk) fs)
mapConjointSPath @hk (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @p)) r
Ob (Conjoint (Path hk) f) => r
(IsPath (Conjoint (Path hk) f), Ob0 hk k, Ob0 hk j) => r
r

  comConUnit :: forall {j :: k} {k :: k} (f :: Path vk j k).
Obj f -> I ~> O (Conjoint (Path hk) f) (Companion (Path hk) f)
comConUnit Obj f
fs' = case Obj f -> SPath f
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath Obj f
fs' of
    SPath f
SNil -> I ~> O (Conjoint (Path hk) f) (Companion (Path hk) f)
Strictified Nil Nil
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path hk j j). Ob a => Strictified a a
id
    SCons Obj p
f SPath ps
sfs ->
      let fs :: Obj ps
fs = 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
sfs
          ls :: Companion (Path hk) ps ~> Companion (Path hk) ps
ls = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @(Path hk) Obj ps
fs
          l :: Companion hk p ~> Companion hk p
l = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj p
f
          rs :: Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @(Path hk) Obj ps
fs
          r :: Conjoint hk p ~> Conjoint hk p
r = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj p
f
          r' :: (Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' = (Conjoint hk p ~> Conjoint hk p)
-> (Conjoint hk p ::: Nil) ~> (Conjoint hk 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 Conjoint hk p ~> Conjoint hk p
r
      in ( ((((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil))
-> (Conjoint (Path hk) ps ~> Conjoint (Path hk) ps)
-> (Companion (Path hk) ps ~> Companion (Path hk) ps)
-> O (Conjoint hk p ::: Nil)
     (O (Conjoint (Path hk) ps) (Companion (Path hk) ps))
   ~> O (O (Conjoint hk p ::: Nil) (Conjoint (Path hk) ps))
        (Companion (Path hk) ps)
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' (Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs Companion (Path hk) ps ~> Companion (Path hk) ps
ls Strictified
  ((Companion (Path hk) ps +++ Conjoint (Path hk) ps)
   +++ (Conjoint hk p ::: Nil))
  (Companion (Path hk) ps
   +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))
-> Strictified
     (Nil +++ (Conjoint hk p ::: Nil))
     ((Companion (Path hk) ps +++ Conjoint (Path hk) ps)
      +++ (Conjoint hk p ::: Nil))
-> Strictified
     (Nil +++ (Conjoint hk p ::: Nil))
     (Companion (Path hk) ps
      +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. ((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' ((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil))
-> (Nil ~> (Companion (Path hk) ps +++ Conjoint (Path hk) ps))
-> O (Conjoint hk p ::: Nil) Nil
   ~> O (Conjoint hk p ::: Nil)
        (Companion (Path hk) ps +++ Conjoint (Path hk) ps)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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 ps -> I ~> O (Conjoint (Path hk) ps) (Companion (Path hk) ps)
forall {j :: k} {k :: k} (f :: Path vk j k).
Obj f -> I ~> O (Conjoint (Path hk) f) (Companion (Path hk) f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj ps
fs)) ((Nil +++ (Conjoint hk p ::: Nil))
 ~> (Companion (Path hk) ps
     +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))))
-> ((Companion hk p ::: Nil) ~> (Companion hk p ::: Nil))
-> O (Nil +++ (Conjoint hk p ::: Nil)) (Companion hk p ::: Nil)
   ~> O (Companion (Path hk) ps
         +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))
        (Companion hk p ::: Nil)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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` (Companion hk p ~> Companion hk p)
-> (Companion hk p ::: Nil) ~> (Companion hk 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 Companion hk p ~> Companion hk p
l)
            Strictified
  ((Companion hk p ::: Nil) +++ (Nil +++ (Conjoint hk p ::: Nil)))
  (Companion hk p
   ::: (Companion (Path hk) ps
        +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))))
-> Strictified
     Nil
     ((Companion hk p ::: Nil) +++ (Nil +++ (Conjoint hk p ::: Nil)))
-> Strictified
     Nil
     (Companion hk p
      ::: (Companion (Path hk) ps
           +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. (O (Conjoint hk p) (Companion hk p) ::: Nil)
~> (Companion hk p ::: (Conjoint hk p ::: Nil))
Strictified
  (O (Conjoint hk p) (Companion hk p) ::: Nil)
  ((Companion hk p ::: Nil) +++ (Nil +++ (Conjoint hk p ::: Nil)))
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
            Strictified
  (O (Conjoint hk p) (Companion hk p) ::: Nil)
  ((Companion hk p ::: Nil) +++ (Nil +++ (Conjoint hk p ::: Nil)))
-> Strictified Nil (O (Conjoint hk p) (Companion hk p) ::: Nil)
-> Strictified
     Nil
     ((Companion hk p ::: Nil) +++ (Nil +++ (Conjoint hk p ::: Nil)))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. (I ~> O (Conjoint hk p) (Companion hk p))
-> (I ::: Nil) ~> (O (Conjoint hk p) (Companion hk 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 -> I ~> O (Conjoint hk p) (Companion hk p)
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> I ~> O (Conjoint hk f) (Companion hk f)
comConUnit Obj p
f)
            Strictified
  (I ::: Nil) (O (Conjoint hk p) (Companion hk p) ::: Nil)
-> Strictified Nil (I ::: Nil)
-> Strictified Nil (O (Conjoint hk p) (Companion hk p) ::: Nil)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. Nil ~> (I ::: Nil)
Strictified Nil (I ::: Nil)
forall {k} {kk :: CAT k} {j :: k}.
(Ob0 kk j, Bicategory kk) =>
Nil ~> (I ::: Nil)
introI
         )
          ((Ob0 hk j, Ob0 hk j, Ob (Companion hk p), Ob (Companion hk p)) =>
 Strictified
   Nil
   (Companion hk p
    ::: (Companion (Path hk) ps
         +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))))
-> (Companion hk p ~> Companion hk p)
-> Strictified
     Nil
     (Companion hk p
      ::: (Companion (Path hk) ps
           +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))))
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ Companion hk p ~> Companion hk p
l
          ((Ob0 hk j, Ob0 hk j, Ob (Conjoint hk p), Ob (Conjoint hk p)) =>
 Strictified
   Nil
   (Companion hk p
    ::: (Companion (Path hk) ps
         +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))))
-> (Conjoint hk p ~> Conjoint hk p)
-> Strictified
     Nil
     (Companion hk p
      ::: (Companion (Path hk) ps
           +++ (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))))
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ Conjoint hk p ~> Conjoint hk p
r

  comConCounit :: forall {j :: k} {k :: k} (f :: Path vk j k).
Obj f -> O (Companion (Path hk) f) (Conjoint (Path hk) f) ~> I
comConCounit Obj f
fs' = case Obj f -> SPath f
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
Obj ps -> SPath ps
asSPath Obj f
fs' of
    SPath f
SNil -> O (Companion (Path hk) f) (Conjoint (Path hk) f) ~> I
Strictified Nil Nil
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path hk j j). Ob a => Strictified a a
id
    SCons @f Obj p
f SPath ps
sfs ->
      let fs :: Obj ps
fs = 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
sfs
          ls :: Companion (Path hk) ps ~> Companion (Path hk) ps
ls = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @(Path hk) Obj ps
fs
          l :: Companion hk p ~> Companion hk p
l = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj p
f
          l' :: (Companion hk p ::: Nil) ~> (Companion hk p ::: Nil)
l' = (Companion hk p ~> Companion hk p)
-> (Companion hk p ::: Nil) ~> (Companion hk 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 Companion hk p ~> Companion hk p
l
          rs :: Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @(Path hk) Obj ps
fs
          r :: Conjoint hk p ~> Conjoint hk p
r = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk Obj p
f
          r' :: (Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' = (Conjoint hk p ~> Conjoint hk p)
-> (Conjoint hk p ::: Nil) ~> (Conjoint hk 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 Conjoint hk p ~> Conjoint hk p
r
      in ( Obj ps -> O (Companion (Path hk) ps) (Conjoint (Path hk) ps) ~> I
forall {j :: k} {k :: k} (f :: Path vk j k).
Obj f -> O (Companion (Path hk) f) (Conjoint (Path hk) f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit Obj ps
fs
            Strictified (Conjoint (Path hk) ps +++ Companion (Path hk) ps) Nil
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     (Conjoint (Path hk) ps +++ Companion (Path hk) ps)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     Nil
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k k) (c :: Path hk k k) (a :: Path hk k k).
Strictified b c -> Strictified a b -> Strictified a c
. ( Companion (Path hk) ps ~> Companion (Path hk) ps
ls
                  (Companion (Path hk) ps ~> Companion (Path hk) ps)
-> (((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
     +++ (Companion hk p ::: Nil))
    ~> Conjoint (Path hk) ps)
-> O (Companion (Path hk) ps)
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Nil))
   ~> O (Companion (Path hk) ps) (Conjoint (Path hk) ps)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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` ( ((Conjoint hk p ::: (Companion hk p ::: Nil)) ~> I)
-> (Conjoint (Path hk) ps ~> Conjoint (Path hk) ps)
-> O (Conjoint hk p ::: (Companion hk p ::: Nil))
     (Conjoint (Path hk) ps)
   ~> Conjoint (Path hk) ps
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (c :: kk i2 i2)
       (a :: kk i1 i2) (b :: kk i1 i2).
Bicategory kk =>
(c ~> I) -> (a ~> b) -> O c a ~> b
leftUnitorWith ((I ::: Nil) ~> Nil
Strictified (I ::: Nil) Nil
forall {s} {kk :: CAT s} {j :: s}.
(Ob0 kk j, Bicategory kk) =>
(I ::: Nil) ~> Nil
elimI Strictified (I ::: Nil) Nil
-> Strictified
     (Conjoint hk p ::: (Companion hk p ::: Nil)) (I ::: Nil)
-> Strictified (Conjoint hk p ::: (Companion hk p ::: Nil)) Nil
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. (O (Companion hk p) (Conjoint hk p) ~> I)
-> (O (Companion hk p) (Conjoint hk p) ::: Nil) ~> (I ::: 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 -> O (Companion hk p) (Conjoint hk p) ~> I
forall {j :: k} {k :: k} (f :: vk j k).
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k).
Equipment hk vk =>
Obj f -> O (Companion hk f) (Conjoint hk f) ~> I
comConCounit Obj p
f) Strictified
  (O (Companion hk p) (Conjoint hk p) ::: Nil) (I ::: Nil)
-> Strictified
     (Conjoint hk p ::: (Companion hk p ::: Nil))
     (O (Companion hk p) (Conjoint hk p) ::: Nil)
-> Strictified
     (Conjoint hk p ::: (Companion hk p ::: Nil)) (I ::: Nil)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk j j) (c :: Path hk j j) (a :: Path hk j j).
Strictified b c -> Strictified a b -> Strictified a c
. forall (p :: hk j j) (q :: hk j j).
(Ob0 hk j, Ob0 hk j, Ob0 hk j, Bicategory hk, Ob p, Ob q) =>
(p ::: (q ::: Nil)) ~> (O q p ::: Nil)
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 @(Conjoint hk f) @(Companion hk f)) Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs
                          Strictified
  (Conjoint (Path hk) ps
   +++ (Conjoint hk p ::: (Companion hk p ::: Nil)))
  (Conjoint (Path hk) ps)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Nil))
     (Conjoint (Path hk) ps
      +++ (Conjoint hk p ::: (Companion hk p ::: Nil)))
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Nil))
     (Conjoint (Path hk) ps)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k j) (c :: Path hk k j) (a :: Path hk k j).
Strictified b c -> Strictified a b -> Strictified a c
. ((Companion hk p ::: Nil) ~> (Companion hk p ::: Nil))
-> ((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil))
-> (Conjoint (Path hk) ps ~> Conjoint (Path hk) ps)
-> O (Companion hk p ::: Nil)
     (O (Conjoint hk p ::: Nil) (Conjoint (Path hk) ps))
   ~> O (O (Companion hk p ::: Nil) (Conjoint hk p ::: Nil))
        (Conjoint (Path hk) ps)
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' (Companion hk p ::: Nil) ~> (Companion hk p ::: Nil)
l' (Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs
                      )
              )
            Strictified
  (((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
    +++ (Companion hk p ::: Nil))
   +++ Companion (Path hk) ps)
  (Conjoint (Path hk) ps +++ Companion (Path hk) ps)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     (((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
       +++ (Companion hk p ::: Nil))
      +++ Companion (Path hk) ps)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     (Conjoint (Path hk) ps +++ Companion (Path hk) ps)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path hk k k) (c :: Path hk k k) (a :: Path hk k k).
Strictified b c -> Strictified a b -> Strictified a c
. (Companion (Path hk) ps ~> Companion (Path hk) ps)
-> ((Companion hk p ::: Nil) ~> (Companion hk p ::: Nil))
-> Obj (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
-> O (O (Companion (Path hk) ps) (Companion hk p ::: Nil))
     (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
   ~> O (Companion (Path hk) ps)
        (O (Companion hk p ::: Nil)
           (Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil)))
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' Companion (Path hk) ps ~> Companion (Path hk) ps
ls (Companion hk p ::: Nil) ~> (Companion hk p ::: Nil)
l' ((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil)
r' ((Conjoint hk p ::: Nil) ~> (Conjoint hk p ::: Nil))
-> (Conjoint (Path hk) ps ~> Conjoint (Path hk) ps)
-> O (Conjoint hk p ::: Nil) (Conjoint (Path hk) ps)
   ~> O (Conjoint hk p ::: Nil) (Conjoint (Path hk) ps)
forall {i :: k} (j :: k) (k :: k) (a :: Path hk j k)
       (b :: Path hk j k) (c :: Path hk i j) (d :: Path hk 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` Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs)
         )
          ((Ob0 (Path hk) k, Ob0 (Path hk) j, Ob (Conjoint (Path hk) ps),
  Ob (Conjoint (Path hk) ps)) =>
 Strictified
   ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
    +++ (Companion hk p ::: Companion (Path hk) ps))
   Nil)
-> (Conjoint (Path hk) ps ~> Conjoint (Path hk) ps)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     Nil
forall (i :: k) (j :: k) (ps :: Path hk i j) (qs :: Path hk i j) r.
((Ob0 (Path hk) i, Ob0 (Path hk) 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
\\\ Conjoint (Path hk) ps ~> Conjoint (Path hk) ps
rs
          ((Ob0 hk j, Ob0 hk j, Ob (Companion hk p), Ob (Companion hk p)) =>
 Strictified
   ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
    +++ (Companion hk p ::: Companion (Path hk) ps))
   Nil)
-> (Companion hk p ~> Companion hk p)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     Nil
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ Companion hk p ~> Companion hk p
l
          ((Ob0 hk j, Ob0 hk j, Ob (Conjoint hk p), Ob (Conjoint hk p)) =>
 Strictified
   ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
    +++ (Companion hk p ::: Companion (Path hk) ps))
   Nil)
-> (Conjoint hk p ~> Conjoint hk p)
-> Strictified
     ((Conjoint (Path hk) ps +++ (Conjoint hk p ::: Nil))
      +++ (Companion hk p ::: Companion (Path hk) ps))
     Nil
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk 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
\\\ Conjoint hk p ~> Conjoint hk p
r
instance (Bicategory kk, Ob0 kk a) => Monad (Nil :: Path kk a a) where
  eta :: I ~> Nil
eta = I ~> Nil
Strictified Nil Nil
forall {k} (p :: 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id

instance (Monad s, Ob s) => Monad (s ::: Nil) where
  eta :: I ~> (s ::: Nil)
eta = forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @Nil @(s ::: Nil) 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 = forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @(s ::: s ::: Nil) @(s ::: Nil) 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 = Nil ~> I
Strictified Nil Nil
forall {k} (p :: 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id

instance (Adjunction l r, Ob r, Ob l) => Monad (l ::: r ::: Nil) where
  eta :: I ~> (l ::: (r ::: Nil))
eta = forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @Nil @(l ::: r ::: Nil) (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 = 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)
-> ((r ::: (l ::: Nil)) ~> Nil)
-> O (r ::: Nil) (r ::: (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
|| forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk i i) (qs :: Path kk i i).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @(r ::: l ::: Nil) @Nil (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 ::: (l ::: Nil)) +++ (r ::: Nil)) ~> (Nil +++ (r ::: Nil)))
-> ((l ::: Nil) ~> (l ::: Nil))
-> O ((r ::: (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
|| 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

instance (Adjunction l r, Ob r, Ob l) => Comonad (r ::: l ::: Nil) where
  epsilon :: (r ::: (l ::: Nil)) ~> I
epsilon = forall {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @(r ::: l ::: Nil) @Nil (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 = 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)
-> (Nil ~> (l ::: (r ::: Nil)))
-> O (l ::: Nil) Nil ~> O (l ::: Nil) (l ::: (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 {k} {kk :: CAT k} {i :: k} {j :: k} (ps :: Path kk i j)
       (qs :: Path kk i j).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk i i) (qs :: Path kk i i).
(Bicategory kk, Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
st @Nil @(l ::: r ::: Nil) (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 ::: (r ::: Nil)) +++ (l ::: Nil)))
-> ((r ::: Nil) ~> (r ::: Nil))
-> O (Nil +++ (l ::: Nil)) (r ::: Nil)
   ~> O ((l ::: (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
|| 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