{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __glass__ (Clarke et al., /Profunctor optics: a categorical update/): the optic for the
-- combined action of the product and the exponential,
--
-- > Glass s t a b = exists c d. (s ~> c && (d ~~> a), (c && (d ~~> b)) ~> t)
--
-- which collapses to the single leg @(s && ((s ~~> a) ~~> b)) ~> t@: given the source and a way
-- to turn any /selector/ @s ~~> a@ into a @b@, produce a @t@. A lens is the case @d = Unit@ (it
-- applies the selector to the source it was given), a grate the case @c = Unit@ (it ignores the
-- source and feeds the selector through its exponent), so 'GlassFl' is the join of
-- 'Proarrow.Optic.Lens.LensFl' and 'Proarrow.Optic.Grate.GrateFl' -- what
-- 'Proarrow.Optic.AffineTraversal.AffineTravFl' is to lenses and prisms, one column over. Like
-- that flavor it has no witnesses of its own: its generating pairs are the product pair and the
-- exponential pair, and 'glass' packs its single leg as their composite.
--
-- It sits directly below 'Proarrow.Optic.Setter.SetterFl': a glass sets, but it neither folds
-- (grates do not) nor distributes an applicative (lenses do not).
module Proarrow.Optic.Glass where

import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), type (**))
import Proarrow.Category.Monoidal.Cartesian (CCC, productToTensor, tensorToProduct)
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp, comp, mkExponential, swapClosed)
import Proarrow.Category.Monoidal.CopyDiscard (fst, snd, (&&&))
import Proarrow.Core (CategoryOf (..), Promonad (..), obj, type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (type (&&)), Product)
import Proarrow.Limit.BinaryProduct qualified as P
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.Setter (SetterFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

-- | The glass flavor. Its one method is the collapsed leg; everything is stated in a cartesian
-- closed category, where the residual can be copied and selectors can be internalised.
type GlassFl :: forall {k}. FLAVOR k k
class (SetterFl p q) => GlassFl (p :: k +-> k) (q :: k +-> k) where
  glassP :: (CCC k) => p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t

-- | Feed a fixed selector @s ~> a@ to a selector-consumer.
applySel :: forall {k} (s :: k) a b. (Closed k, Ob s, Ob a, Ob b) => (s ~> a) -> ((s ~~> a) ~~> b) ~> b
applySel :: forall {k} (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> ((s ~~> a) ~~> b) ~> b
applySel s ~> a
sel =
  forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => ((s ~~> a) ~~> b) ~> b)
 -> ((s ~~> a) ~~> b) ~> b)
-> (Ob (s ~~> a) => ((s ~~> a) ~~> b) ~> b)
-> ((s ~~> a) ~~> b) ~> b
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => ((s ~~> a) ~~> b) ~> b)
 -> ((s ~~> a) ~~> b) ~> b)
-> (Ob ((s ~~> a) ~~> b) => ((s ~~> a) ~~> b) ~> b)
-> ((s ~~> a) ~~> b) ~> b
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @(s ~~> a) @b ((((s ~~> a) ~~> b) ** (s ~~> a)) ~> b)
-> (((s ~~> a) ~~> b) ~> (((s ~~> a) ~~> b) ** (s ~~> a)))
-> ((s ~~> a) ~~> b) ~> 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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @((s ~~> a) ~~> b) Obj ((s ~~> a) ~~> b)
-> (Unit ~> (s ~~> a))
-> (((s ~~> a) ~~> b) ** Unit) ~> (((s ~~> a) ~~> b) ** (s ~~> a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (s ~> a) -> Unit ~> (s ~~> a)
forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
mkExponential s ~> a
sel) ((((s ~~> a) ~~> b) ** Unit) ~> (((s ~~> a) ~~> b) ** (s ~~> a)))
-> (((s ~~> a) ~~> b) ~> (((s ~~> a) ~~> b) ** Unit))
-> ((s ~~> a) ~~> b) ~> (((s ~~> a) ~~> b) ** (s ~~> a))
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
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @((s ~~> a) ~~> b)

-- | The product pair, a lens witness: the selector is the lens's own @get@, applied to the source
-- at hand; the residual is kept.
instance (HasBinaryProducts k, Ob (c :: k)) => GlassFl (Rep (Product c)) (Corep (Product c)) where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
Rep (Product c) s a
-> Corep (Product c) b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @s @a @b (Rep h :: s ~> (Product c @ a)
h@s ~> (Product c @ a)
s ~> (c && a)
Objs) (Corep (Product c @ b) ~> t
i) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
        (Product c @ b) ~> t
(c && b) ~> t
i
          ((c && b) ~> t)
-> ((s && ((s ~~> a) ~~> b)) ~> (c && b))
-> (s && ((s ~~> a) ~~> b)) ~> t
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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
tensorToProduct @c @b
          ((c ** b) ~> (c && b))
-> ((s && ((s ~~> a) ~~> b)) ~> (c ** b))
-> (s && ((s ~~> a) ~~> b)) ~> (c && 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
. ( (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
P.fst @k @c @a ((c && a) ~> c)
-> ((s ** ((s ~~> a) ~~> b)) ~> (c && a))
-> (s ** ((s ~~> a) ~~> b)) ~> c
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
. s ~> (Product c @ a)
s ~> (c && a)
h (s ~> (c && a))
-> ((s ** ((s ~~> a) ~~> b)) ~> s)
-> (s ** ((s ~~> a) ~~> b)) ~> (c && a)
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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @s @((s ~~> a) ~~> b))
                ((s ** ((s ~~> a) ~~> b)) ~> c)
-> ((s ** ((s ~~> a) ~~> b)) ~> b)
-> (s ** ((s ~~> a) ~~> b)) ~> (c ** b)
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (forall (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> ((s ~~> a) ~~> b) ~> b
forall {k} (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> ((s ~~> a) ~~> b) ~> b
applySel @s @a @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
P.snd @k @c @a ((c && a) ~> a) -> (s ~> (c && a)) -> s ~> a
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
. s ~> (Product c @ a)
s ~> (c && a)
h) (((s ~~> a) ~~> b) ~> b)
-> ((s ** ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> (s ** ((s ~~> a) ~~> b)) ~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @s @((s ~~> a) ~~> b))
            )
          ((s ** ((s ~~> a) ~~> b)) ~> (c ** b))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> a) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> (c ** 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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
productToTensor @s @((s ~~> a) ~~> b)

-- | The exponential pair, a grate witness: the source is ignored, and the consumer is fed the
-- selector @\\s -> h s d@ for each point @d@ of the exponent.
instance (Closed k, Ob (d :: k)) => GlassFl (Rep (Exp d)) (Corep (Exp d)) where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
Rep (Exp d) s a
-> Corep (Exp d) b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @s @a @b (Rep h :: s ~> (Exp d @ a)
h@s ~> (Exp d @ a)
s ~> (d ~~> a)
Objs) (Corep (Exp d @ b) ~> t
i) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
        (Exp d @ b) ~> t
(d ~~> b) ~> t
i
          ((d ~~> b) ~> t)
-> ((s && ((s ~~> a) ~~> b)) ~> (d ~~> b))
-> (s && ((s ~~> a) ~~> b)) ~> t
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
. forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @((s ~~> a) ~~> b) @d (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @(s ~~> a) @b ((((s ~~> a) ~~> b) ** (s ~~> a)) ~> b)
-> ((((s ~~> a) ~~> b) ** d) ~> (((s ~~> a) ~~> b) ** (s ~~> a)))
-> (((s ~~> a) ~~> b) ** d) ~> 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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @((s ~~> a) ~~> b) Obj ((s ~~> a) ~~> b)
-> (d ~> (s ~~> a))
-> (((s ~~> a) ~~> b) ** d) ~> (((s ~~> a) ~~> b) ** (s ~~> a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapClosed @a @s @d s ~> (Exp d @ a)
s ~> (d ~~> a)
h))
          (((s ~~> a) ~~> b) ~> (d ~~> b))
-> ((s && ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> (s && ((s ~~> a) ~~> b)) ~> (d ~~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @s @((s ~~> a) ~~> b)
          ((s ** ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> a) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> 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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
productToTensor @s @((s ~~> a) ~~> b)

instance (CategoryOf k) => GlassFl (Id :: k +-> k) (Id :: k +-> k) where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
Id s a -> Id b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @s @a @b (Id l :: s ~> a
l@s ~> a
Objs) (Id r :: b ~> t
r@b ~> t
Objs) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
        b ~> t
r (b ~> t)
-> ((s && ((s ~~> a) ~~> b)) ~> b) -> (s && ((s ~~> a) ~~> b)) ~> t
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
. forall (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> ((s ~~> a) ~~> b) ~> b
forall {k} (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> ((s ~~> a) ~~> b) ~> b
applySel @s @a @b s ~> a
l (((s ~~> a) ~~> b) ~> b)
-> ((s && ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> (s && ((s ~~> a) ~~> b)) ~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @s @((s ~~> a) ~~> b) ((s ** ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> a) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> 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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
productToTensor @s @((s ~~> a) ~~> b)

-- | Composition threads the selector through: the outer glass is given the consumer
-- @\\sel -> inner (sel s, \\sel' -> k (sel' . sel))@.
instance
  forall k (f :: k +-> k) (f' :: k +-> k) (g :: k +-> k) (g' :: k +-> k)
   . (GlassFl f g, GlassFl f' g')
  => GlassFl (f :.: f') (g' :.: g)
  where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
(:.:) f f' s a -> (:.:) g' g b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @s @a @b (f :: f s b
f@f s b
Objs :.: (f' :: f' b a
f'@f' b a
Objs :: f' x a)) ((g' :: g' b b
g'@g' b b
Objs :: g' b y) :.: g :: g b t
g@g b t
Objs) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @x ((Ob (s ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> x) @y ((Ob ((s ~~> b) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ~~> b) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @x @a ((Ob (b ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (b ~~> a) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
              forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(x ~~> a) @b ((Ob ((b ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((b ~~> a) ~~> b) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @s @((s ~~> a) ~~> b) ((Ob (s ** ((s ~~> a) ~~> b)) => (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (s ** ((s ~~> a) ~~> b)) => (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
                  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(s ** ((s ~~> a) ~~> b)) @(s ~~> x) ((Ob ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) =>
  (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) =>
    (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
                    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @((s ** ((s ~~> a) ~~> b)) ** (s ~~> x)) @(x ~~> a) ((Ob (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a)) =>
  (s && ((s ~~> a) ~~> b)) ~> t)
 -> (s && ((s ~~> a) ~~> b)) ~> t)
-> (Ob (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a)) =>
    (s && ((s ~~> a) ~~> b)) ~> t)
-> (s && ((s ~~> a) ~~> b)) ~> t
forall a b. (a -> b) -> a -> b
$
                      let
                        -- the inner glass, fed a product-typed pair
                        inner :: (b ** ((b ~~> a) ~~> b)) ~> b
inner = forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @f' @g' f' b a
f' g' b b
g' ((b && ((b ~~> a) ~~> b)) ~> b)
-> ((b ** ((b ~~> a) ~~> b)) ~> (b && ((b ~~> a) ~~> b)))
-> (b ** ((b ~~> a) ~~> b)) ~> 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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
tensorToProduct @x @((x ~~> a) ~~> b)
                        -- the source of the inner glass: the outer selector applied to @s@
                        xpart :: ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> b
xpart =
                          forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @s @x
                            (((s ~~> b) ** s) ~> b)
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> ((s ~~> b) ** s))
-> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> 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
. ( forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @(s ** ((s ~~> a) ~~> b)) @(s ~~> x)
                                  (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> (s ~~> b))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> s)
-> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> ((s ~~> b) ** s)
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @s @((s ~~> a) ~~> b) ((s ** ((s ~~> a) ~~> b)) ~> s)
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b))
    ~> (s ** ((s ~~> a) ~~> b)))
-> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> s
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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @(s ** ((s ~~> a) ~~> b)) @(s ~~> x))
                              )
                        -- the inner consumer: compose the selectors, hand the result to @k@
                        kk :: (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
~> ((s ~~> a) ~~> b)
kk =
                          forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @s @((s ~~> a) ~~> b)
                            ((s ** ((s ~~> a) ~~> b)) ~> ((s ~~> a) ~~> b))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> (s ** ((s ~~> a) ~~> b)))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> ((s ~~> a) ~~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @(s ** ((s ~~> a) ~~> b)) @(s ~~> x)
                            (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b))
 ~> (s ** ((s ~~> a) ~~> b)))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> (s ** ((s ~~> a) ~~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @((s ** ((s ~~> a) ~~> b)) ** (s ~~> x)) @(x ~~> a)
                        sel :: (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a)) ~> (s ~~> a)
sel =
                          forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
comp @s @x @a
                            (((b ~~> a) ** (s ~~> b)) ~> (s ~~> a))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> ((b ~~> a) ** (s ~~> b)))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> (s ~~> a)
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
. ( forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @((s ** ((s ~~> a) ~~> b)) ** (s ~~> x)) @(x ~~> a)
                                  ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
 ~> (b ~~> a))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> (s ~~> b))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> ((b ~~> a) ** (s ~~> b))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd @(s ** ((s ~~> a) ~~> b)) @(s ~~> x) (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> (s ~~> b))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> (s ~~> 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
. forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @((s ** ((s ~~> a) ~~> b)) ** (s ~~> x)) @(x ~~> a))
                              )
                        kipart :: ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> ((b ~~> a) ~~> b)
kipart = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @((s ** ((s ~~> a) ~~> b)) ** (s ~~> x)) @(x ~~> a) (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @(s ~~> a) @b ((((s ~~> a) ~~> b) ** (s ~~> a)) ~> b)
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> (((s ~~> a) ~~> b) ** (s ~~> a)))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a)) ~> 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
. ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
~> ((s ~~> a) ~~> b)
kk ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
 ~> ((s ~~> a) ~~> b))
-> ((((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
    ~> (s ~~> a))
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a))
   ~> (((s ~~> a) ~~> b) ** (s ~~> a))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ** (b ~~> a)) ~> (s ~~> a)
sel))
                        body :: ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> b
body = (b ** ((b ~~> a) ~~> b)) ~> b
inner ((b ** ((b ~~> a) ~~> b)) ~> b)
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b))
    ~> (b ** ((b ~~> a) ~~> b)))
-> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> 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
. (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> b
xpart (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> b)
-> (((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> ((b ~~> a) ~~> b))
-> ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b))
   ~> (b ** ((b ~~> a) ~~> b))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> ((b ~~> a) ~~> b)
kipart)
                      in
                        forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @f @g f s b
f g b t
g
                          ((s && ((s ~~> b) ~~> b)) ~> t)
-> ((s && ((s ~~> a) ~~> b)) ~> (s && ((s ~~> b) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> t
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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a ** b) ~> (a && b)
tensorToProduct @s @((s ~~> x) ~~> y)
                          ((s ** ((s ~~> b) ~~> b)) ~> (s && ((s ~~> b) ~~> b)))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> b) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> (s && ((s ~~> b) ~~> 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
. (forall (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
forall {k} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst @s @((s ~~> a) ~~> b) ((s ** ((s ~~> a) ~~> b)) ~> s)
-> ((s ** ((s ~~> a) ~~> b)) ~> ((s ~~> b) ~~> b))
-> (s ** ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> b) ~~> b))
forall {k} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(s ** ((s ~~> a) ~~> b)) @(s ~~> x) ((s ** ((s ~~> a) ~~> b)) ** (s ~~> b)) ~> b
body)
                          ((s ** ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> b) ~~> b)))
-> ((s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> a) ~~> b)))
-> (s && ((s ~~> a) ~~> b)) ~> (s ** ((s ~~> b) ~~> 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
. forall (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) =>
(a && b) ~> (a ** b)
productToTensor @s @((s ~~> a) ~~> b)

type Glass (s :: k) (t :: k) a b = Optic (Prostrong GlassFl) s t a b
type Glass' s a = Glass s s a a

-- | Build a glass from its single leg. The residuals are the whole source and the "logarithm"
-- @s ~~> a@, so the witness is the lens witness at @s@ composed with the grate witness at @s ~~> a@.
glass
  :: forall {k} (s :: k) (t :: k) a b
   . (CCC k, Ob s, Ob a, Ob b)
  => ((s && ((s ~~> a) ~~> b)) ~> t) -> Glass s t a b
glass :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(CCC k, Ob s, Ob a, Ob b) =>
((s && ((s ~~> a) ~~> b)) ~> t) -> Glass s t a b
glass (s && ((s ~~> a) ~~> b)) ~> t
f =
  forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @s @a ((Ob (s ~~> a) => Glass s t a b) -> Glass s t a b)
-> (Ob (s ~~> a) => Glass s t a b) -> Glass s t a b
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @a ((Ob ((s ~~> a) ~~> a) => Glass s t a b) -> Glass s t a b)
-> (Ob ((s ~~> a) ~~> a) => Glass s t a b) -> Glass s t a b
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(s ~~> a) @b ((Ob ((s ~~> a) ~~> b) => Glass s t a b) -> Glass s t a b)
-> (Ob ((s ~~> a) ~~> b) => Glass s t a b) -> Glass s t a b
forall a b. (a -> b) -> a -> b
$
        let ev :: s ~> ((s ~~> a) ~~> a)
ev = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @s @(s ~~> a) (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @s @a (((s ~~> a) ** s) ~> a)
-> ((s ** (s ~~> a)) ~> ((s ~~> a) ** s)) -> (s ** (s ~~> a)) ~> a
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
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @s @(s ~~> a))
        in 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 k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @GlassFl
             (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @((s ~~> a) ~~> a) @(Product s) (s ~> s
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (s ~> s)
-> (s ~> ((s ~~> a) ~~> a)) -> s ~> (s && ((s ~~> a) ~~> a))
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
P.&&& s ~> ((s ~~> a) ~~> a)
ev) Rep (Product s) s ((s ~~> a) ~~> a)
-> Rep (Exp (s ~~> a)) ((s ~~> a) ~~> a) a
-> (:.:) (Rep (Product s)) (Rep (Exp (s ~~> a))) s 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
:.: forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(Exp (s ~~> a)) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @((s ~~> a) ~~> a)))
             (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(Exp (s ~~> a)) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @((s ~~> a) ~~> b)) Corep (Exp (s ~~> a)) b ((s ~~> a) ~~> b)
-> Corep (Product s) ((s ~~> a) ~~> b) t
-> (:.:) (Corep (Exp (s ~~> a))) (Corep (Product s)) b 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
:.: forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @((s ~~> a) ~~> b) @(Product s) (Product s @ ((s ~~> a) ~~> b)) ~> t
(s && ((s ~~> a) ~~> b)) ~> t
f)

-- | Eliminate any glass-flavored optic (a lens, a grate, or a composite of both, in either
-- encoding) to its single leg.
withGlass
  :: forall {k} c (s :: k) (t :: k) a b r
   . (CCC k, (Ob a, Ob b) => c (ExOptic GlassFl a b))
  => Optic c s t a b -> (((s && ((s ~~> a) ~~> b)) ~> t) -> r) -> r
withGlass :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(CCC k, (Ob a, Ob b) => c (ExOptic GlassFl a b)) =>
Optic c s t a b -> (((s && ((s ~~> a) ~~> b)) ~> t) -> r) -> r
withGlass Optic c s t a b
o ((s && ((s ~~> a) ~~> b)) ~> t) -> r
k = 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 k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @GlassFl Optic c s t a b
o \ @p @q p s a
p q b t
q -> ((s && ((s ~~> a) ~~> b)) ~> t) -> r
k (forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
(GlassFl p q, CCC k) =>
p s a -> q b t -> (s && ((s ~~> a) ~~> b)) ~> t
glassP @p @q p s a
p q b t
q)