{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares where

import Proarrow.Category.Bicategory (Bicategory (..), Ob')
import Proarrow.Category.Bicategory.Strictified
  ( Fold
  , IsPath (..)
  , Path (..)
  , SPath (..)
  , Strictified (..)
  , asObj
  , companionFold
  , fold
  , foldCompanion
  , mapCompanionSPath
  , singleton
  , type (+++)
  )
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..))
import Proarrow.Category.Equipment qualified as E
import Proarrow.Core (CategoryOf (..), Obj, Promonad ((.)), (\\))

infixl 6 |||
infixl 5 ===

-- | The empty square for an object.
--
-- > K-----K
-- > |     |
-- > |     |
-- > |     |
-- > K-----K
object :: (HasCompanions hk vk, Ob0 vk k) => Sq '(Nil :: Path hk k k, Nil :: Path vk k k) '(Nil, Nil)
object :: forall {k} (hk :: CAT k) (vk :: CAT k) (k :: k).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, Nil)
object = Sq '(I, I) '(I, I)
Sq '(Nil, Nil) '(Nil, Nil)
forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(I, I) '(I, I)
E.object

-- | Make a square from a horizontal proarrow
--
-- > K-----K
-- > |     |
-- > p--@--q
-- > |     |
-- > J-----J
hArr
  :: forall {hk} {vk} {j} {k} (p :: hk j k) q
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => p ~> q
  -> Sq '(p ::: Nil, Nil :: Path vk k k) '(q ::: Nil, Nil :: Path vk j j)
hArr :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {j :: k}
       {k :: k} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
hArr = ((p ::: Nil) ~> (q ::: Nil)) -> Sq '(p ::: Nil, I) '(q ::: Nil, I)
Strictified (p ::: Nil) (q ::: Nil)
-> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {j :: s}
       {k :: s} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
E.hArr (Strictified (p ::: Nil) (q ::: Nil)
 -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil))
-> ((p ~> q) -> Strictified (p ::: Nil) (q ::: Nil))
-> (p ~> q)
-> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
(p ~> q) -> Strictified (p ::: Nil) (q ::: 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

-- | A horizontal identity square.
--
-- > J-----J
-- > |     |
-- > p-----p
-- > |     |
-- > K-----K
hId
  :: (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (p :: hk k j)) => Sq '(p ::: Nil, Nil :: Path vk j j) '(p ::: Nil, Nil)
hId :: forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
       (p :: hk k j).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) =>
Sq '(p ::: Nil, Nil) '(p ::: Nil, Nil)
hId = Sq '(p ::: Nil, I) '(p ::: Nil, I)
Sq '(p ::: Nil, Nil) '(p ::: Nil, Nil)
forall {s} (hk :: CAT s) (vk :: CAT s) (j :: s) (k :: s)
       (p :: hk k j).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) =>
Sq '(p, I) '(p, I)
E.hId

-- | A horizontal identity square for a companion.
--
-- Requires a type application: @compId \@f@
--
-- > K-----K
-- > |     |
-- > f>--->f
-- > |     |
-- > J-----J
compId
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Companion hk f ::: Nil, Nil :: Path vk k k) '(Companion hk f ::: Nil, Nil :: Path vk j j)
compId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Companion hk f ::: Nil, Nil)
compId = forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Companion hk f, I) '(Companion hk f, I)
forall (f :: Path vk j k).
(HasCompanions (Path hk) (Path vk), Ob0 (Path vk) j,
 Ob0 (Path vk) k, Ob f) =>
Sq '(Companion (Path hk) f, I) '(Companion (Path hk) f, I)
E.compId @(f ::: Nil)

-- | A horizontal identity square for a conjoint.
--
-- Requires a type application: @conjId \@f@
--
-- > J-----J
-- > |     |
-- > f>--->f
-- > |     |
-- > K-----K
conjId
  :: forall {hk} {vk} {j} {k} f
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Conjoint hk f ::: Nil, Nil :: Path vk j j) '(Conjoint hk f ::: Nil, Nil :: Path vk k k)
conjId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f ::: Nil, Nil) '(Conjoint hk f ::: Nil, Nil)
conjId = forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, I) '(Conjoint hk f, I)
forall (f :: Path vk j k).
(Equipment (Path hk) (Path vk), Ob0 (Path vk) j, Ob0 (Path vk) k,
 Ob f) =>
Sq '(Conjoint (Path hk) f, I) '(Conjoint (Path hk) f, I)
E.conjId @(f ::: Nil)

-- | Make a square from a vertical arrow
--
-- > J--f--K
-- > |  v  |
-- > |  @  |
-- > |  v  |
-- > J--g--K
vArr
  :: forall {hk} {vk} {j} {k} (f :: vk j k) g
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => f ~> g
  -> Sq '(Nil :: Path hk j j, f ::: Nil) '(I :: Path hk k k, g ::: Nil)
vArr :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr = ((f ::: Nil) ~> (g ::: Nil)) -> Sq '(I, f ::: Nil) '(I, g ::: Nil)
Strictified (f ::: Nil) (g ::: Nil)
-> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
E.vArr (Strictified (f ::: Nil) (g ::: Nil)
 -> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil))
-> ((f ~> g) -> Strictified (f ::: Nil) (g ::: Nil))
-> (f ~> g)
-> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (f ~> g) -> (f ::: Nil) ~> (g ::: Nil)
(f ~> g) -> Strictified (f ::: Nil) (g ::: 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

-- | A vertical identity square.
--
-- > J--f--K
-- > |  v  |
-- > |  |  |
-- > |  v  |
-- > J--f--K
vId
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Nil :: Path hk j j, f ::: Nil) '(Nil :: Path hk k k, f ::: Nil)
vId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId = Sq '(I, f ::: Nil) '(I, f ::: Nil)
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, f) '(I, f)
E.vId

vId'
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => Obj f
  -> Sq '(Nil :: Path hk j j, f ::: Nil) '(Nil :: Path hk k k, f ::: Nil)
vId' :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId' Obj f
f = Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
(Ob f, Ob f) => Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId ((Ob f, Ob f) => Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil))
-> Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj f
f

-- | Horizontal composition
--
-- > L--d--H     H--f--I     L-d+f-I
-- > |  v  |     |  v  |     |  v  |
-- > p--@--q ||| q--@--r  =  p--@--r
-- > |  v  |     |  v  |     |  v  |
-- > M--e--J     J--g--K     M-e+g-K
(|||)
  :: forall {hk} {vk} {h} {l} {m} (ps :: Path hk m l) qs rs (ds :: Path vk l h) es fs gs
   . (HasCompanions hk vk)
  => Sq '(ps, ds) '(qs, es)
  -> Sq '(qs, fs) '(rs, gs)
  -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| :: forall {k} {b :: k} {k :: k} {i :: k} {hk :: CAT k} {vk :: CAT k}
       {h :: k} {l :: k} {m :: k} (ps :: Path hk m l) (qs :: Path hk b h)
       (rs :: Path hk k i) (ds :: Path vk l h) (es :: Path vk m b)
       (fs :: Path vk h i) (gs :: Path vk b k).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
(|||) = Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, O fs ds) '(rs, O gs es)
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
forall {c} {j :: c} {k :: c} {i :: c} {hk :: c -> c -> Type}
       {vk :: c -> c -> Type} {h :: c} {l :: c} {m :: c} (p :: hk m l)
       (q :: hk j h) (r :: hk k i) (d :: vk l h) (e :: vk m j)
       (f :: vk h i) (g :: vk j k).
HasCompanions hk vk =>
Sq '(p, d) '(q, e)
-> Sq '(q, f) '(r, g) -> Sq '(p, O f d) '(r, O g e)
(E.|||)

-- | Vertical composition
--
-- >  H--e--I
-- >  |  v  |
-- >  r--@--s
-- >  |  v  |
-- >  J--f--K
-- >    ===
-- >  J--f--K
-- >  |  v  |
-- >  p--@--q
-- >  |  v  |
-- >  L--g--M
-- >
-- >    v v
-- >
-- >  H--e--I
-- >  |  v  |
-- > p+r-@-q+s
-- >  |  v  |
-- >  J--g--K
(===)
  :: forall {hk} {vk} {h} {i} {j} {l} (ps :: Path hk l j) qs rs ss (es :: Path vk h i) fs gs
   . (HasCompanions hk vk)
  => Sq '(rs, es) '(ss, fs)
  -> Sq '(ps, fs) '(qs, gs)
  -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== :: forall {k} {k :: k} {b :: k} {hk :: CAT k} {vk :: CAT k} {h :: k}
       {i :: k} {j :: k} {l :: k} (ps :: Path hk l j) (qs :: Path hk k b)
       (rs :: Path hk j h) (ss :: Path hk b i) (es :: Path vk h i)
       (fs :: Path vk j b) (gs :: Path vk l k).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
(===) = Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(O rs ps, es) '(O ss qs, gs)
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
(E.===)

-- | Bend a vertical arrow in the companion direction.
--
-- > J--f--K
-- > |  v  |
-- > |  \->f
-- > |     |
-- > J-----J
toRight
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob' (f :: vk j k))
  => Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
toRight :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
toRight = Sq '(I, f ::: Nil) '(Companion (Path hk) (f ::: Nil), I)
Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(I, f) '(Companion hk f, I)
E.toRight

-- | Bend a vertical arrow in the conjoint direction.
--
-- > J--f--K
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > K-----K
toLeft
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft = Sq '(Conjoint (Path hk) (f ::: Nil), f ::: Nil) '(I, I)
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, f) '(I, I)
E.toLeft

-- | Bend a companion proarrow back to a vertical arrow.
--
-- > K-----K
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > J--f--K
fromLeft
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob' (f :: vk j k))
  => Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft = Sq '(Companion (Path hk) (f ::: Nil), I) '(I, f ::: Nil)
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
forall {s} {hk :: CAT s} {vk :: CAT s} {j :: s} {k :: s}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f, I) '(I, f)
E.fromLeft

-- | Bend a conjoint proarrow back to a vertical arrow.
--
-- > J-----J
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > J--f--K
fromRight
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f)
  => Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight = Sq '(I, I) '(Conjoint (Path hk) (f ::: Nil), f ::: Nil)
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, I) '(Conjoint hk f, f)
E.fromRight

-- > K--I--K
-- > |  v  |
-- > |  @  |
-- > |     |
-- > K-----K
vUnitor
  :: forall hk vk k
   . (HasCompanions hk vk, Ob0 vk k)
  => Sq '(Nil :: Path hk k k, I ::: Nil) '(Nil :: Path hk k k, Nil :: Path vk k k)
vUnitor :: forall {k} (hk :: CAT k) (vk :: CAT k) (k :: k).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, I ::: Nil) '(Nil, Nil)
vUnitor = Sq '(Nil, I ::: Nil) '(Nil, Nil)
Sq '(Nil, Fold Nil ::: Nil) '(Nil, Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll

-- > K-----K
-- > |     |
-- > |  @  |
-- > |  v  |
-- > K--I--K
vUnitorInv
  :: forall hk vk k
   . (HasCompanions hk vk, Ob0 vk k)
  => Sq '(Nil :: Path hk k k, Nil :: Path vk k k) '(Nil :: Path hk k k, I ::: Nil)
vUnitorInv :: forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, I ::: Nil)
vUnitorInv = Sq '(Nil, Nil) '(Nil, I ::: Nil)
Sq '(Nil, Nil) '(Nil, Fold Nil ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll

-- > I-f-g-K
-- > | v v |
-- > | \@/ |
-- > |  v  |
-- > I-gof-K
vCombine
  :: forall {hk} {vk} {i} {j} {k} (f :: vk i j) (g :: vk j k)
   . (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g)
  => Sq '(Nil :: Path hk i i, f ::: g ::: Nil) '(Nil, g `O` f ::: Nil)
vCombine :: forall {k} {hk :: CAT k} {vk :: CAT k} {i :: k} {j :: k} {k :: k}
       (f :: vk i j) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine = Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
Sq
  '(Nil, f ::: (g ::: Nil)) '(Nil, Fold (f ::: (g ::: Nil)) ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll

-- > I-gof-K
-- > |  v  |
-- > | /@\ |
-- > | v v |
-- > I-f-g-K
vSplit
  :: forall {hk} {vk} {i} {j} {k} (f :: vk i j) (g :: vk j k)
   . (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g)
  => Sq '(Nil :: Path hk i i, g `O` f ::: Nil) '(Nil, f ::: g ::: Nil)
vSplit :: forall {k} {hk :: CAT k} {vk :: CAT k} {i :: k} {j :: k} {k :: k}
       (f :: vk i j) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit = Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
Sq
  '(Nil, Fold (f ::: (g ::: Nil)) ::: Nil) '(Nil, f ::: (g ::: Nil))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll

-- | Combine a whole bunch of vertical arrows into one composed arrow.
--
-- > J-p..-K
-- > | vvv |
-- > | \@/ |
-- > |  v  |
-- > J--f--K
vCombineAll
  :: forall {hk} {vk} {j} {k} (ps :: Path vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Nil :: Path hk j j, ps) '(Nil :: Path hk k k, Fold ps ::: Nil)
vCombineAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll =
  let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = 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
ps
  in (O (Companion (Path hk) ps) Nil
 ~> O Nil (Companion (Path hk) (Fold ps ::: Nil)))
-> Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
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 (SPath (Companion (Path hk) ps)
-> SPath (Companion hk (Fold ps) ::: Nil)
-> (Fold (Companion (Path hk) ps)
    ~> Fold (Companion hk (Fold ps) ::: Nil))
-> Strictified
     (Companion (Path hk) ps) (Companion hk (Fold ps) ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (SPath ps -> SPath (Companion (Path hk) ps)
forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath ps
ps) (Obj (Companion hk (Fold ps))
-> SPath Nil -> SPath (Companion hk (Fold ps) ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons ((Fold ps ~> Fold ps) -> Obj (Companion hk (Fold ps))
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 Fold ps ~> Fold ps
fps) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) (SPath ps -> Fold (Companion (Path hk) ps) ~> Companion hk (Fold ps)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath ps
ps)) ((Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Nil, ps) '(Nil, Fold ps ::: Nil))
-> (Fold ps ~> Fold ps) -> Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold ps ~> Fold ps
fps

-- | Split one composed arrow into a whole bunch of vertical arrows.
--
-- > J--f--K
-- > |  v  |
-- > | /@\ |
-- > | vvv |
-- > J-p..-K
vSplitAll
  :: forall {hk} {vk} {j} {k} (ps :: Path vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Nil :: Path hk j j, Fold ps ::: Nil) '(Nil :: Path hk k k, ps)
vSplitAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll =
  let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = 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
ps; cps :: SPath (Companion (Path hk) ps)
cps = forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k2 :: k}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath @hk SPath ps
ps
  in (O (Companion (Path hk) (Fold ps ::: Nil)) Nil
 ~> O Nil (Companion (Path hk) ps))
-> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
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 (SPath (Companion hk (Fold ps) ::: Nil)
-> SPath (Companion (Path hk) ps)
-> (Fold (Companion hk (Fold ps) ::: Nil)
    ~> Fold (Companion (Path hk) ps))
-> Strictified
     (Companion hk (Fold ps) ::: Nil) (Companion (Path hk) ps)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str (Obj (Companion hk (Fold ps))
-> SPath Nil -> SPath (Companion hk (Fold ps) ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons ((Fold ps ~> Fold ps) -> Obj (Companion hk (Fold ps))
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 Fold ps ~> Fold ps
fps) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) SPath (Companion (Path hk) ps)
cps (SPath ps -> Companion hk (Fold ps) ~> Fold (Companion (Path hk) ps)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath ps
ps)) ((Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Nil, Fold ps ::: Nil) '(Nil, ps))
-> (Fold ps ~> Fold ps) -> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold ps ~> Fold ps
fps ((Ob (Companion (Path hk) ps), Ob (Companion (Path hk) ps)) =>
 Sq '(Nil, Fold ps ::: Nil) '(Nil, ps))
-> Strictified (Companion (Path hk) ps) (Companion (Path hk) ps)
-> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path hk j k) (b :: Path hk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath (Companion (Path hk) ps) -> Obj (Companion (Path hk) ps)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath (Companion (Path hk) ps)
cps

-- | Combine a whole bunch of horizontal proarrows into one composed proarrow.
--
-- > K-----K
-- > p--\  |
-- > :--@--f
-- > :--/  |
-- > J-----J
hCombineAll
  :: forall {hk} {vk} {j} {k} (ps :: Path hk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(ps, Nil :: Path vk k k) '(Fold ps ::: Nil, Nil)
hCombineAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(ps, Nil) '(Fold ps ::: Nil, Nil)
hCombineAll = let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path hk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = 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
ps in (O (Companion (Path hk) Nil) ps
 ~> O (Fold ps ::: Nil) (Companion (Path hk) Nil))
-> Sq '(ps, Nil) '(Fold ps ::: Nil, Nil)
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 (SPath ps
-> SPath (Fold ps ::: Nil)
-> (Fold ps ~> Fold (Fold ps ::: Nil))
-> Strictified ps (Fold ps ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath ps
ps ((Fold ps ~> Fold ps) -> SPath Nil -> SPath (Fold ps ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Fold ps ~> Fold ps
fps SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) Fold ps ~> Fold ps
Fold ps ~> Fold (Fold ps ::: Nil)
fps) ((Ob0 hk j, Ob0 hk k, Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(ps, Nil) '(Fold ps ::: Nil, Nil))
-> (Fold ps ~> Fold ps) -> Sq '(ps, Nil) '(Fold ps ::: Nil, 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
\\\ Fold ps ~> Fold ps
fps

-- | Split one composed proarrow into a whole bunch of horizontal proarrows.
--
-- > K-----K
-- > |  /--p
-- > f--@--:
-- > |  \--:
-- > J-----J
hSplitAll
  :: forall {hk} {vk} {j} {k} (ps :: Path hk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Fold ps ::: Nil, Nil :: Path vk k k) '(ps, Nil)
hSplitAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Fold ps ::: Nil, Nil) '(ps, Nil)
hSplitAll = let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path hk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = 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
ps in (O (Companion (Path hk) Nil) (Fold ps ::: Nil)
 ~> O ps (Companion (Path hk) Nil))
-> Sq '(Fold ps ::: Nil, Nil) '(ps, Nil)
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 (SPath (Fold ps ::: Nil)
-> SPath ps
-> (Fold (Fold ps ::: Nil) ~> Fold ps)
-> Strictified (Fold ps ::: Nil) ps
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str ((Fold ps ~> Fold ps) -> SPath Nil -> SPath (Fold ps ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Fold ps ~> Fold ps
fps SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) SPath ps
ps Fold ps ~> Fold ps
Fold (Fold ps ::: Nil) ~> Fold ps
fps) ((Ob0 hk j, Ob0 hk k, Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Fold ps ::: Nil, Nil) '(ps, Nil))
-> (Fold ps ~> Fold ps) -> Sq '(Fold ps ::: Nil, Nil) '(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
\\\ Fold ps ~> Fold ps
fps