{-# 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