{-# 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 (..), RetroSq (..), Sq (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, id, src, tgt)
import Proarrow.Object (Obj, obj)
import Prelude (($), type (~))

infixr 5 :::
infixl 5 +++

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

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

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

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

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

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

withIsPath :: (Bicategory kk) => SPath (ps :: Path kk j k) -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath :: forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
SNil (IsPath ps, Ob0 kk j, Ob0 kk k) => r
r = r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
r
withIsPath (SCons Obj p
p SPath ps
ps) (IsPath ps, Ob0 kk j, Ob0 kk k) => r
r = SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((IsPath ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
ps r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
(IsPath ps, Ob0 kk j, Ob0 kk k) => r
r ((Ob0 kk j, Ob0 kk j, Ob p, Ob p) => r) -> Obj p -> r
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ Obj p
p

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

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

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

asObj :: (Bicategory kk) => SPath (ps :: Path kk i j) -> Obj ps
asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps
SNil = Obj Nil
ps ~> ps
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
asObj (SCons Obj p
p SPath ps
SNil) = (p ~> p) -> (p ::: Nil) ~> (p ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton p ~> p
Obj p
p
asObj (SCons Obj p
p ps :: SPath ps
ps@SCons{}) = SPath ps -> Obj ps
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps
ps ((p ::: ps) ~> (p ::: ps))
-> ((p ::: Nil) ~> (p ::: Nil))
-> O (p ::: ps) (p ::: Nil) ~> O (p ::: ps) (p ::: Nil)
forall {i :: k} (j :: k) (k :: k) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj p -> (p ::: Nil) ~> (p ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton Obj p
p ((Ob p, Ob p) => Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps)))
-> Obj p -> Strictified (p ::: (p ::: ps)) (p ::: (p ::: ps))
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj p
p

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

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

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

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

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

fold :: forall {kk} {i} {j} (as :: Path kk i j). (Bicategory kk) => SPath as -> Fold as ~> Fold as
fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath as
SNil = Obj I
Fold as ~> Fold as
forall (i :: k). Ob0 kk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
fold (SCons Obj p
p SPath ps
SNil) = Fold as ~> Fold as
Obj p
p
fold (SCons Obj p
p fs :: SPath ps
fs@SCons{}) = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
fs (Fold (p ::: ps) ~> Fold (p ::: ps))
-> Obj p -> O (Fold (p ::: ps)) p ~> O (Fold (p ::: ps)) p
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj p
p

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

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

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

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

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

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

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

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

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

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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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

  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 Obj I
Fold Nil ~> Fold Nil
forall (i :: k). Ob0 hk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  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 Obj I
Fold Nil ~> Fold Nil
forall (i :: k). Ob0 hk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj
  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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
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 :: PRO k2 k1).
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 :: PRO 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 :: PRO k2 k1).
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 :: PRO 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 :: PRO 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

  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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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 :: PRO 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

adjVK
  :: forall hk vk i j k f g v w x y
   . (Adjunction x v, Adjunction y w, HasCompanions hk vk, Ob v, Ob w)
  => RetroSq '(y :: hk i k, g) '(x, f :: vk j k)
  -> Sq '(v, g) '(w, f)
adjVK :: forall {k} {h :: k} (hk :: CAT k) (vk :: CAT k) (i :: k) (j :: k)
       (k :: k) (f :: vk j k) (g :: vk h i) (v :: hk j h) (w :: hk k i)
       (x :: hk h j) (y :: hk i k).
(Adjunction x v, Adjunction y w, HasCompanions hk vk, Ob v,
 Ob w) =>
RetroSq '(y, g) '(x, f) -> Sq '(v, g) '(w, f)
adjVK (RetroSq O q (Companion hk g) ~> O (Companion hk f) p
sq) =
  let cf :: Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
cf = 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) (forall (p :: vk j k).
(Bicategory vk, Ob p, Ob0 vk j, Ob0 vk k) =>
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 @f)
      cg :: Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
cg = 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) (forall (p :: vk h i).
(Bicategory vk, Ob p, Ob0 vk h, Ob0 vk 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 @g)
      v :: Obj (v ::: Nil)
v = forall (p :: hk j h).
(Bicategory hk, Ob p, Ob0 hk j, Ob0 hk h) =>
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 @v
      w :: Obj (w ::: Nil)
w = forall (p :: hk k i).
(Bicategory hk, Ob p, Ob0 hk k, Ob0 hk 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 @w
      x :: Obj (x ::: Nil)
x = forall (p :: hk h j).
(Bicategory hk, Ob p, Ob0 hk h, Ob0 hk j) =>
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 @x
      y :: Obj (y ::: Nil)
y = forall (p :: hk i k).
(Bicategory hk, Ob p, Ob0 hk i, Ob0 hk k) =>
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 @y
      counit' :: Strictified ((v ::: Nil) +++ (x ::: Nil)) Nil
counit' = Obj ((v ::: Nil) +++ (x ::: Nil))
-> Obj Nil
-> (Fold ((v ::: Nil) +++ (x ::: Nil)) ~> Fold Nil)
-> Strictified ((v ::: Nil) +++ (x ::: Nil)) Nil
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (Obj (x ::: Nil)
x Obj (x ::: Nil)
-> Obj (v ::: Nil)
-> O (x ::: Nil) (v ::: Nil) ~> O (x ::: Nil) (v ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (v ::: Nil)
v) Obj I
Obj Nil
forall (i :: k). Ob0 (Path hk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (l :: hk h j) (r :: hk j h). 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 @x @v)
      unit' :: Strictified Nil ((y ::: Nil) +++ (w ::: Nil))
unit' = Obj Nil
-> Obj ((y ::: Nil) +++ (w ::: Nil))
-> (Fold Nil ~> Fold ((y ::: Nil) +++ (w ::: Nil)))
-> Strictified Nil ((y ::: Nil) +++ (w ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj I
Obj Nil
forall (i :: k). Ob0 (Path hk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (Obj (w ::: Nil)
w Obj (w ::: Nil)
-> Obj (y ::: Nil)
-> O (w ::: Nil) (y ::: Nil) ~> O (w ::: Nil) (y ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (y ::: Nil)
y) (forall (l :: hk i k) (r :: hk k 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 @y @w)
      sq' :: Strictified
  ((Companion hk g ::: Nil) +++ (y ::: Nil))
  ((x ::: Nil) +++ (Companion hk f ::: Nil))
sq' = Obj ((Companion hk g ::: Nil) +++ (y ::: Nil))
-> Obj ((x ::: Nil) +++ (Companion hk f ::: Nil))
-> (Fold ((Companion hk g ::: Nil) +++ (y ::: Nil))
    ~> Fold ((x ::: Nil) +++ (Companion hk f ::: Nil)))
-> Strictified
     ((Companion hk g ::: Nil) +++ (y ::: Nil))
     ((x ::: Nil) +++ (Companion hk f ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (Obj (y ::: Nil)
y Obj (y ::: Nil)
-> ((Companion hk g ::: Nil) ~> (Companion hk g ::: Nil))
-> O (y ::: Nil) (Companion hk g ::: Nil)
   ~> O (y ::: Nil) (Companion hk g ::: 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
|| Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
(Companion hk g ::: Nil) ~> (Companion hk g ::: Nil)
cg) (Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
(Companion hk f ::: Nil) ~> (Companion hk f ::: Nil)
cf ((Companion hk f ::: Nil) ~> (Companion hk f ::: Nil))
-> Obj (x ::: Nil)
-> O (Companion hk f ::: Nil) (x ::: Nil)
   ~> O (Companion hk f ::: Nil) (x ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (x ::: Nil)
x) O q (Companion hk g) ~> O (Companion hk f) p
Fold ((Companion hk g ::: Nil) +++ (y ::: Nil))
~> Fold ((x ::: Nil) +++ (Companion hk f ::: Nil))
sq
  in (O (Companion hk g) v ~> O w (Companion hk f))
-> Sq '(v, g) '(w, f)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq
      ( Strictified
  ((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
  (Nil +++ ((Companion hk f ::: Nil) +++ (w ::: Nil)))
-> Fold ((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
   ~> Fold (Nil +++ ((Companion hk f ::: Nil) +++ (w ::: Nil)))
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
          ( Nil ~> (y ::: (w ::: Nil))
Strictified Nil ((y ::: Nil) +++ (w ::: Nil))
unit' (Nil ~> (y ::: (w ::: Nil)))
-> ((Companion hk g ::: Nil) ~> (Companion hk g ::: Nil))
-> O Nil (Companion hk g ::: Nil)
   ~> O (y ::: (w ::: Nil)) (Companion hk g ::: 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
|| Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
(Companion hk g ::: Nil) ~> (Companion hk g ::: Nil)
cg (((Companion hk g ::: Nil) +++ Nil)
 ~> ((Companion hk g ::: Nil) +++ (y ::: (w ::: Nil))))
-> Obj (v ::: Nil)
-> O ((Companion hk g ::: Nil) +++ Nil) (v ::: Nil)
   ~> O ((Companion hk g ::: Nil) +++ (y ::: (w ::: Nil))) (v ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (v ::: Nil)
v
              (((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
 ~> ((v ::: Nil)
     +++ ((Companion hk g ::: Nil) +++ (y ::: (w ::: Nil)))))
-> (((v ::: Nil)
     +++ ((Companion hk g ::: Nil) +++ (y ::: (w ::: Nil))))
    ~> ((v ::: Nil)
        +++ ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil))))
-> ((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
   ~> ((v ::: Nil)
       +++ ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil)))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj (w ::: Nil)
w Obj (w ::: Nil)
-> ((Companion hk g ::: (y ::: Nil))
    ~> (x ::: (Companion hk f ::: Nil)))
-> O (w ::: Nil) (Companion hk g ::: (y ::: Nil))
   ~> O (w ::: Nil) (x ::: (Companion hk f ::: 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
|| (Companion hk g ::: (y ::: Nil))
~> (x ::: (Companion hk f ::: Nil))
Strictified
  ((Companion hk g ::: Nil) +++ (y ::: Nil))
  ((x ::: Nil) +++ (Companion hk f ::: Nil))
sq' (((Companion hk g ::: (y ::: Nil)) +++ (w ::: Nil))
 ~> ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil)))
-> Obj (v ::: Nil)
-> O ((Companion hk g ::: (y ::: Nil)) +++ (w ::: Nil)) (v ::: Nil)
   ~> O ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil)) (v ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (v ::: Nil)
v
              (((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
 ~> ((v ::: Nil)
     +++ ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil))))
-> (((v ::: Nil)
     +++ ((x ::: (Companion hk f ::: Nil)) +++ (w ::: Nil)))
    ~> (Nil +++ ((Companion hk f ::: Nil) +++ (w ::: Nil))))
-> ((v ::: Nil) +++ ((Companion hk g ::: Nil) +++ Nil))
   ~> (Nil +++ ((Companion hk f ::: Nil) +++ (w ::: Nil)))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj (w ::: Nil)
w Obj (w ::: Nil)
-> ((Companion hk f ::: Nil) ~> (Companion hk f ::: Nil))
-> O (w ::: Nil) (Companion hk f ::: Nil)
   ~> O (w ::: Nil) (Companion hk f ::: 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
|| Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
(Companion hk f ::: Nil) ~> (Companion hk f ::: Nil)
cf (((Companion hk f ::: Nil) +++ (w ::: Nil))
 ~> ((Companion hk f ::: Nil) +++ (w ::: Nil)))
-> ((v ::: (x ::: Nil)) ~> Nil)
-> O ((Companion hk f ::: Nil) +++ (w ::: Nil)) (v ::: (x ::: Nil))
   ~> O ((Companion hk f ::: Nil) +++ (w ::: 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
|| (v ::: (x ::: Nil)) ~> Nil
Strictified ((v ::: Nil) +++ (x ::: Nil)) Nil
counit'
          )
      )
      ((Ob0 hk h, Ob0 hk k, Ob (O y (Companion hk g)),
  Ob (O (Companion hk f) x)) =>
 Sq '(v, g) '(w, f))
-> (O y (Companion hk g) ~> O (Companion hk f) x)
-> Sq '(v, g) '(w, f)
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 y (Companion hk g) ~> O (Companion hk f) x
O q (Companion hk g) ~> O (Companion hk f) p
sq

adjHK
  :: forall hk vk i j k e f g h v w
   . (Adjunction f h, Adjunction g e, HasCompanions hk vk, Ob f, Ob g)
  => RetroSq '(v :: hk i k, h) '(w, e :: vk j k)
  -> Sq '(v, g) '(w, f)
adjHK :: forall {c} {k :: c} (hk :: CAT c) (vk :: CAT c) (i :: c) (j :: c)
       (k :: c) (e :: vk j k) (f :: vk i k) (g :: vk k j) (h :: vk k i)
       (v :: hk i k) (w :: hk k j).
(Adjunction f h, Adjunction g e, HasCompanions hk vk, Ob f,
 Ob g) =>
RetroSq '(v, h) '(w, e) -> Sq '(v, g) '(w, f)
adjHK (RetroSq O q (Companion hk g) ~> O (Companion hk f) p
sq) =
  let v :: Obj (v ::: Nil)
v = forall (p :: hk i k).
(Bicategory hk, Ob p, Ob0 hk i, Ob0 hk k) =>
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 @v
      w :: Obj (w ::: Nil)
w = forall (p :: hk k j).
(Bicategory hk, Ob p, Ob0 hk k, Ob0 hk j) =>
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 @w
      e :: Obj (e ::: Nil)
e = forall (p :: vk j k).
(Bicategory vk, Ob p, Ob0 vk j, Ob0 vk k) =>
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 @e
      f :: Obj (f ::: Nil)
f = forall (p :: vk i k).
(Bicategory vk, Ob p, Ob0 vk i, Ob0 vk k) =>
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 @f
      g :: Obj (g ::: Nil)
g = forall (p :: vk k j).
(Bicategory vk, Ob p, Ob0 vk k, Ob0 vk j) =>
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 @g
      h :: Obj (h ::: Nil)
h = forall (p :: vk k i).
(Bicategory vk, Ob p, Ob0 vk k, Ob0 vk 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 @h
      ce :: Companion (Path hk) (e ::: Nil) ~> Companion (Path hk) (e ::: Nil)
ce = 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 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 @(Path hk) Obj (e ::: Nil)
e
      cf :: Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
cf = 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 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 @(Path hk) Obj (f ::: Nil)
f
      cg :: Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
cg = 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 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 @(Path hk) Obj (g ::: Nil)
g
      ch :: Companion (Path hk) (h ::: Nil) ~> Companion (Path hk) (h ::: Nil)
ch = 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 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 @(Path hk) Obj (h ::: Nil)
h
      counit' :: Companion (Path hk) ((e ::: Nil) +++ (g ::: Nil))
~> Companion (Path hk) Nil
counit' = 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 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 @(Path hk) (Obj ((e ::: Nil) +++ (g ::: Nil))
-> Obj Nil
-> (Fold ((e ::: Nil) +++ (g ::: Nil)) ~> Fold Nil)
-> Strictified ((e ::: Nil) +++ (g ::: Nil)) Nil
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (Obj (g ::: Nil)
g Obj (g ::: Nil)
-> Obj (e ::: Nil)
-> O (g ::: Nil) (e ::: Nil) ~> O (g ::: Nil) (e ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (e ::: Nil)
e) Obj I
Obj Nil
forall (i :: c). Ob0 (Path vk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (forall (l :: vk k j) (r :: vk j k). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @g @e))
      unit' :: Companion (Path hk) Nil
~> Companion (Path hk) ((f ::: Nil) +++ (h ::: Nil))
unit' = 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 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 @(Path hk) (Obj Nil
-> Obj ((f ::: Nil) +++ (h ::: Nil))
-> (Fold Nil ~> Fold ((f ::: Nil) +++ (h ::: Nil)))
-> Strictified Nil ((f ::: Nil) +++ (h ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str Obj I
Obj Nil
forall (i :: c). Ob0 (Path vk) i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj (Obj (h ::: Nil)
h Obj (h ::: Nil)
-> Obj (f ::: Nil)
-> O (h ::: Nil) (f ::: Nil) ~> O (h ::: Nil) (f ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (f ::: Nil)
f) (forall (l :: vk i k) (r :: vk k 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 @f @h))
      sq' :: Strictified
  ((Companion hk h ::: Nil) +++ (v ::: Nil))
  ((w ::: Nil) +++ (Companion hk e ::: Nil))
sq' = Obj ((Companion hk h ::: Nil) +++ (v ::: Nil))
-> Obj ((w ::: Nil) +++ (Companion hk e ::: Nil))
-> (Fold ((Companion hk h ::: Nil) +++ (v ::: Nil))
    ~> Fold ((w ::: Nil) +++ (Companion hk e ::: Nil)))
-> Strictified
     ((Companion hk h ::: Nil) +++ (v ::: Nil))
     ((w ::: Nil) +++ (Companion hk e ::: Nil))
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Bicategory kk =>
Obj ps -> Obj qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
str (Obj (v ::: Nil)
v Obj (v ::: Nil)
-> ((Companion hk h ::: Nil) ~> (Companion hk h ::: Nil))
-> O (v ::: Nil) (Companion hk h ::: Nil)
   ~> O (v ::: Nil) (Companion hk h ::: 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
|| Companion (Path hk) (h ::: Nil) ~> Companion (Path hk) (h ::: Nil)
(Companion hk h ::: Nil) ~> (Companion hk h ::: Nil)
ch) (Companion (Path hk) (e ::: Nil) ~> Companion (Path hk) (e ::: Nil)
(Companion hk e ::: Nil) ~> (Companion hk e ::: Nil)
ce ((Companion hk e ::: Nil) ~> (Companion hk e ::: Nil))
-> Obj (w ::: Nil)
-> O (Companion hk e ::: Nil) (w ::: Nil)
   ~> O (Companion hk e ::: Nil) (w ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (w ::: Nil)
w) O q (Companion hk g) ~> O (Companion hk f) p
Fold ((Companion hk h ::: Nil) +++ (v ::: Nil))
~> Fold ((w ::: Nil) +++ (Companion hk e ::: Nil))
sq
  in (O (Companion hk g) v ~> O w (Companion hk f))
-> Sq '(v, g) '(w, f)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq
      ( Strictified
  (Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
  ((Companion hk f ::: Nil) +++ ((w ::: Nil) +++ Nil))
-> Fold (Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
   ~> Fold ((Companion hk f ::: Nil) +++ ((w ::: Nil) +++ Nil))
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
          ( Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
(Companion hk g ::: Nil) ~> (Companion hk g ::: Nil)
cg ((Companion hk g ::: Nil) ~> (Companion hk g ::: Nil))
-> Obj (v ::: Nil)
-> O (Companion hk g ::: Nil) (v ::: Nil)
   ~> O (Companion hk g ::: Nil) (v ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (v ::: Nil)
v (((v ::: Nil) +++ (Companion hk g ::: Nil))
 ~> ((v ::: Nil) +++ (Companion hk g ::: Nil)))
-> (Nil ~> (Companion hk f ::: (Companion hk h ::: Nil)))
-> O ((v ::: Nil) +++ (Companion hk g ::: Nil)) Nil
   ~> O ((v ::: Nil) +++ (Companion hk g ::: Nil))
        (Companion hk f ::: (Companion hk h ::: 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
|| Companion (Path hk) Nil
~> Companion (Path hk) ((f ::: Nil) +++ (h ::: Nil))
Nil ~> (Companion hk f ::: (Companion hk h ::: Nil))
unit'
              ((Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
 ~> ((Companion hk f ::: (Companion hk h ::: Nil))
     +++ ((v ::: Nil) +++ (Companion hk g ::: Nil))))
-> (((Companion hk f ::: (Companion hk h ::: Nil))
     +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
    ~> ((Companion hk f ::: Nil)
        +++ ((w ::: (Companion hk e ::: Nil))
             +++ (Companion hk g ::: Nil))))
-> (Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
   ~> ((Companion hk f ::: Nil)
       +++ ((w ::: (Companion hk e ::: Nil))
            +++ (Companion hk g ::: Nil)))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Companion (Path hk) (g ::: Nil) ~> Companion (Path hk) (g ::: Nil)
(Companion hk g ::: Nil) ~> (Companion hk g ::: Nil)
cg ((Companion hk g ::: Nil) ~> (Companion hk g ::: Nil))
-> ((Companion hk h ::: (v ::: Nil))
    ~> (w ::: (Companion hk e ::: Nil)))
-> O (Companion hk g ::: Nil) (Companion hk h ::: (v ::: Nil))
   ~> O (Companion hk g ::: Nil) (w ::: (Companion hk e ::: 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
|| (Companion hk h ::: (v ::: Nil))
~> (w ::: (Companion hk e ::: Nil))
Strictified
  ((Companion hk h ::: Nil) +++ (v ::: Nil))
  ((w ::: Nil) +++ (Companion hk e ::: Nil))
sq' (((Companion hk h ::: (v ::: Nil)) +++ (Companion hk g ::: Nil))
 ~> ((w ::: (Companion hk e ::: Nil)) +++ (Companion hk g ::: Nil)))
-> ((Companion hk f ::: Nil) ~> (Companion hk f ::: Nil))
-> O ((Companion hk h ::: (v ::: Nil))
      +++ (Companion hk g ::: Nil))
     (Companion hk f ::: Nil)
   ~> O ((w ::: (Companion hk e ::: Nil))
         +++ (Companion hk g ::: Nil))
        (Companion hk f ::: 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
|| Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
(Companion hk f ::: Nil) ~> (Companion hk f ::: Nil)
cf
              ((Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
 ~> ((Companion hk f ::: Nil)
     +++ ((w ::: (Companion hk e ::: Nil))
          +++ (Companion hk g ::: Nil))))
-> (((Companion hk f ::: Nil)
     +++ ((w ::: (Companion hk e ::: Nil))
          +++ (Companion hk g ::: Nil)))
    ~> ((Companion hk f ::: Nil) +++ ((w ::: Nil) +++ Nil)))
-> (Nil +++ ((v ::: Nil) +++ (Companion hk g ::: Nil)))
   ~> ((Companion hk f ::: Nil) +++ ((w ::: Nil) +++ Nil))
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Companion (Path hk) ((e ::: Nil) +++ (g ::: Nil))
~> Companion (Path hk) Nil
(Companion hk e ::: (Companion hk g ::: Nil)) ~> Nil
counit' ((Companion hk e ::: (Companion hk g ::: Nil)) ~> Nil)
-> Obj (w ::: Nil)
-> O (Companion hk e ::: (Companion hk g ::: Nil)) (w ::: Nil)
   ~> O Nil (w ::: Nil)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| Obj (w ::: Nil)
w (((w ::: Nil) +++ (Companion hk e ::: (Companion hk g ::: Nil)))
 ~> ((w ::: Nil) +++ Nil))
-> ((Companion hk f ::: Nil) ~> (Companion hk f ::: Nil))
-> O ((w ::: Nil)
      +++ (Companion hk e ::: (Companion hk g ::: Nil)))
     (Companion hk f ::: Nil)
   ~> O ((w ::: Nil) +++ Nil) (Companion hk f ::: 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
|| Companion (Path hk) (f ::: Nil) ~> Companion (Path hk) (f ::: Nil)
(Companion hk f ::: Nil) ~> (Companion hk f ::: Nil)
cf
          )
      )
      ((Ob0 hk k, Ob0 hk k, Ob (O v (Companion hk h)),
  Ob (O (Companion hk e) w)) =>
 Sq '(v, g) '(w, f))
-> (O v (Companion hk h) ~> O (Companion hk e) w)
-> Sq '(v, g) '(w, f)
forall (i :: c) (j :: c) (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 v (Companion hk h) ~> O (Companion hk e) w
O q (Companion hk g) ~> O (Companion hk f) p
sq

-- adj4Sq
--   :: forall hk vk i j k e f g h v w x y
--    . (Adjunction v x, Adjunction w y, Adjunction h f, Adjunction e g, HasCompanions hk vk)
--   => Sq '(v :: hk k j, g) '(w, f :: vk k i)
--   -> Sq '(y, h) '(x, e)
-- adj4Sq (Sq sq) =
--   let v = obj1 @v
--       w = obj1 @w
--       x = obj1 @x
--       y = obj1 @y
--       e = obj1 @e
--       f = obj1 @f
--       g = obj1 @g
--       h = obj1 @h
--       ce = mapCompanion @(Path hk) e
--       cf = mapCompanion @(Path hk) f
--       cg = mapCompanion @(Path hk) g
--       ch = mapCompanion @(Path hk) h
--       unitV = mapCompanion @(Path hk) (str iObj (f || h) (unit @h @f))
--       counitV = mapCompanion @(Path hk) (str (e || g) iObj (counit @e @g))
--       unitH = str iObj (x || v) (unit @v @x)
--       counitH = str (w || y) iObj (counit @w @y)
--       sq' = str (cg || v) (w || cf) sq
--   in Sq
--       ( unStr
--           ( (unitH == x || counitV || v) || ch || y
--               == x || ce || sq' || ch || y
--               == x || ce || (w || unitV || y == counitH)
--           )
--       )

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

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

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

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

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