{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Modification.Tape where

import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<------))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|---)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-), (<<---)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->), (%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic ((<-*-), (<-*--), (<-*---), (.-*-), extract, point)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.TT (TT (TT), type (<::>))
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.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite, (<~), (=#-))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable, Morph (Rotate), Vertical (Up, Down), Occurrence (All))
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root), sub)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Convex, view, replace, mutate)

type Tape structure = Tagged (Zippable structure)
	<:.> (Exactly <:*:> Reverse structure <:*:> structure)

instance {-# OVERLAPS #-} Traversable (->) (->) t => Traversable (->) (->) (Tape t) where
	a -> u b
f <<- :: (a -> u b) -> Tape t a -> u (Tape t b)
<<- Tape t a
z = (\Reverse t b
ls Exactly b
x t b
rs -> T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (T_U Covariant Covariant (:*:) (Reverse t) t)
  b
-> Tape t b
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (T_U Covariant Covariant (:*:) (Reverse t) t)
   b
 -> Tape t b)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) t)
     b
-> Tape t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ Exactly b
x Exactly b
-> T_U Covariant Covariant (:*:) (Reverse t) t b
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) t)
     b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> Reverse t b
ls Reverse t b -> t b -> T_U Covariant Covariant (:*:) (Reverse t) t b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t b
rs)
		(Reverse t b -> Exactly b -> t b -> Tape t b)
-> u (Reverse t b) -> u (Exactly b -> t b -> Tape 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 -> u b) -> Reverse t a -> u (Reverse 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))
<<--- Lens (Reverse t) (Tape t a) a -> Tape t a -> Reverse t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens (Reverse t) (Tape t a) a -> Tape t a -> Reverse t a)
-> Lens (Reverse t) (Tape t a) a -> Tape t a -> Reverse t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (Tape t a -> Reverse t a) -> Tape t a -> Reverse t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape t a
z
		u (Exactly b -> t b -> Tape t b)
-> u (Exactly b) -> u (t b -> Tape t b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*--- a -> u b
f (a -> u b) -> Exactly a -> u (Exactly 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))
<<--- Lens Exactly (Tape t a) a -> Tape t a -> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Exactly (Tape t a) a -> Tape t a -> Exactly a)
-> Lens Exactly (Tape t a) a -> Tape t a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root (Tape t a -> Exactly a) -> Tape t a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape t a
z
		u (t b -> Tape t b) -> u (t b) -> u (Tape t b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) 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))
<<--- Lens t (Tape t a) a -> Tape t a -> t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens t (Tape t a) a -> Tape t a -> t a)
-> Lens t (Tape t a) a -> Tape t a -> t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (Tape t a -> t a) -> Tape t a -> t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape t a
z

instance Covariant (->) (->) t => Impliable (Tape t a) where
	type Arguments (Tape t a) = a -> t a -> t a -> Tape t a
	imply :: Arguments (Tape t a)
imply a
focused t a
left t a
right = T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (T_U Covariant Covariant (:*:) (Reverse t) t)
  a
-> Tape t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (T_U Covariant Covariant (:*:) (Reverse t) t)
   a
 -> Tape t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) t)
     a
-> Tape t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ a -> Exactly a
forall a. a -> Exactly a
Exactly a
focused Exactly a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) t)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
left Reverse t a -> t a -> T_U Covariant Covariant (:*:) (Reverse t) t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) > a
<:*:> t a
right

instance Covariant (->) (->) t => Substructure Left (Tape t) where
	type Substance Left (Tape t) = Reverse t
	substructure :: Lens
  (Substance 'Left (Tape t)) ((<:.>) (Tagged 'Left) (Tape t) a) a
substructure = ((<:.>) (Tagged 'Left) (Tape t) a
 -> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->) Store (Reverse t) ((<:.>) (Tagged 'Left) (Tape t) a) 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) (Tape t) a
  -> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a))
 -> P_Q_T
      (->) Store (Reverse t) ((<:.>) (Tagged 'Left) (Tape t) a) a)
-> ((<:.>) (Tagged 'Left) (Tape t) a
    -> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->) Store (Reverse t) ((<:.>) (Tagged 'Left) (Tape t) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Left) (Tape t) a
zipper -> case (<:*:>) Exactly (Reverse t <:*:> t) a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<:*:>) Exactly (Reverse t <:*:> t) a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
    -> (<:*:>) Exactly (Reverse t <:*:> t) a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> (<:*:>) Exactly (Reverse t <:*:> t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Left) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (Tape t) a
zipper of
		Exactly a
x :*: T_U (Reverse t a
ls :*: t a
rs) -> (((:*:) (Reverse t a) :. (->) (Reverse t a))
 > (<:.>) (Tagged 'Left) (Tape t) a)
-> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Reverse t a) :. (->) (Reverse t a))
  > (<:.>) (Tagged 'Left) (Tape t) a)
 -> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a))
-> (((:*:) (Reverse t a) :. (->) (Reverse t a))
    > (<:.>) (Tagged 'Left) (Tape t) a)
-> Store (Reverse t a) ((<:.>) (Tagged 'Left) (Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Reverse t a
ls Reverse t a
-> (Reverse t a -> (<:.>) (Tagged 'Left) (Tape t) a)
-> ((:*:) (Reverse t a) :. (->) (Reverse t a))
   > (<:.>) (Tagged 'Left) (Tape t) a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> (<:.>) (Tagged 'Left) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> (<:.>) (Tagged 'Left) (Tape t) a)
-> (Reverse t a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
-> Reverse t a
-> (<:.>) (Tagged 'Left) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a
-> t a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) a
x (t a
 -> t a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> t a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> (Reverse t a -> t a)
-> Reverse t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse t a -> t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance Covariant (->) (->) t => Substructure Right (Tape t) where
	type Substance Right (Tape t) = t
	substructure :: Lens
  (Substance 'Right (Tape t)) ((<:.>) (Tagged 'Right) (Tape t) a) a
substructure = ((<:.>) (Tagged 'Right) (Tape t) a
 -> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Right) (Tape t) a) 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) (Tape t) a
  -> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a))
 -> P_Q_T (->) Store t ((<:.>) (Tagged 'Right) (Tape t) a) a)
-> ((<:.>) (Tagged 'Right) (Tape t) a
    -> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Right) (Tape t) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Right) (Tape t) a
zipper -> case (<:*:>) Exactly (Reverse t <:*:> t) a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<:*:>) Exactly (Reverse t <:*:> t) a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
    -> (<:*:>) Exactly (Reverse t <:*:> t) a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> (<:*:>) Exactly (Reverse t <:*:> t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Right) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) (Tape t) a
zipper of
		Exactly a
x :*: T_U (Reverse t a
ls :*: t a
rs) -> (((:*:) (t a) :. (->) (t a)) > (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (t a) :. (->) (t a)) > (<:.>) (Tagged 'Right) (Tape t) a)
 -> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a))
-> (((:*:) (t a) :. (->) (t a))
    > (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (t a) ((<:.>) (Tagged 'Right) (Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t a
rs t a
-> (t a -> (<:.>) (Tagged 'Right) (Tape t) a)
-> ((:*:) (t a) :. (->) (t a)) > (<:.>) (Tagged 'Right) (Tape t) a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> (<:.>) (Tagged 'Right) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> (<:.>) (Tagged 'Right) (Tape t) a)
-> (t a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
-> t a
-> (<:.>) (Tagged 'Right) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> t a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) a
x t a
ls

instance Covariant (->) (->) t => Substructure Up (Tape t <::> Tape t) where
	type Substance Up (Tape t <::> Tape t) = t <::> Tape t
	substructure :: Lens
  (Substance 'Up (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Store
      (TT Covariant Covariant t (Tape t) a)
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant t (Tape t))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     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 'Up) (Tape t <::> Tape t) a
  -> Store
       (TT Covariant Covariant t (Tape t) a)
       ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (TT Covariant Covariant t (Tape t))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> Store
         (TT Covariant Covariant t (Tape t) a)
         ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant t (Tape t))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
x -> case (<:*:>)
  Exactly
  (Reverse t <:*:> t)
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<:*:>)
   Exactly
   (Reverse t <:*:> t)
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged (Zippable t))
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> (<:*:>)
         Exactly
         (Reverse t <:*:> t)
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> (<:*:>)
      Exactly
      (Reverse t <:*:> t)
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant (Tape t) (Tape t) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged (Zippable t))
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
x of
		Exactly TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused :*: T_U (Reverse t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d :*: t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
u) ->
			(((:*:) (TT Covariant Covariant t (Tape t) a)
  :. (->) (TT Covariant Covariant t (Tape t) a))
 > (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant t (Tape t) a)
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (TT Covariant Covariant t (Tape t) a)
   :. (->) (TT Covariant Covariant t (Tape t) a))
  > (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
 -> Store
      (TT Covariant Covariant t (Tape t) a)
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> (((:*:) (TT Covariant Covariant t (Tape t) a)
     :. (->) (TT Covariant Covariant t (Tape t) a))
    > (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant t (Tape t) a)
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> TT Covariant Covariant t (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
u TT Covariant Covariant t (Tape t) a
-> (TT Covariant Covariant t (Tape t) a
    -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> ((:*:) (TT Covariant Covariant t (Tape t) a)
    :. (->) (TT Covariant Covariant t (Tape t) a))
   > (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant (Tape t) (Tape t) a
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant (Tape t) (Tape t) a
 -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> (TT Covariant Covariant t (Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant t (Tape t) a
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (TT Covariant Covariant t (Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant t (Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d (t (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant t (Tape t) a
    -> t (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant t (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant t (Tape t) a
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance Covariant (->) (->) t => Substructure Down (Tape t <::> Tape t) where
	type Substance Down (Tape t <::> Tape t) = Reverse t <::> Tape t
	substructure :: Lens
  (Substance 'Down (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Store
      (TT Covariant Covariant (Reverse t) (Tape t) a)
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant (Reverse t) (Tape t))
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     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 'Down) (Tape t <::> Tape t) a
  -> Store
       (TT Covariant Covariant (Reverse t) (Tape t) a)
       ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (TT Covariant Covariant (Reverse t) (Tape t))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> Store
         (TT Covariant Covariant (Reverse t) (Tape t) a)
         ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant (Reverse t) (Tape t))
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
ii -> case (<:*:>)
  Exactly
  (Reverse t <:*:> t)
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<:*:>)
   Exactly
   (Reverse t <:*:> t)
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged (Zippable t))
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> (<:*:>)
         Exactly
         (Reverse t <:*:> t)
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> (<:*:>)
      Exactly
      (Reverse t <:*:> t)
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant (Tape t) (Tape t) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged (Zippable t))
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
ii of
		Exactly TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused :*: T_U (Reverse
  t
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d :*: t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
u) ->
			(((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
  :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
 > (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant (Reverse t) (Tape t) a)
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
   :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
  > (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
 -> Store
      (TT Covariant Covariant (Reverse t) (Tape t) a)
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> (((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
     :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
    > (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant (Reverse t) (Tape t) a)
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Reverse
  t
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> TT Covariant Covariant (Reverse t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Reverse
  t
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d TT Covariant Covariant (Reverse t) (Tape t) a
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> ((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
    :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
   > (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant (Tape t) (Tape t) a
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant (Tape t) (Tape t) a
 -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused (t (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> t (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall a b c. (a -> b -> c) -> b -> a -> c
% t (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
u) (t (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> t (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse
  t
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Reverse
   t
   (TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> t (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> Reverse
         t
         (TU
            Covariant
            Covariant
            (Tagged (Zippable t))
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> t (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Reverse t) (Tape t) a
-> Reverse
     t
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure (All Left) (Tape t <::> Tape t) where
	type Substance (All Left) (Tape t <::> Tape t) = Tape t <::> Reverse t
	substructure :: Lens
  (Substance ('All 'Left) (Tape t <::> Tape t))
  ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
 -> Store
      ((<::>) (Tape t) (Reverse t) a)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> Reverse t)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
     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 ('All 'Left)) (Tape t <::> Tape t) a
  -> Store
       ((<::>) (Tape t) (Reverse t) a)
       ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (Tape t <::> Reverse t)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
    -> Store
         ((<::>) (Tape t) (Reverse t) a)
         ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> Reverse t)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source ->
		let target :: (<::>) (Tape t) (Reverse t) a
target = (Lens
  (Reverse t)
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> Reverse t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left) (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (Reverse t a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (Tape t <::> Tape t) a
 -> Primary (Tape t <::> Reverse t) a)
-> ((->) < (<::>) (Tape t) (Tape t) a)
   < (<::>) (Tape t) (Reverse t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source in
		let updated :: TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
new = Reverse t a
-> Lens
     (Reverse t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall (i :: * -> *) source target.
i target -> Lens i source target -> source -> source
replace (Reverse t a
 -> Lens
      (Reverse t)
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> Lens
     (Reverse t)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> Reverse t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (Reverse t a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable t))
           (Exactly <:*:> (Reverse t <:*:> t))
           a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
new TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<::>) (Tape t) (Tape t) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source in
		(((:*:) ((<::>) (Tape t) (Reverse t) a)
  :. (->) ((<::>) (Tape t) (Reverse t) a))
 > (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) (Reverse t) a)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) ((<::>) (Tape t) (Reverse t) a)
   :. (->) ((<::>) (Tape t) (Reverse t) a))
  > (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
 -> Store
      ((<::>) (Tape t) (Reverse t) a)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> (((:*:) ((<::>) (Tape t) (Reverse t) a)
     :. (->) ((<::>) (Tape t) (Reverse t) a))
    > (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) (Reverse t) a)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tape t) (Reverse t) a
target (<::>) (Tape t) (Reverse t) a
-> ((<::>) (Tape t) (Reverse t) a
    -> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> ((:*:) ((<::>) (Tape t) (Reverse t) a)
    :. (->) ((<::>) (Tape t) (Reverse t) a))
   > (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((<::>) (Tape t) (Tape t) a
 -> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> ((<::>) (Tape t) (Reverse t) a -> (<::>) (Tape t) (Tape t) a)
-> (<::>) (Tape t) (Reverse t) a
-> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (Tape t <::> Reverse t) a -> Primary (Tape t <::> Tape t) a
TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated (Primary (Tape t <::> Reverse t) a
 -> Primary (Tape t <::> Tape t) a)
-> (<::>) (Tape t) (Reverse t) a -> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-)

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure (All Right) (Tape t <::> Tape t) where
	type Substance (All Right) (Tape t <::> Tape t) = Tape t <::> t
	substructure :: Lens
  (Substance ('All 'Right) (Tape t <::> Tape t))
  ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
 -> Store
      ((<::>) (Tape t) t a)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> t)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
     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 ('All 'Right)) (Tape t <::> Tape t) a
  -> Store
       ((<::>) (Tape t) t a)
       ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (Tape t <::> t)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
    -> Store
         ((<::>) (Tape t) t a)
         ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> t)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source ->
		let target :: (<::>) (Tape t) t a
target = (Lens
  t
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right) (TU
   Covariant
   Covariant
   (Tagged (Zippable t))
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (t a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (Tape t <::> Tape t) a -> Primary (Tape t <::> t) a)
-> ((->) < (<::>) (Tape t) (Tape t) a) < (<::>) (Tape t) t a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source in
		let updated :: TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
new = t a
-> Lens
     t
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall (i :: * -> *) source target.
i target -> Lens i source target -> source -> source
replace (t a
 -> Lens
      t
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> Lens
     t
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (t a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a
      -> TU
           Covariant
           Covariant
           (Tagged (Zippable t))
           (Exactly <:*:> (Reverse t <:*:> t))
           a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
new TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     a
   -> TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<::>) (Tape t) (Tape t) a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable t))
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged (Zippable t))
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source in
			(((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
 > (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) t a)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
  > (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
 -> Store
      ((<::>) (Tape t) t a)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> (((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
    > (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) t a)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tape t) t a
target (<::>) (Tape t) t a
-> ((<::>) (Tape t) t a
    -> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> ((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
   > (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((<::>) (Tape t) (Tape t) a
 -> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> ((<::>) (Tape t) t a -> (<::>) (Tape t) (Tape t) a)
-> (<::>) (Tape t) t a
-> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (Tape t <::> t) a -> Primary (Tape t <::> Tape t) a
TU
  Covariant
  Covariant
  (Tagged (Zippable t))
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable t))
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged (Zippable t))
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated (Primary (Tape t <::> t) a -> Primary (Tape t <::> Tape t) a)
-> (<::>) (Tape t) t a -> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-)