{-# 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 (($), (#))
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
-> 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.
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
	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.
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
	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.
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
-> 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 ('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 -> ((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 ('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 -> ((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
	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 -> ((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
-> 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 ('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 -> ((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 ('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 -> ((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 ('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 -> ((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 (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