{-# 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 (mult))
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.Some.Store (Store (Store))
import Pandora.Paradigm.Controlflow.Effect.Interpreted ((!), (=||))
import Pandora.Paradigm.Primary.Algebraic ((<-*-), extract)
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->), (%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
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
	mult :: (Tap t a :*: Tap t b) --> Tap t (a :*: b)
mult = ((Tap t a :*: Tap t b) -> Tap t (a :*: b))
-> (Tap t a :*: Tap t b) --> Tap t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Tap t a :*: Tap t b) -> Tap t (a :*: b))
 -> (Tap t a :*: Tap t b) --> Tap t (a :*: b))
-> ((Tap t a :*: Tap t b) -> Tap t (a :*: b))
-> (Tap t a :*: Tap t b) --> Tap t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 :*: b) -> t (a :*: b) -> Tap t (a :*: b))
-> (a :*: b) -> t (a :*: b) -> Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (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)
# (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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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
	mult :: (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
mult = (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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Tap (a
x :*: b
y) t (a :*: b)
xys) -> ((Flip (:*:) (Tap t b) (t a) -> Flip (:*:) (Tap t b) (Tap t a))
-> Primary (Flip (:*:) (Tap t b)) (t a)
-> Primary (Flip (:*:) (Tap t b)) (Tap t a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) @(->) @(Flip _ _) ((t a -> Tap t a)
-> Flip (:*:) (Tap t b) (t a) -> Flip (:*:) (Tap t b) (Tap t a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) (a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x)) ((t a :*: Tap t b) -> Tap t a :*: Tap t b)
-> ((t a :*: t b) -> t a :*: Tap t b)
-> (t a :*: t b)
-> Tap t a :*: Tap t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t b -> Tap t b) -> (t a :*: t b) -> t a :*: Tap t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) (b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
y))) (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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t (a :*: b)
xys)

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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Tap a
x t a
_) -> (One -> a) -> One --> a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\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 (Straight source) (Straight 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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
	forall a. u a -> v a
f /|\ :: (forall a. u a -> v a) -> forall a. Tap u a -> Tap v a
/|\ 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
forall a. u a -> v a
f u a
xs

instance {-# OVERLAPS #-} Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (Tap (t <:.:> t := (:*:))) where
	mult :: (Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
--> Tap ((t <:.:> t) := (:*:)) (a :*: b)
mult = ((Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
 -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> (Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
   --> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
  -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
 -> (Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
    --> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> ((Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
    -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> (Tap ((t <:.:> t) := (:*:)) a :*: Tap ((t <:.:> t) := (:*:)) b)
   --> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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_U Covariant Covariant (:*:) 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_U Covariant Covariant (:*:) t t (a :*: b)
 -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> ((t (a :*: b) :*: t (a :*: b))
    -> T_U Covariant Covariant (:*:) t t (a :*: b))
-> (t (a :*: b) :*: t (a :*: b))
-> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t (a :*: b) :*: t (a :*: b))
-> T_U Covariant Covariant (:*:) 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))
 -> Tap ((t <:.:> t) := (:*:)) (a :*: b))
-> (t (a :*: b) :*: t (a :*: b))
-> Tap ((t <:.:> t) := (:*:)) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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
:*: (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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a
xrs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yrs)

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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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