-- | 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 (..), (\\), type (+->))
import Proarrow.Functor (type (@))
import Proarrow.Optic (FLAVOR, Flavor, Optic, Prostrong (..), legs2prof, 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 ':**:' instead of sharing a single
-- object. (@:*:@ doesn't work here. It forces both witnesses onto the same index kind, so it
-- can't combine optics over different categories/objects.)
type ProdFl :: forall {j1} {k1} {j2} {k2}. FLAVOR j1 k1 -> FLAVOR j2 k2 -> FLAVOR (j1, j2) (k1, k2)
class ProdFl w1 w2 (p :: (k1, k2) +-> (k1, k2)) (q :: (j1, j2) +-> (j1, j2)) where
  -- | Recover the two component witnesses from an opaque, possibly-composite 'ProdFl' 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)
  => ProdFl 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, Flavor w1, Flavor w2)
  => ProdFl 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
  (ProdFl w1 w2 f f', ProdFl w1 w2 g g', Flavor w1, Flavor w2)
  => ProdFl 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.
ProdFl 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.
ProdFl 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.
ProdFl 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.
ProdFl 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)

prodOptic
  :: forall {j1} {k1} {j2} {k2} (w1 :: FLAVOR j1 k1) (w2 :: FLAVOR j2 k2) s1 t1 a1 b1 s2 t2 a2 b2
   . (Flavor w1, Flavor 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 (ProdFl 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).
(Flavor w1, Flavor 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 (ProdFl 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 {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j1 k1) (c :: (k1 -> j1 -> Type) -> Constraint)
       (s :: k1) (t :: j1) (a :: k1) (b :: j1) r.
(CategoryOf j1, CategoryOf k1, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k1 +-> k1) (q :: j1 +-> j1).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @w1 Optic (Prostrong w1) s1 t1 a1 b1
o1 \p s1 a1
l1 q b1 t1
r1 ->
    forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR j2 k2) (c :: (k2 -> j2 -> Type) -> Constraint)
       (s :: k2) (t :: j2) (a :: k2) (b :: j2) r.
(CategoryOf j2, CategoryOf k2, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k2 +-> k2) (q :: j2 +-> j2).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @w2 Optic (Prostrong w2) s2 t2 a2 b2
o2 \p s2 a2
l2 q b2 t2
r2 ->
      forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR (j1, j2) (k1, k2)) (p :: (k1, k2) +-> (k1, k2))
       (q :: (j1, j2) +-> (j1, j2)) (s :: (k1, k2)) (t :: (j1, j2))
       (a :: (k1, k2)) (b :: (j1, j2)).
(CategoryOf (j1, j2), CategoryOf (k1, k2), w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(ProdFl w1 w2) (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) (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 (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2))
-> p s1 a1
-> Optic
     (Prostrong (ProdFl 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 (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2))
-> q b1 t1
-> Optic
     (Prostrong (ProdFl 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 (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2))
-> p s2 a2
-> Optic
     (Prostrong (ProdFl 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 (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2))
-> q b2 t2
-> Optic
     (Prostrong (ProdFl 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

-- | The inverse of 'prodOptic': split a @'ProdFl' 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, Flavor w1, Flavor w2)
  => Optic (Prostrong (ProdFl 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,
 Flavor w1, Flavor w2) =>
Optic
  (Prostrong (ProdFl 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 Optic
  (Prostrong (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
o (Optic (Prostrong w1) s1 t1 a1 b1,
 Optic (Prostrong w2) s2 t2 a2 b2)
-> r
k0 =
  forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR (j1, j2) (k1, k2))
       (c :: ((k1, k2) -> (j1, j2) -> Type) -> Constraint) (s :: (k1, k2))
       (t :: (j1, j2)) (a :: (k1, k2)) (b :: (j1, j2)) r.
(CategoryOf (j1, j2), CategoryOf (k1, k2), Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: (k1, k2) +-> (k1, k2))
           (q :: (j1, j2) +-> (j1, j2)).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @(ProdFl w1 w2) Optic
  (Prostrong (ProdFl w1 w2)) '(s1, s2) '(t1, t2) '(a1, a2) '(b1, b2)
o \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.
ProdFl 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.
ProdFl 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
k0
        (forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j1 k1) (p :: k1 +-> k1) (q :: j1 +-> j1)
       (s :: k1) (t :: j1) (a :: k1) (b :: j1).
(CategoryOf j1, CategoryOf k1, w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @w1 p1 s1 a1
p1 (Fst @ '(s1, s2)) (Fst @ '(a1, a2))
p1 q1 b1 t1
q1 (Fst @ '(b1, b2)) (Fst @ '(t1, t2))
q1, forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR j2 k2) (p :: k2 +-> k2) (q :: j2 +-> j2)
       (s :: k2) (t :: j2) (a :: k2) (b :: j2).
(CategoryOf j2, CategoryOf k2, w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @w2 p2 s2 a2
p2 (Snd @ '(s1, s2)) (Snd @ '(a1, a2))
p2 q2 b2 t2
q2 (Snd @ '(b1, b2)) (Snd @ '(t1, t2))
q2)