{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Double.Quintet where

import Data.Function (($))

import Proarrow.Core (CAT, CategoryOf(..), Promonad (..), Profunctor(..), UN, Is, dimapDefault)
import Proarrow.Category.Double (Double (..))
import Proarrow.Category.Bicategory (Path(..), appendObj, Bicategory (..), type (+++), Fold, IsPath (..), Strictified (..), SPath (..), asObj)
import Proarrow.Category.Bicategory.Co (COK(..), Co(..), concatFoldCo, splitFoldCo)
import Proarrow.Object (obj, src, tgt)


type data QKK kk i j = QK (kk i j)
type instance UN QK (QK p) = p

type Q2 :: CAT (QKK kk i j)
data Q2 a b where
  Q2 :: a ~> b -> Q2 (QK a) (QK b)
instance CategoryOf (kk i j) => Profunctor (Q2 :: CAT (QKK kk i j)) where
  dimap :: forall (c :: QKK kk i j) (a :: QKK kk i j) (b :: QKK kk i j)
       (d :: QKK kk i j).
(c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d
dimap = (c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d
Q2 c a -> Q2 b d -> Q2 a b -> Q2 c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: QKK kk i j) (b :: QKK kk i j) r.
((Ob a, Ob b) => r) -> Q2 a b -> r
\\ Q2 a ~> b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: kk i j) (b :: kk i j) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
p
instance CategoryOf (kk i j) => Promonad (Q2 :: CAT (QKK kk i j)) where
  id :: forall (a :: QKK kk i j). Ob a => Q2 a a
id = (UN QK a ~> UN QK a) -> Q2 (QK (UN QK a)) (QK (UN QK a))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 UN QK a ~> UN QK a
forall (a :: kk i j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Q2 a ~> b
f . :: forall (b :: QKK kk i j) (c :: QKK kk i j) (a :: QKK kk i j).
Q2 b c -> Q2 a b -> Q2 a c
. Q2 a ~> b
g = (a ~> b) -> Q2 (QK a) (QK b)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: kk i j) (c :: kk i j) (a :: kk i j).
(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
. a ~> a
a ~> b
g)
instance CategoryOf (kk i j) => CategoryOf (QKK kk i j) where
  type (~>) = Q2
  type Ob (a :: QKK kk i j) = (Is QK a, Ob (UN QK a))

concatFoldQ
  :: forall {kk} {i} {j} {k} {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k)
   . (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => SPath ps -> UN QK (Fold ps) `O` UN QK (Fold qs) ~> UN QK (Fold (ps +++ qs))
concatFoldQ :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> O (UN QK (Fold ps)) (UN QK (Fold qs))
   ~> UN QK (Fold (ps +++ qs))
concatFoldQ SPath ps
SNil = Obj (UN QK (Fold qs)) -> O I (UN QK (Fold qs)) ~> UN QK (Fold qs)
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
leftUnitor (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs)))
concatFoldQ (SCons @_ @ps1 (Q2 a ~> b
p) SPath ps1
SNil) = case forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (QKK kk) j k). IsPath ps => SPath ps
singPath @qs of
  SPath qs
SNil -> Obj b -> O b I ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
rightUnitor a ~> b
Obj b
p
  SCons{} -> a ~> b
Obj b
p Obj b
-> (UN QK (Fold qs) ~> UN QK (Fold qs))
-> O b (UN QK (Fold qs)) ~> O b (UN QK (Fold qs))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs))
concatFoldQ (SCons @_ @ps1 (Q2 a ~> b
p) ps :: SPath ps1
ps@SCons{})
  = (a ~> b
b ~> b
p (b ~> b)
-> (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs))
    ~> UN QK (Fold (p ::: (ps1 +++ qs))))
-> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
   ~> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> O (UN QK (Fold ps)) (UN QK (Fold qs))
   ~> UN QK (Fold (ps +++ qs))
forall (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk k2, Ob0 kk j, Ob0 kk k) =>
SPath ps1
-> O (UN QK (Fold ps1)) (UN QK (Fold qs))
   ~> UN QK (Fold (ps1 +++ qs))
concatFoldQ @qs SPath ps1
ps)
  (O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
 ~> O b (UN QK (Fold (p ::: (ps1 +++ qs)))))
-> (O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
    ~> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs))))
-> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
   ~> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
forall (b :: kk i k) (c :: kk i k) (a :: kk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> b)
-> Obj (UN QK (Fold (p ::: ps1)))
-> Obj (UN QK (Fold qs))
-> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
   ~> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator a ~> b
b ~> b
p (forall (a :: kk k2 j). (CategoryOf (kk k2 j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold ps1))) (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs)))
  ((Ob (p ::: ps1), Ob (p ::: ps1)) =>
 O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
 ~> O b (UN QK (Fold (p ::: (ps1 +++ qs)))))
-> Strictified (p ::: ps1) (p ::: ps1)
-> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
   ~> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
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 (QKK kk) k2 j) (b :: Path (QKK kk) k2 j) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath ps1 -> Obj ps1
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps1
ps

splitFoldQ
  :: forall {kk} {i} {j} {k} {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k)
   . (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k)
  => SPath ps -> UN QK (Fold (ps +++ qs)) ~> UN QK (Fold ps) `O` UN QK (Fold qs)
splitFoldQ :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> UN QK (Fold (ps +++ qs))
   ~> O (UN QK (Fold ps)) (UN QK (Fold qs))
splitFoldQ SPath ps
SNil = Obj (UN QK (Fold qs)) -> UN QK (Fold qs) ~> O I (UN QK (Fold qs))
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
leftUnitorInv (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs)))
splitFoldQ (SCons @_ @ps1 (Q2 a ~> b
p) SPath ps1
SNil) = case forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (QKK kk) j k). IsPath ps => SPath ps
singPath @qs of
  SPath qs
SNil -> Obj b -> b ~> O b I
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
rightUnitorInv Obj b
a ~> b
p
  SCons{} -> a ~> b
b ~> b
p (b ~> b)
-> (UN QK (Fold qs) ~> UN QK (Fold qs))
-> O b (UN QK (Fold qs)) ~> O b (UN QK (Fold qs))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs))
splitFoldQ (SCons @_ @ps1 (Q2 a ~> b
p) ps :: SPath ps1
ps@SCons{})
  = Obj b
-> Obj (UN QK (Fold (p ::: ps1)))
-> Obj (UN QK (Fold qs))
-> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
   ~> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv a ~> b
Obj b
p (forall (a :: kk k2 j). (CategoryOf (kk k2 j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold ps1))) (forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs)))
  (O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
 ~> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs)))
-> (O b (UN QK (Fold (p ::: (ps1 +++ qs))))
    ~> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs))))
-> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
   ~> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
forall (b :: kk i k) (c :: kk i k) (a :: kk i k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
Obj b
p Obj b
-> (UN QK (Fold (p ::: (ps1 +++ qs)))
    ~> O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
-> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
   ~> O b (O (UN QK (Fold (p ::: ps1))) (UN QK (Fold qs)))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> UN QK (Fold (ps +++ qs))
   ~> O (UN QK (Fold ps)) (UN QK (Fold qs))
forall (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk k2, Ob0 kk j, Ob0 kk k) =>
SPath ps1
-> UN QK (Fold (ps1 +++ qs))
   ~> O (UN QK (Fold ps1)) (UN QK (Fold qs))
splitFoldQ @qs SPath ps1
ps)
  ((Ob (p ::: ps1), Ob (p ::: ps1)) =>
 O b (UN QK (Fold (p ::: (ps1 +++ qs))))
 ~> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs)))
-> Strictified (p ::: ps1) (p ::: ps1)
-> O b (UN QK (Fold (p ::: (ps1 +++ qs))))
   ~> O (O b (UN QK (Fold (p ::: ps1)))) (UN QK (Fold qs))
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 (QKK kk) k2 j) (b :: Path (QKK kk) k2 j) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath ps1 -> Obj ps1
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath ps1
ps

instance Bicategory kk => Bicategory (QKK kk) where
  type Ob0 (QKK kk) k = Ob0 kk k
  type I = QK I
  type O a b = QK (UN QK a `O` UN QK b)
  (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: k) (j :: k) (ps :: QKK kk i j) (qs :: QKK kk i j) r.
((Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Q2 a ~> b
f = r
(Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r
(Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r
r ((Ob0 kk i, Ob0 kk j, Ob a, Ob b) => r) -> (a ~> b) -> 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 k (kk :: CAT k) (i :: k) (j :: k) (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
\\\ a ~> b
f
  Q2 a ~> b
f o :: forall {k1 :: k} (i :: k) (j :: k) (a :: QKK kk i j)
       (b :: QKK kk i j) (c :: QKK kk j k1) (d :: QKK kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Q2 a ~> b
g = (O a a ~> O b b) -> Q2 (QK (O a a)) (QK (O b b))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (a ~> b
f (a ~> b) -> (a ~> b) -> O a a ~> O b b
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a ~> b
g)
  leftUnitor :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> O I a ~> a
leftUnitor (Q2 a ~> b
p) = (O I b ~> b) -> Q2 (QK (O I b)) (QK b)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> O I b ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
leftUnitor a ~> b
Obj b
p)
  leftUnitorInv :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> a ~> O I a
leftUnitorInv (Q2 a ~> b
p) = (b ~> O I b) -> Q2 (QK b) (QK (O I b))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> b ~> O I b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
leftUnitorInv a ~> b
Obj b
p)
  rightUnitor :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> O a I ~> a
rightUnitor (Q2 a ~> b
p) = (O b I ~> b) -> Q2 (QK (O b I)) (QK b)
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> O b I ~> b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
rightUnitor a ~> b
Obj b
p)
  rightUnitorInv :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> a ~> O a I
rightUnitorInv (Q2 a ~> b
p) = (b ~> O b I) -> Q2 (QK b) (QK (O b I))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> b ~> O b I
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
rightUnitorInv a ~> b
Obj b
p)
  associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: QKK kk i j2)
       (b :: QKK kk j2 j1) (c :: QKK kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Q2 a ~> b
p) (Q2 a ~> b
q) (Q2 a ~> b
r) = (O (O b b) b ~> O b (O b b))
-> Q2 (QK (O (O b b) b)) (QK (O b (O b b)))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> Obj b -> Obj b -> O (O b b) b ~> O b (O b b)
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator a ~> b
Obj b
p a ~> b
Obj b
q a ~> b
Obj b
r)
  associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: QKK kk i j2)
       (b :: QKK kk j2 j1) (c :: QKK kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Q2 a ~> b
p) (Q2 a ~> b
q) (Q2 a ~> b
r) = (O b (O b b) ~> O (O b b) b)
-> Q2 (QK (O b (O b b))) (QK (O (O b b) b))
forall {k} {k} {kk :: k -> k -> Type} {i :: k} {j :: k}
       (a :: kk i j) (b :: kk i j).
(a ~> b) -> Q2 (QK a) (QK b)
Q2 (Obj b -> Obj b -> Obj b -> O b (O b b) ~> O (O b b) b
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv a ~> b
Obj b
p a ~> b
Obj b
q a ~> b
Obj b
r)


type Quintet (ps :: Path (QKK kk) h j) = Sq (QKK kk) (COK kk) ps
type Quintet1 (p :: QKK kk h j) = Sq1 (QKK kk) (COK kk) p

-- | The quintet construction. Create a double category of squares @alpha :: ps +++ gs ~> fs +++ qs@ from a bicategory.
instance Bicategory kk => Double (QKK kk) (COK kk) where
  data Sq (QKK kk) (COK kk) ps qs fs gs where
    Q
      :: (IsPath ps, IsPath qs, IsPath fs, IsPath gs)
      => Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
      -> Sq (QKK kk) (COK kk) (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k)
  data Sq1 (QKK kk) (COK kk) p q f g where
    Q1
      :: (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g)
      => UN QK p `O` UN CO g ~> UN CO f `O` UN QK q
      -> Sq1 (QKK kk) (COK kk) (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i) (g :: COK kk j k)
  singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: QKK kk h j)
       (q :: QKK kk i k1) (f :: COK kk h i) (g :: COK kk j k1).
(DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i,
 DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob p, Ob q,
 Ob f, Ob g) =>
Sq1 (QKK kk) (COK kk) p q f g
-> Sq
     (QKK kk) (COK kk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
singleton = Sq1 (QKK kk) (COK kk) p q f g
-> Sq
     (QKK kk) (COK kk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
Sq1
  (QKK kk)
  (COK kk)
  (Fold (p ::: Nil))
  (Fold (q ::: Nil))
  (Fold (f ::: Nil))
  (Fold (g ::: Nil))
-> Sq
     (QKK kk) (COK kk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q
  folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k)
       (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1)
       (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1).
(DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i,
 DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs,
 Ob fs, Ob gs) =>
Sq (QKK kk) (COK kk) ps qs fs gs
-> Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
folded (Q Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
sq) = Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
sq
  (DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i,
 DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs,
 Ob fs, Ob gs) =>
r
r \\\\ :: forall (h :: k) (i :: k) (j :: k) (k1 :: k)
       (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1)
       (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1) r.
((DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i,
  DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs,
  Ob fs, Ob gs) =>
 r)
-> Sq (QKK kk) (COK kk) ps qs fs gs -> r
\\\\ Q (Q1 O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n) = r
(DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i,
 DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs,
 Ob fs, Ob gs) =>
r
(Ob0 kk h, Ob0 kk k1, Ob (O (UN QK (Fold ps)) (UN 'CO (Fold gs))),
 Ob (O (UN 'CO (Fold fs)) (UN QK (Fold qs)))) =>
r
r ((Ob0 kk h, Ob0 kk k1, Ob (O (UN QK (Fold ps)) (UN 'CO (Fold gs))),
  Ob (O (UN 'CO (Fold fs)) (UN QK (Fold qs)))) =>
 r)
-> (O (UN QK (Fold ps)) (UN 'CO (Fold gs))
    ~> O (UN 'CO (Fold fs)) (UN QK (Fold qs)))
-> 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 k (kk :: CAT k) (i :: k) (j :: k) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n
  object :: forall (k1 :: k).
DOb (QKK kk) (COK kk) k1 =>
Sq (QKK kk) (COK kk) Nil Nil Nil Nil
object = Sq1 (QKK kk) (COK kk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
-> Sq (QKK kk) (COK kk) Nil Nil Nil Nil
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q (Sq1 (QKK kk) (COK kk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
 -> Sq (QKK kk) (COK kk) Nil Nil Nil Nil)
-> Sq1
     (QKK kk) (COK kk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
-> Sq (QKK kk) (COK kk) Nil Nil Nil Nil
forall a b. (a -> b) -> a -> b
$ (O (UN QK (QK I)) (UN 'CO ('CO I))
 ~> O (UN 'CO ('CO I)) (UN QK (QK I)))
-> Sq1 (QKK kk) (COK kk) (QK I) (QK I) ('CO I) ('CO I)
forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k :: k)
       (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i)
       (g :: COK kk j k).
(Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g) =>
(O (UN QK p) (UN 'CO g) ~> O (UN 'CO f) (UN QK q))
-> Sq1 (QKK kk) (COK kk) p q f g
Q1 (forall (a :: kk k1 k1). (CategoryOf (kk k1 k1), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @I Obj I -> Obj I -> O I I ~> O I I
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall (a :: kk k1 k1). (CategoryOf (kk k1 k1), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @I)
  hArr :: forall (j :: k) (k1 :: k) (ps :: Path (QKK kk) j k1)
       (qs :: Path (QKK kk) j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(ps ~> qs) -> Sq (QKK kk) (COK kk) ps qs Nil Nil
hArr (Str Fold ps ~> Fold qs
n) = Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold Nil) (Fold Nil)
-> Sq (QKK kk) (COK kk) ps qs Nil Nil
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q ((QK (UN QK (Fold ps)) ~> QK (UN QK (Fold qs)))
-> Sq1
     (QKK kk) (COK kk) (QK (UN QK (Fold ps))) (QK (UN QK (Fold qs))) I I
forall (j :: k) (k1 :: k) (p :: QKK kk j k1) (q :: QKK kk j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(p ~> q) -> Sq1 (QKK kk) (COK kk) p q I I
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k1 :: k)
       (p :: hk j k1) (q :: hk j k1).
(Double hk vk, DOb hk vk j, DOb hk vk k1) =>
(p ~> q) -> Sq1 hk vk p q I I
hArr1 Fold ps ~> Fold qs
QK (UN QK (Fold ps)) ~> QK (UN QK (Fold qs))
n)
  hArr1 :: forall (j :: k) (k1 :: k) (p :: QKK kk j k1) (q :: QKK kk j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(p ~> q) -> Sq1 (QKK kk) (COK kk) p q I I
hArr1 (Q2 a ~> b
n) = (O (UN QK (QK a)) (UN 'CO ('CO I))
 ~> O (UN 'CO ('CO I)) (UN QK (QK b)))
-> Sq1 (QKK kk) (COK kk) (QK a) (QK b) ('CO I) ('CO I)
forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k :: k)
       (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i)
       (g :: COK kk j k).
(Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g) =>
(O (UN QK p) (UN 'CO g) ~> O (UN 'CO f) (UN QK q))
-> Sq1 (QKK kk) (COK kk) p q f g
Q1 (Obj b -> b ~> O I b
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O I a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O I a
leftUnitorInv ((a ~> b) -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> b
n) (b ~> O I b) -> (O a I ~> b) -> O a I ~> O I b
forall (b :: kk j k1) (c :: kk j k1) (a :: kk j k1).
(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
. a ~> b
n (a ~> b) -> (O a I ~> a) -> O a I ~> b
forall (b :: kk j k1) (c :: kk j k1) (a :: kk j k1).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj a -> O a I ~> a
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O a I ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O a I ~> a
rightUnitor ((a ~> b) -> Obj a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a ~> b
n)) ((Ob a, Ob b) =>
 Sq1 (QKK kk) (COK kk) (QK a) (QK b) ('CO I) ('CO I))
-> (a ~> b) -> Sq1 (QKK kk) (COK kk) (QK a) (QK b) ('CO I) ('CO I)
forall (a :: kk j k1) (b :: kk j k1) 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
\\ a ~> b
n
  vArr :: forall (j :: k) (k1 :: k) (fs :: Path (COK kk) j k1)
       (gs :: Path (COK kk) j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(fs ~> gs) -> Sq (QKK kk) (COK kk) Nil Nil fs gs
vArr (Str Fold fs ~> Fold gs
n) = Sq1 (QKK kk) (COK kk) (Fold Nil) (Fold Nil) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) Nil Nil fs gs
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q (('CO (UN 'CO (Fold fs)) ~> 'CO (UN 'CO (Fold gs)))
-> Sq1
     (QKK kk)
     (COK kk)
     I
     I
     ('CO (UN 'CO (Fold fs)))
     ('CO (UN 'CO (Fold gs)))
forall (j :: k) (k1 :: k) (f :: COK kk j k1) (g :: COK kk j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(f ~> g) -> Sq1 (QKK kk) (COK kk) I I f g
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k1 :: k)
       (f :: vk j k1) (g :: vk j k1).
(Double hk vk, DOb hk vk j, DOb hk vk k1) =>
(f ~> g) -> Sq1 hk vk I I f g
vArr1 Fold fs ~> Fold gs
'CO (UN 'CO (Fold fs)) ~> 'CO (UN 'CO (Fold gs))
n)
  vArr1 :: forall (j :: k) (k1 :: k) (f :: COK kk j k1) (g :: COK kk j k1).
(DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) =>
(f ~> g) -> Sq1 (QKK kk) (COK kk) I I f g
vArr1 (Co b1 ~> a1
n) = (O (UN QK (QK I)) (UN 'CO ('CO b1))
 ~> O (UN 'CO ('CO a1)) (UN QK (QK I)))
-> Sq1 (QKK kk) (COK kk) (QK I) (QK I) ('CO a1) ('CO b1)
forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k :: k)
       (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i)
       (g :: COK kk j k).
(Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g) =>
(O (UN QK p) (UN 'CO g) ~> O (UN 'CO f) (UN QK q))
-> Sq1 (QKK kk) (COK kk) p q f g
Q1 (Obj a1 -> a1 ~> O a1 I
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> a ~> O a I
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> a ~> O a I
rightUnitorInv ((b1 ~> a1) -> Obj a1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b1 ~> a1
n) (a1 ~> O a1 I) -> (O I b1 ~> a1) -> O I b1 ~> O a1 I
forall (b :: kk j k1) (c :: kk j k1) (a :: kk j k1).
(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
. b1 ~> a1
n (b1 ~> a1) -> (O I b1 ~> b1) -> O I b1 ~> a1
forall (b :: kk j k1) (c :: kk j k1) (a :: kk j k1).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj b1 -> O I b1 ~> b1
forall (i :: k) (j :: k) (a :: kk i j). Obj a -> O I a ~> a
forall k (kk :: CAT k) (i :: k) (j :: k) (a :: kk i j).
Bicategory kk =>
Obj a -> O I a ~> a
leftUnitor ((b1 ~> a1) -> Obj b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b1 ~> a1
n)) ((Ob b1, Ob a1) =>
 Sq1 (QKK kk) (COK kk) (QK I) (QK I) ('CO a1) ('CO b1))
-> (b1 ~> a1)
-> Sq1 (QKK kk) (COK kk) (QK I) (QK I) ('CO a1) ('CO b1)
forall (a :: kk j k1) (b :: kk j k1) 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
\\ b1 ~> a1
n

  (|||) :: forall {h} {j} (ps :: Path (QKK kk) h j) qs rs fs gs hs is. Quintet ps qs fs gs -> Quintet qs rs hs is -> Quintet ps rs (fs +++ hs) (gs +++ is)
  Q (Q1 O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n) ||| :: forall {b :: k} {b :: k} {c :: k} {c :: k} {h :: k} {j :: k}
       (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) b b)
       (rs :: Path (QKK kk) c c) (fs :: Path (COK kk) h b)
       (gs :: Path (COK kk) j b) (hs :: Path (COK kk) b c)
       (is :: Path (COK kk) b c).
Quintet ps qs fs gs
-> Quintet qs rs hs is -> Quintet ps rs (fs +++ hs) (gs +++ is)
||| Q (Q1 O (UN QK (QK (UN QK (Fold qs)))) (UN 'CO (Fold is))
~> O (UN 'CO (Fold hs)) (UN QK (Fold rs))
m) = forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1}
       (a :: kk i j) (b :: kk j k2) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
forall (a :: Path (COK kk) h b) (b :: Path (COK kk) b c) r.
(Bicategory (Path (COK kk)), Ob0 (Path (COK kk)) h,
 Ob0 (Path (COK kk)) b, Ob0 (Path (COK kk)) c, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj @fs @hs ((Ob (O fs hs) => Quintet ps rs (fs +++ hs) (gs +++ is))
 -> Quintet ps rs (fs +++ hs) (gs +++ is))
-> (Ob (O fs hs) => Quintet ps rs (fs +++ hs) (gs +++ is))
-> Quintet ps rs (fs +++ hs) (gs +++ is)
forall a b. (a -> b) -> a -> b
$ forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1}
       (a :: kk i j) (b :: kk j k2) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
forall (a :: Path (COK kk) j b) (b :: Path (COK kk) b c) r.
(Bicategory (Path (COK kk)), Ob0 (Path (COK kk)) j,
 Ob0 (Path (COK kk)) b, Ob0 (Path (COK kk)) c, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj @gs @is ((Ob (O gs is) => Quintet ps rs (fs +++ hs) (gs +++ is))
 -> Quintet ps rs (fs +++ hs) (gs +++ is))
-> (Ob (O gs is) => Quintet ps rs (fs +++ hs) (gs +++ is))
-> Quintet ps rs (fs +++ hs) (gs +++ is)
forall a b. (a -> b) -> a -> b
$
    let fs :: Obj (UN 'CO (Fold fs))
fs = forall (a :: kk h b). (CategoryOf (kk h b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold fs))
        gs :: Obj (UN 'CO (Fold gs))
gs = forall (a :: kk j b). (CategoryOf (kk j b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold gs))
        hs :: Obj (UN 'CO (Fold hs))
hs = forall (a :: kk b c). (CategoryOf (kk b c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold hs))
        is :: Obj (UN 'CO (Fold is))
is = forall (a :: kk b c). (CategoryOf (kk b c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold is))
        ps :: Obj (UN QK (Fold ps))
ps = forall (a :: kk h j). (CategoryOf (kk h j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold ps))
        qs :: Obj (UN QK (Fold qs))
qs = forall (a :: kk b b). (CategoryOf (kk b b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs))
        rs :: Obj (UN QK (Fold rs))
rs = forall (a :: kk c c). (CategoryOf (kk c c), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold rs))
    in Sq1
  (QKK kk)
  (COK kk)
  (Fold ps)
  (Fold rs)
  (Fold (fs +++ hs))
  (Fold (gs +++ is))
-> Quintet ps rs (fs +++ hs) (gs +++ is)
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q (Sq1
   (QKK kk)
   (COK kk)
   (Fold ps)
   (Fold rs)
   (Fold (fs +++ hs))
   (Fold (gs +++ is))
 -> Quintet ps rs (fs +++ hs) (gs +++ is))
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold ps)
     (Fold rs)
     (Fold (fs +++ hs))
     (Fold (gs +++ is))
-> Quintet ps rs (fs +++ hs) (gs +++ is)
forall a b. (a -> b) -> a -> b
$ (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
 ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs)))
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold ps)
     (Fold rs)
     (Fold (fs +++ hs))
     (Fold (gs +++ is))
forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k :: k)
       (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i)
       (g :: COK kk j k).
(Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g) =>
(O (UN QK p) (UN 'CO g) ~> O (UN 'CO f) (UN QK q))
-> Sq1 (QKK kk) (COK kk) p q f g
Q1
      ((O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
  ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs)))
 -> Sq1
      (QKK kk)
      (COK kk)
      (Fold ps)
      (Fold rs)
      (Fold (fs +++ hs))
      (Fold (gs +++ is)))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs)))
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold ps)
     (Fold rs)
     (Fold (fs +++ hs))
     (Fold (gs +++ is))
forall a b. (a -> b) -> a -> b
$ (forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k2).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) =>
SPath ps
-> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
   ~> UN 'CO (Fold (ps +++ qs))
forall (qs :: Path (COK kk) b c).
(Bicategory kk, Ob qs, Ob0 kk h, Ob0 kk b, Ob0 kk c) =>
SPath fs
-> O (UN 'CO (Fold fs)) (UN 'CO (Fold qs))
   ~> UN 'CO (Fold (fs +++ qs))
concatFoldCo @hs (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (COK kk) h b). IsPath ps => SPath ps
singPath @fs) (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))
 ~> UN 'CO (Fold (fs +++ hs)))
-> Obj (UN QK (Fold rs))
-> O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs))
   ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (UN QK (Fold rs))
rs)
      (O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs))
 ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs)))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs)))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (UN 'CO (Fold (fs +++ hs))) (UN QK (Fold rs))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'CO (Fold fs))
-> Obj (UN 'CO (Fold hs))
-> Obj (UN QK (Fold rs))
-> O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs)))
   ~> O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj (UN 'CO (Fold fs))
fs Obj (UN 'CO (Fold hs))
hs Obj (UN QK (Fold rs))
rs
      (O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs)))
 ~> O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs)))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs))))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (O (UN 'CO (Fold fs)) (UN 'CO (Fold hs))) (UN QK (Fold rs))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (UN 'CO (Fold fs))
fs Obj (UN 'CO (Fold fs))
-> (O (UN QK (Fold qs)) (UN 'CO (Fold is))
    ~> O (UN 'CO (Fold hs)) (UN QK (Fold rs)))
-> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is)))
   ~> O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs)))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` O (UN QK (Fold qs)) (UN 'CO (Fold is))
~> O (UN 'CO (Fold hs)) (UN QK (Fold rs))
O (UN QK (QK (UN QK (Fold qs)))) (UN 'CO (Fold is))
~> O (UN 'CO (Fold hs)) (UN QK (Fold rs))
m)
      (O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is)))
 ~> O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs))))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is))))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (UN 'CO (Fold fs)) (O (UN 'CO (Fold hs)) (UN QK (Fold rs)))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'CO (Fold fs))
-> Obj (UN QK (Fold qs))
-> Obj (UN 'CO (Fold is))
-> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is))
   ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is)))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj (UN 'CO (Fold fs))
fs Obj (UN QK (Fold qs))
qs Obj (UN 'CO (Fold is))
is
      (O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is))
 ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is))))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is)))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN 'CO (Fold is)))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n (O (UN QK (Fold ps)) (UN 'CO (Fold gs))
 ~> O (UN 'CO (Fold fs)) (UN QK (Fold qs)))
-> Obj (UN 'CO (Fold is))
-> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is))
   ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (UN 'CO (Fold is))
is)
      (O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is))
 ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is)))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is)))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN 'CO (Fold is))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN QK (Fold ps))
-> Obj (UN 'CO (Fold gs))
-> Obj (UN 'CO (Fold is))
-> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN 'CO (Fold is)))
   ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj (UN QK (Fold ps))
ps Obj (UN 'CO (Fold gs))
gs Obj (UN 'CO (Fold is))
is
      (O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN 'CO (Fold is)))
 ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is)))
-> (O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
    ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN 'CO (Fold is))))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN 'CO (Fold is))
forall (b :: kk h c) (c :: kk h c) (a :: kk h c).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (UN QK (Fold ps))
ps Obj (UN QK (Fold ps))
-> (UN 'CO (Fold (gs +++ is))
    ~> O (UN 'CO (Fold gs)) (UN 'CO (Fold is)))
-> O (UN QK (Fold ps)) (UN 'CO (Fold (gs +++ is)))
   ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN 'CO (Fold is)))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1}
       {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k2).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) =>
SPath ps
-> UN 'CO (Fold (ps +++ qs))
   ~> O (UN 'CO (Fold ps)) (UN 'CO (Fold qs))
forall (qs :: Path (COK kk) b c).
(Bicategory kk, Ob qs, Ob0 kk j, Ob0 kk b, Ob0 kk c) =>
SPath gs
-> UN 'CO (Fold (gs +++ qs))
   ~> O (UN 'CO (Fold gs)) (UN 'CO (Fold qs))
splitFoldCo @is (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (COK kk) j b). IsPath ps => SPath ps
singPath @gs))

  (===) :: forall {h} {i} (ps :: Path (QKK kk) h i) qs rs ss fs gs hs. Quintet ps qs fs gs -> Quintet rs ss gs hs -> Quintet (ps +++ rs) (qs +++ ss) fs hs
  Q (Q1 O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n) === :: forall {i :: k} {b :: k} {j :: k} {k :: k} {h :: k} {i :: k}
       (ps :: Path (QKK kk) h i) (qs :: Path (QKK kk) i b)
       (rs :: Path (QKK kk) i j) (ss :: Path (QKK kk) b k)
       (fs :: Path (COK kk) h i) (gs :: Path (COK kk) i b)
       (hs :: Path (COK kk) j k).
Quintet ps qs fs gs
-> Quintet rs ss gs hs -> Quintet (ps +++ rs) (qs +++ ss) fs hs
=== Q (Q1 O (UN QK (Fold rs)) (UN 'CO (Fold hs))
~> O (UN 'CO ('CO (UN 'CO (Fold gs)))) (UN QK (Fold ss))
m) = forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1}
       (a :: kk i j) (b :: kk j k2) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
forall (a :: Path (QKK kk) h i) (b :: Path (QKK kk) i j) r.
(Bicategory (Path (QKK kk)), Ob0 (Path (QKK kk)) h,
 Ob0 (Path (QKK kk)) i, Ob0 (Path (QKK kk)) j, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj @ps @rs ((Ob (O ps rs) => Quintet (ps +++ rs) (qs +++ ss) fs hs)
 -> Quintet (ps +++ rs) (qs +++ ss) fs hs)
-> (Ob (O ps rs) => Quintet (ps +++ rs) (qs +++ ss) fs hs)
-> Quintet (ps +++ rs) (qs +++ ss) fs hs
forall a b. (a -> b) -> a -> b
$ forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1}
       (a :: kk i j) (b :: kk j k2) r.
(Bicategory kk, Ob0 kk i, Ob0 kk j, Ob0 kk k2, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
forall (a :: Path (QKK kk) i b) (b :: Path (QKK kk) b k) r.
(Bicategory (Path (QKK kk)), Ob0 (Path (QKK kk)) i,
 Ob0 (Path (QKK kk)) b, Ob0 (Path (QKK kk)) k, Ob a, Ob b) =>
(Ob (O a b) => r) -> r
appendObj @qs @ss ((Ob (O qs ss) => Quintet (ps +++ rs) (qs +++ ss) fs hs)
 -> Quintet (ps +++ rs) (qs +++ ss) fs hs)
-> (Ob (O qs ss) => Quintet (ps +++ rs) (qs +++ ss) fs hs)
-> Quintet (ps +++ rs) (qs +++ ss) fs hs
forall a b. (a -> b) -> a -> b
$
    let fs :: Obj (UN 'CO (Fold fs))
fs = forall (a :: kk h i). (CategoryOf (kk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold fs))
        gs :: Obj (UN 'CO (Fold gs))
gs = forall (a :: kk i b). (CategoryOf (kk i b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold gs))
        hs :: Obj (UN 'CO (Fold hs))
hs = forall (a :: kk j k). (CategoryOf (kk j k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN CO (Fold hs))
        ps :: Obj (UN QK (Fold ps))
ps = forall (a :: kk h i). (CategoryOf (kk h i), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold ps))
        qs :: Obj (UN QK (Fold qs))
qs = forall (a :: kk i b). (CategoryOf (kk i b), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold qs))
        rs :: Obj (UN QK (Fold rs))
rs = forall (a :: kk i j). (CategoryOf (kk i j), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold rs))
        ss :: Obj (UN QK (Fold ss))
ss = forall (a :: kk b k). (CategoryOf (kk b k), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN QK (Fold ss))
    in Sq1
  (QKK kk)
  (COK kk)
  (Fold (ps +++ rs))
  (Fold (qs +++ ss))
  (Fold fs)
  (Fold hs)
-> Quintet (ps +++ rs) (qs +++ ss) fs hs
forall {k} (kk :: k -> k -> Type) (h :: k) (j :: k)
       (ps :: Path (QKK kk) h j) (i :: k) (k :: k)
       (qs :: Path (QKK kk) i k) (fs :: Path (COK kk) h i)
       (gs :: Path (COK kk) j k).
(IsPath ps, IsPath qs, IsPath fs, IsPath gs) =>
Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (QKK kk) (COK kk) ps qs fs gs
Q (Sq1
   (QKK kk)
   (COK kk)
   (Fold (ps +++ rs))
   (Fold (qs +++ ss))
   (Fold fs)
   (Fold hs)
 -> Quintet (ps +++ rs) (qs +++ ss) fs hs)
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold (ps +++ rs))
     (Fold (qs +++ ss))
     (Fold fs)
     (Fold hs)
-> Quintet (ps +++ rs) (qs +++ ss) fs hs
forall a b. (a -> b) -> a -> b
$ (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
 ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss))))
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold (ps +++ rs))
     (Fold (qs +++ ss))
     (Fold fs)
     (Fold hs)
forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k :: k)
       (p :: QKK kk h j) (q :: QKK kk i k) (f :: COK kk h i)
       (g :: COK kk j k).
(Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob p, Ob q, Ob f, Ob g) =>
(O (UN QK p) (UN 'CO g) ~> O (UN 'CO f) (UN QK q))
-> Sq1 (QKK kk) (COK kk) p q f g
Q1
      ((O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
  ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss))))
 -> Sq1
      (QKK kk)
      (COK kk)
      (Fold (ps +++ rs))
      (Fold (qs +++ ss))
      (Fold fs)
      (Fold hs))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss))))
-> Sq1
     (QKK kk)
     (COK kk)
     (Fold (ps +++ rs))
     (Fold (qs +++ ss))
     (Fold fs)
     (Fold hs)
forall a b. (a -> b) -> a -> b
$ (Obj (UN 'CO (Fold fs))
fs Obj (UN 'CO (Fold fs))
-> (O (UN QK (Fold qs)) (UN QK (Fold ss))
    ~> UN QK (Fold (qs +++ ss)))
-> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss)))
   ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss)))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> O (UN QK (Fold ps)) (UN QK (Fold qs))
   ~> UN QK (Fold (ps +++ qs))
forall (qs :: Path (QKK kk) b k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk b, Ob0 kk k) =>
SPath qs
-> O (UN QK (Fold qs)) (UN QK (Fold qs))
   ~> UN QK (Fold (qs +++ qs))
concatFoldQ @ss (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (QKK kk) i b). IsPath ps => SPath ps
singPath @qs))
      (O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss)))
 ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss))))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss))))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (UN 'CO (Fold fs)) (UN QK (Fold (qs +++ ss)))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'CO (Fold fs))
-> Obj (UN QK (Fold qs))
-> Obj (UN QK (Fold ss))
-> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss))
   ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss)))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj (UN 'CO (Fold fs))
fs Obj (UN QK (Fold qs))
qs Obj (UN QK (Fold ss))
ss
      (O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss))
 ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss))))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss)))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (UN 'CO (Fold fs)) (O (UN QK (Fold qs)) (UN QK (Fold ss)))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (O (UN QK (Fold ps)) (UN 'CO (Fold gs))
~> O (UN 'CO (Fold fs)) (UN QK (Fold qs))
n (O (UN QK (Fold ps)) (UN 'CO (Fold gs))
 ~> O (UN 'CO (Fold fs)) (UN QK (Fold qs)))
-> Obj (UN QK (Fold ss))
-> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss))
   ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (UN QK (Fold ss))
ss)
      (O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss))
 ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss)))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss)))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (O (UN 'CO (Fold fs)) (UN QK (Fold qs))) (UN QK (Fold ss))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN QK (Fold ps))
-> Obj (UN 'CO (Fold gs))
-> Obj (UN QK (Fold ss))
-> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss)))
   ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj (UN QK (Fold ps))
ps Obj (UN 'CO (Fold gs))
gs Obj (UN QK (Fold ss))
ss
      (O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss)))
 ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss)))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss))))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (O (UN QK (Fold ps)) (UN 'CO (Fold gs))) (UN QK (Fold ss))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (UN QK (Fold ps))
ps Obj (UN QK (Fold ps))
-> (O (UN QK (Fold rs)) (UN 'CO (Fold hs))
    ~> O (UN 'CO (Fold gs)) (UN QK (Fold ss)))
-> O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs)))
   ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss)))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` O (UN QK (Fold rs)) (UN 'CO (Fold hs))
~> O (UN 'CO (Fold gs)) (UN QK (Fold ss))
O (UN QK (Fold rs)) (UN 'CO (Fold hs))
~> O (UN 'CO ('CO (UN 'CO (Fold gs)))) (UN QK (Fold ss))
m)
      (O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs)))
 ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss))))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs))))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (UN QK (Fold ps)) (O (UN 'CO (Fold gs)) (UN QK (Fold ss)))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN QK (Fold ps))
-> Obj (UN QK (Fold rs))
-> Obj (UN 'CO (Fold hs))
-> O (O (UN QK (Fold ps)) (UN QK (Fold rs))) (UN 'CO (Fold hs))
   ~> O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs)))
forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: kk i j2)
       (b :: kk j2 j1) (c :: kk j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
forall k (kk :: CAT k) {j1 :: k} {k1 :: k} (i :: k) (j2 :: k)
       (a :: kk i j2) (b :: kk j2 j1) (c :: kk j1 k1).
Bicategory kk =>
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj (UN QK (Fold ps))
ps Obj (UN QK (Fold rs))
rs Obj (UN 'CO (Fold hs))
hs
      (O (O (UN QK (Fold ps)) (UN QK (Fold rs))) (UN 'CO (Fold hs))
 ~> O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs))))
-> (O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
    ~> O (O (UN QK (Fold ps)) (UN QK (Fold rs))) (UN 'CO (Fold hs)))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (UN QK (Fold ps)) (O (UN QK (Fold rs)) (UN 'CO (Fold hs)))
forall (b :: kk h k) (c :: kk h k) (a :: kk h k).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k).
(Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
SPath ps
-> UN QK (Fold (ps +++ qs))
   ~> O (UN QK (Fold ps)) (UN QK (Fold qs))
forall (qs :: Path (QKK kk) i j).
(Bicategory kk, Ob qs, Ob0 kk h, Ob0 kk i, Ob0 kk j) =>
SPath ps
-> UN QK (Fold (ps +++ qs))
   ~> O (UN QK (Fold ps)) (UN QK (Fold qs))
splitFoldQ @rs (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path (QKK kk) h i). IsPath ps => SPath ps
singPath @ps) (UN QK (Fold (ps +++ rs)) ~> O (UN QK (Fold ps)) (UN QK (Fold rs)))
-> Obj (UN 'CO (Fold hs))
-> O (UN QK (Fold (ps +++ rs))) (UN 'CO (Fold hs))
   ~> O (O (UN QK (Fold ps)) (UN QK (Fold rs))) (UN 'CO (Fold hs))
forall {k1 :: k} (i :: k) (j :: k) (a :: kk i j) (b :: kk i j)
       (c :: kk j k1) (d :: kk j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall k (kk :: CAT k) {k1 :: k} (i :: k) (j :: k) (a :: kk i j)
       (b :: kk i j) (c :: kk j k1) (d :: kk j k1).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Obj (UN 'CO (Fold hs))
hs)

-- Quintet is not an Equipment