{-# 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.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply_))
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 ((-<*>-))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), twosome)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
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 (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- t a
xs

instance (Covariant t (->) (->)) => Extractable (Tap t) (->) where
	extract :: Tap t a -> a
extract (Tap a
x t a
_) = a
x

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 (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
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 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 (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
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.
Applicative_ t =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Traversable t source target, Covariant u source target,
 Pointable u target, Semimonoidal u target (:*:) (:*:)) =>
source a (u b) -> target (t a) (u (t b))
<<- t a
xs

instance (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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Tap t a
x) (t a -> b) -> t a -> t b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Extendable t source =>
source (t a) b -> source (t a) (t b)
<<= Tap t a -> t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u (->) (->)) =>
t u ~> u
lower Tap t a
x

instance Lowerable Tap where
	lower :: Tap u ~> u
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 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 (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
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 (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
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 (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f (a -> u b) -> Reverse t a -> u (Reverse t b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Traversable t source target, Covariant u source target,
 Pointable u target, Semimonoidal u target (:*:) (:*:)) =>
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.
Applicative_ 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.
Applicative_ t =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Traversable t source target, Covariant u source target,
 Pointable u target, Semimonoidal u target (:*:) (:*:)) =>
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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u (->) (->)) =>
t u ~> u
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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u (->) (->)) =>
u ~> t u
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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance (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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u (->) (->)) =>
t u ~> u
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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u (->) (->)) =>
u ~> t u
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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u (->) (->)) =>
t u ~> u
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 (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u (->) (->)) =>
u ~> t u
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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract