{-# LANGUAGE UndecidableInstances #-}
{-# 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.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
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.Algebraic.Product ((:*:) ((:*:)), attached, twosome)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic (extract)
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.Wye (Wye (Both, Left, Right, End))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Pattern.Morphism.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 :: * -> *) a. Extractable t => 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) => 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 :: * -> *) a. Extractable t => 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 -> Tagged 'Tail (Tap t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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 -> s :*: a
:*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
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.
Semigroupoid 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => 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
nonempty_binary = case (<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph (<:.>)
  (Tagged ('Into ('Preorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		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
		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.
Semigroupoid 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
		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.
Semigroupoid 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
		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.
Semigroupoid 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
nonempty_binary = case (<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph (<:.>)
  (Tagged ('Into ('Inorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		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
		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 -> ((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
		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
forall a. Maybe a
Nothing 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
		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 -> ((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 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
nonempty_binary = case (<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph (<:.>)
  (Tagged ('Into ('Postorder (Construction Maybe))))
  (Construction Wye)
  a
nonempty_binary of
		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
		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 -> ((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
		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 -> ((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
		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 -> ((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

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) = (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) (Construction Wye a
 -> Morphing ('Into (o ds)) (Construction Wye) a)
-> Maybe (Construction Wye a)
-> Maybe (Morphing ('Into (o ds)) (Construction Wye) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (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 (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= Binary a
xs

instance Substructure Left (Flip (:*:) a) where
	type Available Left (Flip (:*:) a) = Identity
	type Substance Left (Flip (:*:) a) = Identity
	substructure :: Lens
  (Available 'Left (Flip (:*:) a))
  ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
  (Substance 'Left (Flip (:*:) a) a)
substructure = ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Flip (:*:) 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 (:*:) a) a
  -> Store
       (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
      (Identity a))
-> ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
    -> Store
         (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Flip (:*:) a) a
product -> case Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip (:*:) a a -> a :*: a) -> Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Flip (:*:) a) a -> Flip (:*:) a a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (Flip (:*:) a) a
product of
		a
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) 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 (:*:) a) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall s a. s -> a -> s :*: a
:*: Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> (Identity (Identity a) -> Flip (:*:) a a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((a :*: a) -> Flip (:*:) a a)
-> (Identity (Identity a) -> a :*: a)
-> Identity (Identity a)
-> Flip (:*:) a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (a -> a :*: a)
-> (Identity (Identity a) -> a) -> Identity (Identity a) -> a :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Substructure Right ((:*:) s) where
	type Available Right ((:*:) s) = Identity
	type Substance Right ((:*:) s) = Identity
	substructure :: Lens
  (Available 'Right ((:*:) s))
  ((<:.>) (Tagged 'Right) ((:*:) s) a)
  (Substance 'Right ((:*:) s) a)
substructure = ((<:.>) (Tagged 'Right) ((:*:) s) a
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((:*:) 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) ((:*:) s) a
  -> Store
       (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) ((:*:) s) a)
      (Identity a))
-> ((<:.>) (Tagged 'Right) ((:*:) s) a
    -> Store
         (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((:*:) s) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) ((:*:) s) a
product -> case (<:.>) (Tagged 'Right) ((:*:) s) a -> s :*: a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((:*:) s) a
product of
		s
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Right) ((:*:) s) a)
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store
     (Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) 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) ((:*:) s) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Right) ((:*:) s) a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a)
-> (Identity (Identity a) -> s :*: a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a)
-> (Identity (Identity a) -> a) -> Identity (Identity a) -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => 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 -> s :*: a
:*: (s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s -> s :*: a) -> (Identity s -> s) -> Identity s -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity s -> s
forall (t :: * -> *) a. Extractable t => 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 -> s :*: a
:*: (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a) -> (Identity a -> a) -> Identity a -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => 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.
Semigroupoid 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 Accessible a (Identity a) where
	access :: Lens Identity (Identity a) a
access = (Identity a -> Store (Identity a) (Identity a))
-> Lens Identity (Identity 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 ((Identity a -> Store (Identity a) (Identity a))
 -> Lens Identity (Identity a) a)
-> (Identity a -> Store (Identity a) (Identity a))
-> Lens Identity (Identity a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Identity a
x) -> (((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
-> Store (Identity a) (Identity a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
 -> Store (Identity a) (Identity a))
-> (((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
-> Store (Identity a) (Identity 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 -> Identity a)
-> ((:*:) (Identity a) :. (->) (Identity a)) := Identity a
forall s a. s -> a -> s :*: a
:*: Identity a -> Identity a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance Possible a (Maybe a) where
	perhaps :: Lens Maybe (Maybe a) a
perhaps = (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe 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 ((Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a)
-> (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \Maybe a
x -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
 -> Store (Maybe a) (Maybe a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Maybe a
x Maybe a
-> (Maybe a -> Maybe a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a
forall s a. s -> a -> s :*: a
:*: Maybe a -> Maybe a
forall (m :: * -> * -> *) a. Category m => m a a
identity

instance Accessible target source => Possible target (Maybe source) where
	perhaps :: Lens Maybe (Maybe source) target
perhaps = let lst :: Lens Identity source target
lst = Accessible target source => Lens Identity source target
forall target source.
Accessible target source =>
Lens Identity source target
access @target @source in (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Maybe source -> Store (Maybe target) (Maybe source))
 -> Lens Maybe (Maybe source) target)
-> (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case
		Just source
source -> let (Identity target
target :*: Identity target -> source
its) = Store (Identity target) source
-> Identity target :*: (Identity target -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Identity target) source
 -> Identity target :*: (Identity target -> source))
-> Store (Identity target) source
-> Identity target :*: (Identity target -> source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Lens Identity source target
lst Lens Identity source target
-> source -> Store (Identity target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source in
			(((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
 -> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ target -> Maybe target
forall a. a -> Maybe a
Just target
target Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: (Identity target -> source
its (Identity target -> source)
-> (target -> Identity target) -> target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. target -> Identity target
forall a. a -> Identity a
Identity (target -> source) -> Maybe target -> Maybe source
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Maybe source
Nothing -> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
 -> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Maybe target
forall a. Maybe a
Nothing Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: \Maybe target
_ -> Maybe source
forall a. Maybe a
Nothing

instance Accessible (Maybe target) source => Possible target source where
	perhaps :: Lens Maybe source target
perhaps = let lst :: Lens Identity source (Maybe target)
lst = Accessible (Maybe target) source =>
Lens Identity source (Maybe target)
forall target source.
Accessible target source =>
Lens Identity source target
access @(Maybe target) @source in (source -> Store (Maybe target) source) -> Lens Maybe source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Maybe target) source)
 -> Lens Maybe source target)
-> (source -> Store (Maybe target) source)
-> Lens Maybe source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source ->
		let Identity (Maybe target)
target :*: Identity (Maybe target) -> source
imts = Store (Identity (Maybe target)) source
-> Identity (Maybe target) :*: (Identity (Maybe target) -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Identity (Maybe target)) source
 -> Identity (Maybe target) :*: (Identity (Maybe target) -> source))
-> Store (Identity (Maybe target)) source
-> Identity (Maybe target) :*: (Identity (Maybe target) -> source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Lens Identity source (Maybe target)
lst Lens Identity source (Maybe target)
-> source -> Store (Identity (Maybe target)) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source in
			(((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity (Maybe target) -> Maybe target
forall (t :: * -> *) a. Extractable t => t a -> a
extract Identity (Maybe target)
target Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: Identity (Maybe target) -> source
imts (Identity (Maybe target) -> source)
-> (Maybe target -> Identity (Maybe target))
-> Maybe target
-> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe target -> Identity (Maybe target)
forall a. a -> Identity a
Identity

instance (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) := (:*:)))
  ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
  (Substance 'Left ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
 -> Store
      (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) ((t <:.:> 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 'Left) ((t <:.:> t) := (:*:)) a
  -> Store
       (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
      (t a))
-> ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
    -> Store
         (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x -> case T_U Covariant Covariant (:*:) t t a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U Covariant Covariant (:*:) t t a -> t a :*: t a)
-> T_U Covariant Covariant (:*:) t t a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> T_U Covariant Covariant (:*:) t t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
 -> Store
      (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> 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
ls Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t t a
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t t a
 -> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> T_U Covariant Covariant (:*:) t t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> T_U Covariant Covariant (:*:) t t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (t a -> t a -> T_U Covariant Covariant (:*:) t t a)
-> t a -> t a -> T_U Covariant Covariant (:*:) t t a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> T_U Covariant Covariant (:*:) t t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance (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) := (:*:)))
  ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
  (Substance 'Right ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
 -> Store
      (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((t <:.:> 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 'Right) ((t <:.:> t) := (:*:)) a
  -> Store
       (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
      (t a))
-> ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
    -> Store
         (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x -> case T_U Covariant Covariant (:*:) t t a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U Covariant Covariant (:*:) t t a -> t a :*: t a)
-> T_U Covariant Covariant (:*:) t t a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> T_U Covariant Covariant (:*:) t t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x of
		t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
 -> Store
      (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
     (Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> 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
rs Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t t a
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t t a
 -> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> T_U Covariant Covariant (:*:) t t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> T_U Covariant Covariant (:*:) t t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome t a
ls) (t a -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> T_U Covariant Covariant (:*:) t t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract