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