{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares where

import Data.Functor.Compose (Compose (..))
import Prelude (Either (..), Traversable, either, ($))

import Proarrow.Category.Bicategory (Adjunction (..), Bicategory (..), obj1, (||))
import Proarrow.Category.Bicategory.Prof (PROFK (..), Prof (..))
import Proarrow.Category.Bicategory.Strictified
  ( Fold
  , Path (..)
  , Strictified (..)
  , combineAll
  , splitAll
  , withIsObTagFold
  , type (+++)
  )
import Proarrow.Category.Bicategory.Sub (SUBCAT (..), Sub (Sub))
import Proarrow.Category.Equipment (Equipment, IsCotight, IsTight, Tight, TightPair)
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), (:~>), (\\), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Star (Star, pattern Star)

-- | The kind of a square @'(q, f) '(p, g)@.
--
-- > h--f--i
-- > |  v  |
-- > p--@--q
-- > |  v  |
-- > j--g--k
type SQ' (kk :: CAT c) h i j k = (kk k i, SUBCAT Tight kk j k) +-> (kk j h, SUBCAT Tight kk h i)

type SQ (kk :: CAT c) = forall {h} {i} {j} {k}. SQ' kk h i j k

type Sq' :: forall {c} {kk :: CAT c}. SQ kk
data Sq' pf qg where
  Sq
    :: forall {kk} {h} {i} {j} {k} (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i) (g :: Path kk j k)
     . (Ob p, Ob q, IsTight f, IsTight g)
    => f `O` p ~> q `O` g
    -> Sq' '(p, SUB f) '(q, SUB g)

type Sq p q f g = Sq' '(p, SUB f) '(q, SUB g)

instance (Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) => Profunctor (Sq' :: SQ' kk h i j k) where
  dimap :: forall (c :: (kk j h, SUBCAT Tight kk h i))
       (a :: (kk j h, SUBCAT Tight kk h i))
       (b :: (kk k i, SUBCAT Tight kk j k))
       (d :: (kk k i, SUBCAT Tight kk j k)).
(c ~> a) -> (b ~> d) -> Sq' a b -> Sq' c d
dimap (a1 ~> b1
p :**: Sub a1 ~> b1
f) (a1 ~> b1
q :**: Sub a1 ~> b1
g) (Sq O f p ~> O q g
sq) = (O a1 a1 ~> O b1 b1) -> Sq' '(a1, SUB a1) '(b1, SUB b1)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((a1 ~> b1
a1 ~> b1
q (a1 ~> b1) -> (a1 ~> b1) -> O a1 a1 ~> O b1 b1
forall {i :: c} (j :: c) (k :: c) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a1 ~> b1
a1 ~> b1
g) Strictified (a1 +++ a1) (b1 +++ b1)
-> Strictified (a1 +++ a1) (a1 +++ a1)
-> Strictified (a1 +++ a1) (b1 +++ b1)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk j i) (c :: Path kk j i) (a :: Path kk j i).
Strictified b c -> Strictified a b -> Strictified a c
. O f p ~> O q g
Strictified (b1 +++ b1) (a1 +++ a1)
sq Strictified (b1 +++ b1) (a1 +++ a1)
-> Strictified (a1 +++ a1) (b1 +++ b1)
-> Strictified (a1 +++ a1) (a1 +++ a1)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk j i) (c :: Path kk j i) (a :: Path kk j i).
Strictified b c -> Strictified a b -> Strictified a c
. (a1 ~> b1
a1 ~> b1
f (a1 ~> b1) -> (a1 ~> b1) -> O a1 a1 ~> O b1 b1
forall {i :: c} (j :: c) (k :: c) (a :: Path kk j k)
       (b :: Path kk j k) (c :: Path kk i j) (d :: Path kk i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` a1 ~> b1
a1 ~> b1
p)) ((Ob a1, Ob b1) => Sq' c d) -> (a1 ~> b1) -> Sq' c d
forall (a :: kk j h) (b :: kk j h) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
p ((Ob a1, Ob b1) => Sq' c d) -> Strictified a1 b1 -> Sq' c d
forall (a :: kk h i) (b :: kk h i) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
Strictified a1 b1
f ((Ob a1, Ob b1) => Sq' c d) -> (a1 ~> b1) -> Sq' c d
forall (a :: kk k i) (b :: kk k i) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
q ((Ob a1, Ob b1) => Sq' c d) -> Strictified a1 b1 -> Sq' c d
forall (a :: kk j k) (b :: kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
Strictified a1 b1
g
  (Ob a, Ob b) => r
r \\ :: forall (a :: (kk j h, SUBCAT Tight kk h i))
       (b :: (kk k i, SUBCAT Tight kk j k)) r.
((Ob a, Ob b) => r) -> Sq' a b -> r
\\ Sq O f p ~> O q g
sq = r
(Ob a, Ob b) => r
(Ob (p +++ f), Ob (g +++ q)) => r
r ((Ob (p +++ f), Ob (g +++ q)) => r)
-> Strictified (p +++ f) (g +++ q) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path kk j i) (b :: Path kk j i) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ O f p ~> O q g
Strictified (p +++ f) (g +++ q)
sq

infixl 6 |||
infixl 5 ===

-- | The empty square for an object.
--
-- > K-----K
-- > |     |
-- > |     |
-- > |     |
-- > K-----K
object :: (Equipment kk, Ob0 kk k) => Sq (Nil :: Path kk k k) (Nil :: Path kk k k) Nil Nil
object :: forall {k} (kk :: CAT k) (k :: k).
(Equipment kk, Ob0 kk k) =>
Sq Nil Nil Nil Nil
object = (O Nil Nil ~> O Nil Nil) -> Sq' '(Nil, SUB Nil) '(Nil, SUB Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O Nil Nil ~> O Nil Nil
Strictified Nil Nil
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk k k). Ob a => Strictified a a
id

-- | Make a square from a horizontal proarrow
--
-- > K-----K
-- > |     |
-- > p--@--q
-- > |     |
-- > J-----J
hArr
  :: forall {kk} {j} {k} (p :: kk j k) q
   . (Equipment kk)
  => p ~> q
  -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (p :: kk j k)
       (q :: kk j k).
Equipment kk =>
(p ~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr p ~> q
pq = (O Nil (p ::: Nil) ~> O (q ::: Nil) Nil)
-> Sq' '(p ::: Nil, SUB Nil) '(q ::: Nil, SUB Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold (p ::: Nil) ~> Fold (q ::: Nil))
-> Strictified (p ::: Nil) (q ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St p ~> q
Fold (p ::: Nil) ~> Fold (q ::: Nil)
pq) ((Ob0 kk j, Ob0 kk k, Ob p, Ob q) =>
 Sq' '(p ::: Nil, SUB Nil) '(q ::: Nil, SUB Nil))
-> (p ~> q) -> Sq' '(p ::: Nil, SUB Nil) '(q ::: Nil, SUB Nil)
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ p ~> q
pq

-- | A horizontal identity square.
--
-- > J-----J
-- > |     |
-- > p-----p
-- > |     |
-- > K-----K
hId
  :: forall {kk} {j} {k} (p :: kk j k)
   . (Equipment kk, Ob p)
  => Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (p :: kk j k).
(Equipment kk, Ob p) =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p ((p ~> p) -> Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (p :: kk j k)
       (q :: kk j k).
Equipment kk =>
(p ~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr p ~> p
forall (a :: kk j k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | Make a square from a vertical arrow
--
-- > J--f--K
-- > |  v  |
-- > |  @  |
-- > |  v  |
-- > J--g--K
vArr
  :: forall {kk} {j} {k} (f :: kk j k) g
   . (Equipment kk, IsTight f, IsTight g)
  => f ~> g
  -> Sq Nil Nil (f ::: Nil) (g ::: Nil)
vArr :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (g :: kk j k).
(Equipment kk, IsTight f, IsTight g) =>
(f ~> g) -> Sq Nil Nil (f ::: Nil) (g ::: Nil)
vArr f ~> g
fg = (O (f ::: Nil) Nil ~> O Nil (g ::: Nil))
-> Sq' '(Nil, SUB (f ::: Nil)) '(Nil, SUB (g ::: Nil))
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold (f ::: Nil) ~> Fold (g ::: Nil))
-> Strictified (f ::: Nil) (g ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St f ~> g
Fold (f ::: Nil) ~> Fold (g ::: Nil)
fg) ((Ob0 kk j, Ob0 kk k, Ob f, Ob g) =>
 Sq' '(Nil, SUB (f ::: Nil)) '(Nil, SUB (g ::: Nil)))
-> (f ~> g) -> Sq' '(Nil, SUB (f ::: Nil)) '(Nil, SUB (g ::: Nil))
forall (i :: k) (j :: k) (ps :: kk i j) (qs :: kk i j) r.
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ f ~> g
fg

-- | A vertical identity square.
--
-- > J--f--K
-- > |  v  |
-- > |  |  |
-- > |  v  |
-- > J--f--K
vId
  :: forall {kk} {j} {k} (f :: kk j k)
   . (Equipment kk, IsTight f)
  => Sq Nil Nil (f ::: Nil) (f ::: Nil)
vId :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k).
(Equipment kk, IsTight f) =>
Sq Nil Nil (f ::: Nil) (f ::: Nil)
vId = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f ((O (f ::: Nil) Nil ~> O Nil (f ::: Nil))
-> Sq Nil Nil (f ::: Nil) (f ::: Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O (f ::: Nil) Nil ~> O Nil (f ::: Nil)
Strictified (f ::: Nil) (f ::: Nil)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk j k). Ob a => Strictified a a
id)

-- | 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 {kk} {h} {l} {m} (ps :: Path kk m l) qs rs (ds :: Path kk l h) es fs gs
   . (Equipment kk)
  => Sq ps qs ds es
  -> Sq qs rs fs gs
  -> Sq ps rs (ds +++ fs) (es +++ gs)
Sq O f p ~> O q g
l ||| :: forall {k} {b :: k} {c :: k} {c :: k} {kk :: CAT k} {h :: k}
       {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h)
       (rs :: Path kk c c) (ds :: Path kk l h) (es :: Path kk m b)
       (fs :: Path kk h c) (gs :: Path kk b c).
Equipment kk =>
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq O f p ~> O q g
r =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @(SUBCAT Tight (Path kk)) @(SUB fs) @(SUB ds) ((Ob (O (SUB fs) (SUB ds)) => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Ob (O (SUB fs) (SUB ds)) => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
    forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @(SUBCAT Tight (Path kk)) @(SUB gs) @(SUB es) ((Ob (O (SUB gs) (SUB es)) => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Ob (O (SUB gs) (SUB es)) => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
      (O (ds +++ fs) ps ~> O rs (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq
        (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @rs @gs @es Strictified (es +++ (gs +++ rs)) ((es +++ gs) +++ rs)
-> Strictified (ps +++ (ds +++ fs)) (es +++ (gs +++ rs))
-> Strictified (ps +++ (ds +++ fs)) ((es +++ gs) +++ rs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk m c) (c :: Path kk m c) (a :: Path kk m c).
Strictified b c -> Strictified a b -> Strictified a c
. ((qs +++ fs) ~> (gs +++ rs)
O f p ~> O q g
r ((qs +++ fs) ~> (gs +++ rs))
-> (es ~> es) -> O (qs +++ fs) es ~> O (gs +++ rs) es
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
forall (a :: Path kk m b). (Bicategory (Path kk), Ob a) => Obj a
obj1 @es) Strictified (es +++ (qs +++ fs)) (es +++ (gs +++ rs))
-> Strictified (ps +++ (ds +++ fs)) (es +++ (qs +++ fs))
-> Strictified (ps +++ (ds +++ fs)) (es +++ (gs +++ rs))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk m c) (c :: Path kk m c) (a :: Path kk m c).
Strictified b c -> Strictified a b -> Strictified a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @fs @qs @es Strictified (es +++ (qs +++ fs)) (es +++ (qs +++ fs))
-> Strictified (ps +++ (ds +++ fs)) (es +++ (qs +++ fs))
-> Strictified (ps +++ (ds +++ fs)) (es +++ (qs +++ fs))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk m c) (c :: Path kk m c) (a :: Path kk m c).
Strictified b c -> Strictified a b -> Strictified a c
. (forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
forall (a :: Path kk h c). (Bicategory (Path kk), Ob a) => Obj a
obj1 @fs Obj fs
-> ((ps +++ ds) ~> (es +++ qs))
-> O fs (ps +++ ds) ~> O fs (es +++ qs)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| (ps +++ ds) ~> (es +++ qs)
O f p ~> O q g
l) Strictified ((ps +++ ds) +++ fs) (es +++ (qs +++ fs))
-> Strictified (ps +++ (ds +++ fs)) ((ps +++ ds) +++ fs)
-> Strictified (ps +++ (ds +++ fs)) (es +++ (qs +++ fs))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk m c) (c :: Path kk m c) (a :: Path kk m c).
Strictified b c -> Strictified a b -> Strictified a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @fs @ds @ps)

-- | 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 {kk} {h} {i} {j} {l} (ps :: Path kk l j) qs rs ss (es :: Path kk h i) fs gs
   . (Equipment kk)
  => Sq rs ss es fs
  -> Sq ps qs fs gs
  -> Sq (ps +++ rs) (qs +++ ss) es gs
Sq O f p ~> O q g
l === :: forall {k} {k :: k} {b :: k} {kk :: CAT k} {h :: k} {i :: k}
       {j :: k} {l :: k} (ps :: Path kk l j) (qs :: Path kk k b)
       (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i)
       (fs :: Path kk j b) (gs :: Path kk l k).
Equipment kk =>
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq O f p ~> O q g
r =
  forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @_ @rs @ps ((Ob (O rs ps) => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Ob (O rs ps) => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
    forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: CAT k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @_ @ss @qs ((Ob (O ss qs) => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Ob (O ss qs) => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
      (O es (ps +++ rs) ~> O (qs +++ ss) gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq
        (forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @_ @ss @qs @gs Strictified ((gs +++ qs) +++ ss) (gs +++ (qs +++ ss))
-> Strictified ((ps +++ rs) +++ es) ((gs +++ qs) +++ ss)
-> Strictified ((ps +++ rs) +++ es) (gs +++ (qs +++ ss))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk l i) (c :: Path kk l i) (a :: Path kk l i).
Strictified b c -> Strictified a b -> Strictified a c
. (forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
forall (a :: Path kk b i). (Bicategory (Path kk), Ob a) => Obj a
obj1 @ss Obj ss
-> ((ps +++ fs) ~> (gs +++ qs))
-> O ss (ps +++ fs) ~> O ss (gs +++ qs)
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| (ps +++ fs) ~> (gs +++ qs)
O f p ~> O q g
r) Strictified ((ps +++ fs) +++ ss) ((gs +++ qs) +++ ss)
-> Strictified ((ps +++ rs) +++ es) ((ps +++ fs) +++ ss)
-> Strictified ((ps +++ rs) +++ es) ((gs +++ qs) +++ ss)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk l i) (c :: Path kk l i) (a :: Path kk l i).
Strictified b c -> Strictified a b -> Strictified a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @ss @fs @ps Strictified (ps +++ (fs +++ ss)) ((ps +++ fs) +++ ss)
-> Strictified ((ps +++ rs) +++ es) (ps +++ (fs +++ ss))
-> Strictified ((ps +++ rs) +++ es) ((ps +++ fs) +++ ss)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk l i) (c :: Path kk l i) (a :: Path kk l i).
Strictified b c -> Strictified a b -> Strictified a c
. ((rs +++ es) ~> (fs +++ ss)
O f p ~> O q g
l ((rs +++ es) ~> (fs +++ ss))
-> (ps ~> ps) -> O (rs +++ es) ps ~> O (fs +++ ss) ps
forall {s} {i1 :: s} (kk :: CAT s) (i2 :: s) (j :: s)
       (a :: kk i2 j) (b :: kk i2 j) (c :: kk i1 i2) (d :: kk i1 i2).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
|| forall {s} {kk :: CAT s} {j :: s} {k :: s} (a :: kk j k).
(Bicategory kk, Ob a) =>
Obj a
forall (a :: Path kk l j). (Bicategory (Path kk), Ob a) => Obj a
obj1 @ps) Strictified (ps +++ (rs +++ es)) (ps +++ (fs +++ ss))
-> Strictified ((ps +++ rs) +++ es) (ps +++ (rs +++ es))
-> Strictified ((ps +++ rs) +++ es) (ps +++ (fs +++ ss))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: Path kk l i) (c :: Path kk l i) (a :: Path kk l i).
Strictified b c -> Strictified a b -> Strictified a c
. forall {s} (kk :: CAT s) {h :: s} {i :: s} {j :: s} {k :: s}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
forall (kk :: CAT k) {h :: k} {i :: k} {j :: k} {k :: k}
       (a :: kk j k) (b :: kk i j) (c :: kk h i).
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b,
 Ob c) =>
O (O a b) c ~> O a (O b c)
associator @_ @es @rs @ps)

-- | Bend a vertical arrow in the companion direction.
--
-- > J--f--K
-- > |  v  |
-- > |  \->f
-- > |     |
-- > J-----J
toRight
  :: forall {kk} {j} {k} (f :: kk j k)
   . (Equipment kk, IsTight f)
  => Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k).
(Equipment kk, IsTight f) =>
Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq Nil (f ::: Nil) (f ::: Nil) Nil)
 -> Sq Nil (f ::: Nil) (f ::: Nil) Nil)
-> ((Ob0 kk j, Ob0 kk k) => Sq Nil (f ::: Nil) (f ::: Nil) Nil)
-> Sq Nil (f ::: Nil) (f ::: Nil) Nil
forall a b. (a -> b) -> a -> b
$ (O (f ::: Nil) Nil ~> O (f ::: Nil) Nil)
-> Sq Nil (f ::: Nil) (f ::: Nil) Nil
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O (f ::: Nil) Nil ~> O (f ::: Nil) Nil
Strictified (f ::: Nil) (f ::: Nil)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk j k). Ob a => Strictified a a
id

-- | Bend a vertical arrow in the conjoint direction.
--
-- > J--f--K
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > K-----K
toLeft
  :: forall {kk} {j} {k} (f :: kk j k) f'
   . (Equipment kk, TightPair f f')
  => Sq (f' ::: Nil) Nil (f ::: Nil) Nil
toLeft :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (f' :: kk k j).
(Equipment kk, TightPair f f') =>
Sq (f' ::: Nil) Nil (f ::: Nil) Nil
toLeft = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq (f' ::: Nil) Nil (f ::: Nil) Nil)
 -> Sq (f' ::: Nil) Nil (f ::: Nil) Nil)
-> ((Ob0 kk j, Ob0 kk k) => Sq (f' ::: Nil) Nil (f ::: Nil) Nil)
-> Sq (f' ::: Nil) Nil (f ::: Nil) Nil
forall a b. (a -> b) -> a -> b
$ (O (f ::: Nil) (f' ::: Nil) ~> O Nil Nil)
-> Sq (f' ::: Nil) Nil (f ::: Nil) Nil
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold (f' ::: (f ::: Nil)) ~> Fold Nil)
-> Strictified (f' ::: (f ::: Nil)) Nil
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk j k) (r :: kk k j). Adjunction l r => O l r ~> I
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
counit @f @f'))

-- | Bend a companion proarrow back to a vertical arrow.
--
-- > K-----K
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > J--f--K
fromLeft
  :: forall {kk} {j} {k} (f :: kk j k)
   . (Equipment kk, IsTight f)
  => Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k).
(Equipment kk, IsTight f) =>
Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq (f ::: Nil) Nil Nil (f ::: Nil))
 -> Sq (f ::: Nil) Nil Nil (f ::: Nil))
-> ((Ob0 kk j, Ob0 kk k) => Sq (f ::: Nil) Nil Nil (f ::: Nil))
-> Sq (f ::: Nil) Nil Nil (f ::: Nil)
forall a b. (a -> b) -> a -> b
$ (O Nil (f ::: Nil) ~> O Nil (f ::: Nil))
-> Sq (f ::: Nil) Nil Nil (f ::: Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O Nil (f ::: Nil) ~> O Nil (f ::: Nil)
Strictified (f ::: Nil) (f ::: Nil)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Path kk j k). Ob a => Strictified a a
id

-- | Bend a conjoint proarrow back to a vertical arrow.
--
-- > J-----J
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > J--f--K
fromRight
  :: forall {kk} {j} {k} (f :: kk j k) f'
   . (Equipment kk, TightPair f f')
  => Sq Nil (f' ::: Nil) Nil (f ::: Nil)
fromRight :: forall {k} {kk :: k -> k -> Type} {j :: k} {k :: k} (f :: kk j k)
       (f' :: kk k j).
(Equipment kk, TightPair f f') =>
Sq Nil (f' ::: Nil) Nil (f ::: Nil)
fromRight = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @f (((Ob0 kk j, Ob0 kk k) => Sq Nil (f' ::: Nil) Nil (f ::: Nil))
 -> Sq Nil (f' ::: Nil) Nil (f ::: Nil))
-> ((Ob0 kk j, Ob0 kk k) => Sq Nil (f' ::: Nil) Nil (f ::: Nil))
-> Sq Nil (f' ::: Nil) Nil (f ::: Nil)
forall a b. (a -> b) -> a -> b
$ (O Nil Nil ~> O (f' ::: Nil) (f ::: Nil))
-> Sq Nil (f' ::: Nil) Nil (f ::: Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold Nil ~> Fold (f ::: (f' ::: Nil)))
-> Strictified Nil (f ::: (f' ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (l :: kk j k) (r :: kk k j). Adjunction l r => I ~> O r l
forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
unit @f @f'))

-- > K--I--K
-- > |  v  |
-- > |  @  |
-- > |     |
-- > K-----K
vUnitor
  :: forall kk k
   . (Equipment kk, Ob0 kk k)
  => Sq Nil Nil ((I :: kk k k) ::: Nil) Nil
vUnitor :: forall {k} (kk :: CAT k) (k :: k).
(Equipment kk, Ob0 kk k) =>
Sq Nil Nil (I ::: Nil) Nil
vUnitor = Sq' '(Nil, SUB (I ::: Nil)) '(Nil, SUB Nil)
Sq Nil Nil (Fold Nil ::: Nil) Nil
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll

-- > K-----K
-- > |     |
-- > |  @  |
-- > |  v  |
-- > K--I--K
vUnitorInv
  :: forall kk k
   . (Equipment kk, Ob0 kk k)
  => Sq Nil Nil Nil ((I :: kk k k) ::: Nil)
vUnitorInv :: forall {k} (kk :: CAT k) (k :: k).
(Equipment kk, Ob0 kk k) =>
Sq Nil Nil Nil (I ::: Nil)
vUnitorInv = Sq' '(Nil, SUB Nil) '(Nil, SUB (I ::: Nil))
Sq Nil Nil Nil (Fold Nil ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll

-- > I-f-g-K
-- > | v v |
-- > | \@/ |
-- > |  v  |
-- > I-gof-K
vCombine
  :: forall {kk} {i} {j} {k} (p :: kk i j) (q :: kk j k)
   . (Equipment kk, IsTight p, IsTight q)
  => Sq Nil Nil (p ::: q ::: Nil) (q `O` p ::: Nil)
vCombine :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (q :: kk j k).
(Equipment kk, IsTight p, IsTight q) =>
Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil)
vCombine = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p (((Ob0 kk i, Ob0 kk j) =>
  Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil))
 -> Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil))
-> ((Ob0 kk i, Ob0 kk j) =>
    Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil))
-> Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil)
forall a b. (a -> b) -> a -> b
$ forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @q Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil)
Sq Nil Nil (p ::: (q ::: Nil)) (Fold (p ::: (q ::: Nil)) ::: Nil)
(Ob0 kk j, Ob0 kk k) =>
Sq Nil Nil (p ::: (q ::: Nil)) (O q p ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll

-- > I-gof-K
-- > |  v  |
-- > | /@\ |
-- > | v v |
-- > I-f-g-K
vSplit
  :: forall {kk} {i} {j} {k} (p :: kk i j) (q :: kk j k)
   . (Equipment kk, IsTight p, IsTight q)
  => Sq Nil Nil (q `O` p ::: Nil) (p ::: q ::: Nil)
vSplit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} {k :: k}
       (p :: kk i j) (q :: kk j k).
(Equipment kk, IsTight p, IsTight q) =>
Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil))
vSplit = forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @p (((Ob0 kk i, Ob0 kk j) =>
  Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil)))
 -> Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil)))
-> ((Ob0 kk i, Ob0 kk j) =>
    Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil)))
-> Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil))
forall a b. (a -> b) -> a -> b
$ forall {s} (kk :: CAT s) {j :: s} {k :: s} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
forall (kk :: CAT k) {j :: k} {k :: k} (a :: kk j k) r.
(Bicategory kk, Ob a) =>
((Ob0 kk j, Ob0 kk k) => r) -> r
withOb0s @kk @q Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil))
Sq Nil Nil (Fold (p ::: (q ::: Nil)) ::: Nil) (p ::: (q ::: Nil))
(Ob0 kk j, Ob0 kk k) =>
Sq Nil Nil (O q p ::: Nil) (p ::: (q ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll

-- | Combine a whole bunch of vertical arrows into one composed arrow.

-- > J-p..-K
-- > | vvv |
-- > | \@/ |
-- > |  v  |
-- > J--f--K
vCombineAll
  :: forall {kk} {j} {k} (ps :: Path kk j k)
   . (Equipment kk, IsTight ps)
  => Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll = let n :: ps ~> (Fold ps ::: Nil)
n = forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
as ~> (Fold as ::: Nil)
forall (as :: Path kk j k).
(Bicategory kk, Ob as) =>
as ~> (Fold as ::: Nil)
combineAll @ps in forall tag (ps :: Path kk j k) r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} tag
       (ps :: Path kk j k2) r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
withIsObTagFold @Tight @ps ((O ps Nil ~> O Nil (Fold ps ::: Nil))
-> Sq Nil Nil ps (Fold ps ::: Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ps ~> (Fold ps ::: Nil)
O ps Nil ~> O Nil (Fold ps ::: Nil)
n ((Ob ps, Ob (Fold ps ::: Nil)) => Sq Nil Nil ps (Fold ps ::: Nil))
-> Strictified ps (Fold ps ::: Nil)
-> Sq Nil Nil ps (Fold ps ::: Nil)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path kk j k) (b :: Path kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ ps ~> (Fold ps ::: Nil)
Strictified ps (Fold ps ::: Nil)
n)

-- | Split one composed arrow into a whole bunch of vertical arrows.
--
-- > J--f--K
-- > |  v  |
-- > | /@\ |
-- > | vvv |
-- > J-p..-K
vSplitAll
  :: forall {kk} {j} {k} (ps :: Path kk j k)
   . (Equipment kk, IsTight ps)
  => Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, IsTight ps) =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll = let n :: (Fold ps ::: Nil) ~> ps
n = forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
(Fold as ::: Nil) ~> as
forall (as :: Path kk j k).
(Bicategory kk, Ob as) =>
(Fold as ::: Nil) ~> as
splitAll @ps in forall tag (ps :: Path kk j k) r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} tag
       (ps :: Path kk j k2) r.
(Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps,
 Ob ps) =>
((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r
withIsObTagFold @Tight @ps ((O (Fold ps ::: Nil) Nil ~> O Nil ps)
-> Sq Nil Nil (Fold ps ::: Nil) ps
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O (Fold ps ::: Nil) Nil ~> O Nil ps
(Fold ps ::: Nil) ~> ps
n ((Ob (Fold ps ::: Nil), Ob ps) => Sq Nil Nil (Fold ps ::: Nil) ps)
-> Strictified (Fold ps ::: Nil) ps
-> Sq Nil Nil (Fold ps ::: Nil) ps
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path kk j k) (b :: Path kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ (Fold ps ::: Nil) ~> ps
Strictified (Fold ps ::: Nil) ps
n)

-- | Combine a whole bunch of horizontal proarrows into one composed proarrow.
--
-- > K-----K
-- > p--\  |
-- > :--@--F
-- > :--/  |
-- > J-----J
hCombineAll
  :: forall {kk} {j} {k} (ps :: Path kk j k)
   . (Equipment kk, Ob ps)
  => Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, Ob ps) =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll = let n :: ps ~> (Fold ps ::: Nil)
n = forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
as ~> (Fold as ::: Nil)
forall (as :: Path kk j k).
(Bicategory kk, Ob as) =>
as ~> (Fold as ::: Nil)
combineAll @ps in (O Nil ps ~> O (Fold ps ::: Nil) Nil)
-> Sq ps (Fold ps ::: Nil) Nil Nil
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ps ~> (Fold ps ::: Nil)
O Nil ps ~> O (Fold ps ::: Nil) Nil
n ((Ob ps, Ob (Fold ps ::: Nil)) => Sq ps (Fold ps ::: Nil) Nil Nil)
-> Strictified ps (Fold ps ::: Nil)
-> Sq ps (Fold ps ::: Nil) Nil Nil
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path kk j k) (b :: Path kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ ps ~> (Fold ps ::: Nil)
Strictified ps (Fold ps ::: Nil)
n

-- | Split one composed proarrow into a whole bunch of horizontal proarrows.
--
-- > K-----K
-- > |  /--p
-- > F--@--:
-- > |  \--:
-- > J-----J
hSplitAll
  :: forall {kk} {j} {k} (ps :: Path kk j k)
   . (Equipment kk, Ob ps)
  => Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll :: forall {k} {kk :: CAT k} {j :: k} {k :: k} (ps :: Path kk j k).
(Equipment kk, Ob ps) =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll = let n :: (Fold ps ::: Nil) ~> ps
n = forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
(Bicategory kk, Ob as) =>
(Fold as ::: Nil) ~> as
forall (as :: Path kk j k).
(Bicategory kk, Ob as) =>
(Fold as ::: Nil) ~> as
splitAll @ps in (O Nil (Fold ps ::: Nil) ~> O ps Nil)
-> Sq (Fold ps ::: Nil) ps Nil Nil
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq O Nil (Fold ps ::: Nil) ~> O ps Nil
(Fold ps ::: Nil) ~> ps
n ((Ob (Fold ps ::: Nil), Ob ps) => Sq (Fold ps ::: Nil) ps Nil Nil)
-> Strictified (Fold ps ::: Nil) ps
-> Sq (Fold ps ::: Nil) ps Nil Nil
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path kk j k) (b :: Path kk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ (Fold ps ::: Nil) ~> ps
Strictified (Fold ps ::: Nil) ps
n

-- | Optics in proarrow equipments.
--
-- > J-------J
-- > s>--@-->a
-- > |   @   |
-- > t<--@--<b
-- > K-------K
type Optic (a :: kk z j) (b :: kk k z) (s :: kk x j) (t :: kk k x) =
  (IsTight a, IsCotight b, IsTight s, IsCotight t) => Sq (t ::: s ::: Nil) (b ::: a ::: Nil) Nil Nil

-- > J-------J
-- > s>-\ /->a
-- > |   @   |
-- > |   v   |
-- > X---m---Z

-- > X---m---Z
-- > |   v   |
-- > |   @   |
-- > t<-/ \-<b
-- > K-------K

-- > J-------J     J-------J
-- > a>--@   |     s>--@   |
-- > |   @---p ==> |   @---p
-- > b<--@   |     t<--@   |
-- > K-------K     K-------K

-- > J-------J     J-------J
-- > a>----->a     s>--@-->a
-- > |       | ==> |   @   |
-- > b<-----<b     t<--@--<b
-- > K-------K     K-------K

-- > J-------J     J-------J
-- > |   @-->a     |   @-->a
-- > |   @   |     |   @-->m
-- > p---@   | ==> p---@   |
-- > |   @   |     |   @--<m
-- > |   @--<b     |   @--<b
-- > K-------K     K-------K

type ProfOptic a b s t = Optic (PK a) (PK b) (PK s) (PK t)
mkProfOptic :: s :.: t :~> a :.: b -> ProfOptic a b s t
mkProfOptic :: forall {x} {j} {k} {z} (s :: x +-> j) (t :: k +-> x) (a :: z +-> j)
       (b :: k +-> z).
((s :.: t) :~> (a :.: b)) -> ProfOptic a b s t
mkProfOptic (s :.: t) :~> (a :.: b)
n = (O Nil (PK t ::: (PK s ::: Nil))
 ~> O (PK b ::: (PK a ::: Nil)) Nil)
-> Sq'
     '(PK t ::: (PK s ::: Nil), SUB Nil)
     '(PK b ::: (PK a ::: Nil), SUB Nil)
forall {s} {kk :: CAT s} {h :: s} {i :: s} {j :: s} {k :: s}
       (p :: Path kk j h) (q :: Path kk k i) (f :: Path kk h i)
       (g :: Path kk j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold (PK t ::: (PK s ::: Nil)) ~> Fold (PK b ::: (PK a ::: Nil)))
-> Strictified (PK t ::: (PK s ::: Nil)) (PK b ::: (PK a ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (((s :.: t) :~> (a :.: b)) -> Prof (PK (s :.: t)) (PK (a :.: b))
forall {j} {k} (p1 :: j +-> k) (q1 :: j +-> k).
(Ob p1, Ob q1) =>
(p1 :~> q1) -> Prof (PK p1) (PK q1)
Prof (:.:) s t a b -> (:.:) a b a b
(s :.: t) :~> (a :.: b)
n))

type HaskOptic a b s t = ProfOptic (Star a) (Costar b) (Star s) (Costar t)
mkHaskOptic
  :: (Functor a, Functor b, Functor s, Functor t)
  => (forall x r. (Ob x) => (forall y. (Ob y) => (s x ~> a y) -> (b y ~> t x) -> r) -> r) -> HaskOptic a b s t
mkHaskOptic :: forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic forall (x :: x) r.
Ob x =>
(forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r
k = ((Star s :.: Costar t) :~> (Star a :.: Costar b))
-> ProfOptic (Star a) (Costar b) (Star s) (Costar t)
forall {x} {j} {k} {z} (s :: x +-> j) (t :: k +-> x) (a :: z +-> j)
       (b :: k +-> z).
((s :.: t) :~> (a :.: b)) -> ProfOptic a b s t
mkProfOptic \(Star @y a ~> s b
s :.: Costar t b ~> b
t) -> forall (x :: x) r.
Ob x =>
(forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r
k @y \s b ~> a y
get b y ~> t b
put -> (a ~> a y) -> Star a a y
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (s b ~> a y
get (s b ~> a y) -> (a ~> s b) -> a ~> a y
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> s b
s) Star a a y -> Costar b y b -> (:.:) (Star a) (Costar b) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b y ~> b) -> Costar b y b
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (t b ~> b
t (t b ~> b) -> (b y ~> t b) -> b y ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b y ~> t b
put)

type Lens s t a b = HaskOptic ((,) a) ((,) b) ((,) s) ((,) t)
mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens :: forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens s -> a
f s -> b -> t
g = (forall x r.
 Ob x =>
 (forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r)
 -> r)
-> HaskOptic ((,) a) ((,) b) ((,) s) ((,) t)
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r
k -> ((s, x) ~> (a, (b -> t, x))) -> ((b, (b -> t, x)) ~> (t, x)) -> r
forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r
k (\(s
s, x
x) -> (s -> a
f s
s, (s -> b -> t
g s
s, x
x))) (\(b
b, (b -> t
bt, x
x)) -> (b -> t
bt b
b, x
x)))

type Prism s t a b = HaskOptic (Either a) (Either b) (Either s) (Either t)
mkPrism :: (s -> Either a t) -> (b -> t) -> Prism s t a b
mkPrism :: forall s a t b. (s -> Either a t) -> (b -> t) -> Prism s t a b
mkPrism s -> Either a t
f b -> t
g = (forall x r.
 Ob x =>
 (forall y.
  Ob y =>
  (Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r)
 -> r)
-> HaskOptic (Either a) (Either b) (Either s) (Either t)
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall y.
Ob y =>
(Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r
k -> (Either s x ~> Either a (Either t x))
-> (Either b (Either t x) ~> Either t x) -> r
forall y.
Ob y =>
(Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r
k ((s -> Either a (Either t x))
-> (x -> Either a (Either t x))
-> Either s x
-> Either a (Either t x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a -> Either a (Either t x))
-> (t -> Either a (Either t x))
-> Either a t
-> Either a (Either t x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either a (Either t x)
forall a b. a -> Either a b
Left (Either t x -> Either a (Either t x)
forall a b. b -> Either a b
Right (Either t x -> Either a (Either t x))
-> (t -> Either t x) -> t -> Either a (Either t x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. t -> Either t x
forall a b. a -> Either a b
Left) (Either a t -> Either a (Either t x))
-> (s -> Either a t) -> s -> Either a (Either t x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s -> Either a t
f) (Either t x -> Either a (Either t x)
forall a b. b -> Either a b
Right (Either t x -> Either a (Either t x))
-> (x -> Either t x) -> x -> Either a (Either t x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x -> Either t x
forall a b. b -> Either a b
Right)) ((b -> Either t x)
-> (Either t x -> Either t x)
-> Either b (Either t x)
-> Either t x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (t -> Either t x
forall a b. a -> Either a b
Left (t -> Either t x) -> (b -> t) -> b -> Either t x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b -> t
g) Either t x -> Either t x
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))

data FlipApp a f = FlipApp {forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp :: f a}
instance (Ob a) => Functor (FlipApp a) where
  map :: forall (a :: k -> Type) (b :: k -> Type).
(a ~> b) -> FlipApp a a ~> FlipApp a b
map (Nat a .~> b
f) (FlipApp a a
x) = b a -> FlipApp a b
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (a a ~> b a
a a -> b a
a .~> b
f a a
x)
type Traversal s t a b = HaskOptic (FlipApp a) (FlipApp b) (FlipApp s) (FlipApp t)
mkTraversal :: (Traversable f, Functor f) => Traversal (f a) (f b) a b
mkTraversal :: forall (f :: Type -> Type) a b.
(Traversable f, Functor f) =>
Traversal (f a) (f b) a b
mkTraversal = (forall (x :: Type -> Type) r.
 Ob x =>
 (forall (y :: Type -> Type).
  Ob y =>
  (FlipApp (f a) x ~> FlipApp a y)
  -> (FlipApp b y ~> FlipApp (f b) x) -> r)
 -> r)
-> HaskOptic
     (FlipApp a) (FlipApp b) (FlipApp (f a)) (FlipApp (f b))
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall (y :: Type -> Type).
Ob y =>
(FlipApp (f a) x ~> FlipApp a y)
-> (FlipApp b y ~> FlipApp (f b) x) -> r
k -> (FlipApp (f a) x ~> FlipApp a (Compose x f))
-> (FlipApp b (Compose x f) ~> FlipApp (f b) x) -> r
forall (y :: Type -> Type).
Ob y =>
(FlipApp (f a) x ~> FlipApp a y)
-> (FlipApp b y ~> FlipApp (f b) x) -> r
k (Compose x f a -> FlipApp a (Compose x f)
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (Compose x f a -> FlipApp a (Compose x f))
-> (FlipApp (f a) x -> Compose x f a)
-> FlipApp (f a) x
-> FlipApp a (Compose x f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x (f a) -> Compose x f a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (x (f a) -> Compose x f a)
-> (FlipApp (f a) x -> x (f a)) -> FlipApp (f a) x -> Compose x f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. FlipApp (f a) x -> x (f a)
forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp) (x (f b) -> FlipApp (f b) x
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (x (f b) -> FlipApp (f b) x)
-> (FlipApp b (Compose x f) -> x (f b))
-> FlipApp b (Compose x f)
-> FlipApp (f b) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Compose x f b -> x (f b)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose x f b -> x (f b))
-> (FlipApp b (Compose x f) -> Compose x f b)
-> FlipApp b (Compose x f)
-> x (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. FlipApp b (Compose x f) -> Compose x f b
forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp))