{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Tap where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Category ((.), ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), Covariant_ ((-<$>-)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
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.Functor.Function ((%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), twosome)
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
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 :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
xs

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 (Avoidable t, Covariant_ t (->) (->)) => Pointable (Tap t) (->) where
	point :: a -> Tap t a
point = a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a -> t a -> Tap t a) -> t a -> a -> Tap t a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
forall (t :: * -> *) a. Avoidable t => t a
empty

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

instance Applicative t => Applicative (Tap t) where
	Tap a -> b
f t (a -> b)
fs <*> :: Tap t (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)
# t (a -> b)
fs t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t a
xs

instance Traversable t => Traversable (Tap t) where
	Tap a
x t a
xs ->> :: Tap t a -> (a -> u b) -> (u :. Tap t) := b
->> a -> u b
f = 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 :: * -> *) a b. Covariant t => (a -> b) -> 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
<*> t a
xs t a -> (a -> u b) -> u (t b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u (->), Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance (Extractable t (->), Alternative t, Bindable t) => Bindable (Tap t) where
	Tap a
x t a
xs >>= :: Tap t a -> (a -> Tap t b) -> Tap t b
>>= a -> Tap t b
f = case a -> Tap t b
f a
x of ~(Tap b
y t b
ys) -> b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
y (t b -> Tap t b) -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t b
ys t b -> t b -> t b
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (t a
xs t a -> (a -> t b) -> t b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= Tap t b -> t b
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (Tap t b -> t b) -> (a -> Tap t b) -> a -> t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Tap t b
f)

instance (Extendable t, Covariant_ t (->) (->)) => Extendable (Tap t) where
	Tap t a
x =>> :: Tap t a -> (Tap t a -> b) -> Tap t b
=>> Tap t a -> b
f = 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 -> t a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower Tap t a
x t a -> (t a -> b) -> t b
forall (t :: * -> *) a b. Extendable t => t a -> (t a -> b) -> t b
=>> Tap t a -> b
f (Tap t a -> b) -> (t a -> Tap t a) -> t a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (Tap t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract 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 {-# OVERLAPS #-} Applicative t => Applicative (Tap (t <:.:> t := (:*:))) where
	Tap a -> b
f (T_U (t (a -> b)
lfs :*: t (a -> b)
rfs)) <*> :: Tap ((t <:.:> t) := (:*:)) (a -> b)
-> Tap ((t <:.:> t) := (:*:)) a -> Tap ((t <:.:> t) := (:*:)) b
<*> Tap a
x (T_U (t a
ls :*: t a
rs)) = b -> (:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> (:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b)
-> b -> (:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x ((:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b)
-> (:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Product (t b) (t b) -> (:=) (t <:.:> t) (:*:) 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)
lfs t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t a
ls t b -> t b -> Product (t b) (t b)
forall s a. s -> a -> Product s a
:*: t (a -> b)
rfs t (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t a
rs)

instance {-# OVERLAPS #-} Traversable t => Traversable (Tap (t <:.:> t := (:*:))) where
	Tap a
x (T_U (t a
future :*: t a
past)) ->> :: Tap ((t <:.:> t) := (:*:)) a
-> (a -> u b) -> (u :. Tap ((t <:.:> t) := (:*:))) := b
->> a -> u b
f = (\Reverse t b
past' b
x' t b
future' -> b -> (:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' ((:=) (t <:.:> t) (:*:) b -> Tap ((t <:.:> t) := (:*:)) b)
-> (:=) (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 <:.:> t) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (t b -> t b -> (:=) (t <:.:> t) (:*:) b)
-> t b -> t b -> (:=) (t <:.:> t) (:*:) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# t b
future' (t b -> (:=) (t <:.:> t) (:*:) b)
-> t b -> (:=) (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 :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
past Reverse t a -> (a -> u b) -> u (Reverse t b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u (->), Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f 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
<*> t a
future t a -> (a -> u b) -> u (t b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u (->), Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance (Covariant t, 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 -> Product 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.
Category 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.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance (Covariant t, 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 -> Product 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.
Category 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.
Category m =>
m b c -> m a b -> m a c
. Product (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 (Product (t a) (t a) -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> Product (t a) (t a))
-> Identity (t a)
-> T_U Covariant Covariant (:*:) t t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (t a -> t a -> Product (t a) (t a)
forall s a. s -> a -> Product s a
:*: t a
past) (t a -> Product (t a) (t a))
-> (Identity (t a) -> t a) -> Identity (t a) -> Product (t a) (t a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance (Covariant t, Covariant_ t (->) (->)) => Substructure Right (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 -> Product 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.
Category 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.
Category m =>
m b c -> m a b -> m a c
. Product (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 (Product (t a) (t a) -> T_U Covariant Covariant (:*:) t t a)
-> (Identity (t a) -> Product (t a) (t a))
-> Identity (t a)
-> T_U Covariant Covariant (:*:) t t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (t a
future t a -> t a -> Product (t a) (t a)
forall s a. s -> a -> Product s a
:*:) (t a -> Product (t a) (t a))
-> (Identity (t a) -> t a) -> Identity (t a) -> Product (t a) (t a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract