{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Tap where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) 
import Pandora.Paradigm.Primary.Algebraic ((-<*>-), extract)
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), twosome)
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), (%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Structure.Ability.Substructure
	(Substructure (Available, Substance, substructure), Segment (Root))

data Tap t a = Tap a (t a)

instance Covariant (->) (->) t => Covariant (->) (->) (Tap t) where
	a -> b
f -<$>- :: (a -> b) -> Tap t a -> Tap t b
-<$>- Tap a
x t a
xs = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x (t b -> Tap t b) -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- t a
xs

instance Semimonoidal (->) (:*:) (:*:) t => Semimonoidal (->) (:*:) (:*:) (Tap t) where
	multiply :: (Tap t a :*: Tap t b) -> Tap t (a :*: b)
multiply (Tap a
x t a
xs :*: Tap b
y t b
ys) = (a :*: b) -> t (a :*: b) -> Tap t (a :*: b)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y) (t (a :*: b) -> Tap t (a :*: b)) -> t (a :*: b) -> Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t a :*: t b) -> t (a :*: b)
forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
multiply ((t a :*: t b) -> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a
xs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
ys

instance Semimonoidal (<--) (:*:) (:*:) t => Semimonoidal (<--) (:*:) (:*:) (Tap t) where
	multiply :: (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
multiply = (Tap t (a :*: b) -> Tap t a :*: Tap t b)
-> (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Tap t (a :*: b) -> Tap t a :*: Tap t b)
 -> (Tap t a :*: Tap t b) <-- Tap t (a :*: b))
-> (Tap t (a :*: b) -> Tap t a :*: Tap t b)
-> (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Tap (a
x :*: b
y) t (a :*: b)
xys) -> 
		let Flip t (a :*: b) -> t a :*: t b
f = forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (<--) (:*:) (:*:) t =>
(t a :*: t b) <-- t (a :*: b)
multiply @(<--) @(:*:) @(:*:) in
		let (t a
xs :*: t b
ys) = t (a :*: b) -> t a :*: t b
forall a b. t (a :*: b) -> t a :*: t b
f t (a :*: b)
xys in a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x t a
xs Tap t a -> Tap t b -> Tap t a :*: Tap t b
forall s a. s -> a -> s :*: a
:*: b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
y t b
ys

instance Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (->) (:*:) (:*:) (Tap t) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- Tap t a
unit Proxy (:*:)
_ = (Tap t a -> One -> a) -> Flip (->) (One -> a) (Tap t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Tap t a -> One -> a) -> Flip (->) (One -> a) (Tap t a))
-> (Tap t a -> One -> a) -> Flip (->) (One -> a) (Tap t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Tap a
x t a
_) -> (\One
_ -> a
x)

instance Traversable (->) (->) t => Traversable (->) (->) (Tap t) where
	a -> u b
f <<- :: (a -> u b) -> Tap t a -> u (Tap t b)
<<- Tap a
x t a
xs = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> u b -> u (t b -> Tap t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f a
x u (t b -> Tap t b) -> u (t b) -> u (Tap t b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal source target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- t a
xs

instance (Semimonoidal (<--) (:*:) (:*:) t, Extendable (->) t, Covariant (->) (->) t) => Extendable (->) (Tap t) where
	Tap t a -> b
f <<= :: (Tap t a -> b) -> Tap t a -> Tap t b
<<= Tap t a
x = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Tap t a -> b
f Tap t a
x (t b -> Tap t b) -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Tap t a -> b
f (Tap t a -> b) -> (t a -> Tap t a) -> t a -> b
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 (Tap t a -> a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract Tap t a
x) (t a -> b) -> t a -> t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Extendable source t =>
source (t a) b -> source (t a) (t b)
<<= Tap t a -> t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower Tap t a
x

instance Lowerable (->) Tap where
	lower :: Tap u a -> u a
lower (Tap a
_ u a
xs) = u a
xs

instance Hoistable Tap where
	u ~> v
f /|\ :: (u ~> v) -> Tap u ~> Tap v
/|\ Tap a
x u a
xs = a -> v a -> Tap v a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (v a -> Tap v a) -> v a -> Tap v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# u a -> v a
u ~> v
f u a
xs

instance {-# OVERLAPS #-} Semimonoidal (->) (:*:) (:*:) t => Semimonoidal (->) (:*:) (:*:) (Tap (t <:.:> t := (:*:))) where
	multiply :: (Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
-> Tap ((t <:.:> t) := (:*:)) (a :*: b)
multiply (Tap a
x (T_U (t a
xls :*: t a
xrs)) :*: Tap b
y (T_U (t b
yls :*: t b
yrs))) = (a :*: b)
-> (:=) (t <:.:> t) (:*:) (a :*: b)
-> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y)
		((:=) (t <:.:> t) (:*:) (a :*: b)
 -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> (:=) (t <:.:> t) (:*:) (a :*: b)
-> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b)
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b))
-> (t (a :*: b) :*: t (a :*: b))
-> (:=) (t <:.:> t) (:*:) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t a :*: t b) -> t (a :*: b)
forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
multiply (t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls) t (a :*: b) -> t (a :*: b) -> t (a :*: b) :*: t (a :*: b)
forall s a. s -> a -> s :*: a
:*: (t a :*: t b) -> t (a :*: b)
forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
multiply (t a
xrs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yrs)

instance {-# OVERLAPS #-} Traversable (->) (->) t => Traversable (->) (->) (Tap (t <:.:> t := (:*:))) where
	a -> u b
f <<- :: (a -> u b)
-> Tap ((t <:.:> t) := (:*:)) a -> u (Tap ((t <:.:> t) := (:*:)) b)
<<- Tap a
x (T_U (t a
future :*: t a
past)) = (\Reverse t b
past' b
x' t b
future' -> b
-> T_U Covariant Covariant (:*:) t t b
-> Tap ((t <:.:> t) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' (T_U Covariant Covariant (:*:) t t b
 -> Tap ((t <:.:> t) := (:*:)) b)
-> T_U Covariant Covariant (:*:) t t b
-> Tap ((t <:.:> t) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t b -> t b -> T_U Covariant Covariant (:*:) t t b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (t b -> t b -> T_U Covariant Covariant (:*:) t t b)
-> t b -> t b -> T_U Covariant Covariant (:*:) t t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# t b
future' (t b -> T_U Covariant Covariant (:*:) t t b)
-> t b -> T_U Covariant Covariant (:*:) t t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Reverse t b -> Primary (Reverse t) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Reverse t b
past')
		(Reverse t b -> b -> t b -> Tap ((t <:.:> t) := (:*:)) b)
-> u (Reverse t b) -> u (b -> t b -> Tap ((t <:.:> t) := (:*:)) b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f (a -> u b) -> Reverse t a -> u (Reverse t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal source target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
past u (b -> t b -> Tap ((t <:.:> t) := (:*:)) b)
-> u b -> u (t b -> Tap ((t <:.:> t) := (:*:)) b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f a
x u (t b -> Tap ((t <:.:> t) := (:*:)) b)
-> u (t b) -> u (Tap ((t <:.:> t) := (:*:)) b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal source target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- t a
future

instance (Covariant (->) (->) t) => Substructure Root (Tap (t <:.:> t := (:*:))) where
	type Available Root (Tap (t <:.:> t := (:*:))) = Identity
	type Substance Root (Tap (t <:.:> t := (:*:))) = Identity
	substructure :: Lens
  (Available 'Root (Tap ((t <:.:> t) := (:*:))))
  ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
  (Substance 'Root (Tap ((t <:.:> t) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) 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 'Root) (Tap ((t <:.:> t) := (:*:))) a
  -> Store
       (Identity (Identity a))
       ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
    -> Store
         (Identity (Identity a))
         ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
-> Tap ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
zipper of
		Tap a
x (:=) (t <:.:> t) (:*:) a
xs -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) 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 'Root) (Tap ((t <:.:> t) := (:*:))) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
forall s a. s -> a -> s :*: a
:*: Tap ((t <:.:> t) := (:*:)) a
-> (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Tap ((t <:.:> t) := (:*:)) a
 -> (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a)
-> (Identity (Identity a) -> Tap ((t <:.:> t) := (:*:)) a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Tap ((t <:.:> t) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> (:=) (t <:.:> t) (:*:) a -> Tap ((t <:.:> t) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a -> (:=) (t <:.:> t) (:*:) a -> Tap ((t <:.:> t) := (:*:)) a)
-> (:=) (t <:.:> t) (:*:) a -> a -> Tap ((t <:.:> t) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% (:=) (t <:.:> t) (:*:) a
xs) (a -> Tap ((t <:.:> t) := (:*:)) a)
-> (Identity (Identity a) -> a)
-> Identity (Identity a)
-> Tap ((t <:.:> t) := (:*:)) 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 (Covariant (->) (->) t) => Substructure Left (Tap (t <:.:> t := (:*:))) where
	type Available Left (Tap (t <:.:> t := (:*:))) = Identity
	type Substance Left (Tap (t <:.:> t := (:*:))) = t
	substructure :: Lens
  (Available 'Left (Tap ((t <:.:> t) := (:*:))))
  ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
  (Substance 'Left (Tap ((t <:.:> t) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Tap ((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) (Tap ((t <:.:> t) := (:*:))) a
  -> Store
       (Identity (t a))
       ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
      (t a))
-> ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
    -> Store
         (Identity (t a))
         ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
-> Tap ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
zipper of
		Tap a
x (T_U (t a
future :*: t a
past)) -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Left) (Tap ((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
future Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
forall s a. s -> a -> s :*: a
:*: Tap ((t <:.:> t) := (:*:)) a
-> (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Tap ((t <:.:> t) := (:*:)) a
 -> (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a)
-> (Identity (t a) -> Tap ((t <:.:> t) := (:*:)) a)
-> Identity (t a)
-> (<:.>) (Tagged 'Left) (Tap ((t <:.:> t) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U Covariant Covariant (:*:) t t a
-> Tap ((t <:.:> t) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U Covariant Covariant (:*:) t t a
 -> Tap ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> T_U Covariant Covariant (:*:) t t a)
-> Identity (t a)
-> Tap ((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 k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: t a) -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> 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
. (t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
past) (t a -> t a :*: t a)
-> (Identity (t a) -> t a) -> Identity (t a) -> t a :*: 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 (Tap (t <:.:> t := (:*:))) where
	type Available Right (Tap (t <:.:> t := (:*:))) = Identity
	type Substance Right (Tap (t <:.:> t := (:*:))) = t
	substructure :: Lens
  (Available 'Right (Tap ((t <:.:> t) := (:*:))))
  ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
  (Substance 'Right (Tap ((t <:.:> t) := (:*:))) a)
substructure = ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) (Tap ((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) (Tap ((t <:.:> t) := (:*:))) a
  -> Store
       (Identity (t a))
       ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
      (t a))
-> ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
    -> Store
         (Identity (t a))
         ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
     (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
zipper -> case (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
-> Tap ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
zipper of
		Tap a
x (T_U (t a
future :*: t a
past)) -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
 -> Store
      (Identity (t a))
      ((<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
-> Store
     (Identity (t a))
     ((<:.>) (Tagged 'Right) (Tap ((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
past Identity (t a)
-> (Identity (t a)
    -> (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
   := (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
forall s a. s -> a -> s :*: a
:*: Tap ((t <:.:> t) := (:*:)) a
-> (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Tap ((t <:.:> t) := (:*:)) a
 -> (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a)
-> (Identity (t a) -> Tap ((t <:.:> t) := (:*:)) a)
-> Identity (t a)
-> (<:.>) (Tagged 'Right) (Tap ((t <:.:> t) := (:*:))) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U Covariant Covariant (:*:) t t a
-> Tap ((t <:.:> t) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (T_U Covariant Covariant (:*:) t t a
 -> Tap ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> T_U Covariant Covariant (:*:) t t a)
-> Identity (t a)
-> Tap ((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 k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: t a) -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> 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
. (t a
future t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*:) (t a -> t a :*: t a)
-> (Identity (t a) -> t a) -> Identity (t a) -> t a :*: 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