{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A profunctor-specific counterpart of "Proarrow.Bicategory.Strictified", hardcoded to
-- @:.:@\/'Id' instead of an arbitrary 'Proarrow.Bicategory.Bicategory'. A 'Path' is a
-- type-level list of profunctors; 'Fold' collapses one down to the single profunctor its
-- elements compose to. Unlike the general (strictified) version, we don't need to track
-- identity 2-cells through the induction -- since our 2-cells are just plain Haskell
-- functions (@:~>@), the identity of any composite is always definitionally @\\x -> x@.
-- The only real work is 'concatFold'\/'splitFold', which do the actual
-- associator\/unitor reshuffling once, by induction, so that "Proarrow.Squares" never has
-- to.
module Proarrow.Path where

import Data.Kind (Constraint, Type)
import Prelude (type (~))

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, rmap, src, tgt, (:~>), type (+->))
import Proarrow.Profunctor.Instance.Composition (o, (:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable)

infixr 5 :::
infixl 5 +++

-- | Identity natural transformation, used as a 2-cell between profunctors that happen to
-- be syntactically equal.
idN :: p :~> p
idN :: forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN p a b
x = p a b
x

-- @:.:@\/'Id' aren't strictly associative\/unital, unlike the 'Proarrow.Bicategory.O'\/
-- 'Proarrow.Bicategory.I' of a strictified bicategory.
leftUnitor :: (Profunctor p) => Id :.: p :~> p
leftUnitor :: forall {k1} {k} (p :: k1 +-> k). Profunctor p => (Id :.: p) :~> p
leftUnitor (Id a ~> b
l :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall (c :: k) (a :: k) (b :: k1). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
l p b b
p

leftUnitorInv :: (Profunctor p) => p :~> Id :.: p
leftUnitorInv :: forall {i} {j} (p :: i +-> j). Profunctor p => p :~> (Id :.: p)
leftUnitorInv p a b
p = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (p a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p a b
p) Id a a -> p a b -> (:.:) Id p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p

rightUnitor :: (Profunctor p) => p :.: Id :~> p
rightUnitor :: forall {k1} {k} (p :: k1 +-> k). Profunctor p => (p :.: Id) :~> p
rightUnitor (p a b
p :.: Id b ~> b
r) = (b ~> b) -> p a b -> p a b
forall (b :: k1) (d :: k1) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
r p a b
p

rightUnitorInv :: (Profunctor p) => p :~> p :.: Id
rightUnitorInv :: forall {i} {k} (p :: i +-> k). Profunctor p => p :~> (p :.: Id)
rightUnitorInv p a b
p = p a b
p p a b -> Id b b -> (:.:) p Id a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (p a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p a b
p)

associator :: (p :.: q) :.: r :~> p :.: (q :.: r)
associator :: forall {k} {k} {j} {i} (p :: k +-> k) (q :: j +-> k) (r :: i +-> j)
       (a :: k) (b :: i).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
associator ((p a b
p :.: q b b
q) :.: r b b
r) = p a b
p p a b -> (:.:) q r b b -> (:.:) p (q :.: r) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (q b b
q q b b -> r b b -> (:.:) q r b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: r b b
r)

associatorInv :: p :.: (q :.: r) :~> (p :.: q) :.: r
associatorInv :: forall {j} {k} {j} {i} (p :: j +-> k) (q :: j +-> j) (r :: i +-> j)
       (a :: k) (b :: i).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
associatorInv (p a b
p :.: (q b b
q :.: r b b
r)) = (p a b
p p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q) (:.:) p q a b -> r b b -> (:.:) (p :.: q) r a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: r b b
r

-- | A type-level list of profunctors, from category @j@ to category @k@.
type Path :: Type -> Type -> Type
type data Path j k where
  Nil :: Path k k
  (:::) :: (i +-> j) -> Path j k -> Path i k

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

-- | @(as +++ bs) +++ cs@ and @as +++ (bs +++ cs)@ are the same 'Path'. Proved once, up
-- front, by (mutual) induction with 'IsOb'\'s superclasses -- see there for how the
-- induction actually goes through -- so that every other associativity fact needed
-- anywhere in "Proarrow.Squares" is a free @~@ coercion instead of a function call.
class ((as +++ bs) +++ cs ~ as +++ (bs +++ cs)) => Assoc as bs cs

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

-- | Fold a 'Path' down to the single profunctor its elements compose to.
type family Fold (ps :: Path j k) :: j +-> k

type instance Fold (Nil :: Path j j) = Id
type instance Fold (p ::: Nil) = p
type instance Fold (p ::: (q ::: ps)) = Fold (q ::: ps) :.: p

-- | Which per-element property a 'SPath' witnesses. @Tight@ plays the role of the tight
-- (vertical, 'Representable') legs of the @Prof@ equipment; a later @Cotight@ would do
-- the same for 'Proarrow.Profunctor.Corepresentable.Corepresentable' legs.
data Tag = Prof | Tight

-- | The per-element constraint a 'Tag' stands for. @c@ is applied homogeneously at every
-- element of a path, each of a (potentially) different @i +-> j@ kind -- a genuinely
-- impredicative use GHC's kind system can't express with @c@ itself as the parameter, so
-- 'Tag' is the (monomorphic, first-order) proxy for it instead. Mirrors
-- "Proarrow.Bicategory.Sub"'s @IsOb@\/@SUBCAT@ tag mechanism.
type family Sat (t :: Tag) (p :: i +-> j) :: Constraint

type instance Sat Prof p = Profunctor p
type instance Sat Tight p = Representable p

-- | Runtime witness that every element of a 'Path' satisfies @'Sat' t@. Replaces having a
-- separate witness type per tag (what used to be @SPath@\/@TPath@), so
-- '(Proarrow.Squares.|||)'\/'(Proarrow.Squares.===)' only need one append lemma
-- ('withObAppend'), not one per kind of leg.
type SPath :: Tag -> Path a b -> Type
data SPath t ps where
  SNil :: (CategoryOf k) => SPath t (Nil :: Path k k)
  SCons :: (Sat t p) => SPath t ps -> SPath t (p ::: ps)

-- | @ps@ is a path all of whose elements satisfy @'Sat' t@. Only two cases (@Nil@\/@Cons@)
-- are needed: the head @p@ stays concrete at each step of 'withObAppend'\'s recursion, so
-- GHC's own instance resolution reattaches it to the recursively-derived
-- @'IsOb' t (ps +++ qs)@ for free -- it never needs to reduce @ps +++ qs@ itself, just
-- match the @(':::')@ shape.
class
  (ps +++ Nil ~ ps, forall b c (qs :: Path k b) (rs :: Path b c). Assoc ps qs rs) =>
  IsOb (t :: Tag) (ps :: Path j k)
  where
  singPath :: SPath t ps

instance (CategoryOf k) => IsOb t (Nil :: Path k k) where
  singPath :: SPath t Nil
singPath = SPath t Nil
forall k (t :: Tag). CategoryOf k => SPath t Nil
SNil
instance (Sat t p, IsOb t ps) => IsOb t (p ::: ps) where
  singPath :: SPath t (p ::: ps)
singPath = SPath t ps -> SPath t (p ::: ps)
forall {a} {a} {b} (t :: Tag) (p :: a +-> a) (ps :: Path a b).
Sat t p =>
SPath t ps -> SPath t (p ::: ps)
SCons SPath t ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | Concatenate two witnesses. Plain recursion, no constraint solving -- unlike
-- 'withObAppend', which additionally proves @'IsOb' t (ps +++ qs)@.
appendPath :: SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath :: forall {a} {b} {b} (t :: Tag) (ps :: Path a b) (qs :: Path b b).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath t ps
SNil SPath t qs
qs = SPath t (ps +++ qs)
SPath t qs
qs
appendPath (SCons SPath t ps
ps) SPath t qs
qs = SPath t (ps +++ qs) -> SPath t (p ::: (ps +++ qs))
forall {a} {a} {b} (t :: Tag) (p :: a +-> a) (ps :: Path a b).
Sat t p =>
SPath t ps -> SPath t (p ::: ps)
SCons (SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
forall {a} {b} {b} (t :: Tag) (ps :: Path a b) (qs :: Path b b).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath t ps
ps SPath t qs
qs)

-- | Bring a specific instantiation of @'IsOb' t ps@\'s quantified @'Assoc' ps qs rs@
-- superclass into scope. Needed explicitly: GHC won't search the superclasses of an
-- arbitrary given constraint to solve an unrelated @~@ goal, so uses of associativity
-- (e.g. in '(Proarrow.Squares.|||)'\/'(Proarrow.Squares.===)') have to ask for it by name
-- at the specific @ps@\/@qs@\/@rs@ in play, even though the fact itself is free once
-- asked for.
withAssoc :: forall ps qs rs t r. (IsOb t ps) => ((Assoc ps qs rs) => r) -> r
withAssoc :: forall {a} {a} {b} {c} (ps :: Path a a) (qs :: Path a b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc Assoc ps qs rs => r
r = r
Assoc ps qs rs => r
r

-- | A well-formed (horizontal) path: every element is a plain 'Profunctor'.
type IsPath = IsOb Prof

-- | A tight (vertical) path: every element is 'Representable'.
type IsTight = IsOb Tight

-- | A tight path is, in particular, a well-formed path ('Representable' implies
-- 'Profunctor'). Needed explicitly because different 'Tag's don't otherwise know
-- anything about each other.
weakenTight :: SPath Tight ps -> SPath Prof ps
weakenTight :: forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight ps
SNil = SPath 'Prof Nil
SPath 'Prof ps
forall k (t :: Tag). CategoryOf k => SPath t Nil
SNil
weakenTight (SCons SPath 'Tight ps
ps) = SPath 'Prof ps -> SPath 'Prof (p ::: ps)
forall {a} {a} {b} (t :: Tag) (p :: a +-> a) (ps :: Path a b).
Sat t p =>
SPath t ps -> SPath t (p ::: ps)
SCons (SPath 'Tight ps -> SPath 'Prof ps
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight ps
ps)

-- | @ps@,@qs@ both satisfy @'Sat' t@ pointwise ⟹ so does @ps +++ qs@.
withObAppend :: forall t ps qs r. (IsOb t qs) => SPath t ps -> ((IsOb t (ps +++ qs)) => r) -> r
withObAppend :: forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend SPath t ps
SNil IsOb t (ps +++ qs) => r
r = r
IsOb t (ps +++ qs) => r
r
withObAppend (SCons SPath t ps
ps) IsOb t (ps +++ qs) => r
r = forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
forall (t :: Tag) (ps :: Path a b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend @t @_ @qs SPath t ps
ps r
IsOb t (ps +++ qs) => r
IsOb t (ps +++ qs) => r
r

-- | Extract 'Profunctor' evidence for @'Fold' ps@ from a runtime witness.
withFoldOb :: SPath Prof ps -> ((Profunctor (Fold ps)) => r) -> r
withFoldOb :: forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof ps
SNil Profunctor (Fold ps) => r
r = r
Profunctor (Fold ps) => r
r
withFoldOb (SCons SPath 'Prof ps
SNil) Profunctor (Fold ps) => r
r = r
Profunctor (Fold ps) => r
r
withFoldOb (SCons cs :: SPath 'Prof ps
cs@(SCons SPath 'Prof ps
_)) Profunctor (Fold ps) => r
r = SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof ps
cs r
Profunctor (Fold ps) => r
Profunctor (Fold ps) => r
r

-- | Extract 'Representable' evidence for @'Fold' ps@ from a runtime witness. The body is
-- identical to 'withFoldOb'\'s -- both just extract @'Sat' t ('Fold' ps)@, which needs the
-- same single-vs-multi-element case split 'Fold' itself has -- but there's no polymorphic
-- @t@ anywhere that would let one definition serve both: every call site already knows
-- its tag concretely, so there's nothing to be generic over.
withFoldRep :: SPath Tight ps -> ((Representable (Fold ps)) => r) -> r
withFoldRep :: forall {j} {k} (ps :: Path j k) r.
SPath 'Tight ps -> (Representable (Fold ps) => r) -> r
withFoldRep SPath 'Tight ps
SNil Representable (Fold ps) => r
r = r
Representable (Fold ps) => r
r
withFoldRep (SCons SPath 'Tight ps
SNil) Representable (Fold ps) => r
r = r
Representable (Fold ps) => r
r
withFoldRep (SCons cs :: SPath 'Tight ps
cs@(SCons SPath 'Tight ps
_)) Representable (Fold ps) => r
r = SPath 'Tight ps -> (Representable (Fold ps) => r) -> r
forall {j} {k} (ps :: Path j k) r.
SPath 'Tight ps -> (Representable (Fold ps) => r) -> r
withFoldRep SPath 'Tight ps
cs r
Representable (Fold ps) => r
Representable (Fold ps) => r
r

-- | Combine the composites of two adjacent paths into the composite of their
-- concatenation.
concatFold :: SPath Prof as -> SPath Prof bs -> Fold bs :.: Fold as :~> Fold (as +++ bs)
concatFold :: forall {j} {b} {k} (as :: Path j b) (bs :: Path b k).
SPath 'Prof as
-> SPath 'Prof bs -> (Fold bs :.: Fold as) :~> Fold (as +++ bs)
concatFold SPath 'Prof as
SNil SPath 'Prof bs
bs = SPath 'Prof bs
-> (Profunctor (Fold bs) => (:.:) (Fold bs) Id a b -> Fold bs a b)
-> (:.:) (Fold bs) Id a b
-> Fold bs a b
forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof bs
bs Profunctor (Fold bs) => (:.:) (Fold bs) Id a b -> Fold bs a b
(:.:) (Fold bs) Id a b -> Fold bs a b
(Fold bs :.: Id) :~> Fold bs
forall {k1} {k} (p :: k1 +-> k). Profunctor p => (p :.: Id) :~> p
rightUnitor
concatFold (SCons SPath 'Prof ps
SNil) SPath 'Prof bs
bs = case SPath 'Prof bs
bs of
  SPath 'Prof bs
SNil -> (:.:) Id p a b -> p a b
(:.:) (Fold bs) (Fold as) a b -> Fold (as +++ bs) a b
(Id :.: p) :~> p
forall {k1} {k} (p :: k1 +-> k). Profunctor p => (Id :.: p) :~> p
leftUnitor
  SCons SPath 'Prof ps
_ -> (:.:) (Fold bs) (Fold as) a b -> Fold (as +++ bs) a b
(:.:) (Fold (p ::: ps)) p a b -> (:.:) (Fold (p ::: ps)) p a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN
concatFold (SCons cs :: SPath 'Prof ps
cs@(SCons SPath 'Prof ps
_)) SPath 'Prof bs
bs = (SPath 'Prof (p ::: ps)
-> SPath 'Prof bs
-> (Fold bs :.: Fold (p ::: ps)) :~> Fold ((p ::: ps) +++ bs)
forall {j} {b} {k} (as :: Path j b) (bs :: Path b k).
SPath 'Prof as
-> SPath 'Prof bs -> (Fold bs :.: Fold as) :~> Fold (as +++ bs)
concatFold SPath 'Prof ps
SPath 'Prof (p ::: ps)
cs SPath 'Prof bs
bs (forall {a :: k} {b :: a}.
 (:.:) (Fold bs) (Fold (p ::: ps)) a b
 -> Fold (p ::: (ps +++ bs)) a b)
-> (p :~> p)
-> ((Fold bs :.: Fold (p ::: ps)) :.: p)
   :~> (Fold (p ::: (ps +++ bs)) :.: p)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` p a b -> p a b
p :~> p
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN) ((:.:) (Fold bs :.: Fold (p ::: ps)) p a b
 -> (:.:) (Fold (p ::: (ps +++ bs))) p a b)
-> ((:.:) (Fold bs) (Fold (p ::: ps) :.: p) a b
    -> (:.:) (Fold bs :.: Fold (p ::: ps)) p a b)
-> (:.:) (Fold bs) (Fold (p ::: ps) :.: p) a b
-> (:.:) (Fold (p ::: (ps +++ bs))) p a b
forall b c a. (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 (p ::: ps) :.: p) a b
-> (:.:) (Fold bs :.: Fold (p ::: ps)) p a b
forall {j} {k} {j} {i} (p :: j +-> k) (q :: j +-> j) (r :: i +-> j)
       (a :: k) (b :: i).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
associatorInv

-- | The inverse of 'concatFold'.
splitFold :: SPath Prof as -> SPath Prof bs -> Fold (as +++ bs) :~> Fold bs :.: Fold as
splitFold :: forall {i} {k} {k} (as :: Path i k) (bs :: Path k k).
SPath 'Prof as
-> SPath 'Prof bs -> Fold (as +++ bs) :~> (Fold bs :.: Fold as)
splitFold SPath 'Prof as
SNil SPath 'Prof bs
bs = SPath 'Prof bs
-> (Profunctor (Fold bs) => Fold bs a b -> (:.:) (Fold bs) Id a b)
-> Fold bs a b
-> (:.:) (Fold bs) Id a b
forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof bs
bs Profunctor (Fold bs) => Fold bs a b -> (:.:) (Fold bs) Id a b
Fold bs a b -> (:.:) (Fold bs) Id a b
Fold bs :~> (Fold bs :.: Id)
forall {i} {k} (p :: i +-> k). Profunctor p => p :~> (p :.: Id)
rightUnitorInv
splitFold (SCons SPath 'Prof ps
SNil) SPath 'Prof bs
bs = case SPath 'Prof bs
bs of
  SPath 'Prof bs
SNil -> p a b -> (:.:) Id p a b
Fold (as +++ bs) a b -> (:.:) (Fold bs) (Fold as) a b
p :~> (Id :.: p)
forall {i} {j} (p :: i +-> j). Profunctor p => p :~> (Id :.: p)
leftUnitorInv
  SCons SPath 'Prof ps
_ -> (:.:) (Fold (p ::: ps)) p a b -> (:.:) (Fold (p ::: ps)) p a b
Fold (as +++ bs) a b -> (:.:) (Fold bs) (Fold as) a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN
splitFold (SCons cs :: SPath 'Prof ps
cs@(SCons SPath 'Prof ps
_)) SPath 'Prof bs
bs = (:.:) (Fold bs :.: Fold (p ::: ps)) p a b
-> (:.:) (Fold bs) (Fold (p ::: ps) :.: p) a b
forall {k} {k} {j} {i} (p :: k +-> k) (q :: j +-> k) (r :: i +-> j)
       (a :: k) (b :: i).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
associator ((:.:) (Fold bs :.: Fold (p ::: ps)) p a b
 -> (:.:) (Fold bs) (Fold (p ::: ps) :.: p) a b)
-> ((:.:) (Fold (p ::: (ps +++ bs))) p a b
    -> (:.:) (Fold bs :.: Fold (p ::: ps)) p a b)
-> (:.:) (Fold (p ::: (ps +++ bs))) p a b
-> (:.:) (Fold bs) (Fold (p ::: ps) :.: p) a b
forall b c a. (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 'Prof (p ::: ps)
-> SPath 'Prof bs
-> Fold ((p ::: ps) +++ bs) :~> (Fold bs :.: Fold (p ::: ps))
forall {i} {k} {k} (as :: Path i k) (bs :: Path k k).
SPath 'Prof as
-> SPath 'Prof bs -> Fold (as +++ bs) :~> (Fold bs :.: Fold as)
splitFold SPath 'Prof ps
SPath 'Prof (p ::: ps)
cs SPath 'Prof bs
bs (forall {a :: k} {b :: a}.
 Fold (p ::: (ps +++ bs)) a b
 -> (:.:) (Fold bs) (Fold (p ::: ps)) a b)
-> (p :~> p)
-> (Fold (p ::: (ps +++ bs)) :.: p)
   :~> ((Fold bs :.: Fold (p ::: ps)) :.: p)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` p a b -> p a b
p :~> p
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN)

-- | Apply a 2-cell inside a concatenation, on the right.
whiskerL
  :: SPath Prof xs -> SPath Prof ys -> SPath Prof zs -> Fold ys :~> Fold zs -> Fold (xs +++ ys) :~> Fold (xs +++ zs)
whiskerL :: forall {j} {b} {k} (xs :: Path j b) (ys :: Path b k)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold ys :~> Fold zs)
-> Fold (xs +++ ys) :~> Fold (xs +++ zs)
whiskerL SPath 'Prof xs
xs SPath 'Prof ys
ys SPath 'Prof zs
zs Fold ys :~> Fold zs
f = SPath 'Prof xs
-> SPath 'Prof zs -> (Fold zs :.: Fold xs) :~> Fold (xs +++ zs)
forall {j} {b} {k} (as :: Path j b) (bs :: Path b k).
SPath 'Prof as
-> SPath 'Prof bs -> (Fold bs :.: Fold as) :~> Fold (as +++ bs)
concatFold SPath 'Prof xs
xs SPath 'Prof zs
zs ((:.:) (Fold zs) (Fold xs) a b -> Fold (xs +++ zs) a b)
-> (Fold (xs +++ ys) a b -> (:.:) (Fold zs) (Fold xs) a b)
-> Fold (xs +++ ys) a b
-> Fold (xs +++ zs) a b
forall b c a. (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 ys a b -> Fold zs a b
Fold ys :~> Fold zs
f (Fold ys :~> Fold zs)
-> (Fold xs :~> Fold xs)
-> (Fold ys :.: Fold xs) :~> (Fold zs :.: Fold xs)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` Fold xs a b -> Fold xs a b
Fold xs :~> Fold xs
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN) ((:.:) (Fold ys) (Fold xs) a b -> (:.:) (Fold zs) (Fold xs) a b)
-> (Fold (xs +++ ys) a b -> (:.:) (Fold ys) (Fold xs) a b)
-> Fold (xs +++ ys) a b
-> (:.:) (Fold zs) (Fold xs) a b
forall b c a. (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 'Prof xs
-> SPath 'Prof ys -> Fold (xs +++ ys) :~> (Fold ys :.: Fold xs)
forall {i} {k} {k} (as :: Path i k) (bs :: Path k k).
SPath 'Prof as
-> SPath 'Prof bs -> Fold (as +++ bs) :~> (Fold bs :.: Fold as)
splitFold SPath 'Prof xs
xs SPath 'Prof ys
ys

-- | Apply a 2-cell inside a concatenation, on the left.
whiskerR
  :: SPath Prof xs -> SPath Prof ys -> SPath Prof zs -> Fold xs :~> Fold ys -> Fold (xs +++ zs) :~> Fold (ys +++ zs)
whiskerR :: forall {j} {b} {k} (xs :: Path j b) (ys :: Path j b)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold xs :~> Fold ys)
-> Fold (xs +++ zs) :~> Fold (ys +++ zs)
whiskerR SPath 'Prof xs
xs SPath 'Prof ys
ys SPath 'Prof zs
zs Fold xs :~> Fold ys
f = SPath 'Prof ys
-> SPath 'Prof zs -> (Fold zs :.: Fold ys) :~> Fold (ys +++ zs)
forall {j} {b} {k} (as :: Path j b) (bs :: Path b k).
SPath 'Prof as
-> SPath 'Prof bs -> (Fold bs :.: Fold as) :~> Fold (as +++ bs)
concatFold SPath 'Prof ys
ys SPath 'Prof zs
zs ((:.:) (Fold zs) (Fold ys) a b -> Fold (ys +++ zs) a b)
-> (Fold (xs +++ zs) a b -> (:.:) (Fold zs) (Fold ys) a b)
-> Fold (xs +++ zs) a b
-> Fold (ys +++ zs) a b
forall b c a. (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 zs a b -> Fold zs a b
forall {a :: k} {b :: b}. Fold zs a b -> Fold zs a b
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN (forall {a :: k} {b :: b}. Fold zs a b -> Fold zs a b)
-> (Fold xs :~> Fold ys)
-> (Fold zs :.: Fold xs) :~> (Fold zs :.: Fold ys)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` Fold xs a b -> Fold ys a b
Fold xs :~> Fold ys
f) ((:.:) (Fold zs) (Fold xs) a b -> (:.:) (Fold zs) (Fold ys) a b)
-> (Fold (xs +++ zs) a b -> (:.:) (Fold zs) (Fold xs) a b)
-> Fold (xs +++ zs) a b
-> (:.:) (Fold zs) (Fold ys) a b
forall b c a. (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 'Prof xs
-> SPath 'Prof zs -> Fold (xs +++ zs) :~> (Fold zs :.: Fold xs)
forall {i} {k} {k} (as :: Path i k) (bs :: Path k k).
SPath 'Prof as
-> SPath 'Prof bs -> Fold (as +++ bs) :~> (Fold bs :.: Fold as)
splitFold SPath 'Prof xs
xs SPath 'Prof zs
zs