-- | A third way to combine two flavors, alongside "Proarrow.Optic.Sum" and "Proarrow.Optic.Day":
-- pair them up over the /product/ of two categories via ':**:'.
module Proarrow.Optic.Prod where

import Proarrow.Category.Instance.Product (Fst, Snd, (:**:) (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Functor (type (@))
import Proarrow.Optic (ClosedUnder, CompactFlavor, ExOptic (..), FLAVOR, Optic, Prostrong (..), ex2prof, withLegs)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

-- | Two flavors combine into one over the product of their (possibly heterogeneous) categories,
-- by pairing up their witness profunctors componentwise via ':**:' rather than sharing a single
-- object (@:*:@ doesn't work here: it forces both witnesses onto the *same* index kind, so it
-- can't combine optics over genuinely different categories/objects).
type ProdRes :: forall {j1} {k1} {j2} {k2}. FLAVOR j1 k1 -> FLAVOR j2 k2 -> FLAVOR (j1, j2) (k1, k2)
class ProdRes w1 w2 (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2)) where
  -- | Recover the two component witnesses from an opaque, possibly-composite 'ProdRes' pair.
  -- Stated via 'Fst'\/'Snd' rather than literal tuple patterns: the existential "middle" object
  -- introduced when recursing through a ':.:' composite isn't syntactically a tuple, even though
  -- (being of a product kind) it always denotes one.
  withProdP
    :: p s a
    -> q b t
    -> ( forall p1 p2 q1 q2
          . (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
         => p1 (Fst @ s) (Fst @ a) -> p2 (Snd @ s) (Snd @ a) -> q1 (Fst @ b) (Fst @ t) -> q2 (Snd @ b) (Snd @ t) -> r
       )
    -> r

instance
  (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
  => ProdRes w1 w2 (p1 :**: p2) (q1 :**: q2)
  where
  withProdP :: forall (s :: (j1, j2)) (a :: (j1, j2)) (b :: (j1, j2))
       (t :: (j1, j2)) r.
(:**:) p1 p2 s a
-> (:**:) q1 q2 b t
-> (forall (p1 :: j1 +-> j1) (p2 :: j2 +-> j2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP (p1 a1 b1
l1 :**: p2 a2 b2
l2) (q1 a1 b1
r1 :**: q2 a2 b2
r2) forall (p1 :: j1 +-> j1) (p2 :: j2 +-> j2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k = p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
forall (p1 :: j1 +-> j1) (p2 :: j2 +-> j2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k p1 a1 b1
p1 (Fst @ s) (Fst @ a)
l1 p2 a2 b2
p2 (Snd @ s) (Snd @ a)
l2 q1 a1 b1
q1 (Fst @ b) (Fst @ t)
r1 q2 a2 b2
q2 (Snd @ b) (Snd @ t)
r2
instance
  (CategoryOf k1, CategoryOf k2, CategoryOf j1, CategoryOf j2, ClosedUnder w1, ClosedUnder w2)
  => ProdRes w1 w2 (Id :: CAT (k1, k2)) (Id :: CAT (j1, j2))
  where
  withProdP :: forall (s :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2))
       (t :: (j1, j2)) r.
Id s a
-> Id b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP (Id (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Id (a1 ~> b1
g1 :**: a2 ~> b2
g2)) forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k = Id (Fst @ s) (Fst @ a)
-> Id (Snd @ s) (Snd @ a)
-> Id (Fst @ b) (Fst @ t)
-> Id (Snd @ b) (Snd @ t)
-> r
forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k ((a1 ~> b1) -> Id a1 b1
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a1 ~> b1
f1) ((a2 ~> b2) -> Id a2 b2
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a2 ~> b2
f2) ((a1 ~> b1) -> Id a1 b1
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a1 ~> b1
g1) ((a2 ~> b2) -> Id a2 b2
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a2 ~> b2
g2)
instance
  (ProdRes w1 w2 f f', ProdRes w1 w2 g g', ClosedUnder w1, ClosedUnder w2)
  => ProdRes w1 w2 (f :.: g) (g' :.: f')
  where
  withProdP :: forall (s :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2))
       (t :: (j1, j2)) r.
(:.:) f g s a
-> (:.:) g' f' b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP (f s b
f :.: g b a
g) (g' b b
g' :.: f' b t
f') forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k =
    forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: (k1, k2) +-> (k1, k2))
       (q :: (j1, j2) +-> (j1, j2)) (s :: (k1, k2)) (a :: (k1, k2))
       (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2))
       (s :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP @w1 @w2 f s b
f f' b t
f' \p1 (Fst @ s) (Fst @ b)
p1 p2 (Snd @ s) (Snd @ b)
p2 q1 (Fst @ b) (Fst @ t)
q1 q2 (Snd @ b) (Snd @ t)
q2 ->
      forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: (k1, k2) +-> (k1, k2))
       (q :: (j1, j2) +-> (j1, j2)) (s :: (k1, k2)) (a :: (k1, k2))
       (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2))
       (s :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP @w1 @w2 g b a
g g' b b
g' \p1 (Fst @ b) (Fst @ a)
p1' p2 (Snd @ b) (Snd @ a)
p2' q1 (Fst @ b) (Fst @ b)
q1' q2 (Snd @ b) (Snd @ b)
q2' ->
        (:.:) p1 p1 (Fst @ s) (Fst @ a)
-> (:.:) p2 p2 (Snd @ s) (Snd @ a)
-> (:.:) q1 q1 (Fst @ b) (Fst @ t)
-> (:.:) q2 q2 (Snd @ b) (Snd @ t)
-> r
forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
       (q2 :: j2 +-> j2).
(w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
 Profunctor q2) =>
p1 (Fst @ s) (Fst @ a)
-> p2 (Snd @ s) (Snd @ a)
-> q1 (Fst @ b) (Fst @ t)
-> q2 (Snd @ b) (Snd @ t)
-> r
k (p1 (Fst @ s) (Fst @ b)
p1 p1 (Fst @ s) (Fst @ b)
-> p1 (Fst @ b) (Fst @ a) -> (:.:) p1 p1 (Fst @ s) (Fst @ a)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p1 (Fst @ b) (Fst @ a)
p1') (p2 (Snd @ s) (Snd @ b)
p2 p2 (Snd @ s) (Snd @ b)
-> p2 (Snd @ b) (Snd @ a) -> (:.:) p2 p2 (Snd @ s) (Snd @ a)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p2 (Snd @ b) (Snd @ a)
p2') (q1 (Fst @ b) (Fst @ b)
q1' q1 (Fst @ b) (Fst @ b)
-> q1 (Fst @ b) (Fst @ t) -> (:.:) q1 q1 (Fst @ b) (Fst @ t)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q1 (Fst @ b) (Fst @ t)
q1) (q2 (Snd @ b) (Snd @ b)
q2' q2 (Snd @ b) (Snd @ b)
-> q2 (Snd @ b) (Snd @ t) -> (:.:) q2 q2 (Snd @ b) (Snd @ t)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q2 (Snd @ b) (Snd @ t)
q2)

instance
  forall j1 k1 j2 k2 (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
   . (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2)
  => CompactFlavor (ProdRes w1 w2)

prodOptic
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s1 t1 a1 b1 s2 t2 a2 b2
   . (CompactFlavor w1, CompactFlavor w2, CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2)
  => Optic (Prostrong w1) s1 t1 a1 b1
  -> Optic (Prostrong w2) s2 t2 a2 b2
  -> Optic (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
prodOptic :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (s1 :: k1) (t1 :: j1) (a1 :: k1) (b1 :: j1)
       (s2 :: k2) (t2 :: j2) (a2 :: k2) (b2 :: j2).
(CompactFlavor w1, CompactFlavor w2, CategoryOf j1, CategoryOf k1,
 CategoryOf j2, CategoryOf k2) =>
Optic (Prostrong w1) s1 t1 a1 b1
-> Optic (Prostrong w2) s2 t2 a2 b2
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
prodOptic Optic (Prostrong w1) s1 t1 a1 b1
o1 Optic (Prostrong w2) s2 t2 a2 b2
o2 =
  (forall (p :: k1 +-> k1) (q :: j1 +-> j1).
 (w1 p q, Profunctor p, Profunctor q) =>
 p s1 a1
 -> q b1 t1
 -> Optic
      (Prostrong (ProdRes w1 w2))
      '(s1, s2)
      '(t1, t2)
      '(a1, a2)
      '(b1, b2))
-> Optic (Prostrong w1) s1 t1 a1 b1
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs
    ( \p s1 a1
l1 q b1 t1
r1 ->
        (forall (p :: k2 +-> k2) (q :: j2 +-> j2).
 (w2 p q, Profunctor p, Profunctor q) =>
 p s2 a2
 -> q b2 t2
 -> Optic
      (Prostrong (ProdRes w1 w2))
      '(s1, s2)
      '(t1, t2)
      '(a1, a2)
      '(b1, b2))
-> Optic (Prostrong w2) s2 t2 a2 b2
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs
          (\p s2 a2
l2 q b2 t2
r2 -> ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2) '(s1, s2) '(t1, t2)
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:)
  ((p :**: p) :.: ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2))
  (q :**: q)
  '(s1, s2)
  '(t1, t2)
-> ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2) '(s1, s2) '(t1, t2)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((p s1 a1
l1 p s1 a1 -> p s2 a2 -> (:**:) p p '(s1, s2) '(a1, a2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: p s2 a2
l2) (:**:) p p '(s1, s2) '(a1, a2)
-> ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2) '(a1, a2) '(b1, b2)
-> (:.:)
     (p :**: p)
     (ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2))
     '(s1, s2)
     '(b1, b2)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ('(a1, a2) ~> '(a1, a2))
-> ('(b1, b2) ~> '(b1, b2))
-> ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2) '(a1, a2) '(b1, b2)
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso '(a1, a2) ~> '(a1, a2)
(:**:) (~>) (~>) '(a1, a2) '(a1, a2)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: (k1, k2)). Ob a => (:**:) (~>) (~>) a a
id '(b1, b2) ~> '(b1, b2)
(:**:) (~>) (~>) '(b1, b2) '(b1, b2)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: (j1, j2)). Ob a => (:**:) (~>) (~>) a a
id (:.:)
  (p :**: p)
  (ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2))
  '(s1, s2)
  '(b1, b2)
-> (:**:) q q '(b1, b2) '(t1, t2)
-> (:.:)
     ((p :**: p) :.: ExOptic (ProdRes w1 w2) '(a1, a2) '(b1, b2))
     (q :**: q)
     '(s1, s2)
     '(t1, t2)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (q b1 t1
r1 q b1 t1 -> q b2 t2 -> (:**:) q q '(b1, b2) '(t1, t2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q b2 t2
r2))) ((Ob s1, Ob a1) =>
 Optic
   (Prostrong (ProdRes w1 w2))
   '(s1, s2)
   '(t1, t2)
   '(a1, a2)
   '(b1, b2))
-> p s1 a1
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall (a :: k1) (b :: k1) r. ((Ob a, Ob b) => r) -> p 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
\\ p s1 a1
l1 ((Ob b1, Ob t1) =>
 Optic
   (Prostrong (ProdRes w1 w2))
   '(s1, s2)
   '(t1, t2)
   '(a1, a2)
   '(b1, b2))
-> q b1 t1
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall (a :: j1) (b :: j1) r. ((Ob a, Ob b) => r) -> q 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
\\ q b1 t1
r1 ((Ob s2, Ob a2) =>
 Optic
   (Prostrong (ProdRes w1 w2))
   '(s1, s2)
   '(t1, t2)
   '(a1, a2)
   '(b1, b2))
-> p s2 a2
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall (a :: k2) (b :: k2) r. ((Ob a, Ob b) => r) -> p 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
\\ p s2 a2
l2 ((Ob b2, Ob t2) =>
 Optic
   (Prostrong (ProdRes w1 w2))
   '(s1, s2)
   '(t1, t2)
   '(a1, a2)
   '(b1, b2))
-> q b2 t2
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
forall (a :: j2) (b :: j2) r. ((Ob a, Ob b) => r) -> q 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
\\ q b2 t2
r2)
          Optic (Prostrong w2) s2 t2 a2 b2
o2
    )
    Optic (Prostrong w1) s1 t1 a1 b1
o1

-- | The inverse of 'prodOptic': split a @'ProdRes' w1 w2@-flavored optic back into its two
-- independent halves.
withProdOptic
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s1 t1 a1 b1 s2 t2 a2 b2 r
   . (CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2, ClosedUnder w1, ClosedUnder w2)
  => Optic (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
  -> ((Optic (Prostrong w1) s1 t1 a1 b1, Optic (Prostrong w2) s2 t2 a2 b2) -> r)
  -> r
withProdOptic :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (s1 :: k1) (t1 :: j1) (a1 :: k1) (b1 :: j1)
       (s2 :: k2) (t2 :: j2) (a2 :: k2) (b2 :: j2) r.
(CategoryOf j1, CategoryOf k1, CategoryOf j2, CategoryOf k2,
 ClosedUnder w1, ClosedUnder w2) =>
Optic
  (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
-> ((Optic (Prostrong w1) s1 t1 a1 b1,
     Optic (Prostrong w2) s2 t2 a2 b2)
    -> r)
-> r
withProdOptic =
  (forall (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2)).
 (ProdRes w1 w2 p q, Profunctor p, Profunctor q) =>
 p '(s1, s2) '(a1, a2)
 -> q '(b1, b2) '(t1, t2)
 -> ((Optic (Prostrong w1) s1 t1 a1 b1,
      Optic (Prostrong w2) s2 t2 a2 b2)
     -> r)
 -> r)
-> Optic
     (Prostrong (ProdRes w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
-> ((Optic (Prostrong w1) s1 t1 a1 b1,
     Optic (Prostrong w2) s2 t2 a2 b2)
    -> r)
-> r
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \p '(s1, s2) '(a1, a2)
l q '(b1, b2) '(t1, t2)
r ->
    forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1)
       (w2 :: FLAVOR j2 k2) (p :: (k1, k2) +-> (k1, k2))
       (q :: (j1, j2) +-> (j1, j2)) (s :: (k1, k2)) (a :: (k1, k2))
       (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
forall (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2)
       (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2))
       (s :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2)) (t :: (j1, j2)) r.
ProdRes w1 w2 p q =>
p s a
-> q b t
-> (forall (p1 :: k1 +-> k1) (p2 :: k2 +-> k2) (q1 :: j1 +-> j1)
           (q2 :: j2 +-> j2).
    (w1 p1 q1, w2 p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
     Profunctor q2) =>
    p1 (Fst @ s) (Fst @ a)
    -> p2 (Snd @ s) (Snd @ a)
    -> q1 (Fst @ b) (Fst @ t)
    -> q2 (Snd @ b) (Snd @ t)
    -> r)
-> r
withProdP @w1 @w2 p '(s1, s2) '(a1, a2)
l q '(b1, b2) '(t1, t2)
r \p1 (Fst @ '(s1, s2)) (Fst @ '(a1, a2))
p1 p2 (Snd @ '(s1, s2)) (Snd @ '(a1, a2))
p2 q1 (Fst @ '(b1, b2)) (Fst @ '(t1, t2))
q1 q2 (Snd @ '(b1, b2)) (Snd @ '(t1, t2))
q2 (Optic (Prostrong w1) s1 t1 a1 b1,
 Optic (Prostrong w2) s2 t2 a2 b2)
-> r
k ->
      (Optic (Prostrong w1) s1 t1 a1 b1,
 Optic (Prostrong w2) s2 t2 a2 b2)
-> r
k
        ( ExOptic w1 a1 b1 s1 t1 -> Optic (Prostrong w1) s1 t1 a1 b1
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (p1 :.: ExOptic w1 a1 b1) q1 s1 t1 -> ExOptic w1 a1 b1 s1 t1
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (p1 s1 a1
p1 (Fst @ '(s1, s2)) (Fst @ '(a1, a2))
p1 p1 s1 a1
-> ExOptic w1 a1 b1 a1 b1 -> (:.:) p1 (ExOptic w1 a1 b1) s1 b1
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a1 ~> a1) -> (b1 ~> b1) -> ExOptic w1 a1 b1 a1 b1
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a1 ~> a1
forall (a :: k1). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b1 ~> b1
forall (a :: j1). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) p1 (ExOptic w1 a1 b1) s1 b1
-> q1 b1 t1 -> (:.:) (p1 :.: ExOptic w1 a1 b1) q1 s1 t1
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q1 b1 t1
q1 (Fst @ '(b1, b2)) (Fst @ '(t1, t2))
q1)) ((Ob s1, Ob a1) => Optic (Prostrong w1) s1 t1 a1 b1)
-> p1 s1 a1 -> Optic (Prostrong w1) s1 t1 a1 b1
forall (a :: k1) (b :: k1) r. ((Ob a, Ob b) => r) -> p1 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
\\ p1 s1 a1
p1 (Fst @ '(s1, s2)) (Fst @ '(a1, a2))
p1 ((Ob b1, Ob t1) => Optic (Prostrong w1) s1 t1 a1 b1)
-> q1 b1 t1 -> Optic (Prostrong w1) s1 t1 a1 b1
forall (a :: j1) (b :: j1) r. ((Ob a, Ob b) => r) -> q1 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
\\ q1 b1 t1
q1 (Fst @ '(b1, b2)) (Fst @ '(t1, t2))
q1
        , ExOptic w2 a2 b2 s2 t2 -> Optic (Prostrong w2) s2 t2 a2 b2
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof ((:.:) (p2 :.: ExOptic w2 a2 b2) q2 s2 t2 -> ExOptic w2 a2 b2 s2 t2
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (p2 s2 a2
p2 (Snd @ '(s1, s2)) (Snd @ '(a1, a2))
p2 p2 s2 a2
-> ExOptic w2 a2 b2 a2 b2 -> (:.:) p2 (ExOptic w2 a2 b2) s2 b2
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a2 ~> a2) -> (b2 ~> b2) -> ExOptic w2 a2 b2 a2 b2
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a2 ~> a2
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b2 ~> b2
forall (a :: j2). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) p2 (ExOptic w2 a2 b2) s2 b2
-> q2 b2 t2 -> (:.:) (p2 :.: ExOptic w2 a2 b2) q2 s2 t2
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q2 b2 t2
q2 (Snd @ '(b1, b2)) (Snd @ '(t1, t2))
q2)) ((Ob s2, Ob a2) => Optic (Prostrong w2) s2 t2 a2 b2)
-> p2 s2 a2 -> Optic (Prostrong w2) s2 t2 a2 b2
forall (a :: k2) (b :: k2) r. ((Ob a, Ob b) => r) -> p2 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
\\ p2 s2 a2
p2 (Snd @ '(s1, s2)) (Snd @ '(a1, a2))
p2 ((Ob b2, Ob t2) => Optic (Prostrong w2) s2 t2 a2 b2)
-> q2 b2 t2 -> Optic (Prostrong w2) s2 t2 a2 b2
forall (a :: j2) (b :: j2) r. ((Ob a, Ob b) => r) -> q2 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
\\ q2 b2 t2
q2 (Snd @ '(b1, b2)) (Snd @ '(t1, t2))
q2
        )