{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure (module Exports) where

import Pandora.Paradigm.Structure.Ability as Exports
import Pandora.Paradigm.Structure.Interface as Exports
import Pandora.Paradigm.Structure.Modification as Exports
import Pandora.Paradigm.Structure.Some as Exports

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Category (($), (.), (#))
import Pandora.Pattern.Functor.Covariant (Covariant (comap), Covariant_)
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Pointable (point)
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
import Pandora.Paradigm.Inventory.Optics ()
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Functor.Function ((%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.T_U ( type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))

instance Monotonic s a => Monotonic s (s :*: a) where
	reduce :: (s -> r -> r) -> r -> (s :*: a) -> r
reduce s -> r -> r
f r
r s :*: a
x = (s -> r -> r) -> r -> a -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce s -> r -> r
f (r -> a -> r) -> r -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# s -> r -> r
f ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x) r
r (a -> r) -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x

instance Nullable Maybe where
	null :: (Predicate :. Maybe) := a
null = (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Maybe a -> Boolean) -> (Predicate :. Maybe) := a)
-> (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case { Just a
_ -> Boolean
True ; Maybe a
_ -> Boolean
False }

instance (Covariant t, Covariant_ t (->) (->)) => Substructure Tail (Tap t) where
	type Available Tail (Tap t) = Identity
	type Substance Tail (Tap t) = t
	substructure :: Lens
  (Available 'Tail (Tap t))
  ((<:.>) (Tagged 'Tail) (Tap t) a)
  (Substance 'Tail (Tap t) a)
substructure = ((<:.>) (Tagged 'Tail) (Tap t) a
 -> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Tail) (Tap t) a
  -> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
 -> P_Q_T
      (->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a))
-> ((<:.>) (Tagged 'Tail) (Tap t) a
    -> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Tail) (Tap t) a
tap -> case Tagged 'Tail (Tap t a) -> Tap t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Tagged 'Tail (Tap t a) -> Tap t a)
-> Tagged 'Tail (Tap t a) -> Tap t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Tail) (Tap t) a
-> Primary (Tagged 'Tail <:.> Tap t) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Tail) (Tap t) a
tap of
		Tap a
x t a
xs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Tail) (Tap t) a)
 -> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
xs Identity (t a)
-> (Identity (t a) -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Tail) (Tap t) a
forall s a. s -> a -> Product s a
:*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> (Identity (t a) -> Tap t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Tail) (Tap t) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (t a -> Tap t a)
-> (Identity (t a) -> t a) -> Identity (t a) -> Tap t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance Morphable (Into (Preorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Preorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Preorder (Construction Maybe))) (Construction Wye) a
morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x Wye (Construction Wye a)
End) = a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Left Construction Wye a
lst)) = a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Right Construction Wye a
rst)) = a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst
	morphing ((<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) = a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
     ('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst

instance Morphable (Into (Inorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Inorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Inorder (Construction Maybe))) (Construction Wye) a
morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x Wye (Construction Wye a)
End) = a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Left Construction Wye a
lst)) = Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Right Construction Wye a
rst)) = a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst
	morphing ((<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) = Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst

instance Morphable (Into (Postorder (Construction Maybe))) (Construction Wye) where
	type Morphing (Into (Postorder (Construction Maybe))) (Construction Wye) = Construction Maybe
	morphing :: (<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Morphing
     ('Into ('Postorder (Construction Maybe))) (Construction Wye) a
morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x Wye (Construction Wye a)
End) = a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Left Construction Wye a
lst)) = Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Right Construction Wye a
rst)) = Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x
	morphing ((<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) = Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
     ('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> Construction Maybe a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point a
x

instance Morphable (Into (o ds)) (Construction Wye) => Morphable (Into (o ds)) Binary where
	type Morphing (Into (o ds)) Binary = Maybe <:.> Morphing (Into (o ds)) (Construction Wye)
	morphing :: (<:.>) (Tagged ('Into (o ds))) Binary a
-> Morphing ('Into (o ds)) Binary a
morphing ((<:.>) (Tagged ('Into (o ds))) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Binary a
xs) = (Construction Wye a
 -> Morphing ('Into (o ds)) (Construction Wye) a)
-> Maybe (Construction Wye a)
-> Maybe (Morphing ('Into (o ds)) (Construction Wye) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap (forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into (o ds)) struct =>
struct ~> Morphing ('Into (o ds)) struct
into @(o ds)) (Primary Binary a
 -> Primary
      (TU
         Covariant
         Covariant
         Maybe
         (Morphing ('Into (o ds)) (Construction Wye)))
      a)
-> Binary a
-> TU
     Covariant
     Covariant
     Maybe
     (Morphing ('Into (o ds)) (Construction Wye))
     a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Binary a
xs

instance Substructure Left (Flip Product a) where
	type Available Left (Flip Product a) = Identity
	type Substance Left (Flip Product a) = Identity
	substructure :: Lens
  (Available 'Left (Flip Product a))
  ((<:.>) (Tagged 'Left) (Flip Product a) a)
  (Substance 'Left (Flip Product a) a)
substructure = ((<:.>) (Tagged 'Left) (Flip Product a) a
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Flip Product a) a)
     (Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Flip Product a) a
  -> Store
       (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) (Flip Product a) a)
      (Identity a))
-> ((<:.>) (Tagged 'Left) (Flip Product a) a
    -> Store
         (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Flip Product a) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Flip Product a) a
product -> case Flip Product a a -> Product a a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Flip Product a a -> Product a a)
-> Flip Product a a -> Product a a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Flip Product a) a -> Flip Product a a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Left) (Flip Product a) a
product of
		a
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Left) (Flip Product a) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Left) (Flip Product a) a)
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Left) (Flip Product a) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip Product a) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
s) Identity (Identity a)
-> (Identity (Identity a)
    -> (<:.>) (Tagged 'Left) (Flip Product a) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Left) (Flip Product a) a
forall s a. s -> a -> Product s a
:*: Flip Product a a -> (<:.>) (Tagged 'Left) (Flip Product a) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Flip Product a a -> (<:.>) (Tagged 'Left) (Flip Product a) a)
-> (Identity (Identity a) -> Flip Product a a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Left) (Flip Product a) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product a a -> Flip Product a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Product a a -> Flip Product a a)
-> (Identity (Identity a) -> Product a a)
-> Identity (Identity a)
-> Flip Product a a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> a -> Product a a
forall s a. s -> a -> Product s a
:*: a
x) (a -> Product a a)
-> (Identity (Identity a) -> a)
-> Identity (Identity a)
-> Product a a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance Substructure Right (Product s) where
	type Available Right (Product s) = Identity
	type Substance Right (Product s) = Identity
	substructure :: Lens
  (Available 'Right (Product s))
  ((<:.>) (Tagged 'Right) (Product s) a)
  (Substance 'Right (Product s) a)
substructure = ((<:.>) (Tagged 'Right) (Product s) a
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) (Product s) a)
     (Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) (Product s) a
  -> Store
       (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) (Product s) a)
      (Identity a))
-> ((<:.>) (Tagged 'Right) (Product s) a
    -> Store
         (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) (Product s) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) (Product s) a
product -> case (<:.>) (Tagged 'Right) (Product s) a -> Product s a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Right) (Product s) a
product of
		s
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Right) (Product s) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Right) (Product s) a)
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Right) (Product s) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Right) (Product s) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
x) Identity (Identity a)
-> (Identity (Identity a) -> (<:.>) (Tagged 'Right) (Product s) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Right) (Product s) a
forall s a. s -> a -> Product s a
:*: Product s a -> (<:.>) (Tagged 'Right) (Product s) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Product s a -> (<:.>) (Tagged 'Right) (Product s) a)
-> (Identity (Identity a) -> Product s a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Right) (Product s) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (s
s s -> a -> Product s a
forall s a. s -> a -> Product s a
:*:) (a -> Product s a)
-> (Identity (Identity a) -> a)
-> Identity (Identity a)
-> Product s a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance Accessible s (s :*: a) where
	access :: Lens Identity (s :*: a) s
access = ((s :*: a) -> Store (Identity s) (s :*: a))
-> Lens Identity (s :*: a) s
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Identity s) (s :*: a))
 -> Lens Identity (s :*: a) s)
-> ((s :*: a) -> Store (Identity s) (s :*: a))
-> Lens Identity (s :*: a) s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
s :*: a
x) -> (((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
-> Store (Identity s) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
 -> Store (Identity s) (s :*: a))
-> (((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
-> Store (Identity s) (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ s -> Identity s
forall a. a -> Identity a
Identity s
s Identity s
-> (Identity s -> s :*: a)
-> ((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a)
forall s a. s -> a -> Product s a
:*: (s -> a -> s :*: a
forall s a. s -> a -> Product s a
:*: a
x) (s -> s :*: a) -> (Identity s -> s) -> Identity s -> s :*: a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity s -> s
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance Accessible a (s :*: a) where
	access :: Lens Identity (s :*: a) a
access = ((s :*: a) -> Store (Identity a) (s :*: a))
-> Lens Identity (s :*: a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Identity a) (s :*: a))
 -> Lens Identity (s :*: a) a)
-> ((s :*: a) -> Store (Identity a) (s :*: a))
-> Lens Identity (s :*: a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
s :*: a
x) -> (((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
-> Store (Identity a) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
 -> Store (Identity a) (s :*: a))
-> (((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
-> Store (Identity a) (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> s :*: a)
-> ((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a)
forall s a. s -> a -> Product s a
:*: (s
s s -> a -> s :*: a
forall s a. s -> a -> Product s a
:*:) (a -> s :*: a) -> (Identity a -> a) -> Identity a -> s :*: a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
	access :: Lens Identity (s :*: a) b
access = forall source. Accessible b source => Lens Identity source b
forall target source.
Accessible target source =>
Lens Identity source target
access @b Lens Identity a b
-> P_Q_T (->) Store Identity (s :*: a) a
-> Lens Identity (s :*: a) b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall source. Accessible a source => Lens Identity source a
forall target source.
Accessible target source =>
Lens Identity source target
access @a

instance (Covariant t, Covariant_ t (->) (->)) => Substructure Left (t <:.:> t := (:*:)) where
	type Available Left (t <:.:> t := (:*:)) = Identity
	type Substance Left (t <:.:> t := (:*:)) = t
	substructure :: Lens
  (Available 'Left ((t <:.:> t) := Product))
  ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
  (Substance 'Left ((t <:.:> t) := Product) a)
substructure = ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
     (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
  -> Store
       (Identity (t a))
       ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
      (t a))
-> ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
    -> Store
         (Identity (t a))
         ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
x -> case T_U Covariant Covariant Product t t a -> Product (t a) (t a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U Covariant Covariant Product t t a -> Product (t a) (t a))
-> T_U Covariant Covariant Product t t a -> Product (t a) (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
-> T_U Covariant Covariant Product t t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
ls Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
forall s a. s -> a -> Product s a
:*: T_U Covariant Covariant Product t t a
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (T_U Covariant Covariant Product t t a
 -> (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a)
-> (Identity (t a) -> T_U Covariant Covariant Product t t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := Product) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (t a -> t a -> T_U Covariant Covariant Product t t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (t a -> t a -> T_U Covariant Covariant Product t t a)
-> t a -> t a -> T_U Covariant Covariant Product t t a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a -> T_U Covariant Covariant Product t t a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> T_U Covariant Covariant Product t t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance (Covariant t, Covariant_ t (->) (->)) => Substructure Right (t <:.:> t := (:*:)) where
	type Available Right (t <:.:> t := (:*:)) = Identity
	type Substance Right (t <:.:> t := (:*:)) = t
	substructure :: Lens
  (Available 'Right ((t <:.:> t) := Product))
  ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
  (Substance 'Right ((t <:.:> t) := Product) a)
substructure = ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
     (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
  -> Store
       (Identity (t a))
       ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
      (t a))
-> ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
    -> Store
         (Identity (t a))
         ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
x -> case T_U Covariant Covariant Product t t a -> Product (t a) (t a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U Covariant Covariant Product t t a -> Product (t a) (t a))
-> T_U Covariant Covariant Product t t a -> Product (t a) (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
-> T_U Covariant Covariant Product t t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
rs Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
forall s a. s -> a -> Product s a
:*: T_U Covariant Covariant Product t t a
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (T_U Covariant Covariant Product t t a
 -> (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a)
-> (Identity (t a) -> T_U Covariant Covariant Product t t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := Product) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (t a -> t a -> T_U Covariant Covariant Product t t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome t a
ls) (t a -> T_U Covariant Covariant Product t t a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> T_U Covariant Covariant Product t t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract