{-# 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