{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Strictified where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Bicategory
  ( Adj (..)
  , Adjunction (..)
  , Adjunction_ (..)
  , Bicategory (..)
  , Comonad (..)
  , Monad (..)
  , associator'
  , associatorInv'
  , (||)
  )
import Proarrow.Category.Bicategory.Sub (IsOb, SUBCAT, WithObO2 (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, id)
import Proarrow.Object (Obj, obj)
import Prelude (type (~))

infixr 5 :::
infixl 5 +++

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

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

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

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

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

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

withIsPath :: (Bicategory kk) => SPath (ps :: Path kk j k) -> ((Ob 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 -> ((Ob ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
SNil (Ob ps, Ob0 kk j, Ob0 kk k) => r
r = r
(Ob ps, Ob0 kk j, Ob0 kk k) => r
r
withIsPath (SCons Obj p
p SPath ps
ps) (Ob ps, Ob0 kk j, Ob0 kk k) => r
r = SPath ps -> ((Ob 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 -> ((Ob ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
ps r
(Ob ps, Ob0 kk j, Ob0 kk k) => r
(Ob 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 = (Fold (p ::: Nil) ~> Fold (q ::: Nil))
-> Strictified (p ::: Nil) (q ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St p ~> q
Fold (p ::: Nil) ~> Fold (q ::: Nil)
f ((Ob0 kk i, Ob0 kk j, Ob p, Ob q) =>
 Strictified (p ::: Nil) (q ::: Nil))
-> (p ~> q) -> Strictified (p ::: Nil) (q ::: Nil)
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ p ~> q
f

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

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

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

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

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

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

combineAll :: forall {kk} {i} {j} (as :: Path kk i j). (Bicategory kk, Ob as) => as ~> (Fold as ::: Nil)
combineAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
as ~> (Fold as ::: Nil)
combineAll = let n :: Fold as ~> Fold as
n = SPath as -> Fold as ~> Fold as
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk i j). IsPath ps => SPath ps
singPath @as) in (Fold as ~> Fold (Fold as ::: Nil))
-> Strictified as (Fold as ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St Fold as ~> Fold as
Fold as ~> Fold (Fold as ::: Nil)
n ((Ob (Fold as), Ob (Fold as)) => Strictified as (Fold as ::: Nil))
-> (Fold as ~> Fold as) -> Strictified as (Fold as ::: Nil)
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold as ~> Fold as
n

splitAll :: forall {kk} {i} {j} (as :: Path kk i j). (Bicategory kk, Ob as) => (Fold as ::: Nil) ~> as
splitAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
(Fold as ::: Nil) ~> as
splitAll = let n :: Fold as ~> Fold as
n = SPath as -> Fold as ~> Fold as
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk i j). IsPath ps => SPath ps
singPath @as) in (Fold (Fold as ::: Nil) ~> Fold as)
-> Strictified (Fold as ::: Nil) as
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St Fold as ~> Fold as
Fold (Fold as ::: Nil) ~> Fold as
n ((Ob (Fold as), Ob (Fold as)) => Strictified (Fold as ::: Nil) as)
-> (Fold as ~> Fold as) -> Strictified (Fold as ::: Nil) as
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold as ~> Fold as
n

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

view :: Strictified (ps :: Path kk j k) qs -> (Strictified ps qs, SPath ps, SPath qs)
view :: forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k)
       (qs :: Path kk j k).
Strictified ps qs -> (Strictified ps qs, SPath ps, SPath qs)
view (St Fold ps ~> Fold qs
f) = ((Fold ps ~> Fold qs) -> Strictified ps qs
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St Fold ps ~> Fold qs
f, SPath ps
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
singPath, SPath qs
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
singPath)

pattern Str
  :: forall {kk} {j} {k} (ps :: Path kk j k) (qs :: Path kk j k)
   . (Bicategory kk)
  => (Ob0 kk j, Ob0 kk k)
  => SPath ps
  -> SPath qs
  -> (Fold ps ~> Fold qs)
  -> Strictified ps qs
pattern $bStr :: forall {k1} {kk :: CAT k1} {j :: k1} {k :: k1} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Bicategory kk, Ob0 kk j, Ob0 kk k) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
$mStr :: forall {r} {k1} {kk :: CAT k1} {j :: k1} {k :: k1}
       {ps :: Path kk j k} {qs :: Path kk j k}.
Bicategory kk =>
Strictified ps qs
-> ((Ob0 kk j, Ob0 kk k) =>
    SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> r)
-> ((# #) -> r)
-> r
Str ps qs f <- (view -> (St f, ps, qs))
  where
    Str SPath ps
ps SPath qs
qs Fold ps ~> Fold qs
f = SPath ps
-> ((Ob ps, Ob0 kk j, Ob0 kk k2) => Strictified ps qs)
-> Strictified ps qs
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((Ob ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath ps
ps (SPath qs
-> ((Ob qs, Ob0 kk j, Ob0 kk k2) => Strictified ps qs)
-> Strictified ps qs
forall {k} (kk :: CAT k) (j :: k) (k :: k) (ps :: Path kk j k) r.
Bicategory kk =>
SPath ps -> ((Ob ps, Ob0 kk j, Ob0 kk k) => r) -> r
withIsPath SPath qs
qs (forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk j k2) (qs :: Path kk j k2).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @ps @qs Fold ps ~> Fold qs
f))

{-# COMPLETE Str #-}

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 (St Fold ps ~> Fold qs
f) = Fold ps ~> Fold qs
f

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

introI :: forall {kk} {j}. (Ob0 kk j, Bicategory kk) => (Nil :: Path kk j j) ~> (I ::: Nil)
introI :: forall {k} {kk :: CAT k} {j :: k}.
(Ob0 kk j, Bicategory kk) =>
Nil ~> (I ::: Nil)
introI = (Fold Nil ~> Fold (I ::: Nil)) -> Strictified Nil (I ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St I ~> I
Fold Nil ~> Fold (I ::: Nil)
forall (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

elimI :: forall {kk} {j}. (Ob0 kk j, Bicategory kk) => (I ::: Nil) ~> (Nil :: Path kk j j)
elimI :: forall {s} {kk :: CAT s} {j :: s}.
(Ob0 kk j, Bicategory kk) =>
(I ::: Nil) ~> Nil
elimI = (Fold (I ::: Nil) ~> Fold Nil) -> Strictified (I ::: Nil) Nil
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St I ~> I
Fold (I ::: Nil) ~> Fold Nil
forall (a :: kk j j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

introO
  :: forall {kk} {i} {j} {k} (p :: kk i j) (q :: kk j k)
   . (Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q)
  => (p ::: q ::: Nil) ~> (q `O` p ::: Nil)
introO :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (q :: kk j k).
(Ob0 kk i, Ob0 kk j, Ob0 kk k, Bicategory kk, Ob p, Ob q) =>
(p ::: (q ::: Nil)) ~> (O q p ::: Nil)
introO = let p :: Obj p
p = forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @p; q :: Obj q
q = forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @q; pq :: O q p ~> O q p
pq = Obj q
q Obj q -> Obj p -> O q p ~> O q p
forall {i :: k} (j :: k) (k :: k) (a :: kk j k) (b :: kk j k)
       (c :: kk i j) (d :: kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj p
p in (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).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St O q p ~> O q p
Fold (p ::: (q ::: Nil)) ~> Fold (O q p ::: Nil)
pq ((Ob (O q p), Ob (O q p)) =>
 Strictified (p ::: (q ::: Nil)) (O q p ::: Nil))
-> (O q p ~> O q p)
-> Strictified (p ::: (q ::: Nil)) (O q p ::: Nil)
forall (a :: kk i k) (b :: kk i k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ O q p ~> O q p
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 (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).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St O q p ~> O q p
Fold (O q p ::: Nil) ~> Fold (p ::: (q ::: Nil))
pq ((Ob (O q p), Ob (O q p)) =>
 Strictified (O q p ::: Nil) (p ::: (q ::: Nil)))
-> (O q p ~> O q p)
-> Strictified (O q p ::: Nil) (p ::: (q ::: Nil))
forall (a :: kk i k) (b :: kk i k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ O q p ~> O q p
pq

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

stUnit :: forall {kk} {i} {j} (p :: kk i j) q. (Adjunction p q, Ob p, Ob q) => Nil ~> p ::: q ::: Nil
stUnit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j)
       (q :: kk j i).
(Adjunction p q, Ob p, Ob q) =>
Nil ~> (p ::: (q ::: Nil))
stUnit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p ((Fold Nil ~> Fold (p ::: (q ::: Nil)))
-> Strictified Nil (p ::: (q ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk i j) (r :: kk j 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 @p @q))

stCounit :: forall {kk} {i} {j} (p :: kk i j) q. (Adjunction p q, Ob p, Ob q) => q ::: p ::: Nil ~> Nil
stCounit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j)
       (q :: kk j i).
(Adjunction p q, Ob p, Ob q) =>
(q ::: (p ::: Nil)) ~> Nil
stCounit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p ((Fold (q ::: (p ::: Nil)) ~> Fold Nil)
-> Strictified (q ::: (p ::: Nil)) Nil
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk i j) (r :: kk j 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 @p @q))

instance (Bicategory kk, Ob0 kk a) => Adjunction_ (Nil :: Path kk a a) Nil where
  adj :: Adj Nil Nil
adj = (I ~> O Nil Nil) -> (O Nil Nil ~> I) -> Adj Nil Nil
forall {k} (kk :: k -> k -> Type) (c :: k) (d :: k) (l :: kk c d)
       (r :: kk d c).
(Bicategory kk, Ob l, Ob r) =>
(I ~> O r l) -> (O l r ~> I) -> Adj l r
Adj I ~> O Nil Nil
Strictified Nil Nil
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id O Nil Nil ~> I
Strictified Nil Nil
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk a a). Ob a => Strictified a a
id

instance (Bicategory kk, Adjunction (l :: kk j k) r, Ob0 kk j, Ob0 kk k) => Adjunction_ (l ::: Nil) (r ::: Nil) where
  adj :: Adj (l ::: Nil) (r ::: Nil)
adj = Adj{adjUnit :: I ~> O (r ::: Nil) (l ::: Nil)
adjUnit = (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).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk j k) (r :: kk k j). 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), adjCounit :: O (l ::: Nil) (r ::: Nil) ~> I
adjCounit = (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).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk j k) (r :: kk k j). 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)}

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

instance (Monad s, Ob (s :: kk a a), Ob0 kk a) => Monad (s ::: Nil) where
  eta :: I ~> (s ::: Nil)
eta = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @Nil @(s ::: Nil) I ~> s
Fold Nil ~> Fold (s ::: Nil)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
I ~> t
eta
  mu :: O (s ::: Nil) (s ::: Nil) ~> (s ::: Nil)
mu = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       (qs :: Path kk j k).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @(s ::: s ::: Nil) @(s ::: Nil) O s s ~> s
Fold (s ::: (s ::: Nil)) ~> Fold (s ::: Nil)
forall {k} {kk :: k -> k -> Type} {a :: k} (t :: kk a a).
Monad t =>
O t t ~> t
mu

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

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

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

type instance IsOb tag Nil = ()
type instance IsOb tag (p ::: ps) = (IsOb tag p, IsOb tag ps)
instance (WithObO2 tag kk) => WithObO2 tag (Path kk) where
  withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: Path kk j k)
       (b :: Path kk i j) r.
(Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @a @b (IsOb tag (O a b), Ob (O a b)) => r
r = forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k)
       {c :: k} tag (qs :: Path kk k c) r.
(IsPath ps, IsOb tag ps, IsOb tag qs, Ob qs) =>
((IsOb tag (ps +++ qs), Ob (ps +++ qs)) => r) -> r
forall (ps :: Path kk i j) {c :: s} tag (qs :: Path kk j c) r.
(IsPath ps, IsOb tag ps, IsOb tag qs, Ob qs) =>
((IsOb tag (ps +++ qs), Ob (ps +++ qs)) => r) -> r
withPathO2 @b @tag @a r
(IsOb tag (O a b), Ob (O a b)) => r
(IsOb tag (b +++ a), Ob (b +++ a)) => r
r

withIsObTagFold
  :: forall {kk} {j} {k} tag (ps :: Path kk j k) r
   . (Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps, Ob ps) => ((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
withIsObTagFold :: forall {k} {kk :: CAT k} {j :: k} {k :: k} tag (ps :: Path kk j k)
       r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
withIsObTagFold (IsOb tag (Fold ps), Ob (Fold ps)) => r
r = case forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
IsPath ps =>
SPath ps
forall (ps :: Path kk j k). IsPath ps => SPath ps
singPath @ps of
  SPath ps
SNil -> r
(IsOb tag (Fold ps), Ob (Fold ps)) => r
r
  SCons Obj p
c SPath ps
SNil -> r
(Ob p, Ob p) => r
(IsOb tag (Fold ps), Ob (Fold ps)) => r
r ((Ob p, Ob p) => r) -> (p ~> p) -> r
forall (a :: kk j j) (b :: kk j j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p ~> p
Obj p
c
  SCons @p @ps' Obj p
c cs :: SPath ps
cs@SCons{} -> forall tag (ps :: Path kk j k) r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
forall {k} {kk :: CAT k} {j :: k} {k :: k} tag (ps :: Path kk j k)
       r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
withIsObTagFold @tag @ps' (forall {s} tag (kk :: s -> s -> Type) {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
forall tag (kk :: k -> k -> Type) {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) r.
(WithObO2 tag kk, Ob a, Ob b, IsOb tag a, IsOb tag b) =>
((IsOb tag (O a b), Ob (O a b)) => r) -> r
withObO2 @tag @kk @(Fold ps') @p r
(IsOb tag (O (Fold ps) p), Ob (O (Fold ps) p)) => r
(IsOb tag (Fold ps), Ob (Fold ps)) => r
r) ((Ob0 (Path kk) j, Ob0 (Path kk) k, Ob (p ::: ps),
  Ob (p ::: ps)) =>
 r)
-> ((p ::: ps) ~> (p ::: ps)) -> r
forall (i :: k) (j :: k) (ps :: Path kk i j) (qs :: Path kk i j) r.
((Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
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
\\\ 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
cs ((Ob p, Ob p) => r) -> Obj p -> r
forall (a :: kk j j) (b :: kk j j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj p
c