{-# 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.Pattern.Category (($), (.), (#))
import Pandora.Pattern.Functor.Covariant (Covariant (comap))
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.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)
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.PQ_ (PQ_ (PQ_))

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)
# a <:= Product s
forall (t :: * -> *) a. Extractable t => a <:= t
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 => Substructure Tail (Tap t) where
	type Substructural Tail (Tap t) = t
	substructure :: Lens
  ((<:.>) (Tagged 'Tail) (Tap t) a) (Substructural 'Tail (Tap t) a)
substructure = ((<:.>) (Tagged 'Tail) (Tap t) a
 -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> PQ_ (->) Store ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Tail) (Tap t) a
  -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a))
 -> PQ_ (->) Store ((<:.>) (Tagged 'Tail) (Tap t) a) (t a))
-> ((<:.>) (Tagged 'Tail) (Tap t) a
    -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> PQ_ (->) Store ((<:.>) (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 Tap t a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Tap t a <:= Tagged 'Tail) -> Tap t a <:= Tagged 'Tail
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 -> (((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
 -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> (((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a
xs t a
-> (t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> ((:*:) (t a) :. (->) (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)
-> (t a -> Tap t a) -> 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

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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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
forall (t :: * -> *) a. Pointable t => a :=> t
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 Substructural Left (Flip Product a) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Left) (Flip Product a) a)
  (Substructural 'Left (Flip Product a) a)
substructure = ((<:.>) (Tagged 'Left) (Flip Product a) a
 -> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> PQ_
     (->) Store ((<:.>) (Tagged 'Left) (Flip Product a) a) (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Left) (Flip Product a) a
  -> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a))
 -> PQ_
      (->) Store ((<:.>) (Tagged 'Left) (Flip Product a) a) (Identity a))
-> ((<:.>) (Tagged 'Left) (Flip Product a) a
    -> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> PQ_
     (->) Store ((<:.>) (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 a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Left) (Flip Product a) a)
-> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Left) (Flip Product a) a)
 -> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Left) (Flip Product a) a)
-> Store (Identity a) ((<:.>) (Tagged 'Left) (Flip Product a) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
s Identity a
-> (Identity a -> (<:.>) (Tagged 'Left) (Flip Product a) a)
-> ((:*:) (Identity a) :. (->) (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 a -> Flip Product a a)
-> 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 a -> Product a a) -> 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 a -> a) -> 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 :: * -> *) a. Extractable t => a <:= t
extract

instance Substructure Right (Product s) where
	type Substructural Right (Product s) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Right) (Product s) a)
  (Substructural 'Right (Product s) a)
substructure = ((<:.>) (Tagged 'Right) (Product s) a
 -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a))
-> PQ_
     (->) Store ((<:.>) (Tagged 'Right) (Product s) a) (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Right) (Product s) a
  -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a))
 -> PQ_
      (->) Store ((<:.>) (Tagged 'Right) (Product s) a) (Identity a))
-> ((<:.>) (Tagged 'Right) (Product s) a
    -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a))
-> PQ_
     (->) Store ((<:.>) (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 a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Right) (Product s) a)
-> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Right) (Product s) a)
 -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Right) (Product s) a)
-> Store (Identity a) ((<:.>) (Tagged 'Right) (Product 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 -> (<:.>) (Tagged 'Right) (Product s) a)
-> ((:*:) (Identity a) :. (->) (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 a -> Product s a)
-> 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 a -> a) -> 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 :: * -> *) a. Extractable t => a <:= t
extract

instance Accessible s (s :*: a) where
	access :: (s :*: a) :-. s
access = ((s :*: a) -> Store s (s :*: a)) -> (s :*: a) :-. s
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((s :*: a) -> Store s (s :*: a)) -> (s :*: a) :-. s)
-> ((s :*: a) -> Store s (s :*: a)) -> (s :*: a) :-. s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
s :*: a
x) -> (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a))
-> (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ s
s s -> (s -> s :*: a) -> ((:*:) s :. (->) 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)

instance Accessible a (s :*: a) where
	access :: (s :*: a) :-. a
access = ((s :*: a) -> Store a (s :*: a)) -> (s :*: a) :-. a
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((s :*: a) -> Store a (s :*: a)) -> (s :*: a) :-. a)
-> ((s :*: a) -> Store a (s :*: a)) -> (s :*: a) :-. a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(s
s :*: a
x) -> (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a))
-> (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
x a -> (a -> s :*: a) -> ((:*:) a :. (->) 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
:*:)

instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
	access :: (s :*: a) :-. b
access = forall src. Accessible b src => src :-. b
forall tgt src. Accessible tgt src => src :-. tgt
access @b (a :-. b) -> PQ_ (->) Store (s :*: a) a -> (s :*: a) :-. b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall src. Accessible a src => src :-. a
forall tgt src. Accessible tgt src => src :-. tgt
access @a