{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares where

import Proarrow.Category.Bicategory (Bicategory (..), Ob')
import Proarrow.Category.Bicategory.Strictified (Path (..), SPath (..), Strictified (..), singleton, type (+++))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..))
import Proarrow.Category.Equipment qualified as E
import Proarrow.Core (CategoryOf (..), Promonad ((.)), obj, Obj, (\\))

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, Ob0 hk j, Ob0 hk 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, Ob0 hk j, Ob0 hk 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 hk f ::: Nil, f ::: Nil) '(Nil, Nil)
Sq '(Conjoint (Path hk) (f ::: Nil), f ::: Nil) '(I, I)
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 hk f ::: Nil, Nil) '(Nil, f ::: Nil)
Sq '(Companion (Path hk) (f ::: Nil), I) '(I, 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--------k
-- -- > |        |
-- -- > g>----\  |
-- -- > |     |  |
-- -- > f>-\  |  |
-- -- > |  v  v  |
-- -- > i--f--g--k
-- fromLeft2
--   :: forall {hk} {vk} {i} {j} {k} (f :: vk i j) (g :: vk j k)
--    . (Equipment hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g)
--   => Sq '(Companion hk f ::: Companion hk g ::: Nil, Nil) '(Nil, f ::: g ::: Nil)
-- fromLeft2 =
--   fromLeft
--     === fromLeft ||| vId

-- > 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 = (O (Companion (Path hk) (I ::: Nil)) Nil
 ~> O Nil (Companion (Path hk) Nil))
-> Sq '(Nil, I ::: Nil) '(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 (Companion hk I ::: Nil)
-> SPath Nil
-> (Fold (Companion hk I ::: Nil) ~> Fold Nil)
-> Strictified (Companion hk I ::: Nil) 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 (Obj (Companion hk I) -> SPath Nil -> SPath (Companion hk I ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk I ~> I
forall (i :: k). Ob0 vk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil Fold (Companion hk I ::: Nil) ~> Fold Nil
Companion hk I ~> I
forall (k :: k). Ob0 vk k => Companion hk I ~> I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Companion hk I ~> I
compToId) ((Ob0 vk k, Ob0 vk k, Ob I, Ob I) =>
 Sq '(Nil, I ::: Nil) '(Nil, Nil))
-> (I ~> I) -> Sq '(Nil, I ::: Nil) '(Nil, Nil)
forall (i :: k) (j :: k) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
forall (kk :: CAT k) (i :: k). (Bicategory kk, Ob0 kk i) => Obj I
iObj @vk @k

-- > 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 = (O (Companion (Path hk) Nil) Nil
 ~> O Nil (Companion (Path hk) (I ::: Nil)))
-> Sq '(Nil, Nil) '(Nil, I ::: 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 Nil
-> SPath (Companion hk I ::: Nil)
-> (Fold Nil ~> Fold (Companion hk I ::: Nil))
-> Strictified Nil (Companion hk I ::: 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 Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil (Obj (Companion hk I) -> SPath Nil -> SPath (Companion hk I ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT s) (vk :: CAT s) {j :: s} {k :: s} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk I ~> I
forall (i :: s). Ob0 vk i => Obj I
forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
iObj) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) I ~> Companion hk I
Fold Nil ~> Fold (Companion hk I ::: Nil)
forall (k :: s). Ob0 vk k => I ~> Companion hk I
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
I ~> Companion hk I
compFromId) ((Ob0 vk k, Ob0 vk k, Ob I, Ob I) =>
 Sq '(Nil, Nil) '(Nil, I ::: Nil))
-> (I ~> I) -> Sq '(Nil, Nil) '(Nil, I ::: Nil)
forall (i :: s) (j :: s) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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
\\\ forall {s} (kk :: CAT s) (i :: s).
(Bicategory kk, Ob0 kk i) =>
Obj I
forall (kk :: CAT s) (i :: s). (Bicategory kk, Ob0 kk i) => Obj I
iObj @vk @k

-- > 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, Ob0 hk i, Ob0 hk j, Ob0 hk 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, Ob0 hk i,
 Ob0 hk j, Ob0 hk k, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine =
  let f :: Obj f
f = forall (a :: vk i j). (CategoryOf (vk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; g :: Obj g
g = forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g
  in (O (Companion (Path hk) (f ::: (g ::: Nil))) Nil
 ~> O Nil (Companion (Path hk) (O g f ::: Nil)))
-> Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: 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 hk f ::: (Companion hk g ::: Nil))
-> SPath (Companion hk (O g f) ::: Nil)
-> (Fold (Companion hk f ::: (Companion hk g ::: Nil))
    ~> Fold (Companion hk (O g f) ::: Nil))
-> Strictified
     (Companion hk f ::: (Companion hk g ::: Nil))
     (Companion hk (O g f) ::: 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
          (Obj (Companion hk f)
-> SPath (Companion hk g ::: Nil)
-> SPath (Companion hk f ::: (Companion hk g ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj f
f) (Obj (Companion hk g) -> SPath Nil -> SPath (Companion hk g ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj g
g) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))
          (Obj (Companion hk (O g f))
-> SPath Nil -> SPath (Companion hk (O g f) ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (Obj g
g Obj g -> Obj f -> O g f ~> O g f
forall {i :: k} (j :: k) (k :: k) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk 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 f
f)) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)
          (Obj g
-> Obj f
-> O (Companion hk g) (Companion hk f) ~> Companion hk (O g f)
forall {j1 :: k} {j2 :: k} {k :: k} (f :: vk j2 k) (g :: vk j1 j2).
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
forall {c} (hk :: CAT c) (vk :: CAT c) {j1 :: c} {j2 :: c} {k :: c}
       (f :: vk j2 k) (g :: vk j1 j2).
HasCompanions hk vk =>
Obj f
-> Obj g
-> O (Companion hk f) (Companion hk g) ~> Companion hk (O f g)
compFromCompose Obj g
g Obj f
f)
      )
      ((Ob0 vk i, Ob0 vk k, Ob (O g f), Ob (O g f)) =>
 Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil))
-> (O g f ~> O g f)
-> Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
forall (i :: k) (j :: k) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 g
g Obj g -> Obj f -> O g f ~> O g f
forall {i :: k} (j :: k) (k :: k) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk 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 f
f)

-- > 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, Ob0 hk i, Ob0 hk j, Ob0 hk 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, Ob0 hk i,
 Ob0 hk j, Ob0 hk k, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit =
  let f :: Obj f
f = forall (a :: vk i j). (CategoryOf (vk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; g :: Obj g
g = forall (a :: vk j k). (CategoryOf (vk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @g
  in (O (Companion (Path hk) (O g f ::: Nil)) Nil
 ~> O Nil (Companion (Path hk) (f ::: (g ::: Nil))))
-> Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: 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 hk (O g f) ::: Nil)
-> SPath (Companion hk f ::: (Companion hk g ::: Nil))
-> (Fold (Companion hk (O g f) ::: Nil)
    ~> Fold (Companion hk f ::: (Companion hk g ::: Nil)))
-> Strictified
     (Companion hk (O g f) ::: Nil)
     (Companion hk f ::: (Companion hk g ::: 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
          (Obj (Companion hk (O g f))
-> SPath Nil -> SPath (Companion hk (O g f) ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (Obj g
g Obj g -> Obj f -> O g f ~> O g f
forall {i :: k} (j :: k) (k :: k) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk 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 f
f)) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)
          (Obj (Companion hk f)
-> SPath (Companion hk g ::: Nil)
-> SPath (Companion hk f ::: (Companion hk g ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj f
f) (Obj (Companion hk g) -> SPath Nil -> SPath (Companion hk g ::: 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 (forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk Obj g
g) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))
          (Obj g
-> Obj f
-> Companion hk (O g f) ~> O (Companion hk g) (Companion hk f)
forall {i :: k} {j :: k} {k :: k} (f :: vk j k) (g :: vk i j).
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
forall {c} (hk :: CAT c) (vk :: CAT c) {i :: c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk i j).
HasCompanions hk vk =>
Obj f
-> Obj g
-> Companion hk (O f g) ~> O (Companion hk f) (Companion hk g)
compToCompose Obj g
g Obj f
f)
      )
      ((Ob0 vk i, Ob0 vk k, Ob (O g f), Ob (O g f)) =>
 Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil)))
-> (O g f ~> O g f)
-> Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
forall (i :: k) (j :: k) (ps :: vk i j) (qs :: vk i j) r.
((Ob0 vk i, Ob0 vk 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 g
g Obj g -> Obj f -> O g f ~> O g f
forall {i :: k} (j :: k) (k :: k) (a :: vk j k) (b :: vk j k)
       (c :: vk i j) (d :: vk 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 f
f)