{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Pandora.Paradigm.Structure.Ability.Zipper where

import Pandora.Core.Functor (type (>), type (<), type (:.), type (:::))
import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
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.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->), (%))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), type (<:*:>))
import Pandora.Paradigm.Primary.Algebraic ((<-*-), (<-*--), point)
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Primary (twosome)
import Pandora.Paradigm.Schemes.TT (TT (TT), type (<::>))
import Pandora.Paradigm.Schemes.TU (TU (TU), 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.Structure.Ability.Morphable (Morphable, Morph (Rotate), Vertical (Up, Down), Occurrence (All))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root), sub)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (<~), (=#-))
import Pandora.Paradigm.Inventory.Ability.Gettable (get)
import Pandora.Paradigm.Inventory.Ability.Settable (set)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Convex, view, replace, mutate)

class Zippable (structure :: * -> *) where
	type Breadcrumbs structure :: * -> *

type Zipper (structure :: * -> *) = Tagged Zippable <:.> (Exactly <:*:> Breadcrumbs structure)

type Breadcrumbed structure t = (Zippable structure, Breadcrumbs structure ~ t)

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t
	=> Semimonoidal (<--) (:*:) (:*:) (Exactly <:.:> t > (:*:)) where
	mult :: ((>) (Exactly <:.:> t) (:*:) a :*: (>) (Exactly <:.:> t) (:*:) b)
<-- (>) (Exactly <:.:> t) (:*:) (a :*: b)
mult = ((>) (Exactly <:.:> t) (:*:) (a :*: b)
 -> (>) (Exactly <:.:> t) (:*:) a :*: (>) (Exactly <:.:> t) (:*:) b)
-> ((>) (Exactly <:.:> t) (:*:) a
    :*: (>) (Exactly <:.:> t) (:*:) b)
   <-- (>) (Exactly <:.:> t) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((>) (Exactly <:.:> t) (:*:) (a :*: b)
  -> (>) (Exactly <:.:> t) (:*:) a :*: (>) (Exactly <:.:> t) (:*:) b)
 -> ((>) (Exactly <:.:> t) (:*:) a
     :*: (>) (Exactly <:.:> t) (:*:) b)
    <-- (>) (Exactly <:.:> t) (:*:) (a :*: b))
-> ((>) (Exactly <:.:> t) (:*:) (a :*: b)
    -> (>) (Exactly <:.:> t) (:*:) a :*: (>) (Exactly <:.:> t) (:*:) b)
-> ((>) (Exactly <:.:> t) (:*:) a
    :*: (>) (Exactly <:.:> t) (:*:) b)
   <-- (>) (Exactly <:.:> t) (:*:) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (Exactly (a
x :*: b
y) :*: t (a :*: b)
xys)) ->
		let t a
xs :*: t b
ys = 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 in
			(Exactly a :*: t a) -> (>) (Exactly <:.:> 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 (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a -> t a -> Exactly a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
xs) (>) (Exactly <:.:> t) (:*:) a
-> (>) (Exactly <:.:> t) (:*:) b
-> (>) (Exactly <:.:> t) (:*:) a :*: (>) (Exactly <:.:> t) (:*:) b
forall s a. s -> a -> s :*: a
:*: (Exactly b :*: t b) -> (>) (Exactly <:.:> t) (:*:) b
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (b -> Exactly b
forall a. a -> Exactly a
Exactly b
y Exactly b -> t b -> Exactly b :*: t b
forall s a. s -> a -> s :*: a
:*: t b
ys)

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (-->) (:*:) (:*:) (Exactly <:.:> t > (:*:)) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- (>) (Exactly <:.:> t) (:*:) a
unit Proxy (:*:)
_ = ((>) (Exactly <:.:> t) (:*:) a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((>) (Exactly <:.:> t) (:*:) a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((>) (Exactly <:.:> t) (:*:) a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) ((>) (Exactly <:.:> t) (:*:) a))
-> ((>) (Exactly <:.:> t) (:*:) a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((>) (Exactly <:.:> t) (:*:) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (Exactly a
x :*: t a
_)) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

type family Fastenable structure rs where
	Fastenable structure (r ::: rs) = (Morphable < Rotate r < structure, Fastenable structure rs)
	Fastenable structure r = Morphable < Rotate r < structure

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

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)
<---- 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
twosome (Exactly a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U Covariant Covariant (:*:) (Reverse t) t)
      a)
-> Exactly a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) 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 
			(T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U Covariant Covariant (:*:) (Reverse t) t)
      a)
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U Covariant Covariant (:*:) (Reverse t) t)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- 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
twosome (Reverse t a
 -> t a -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Reverse t a
-> t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
left (t a -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> t a -> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- t a
right

-- TODO: Isn't too fragile to define such an instance without any hints about zippers?
instance Covariant (->) (->) t => Substructure Root (Tape t) where
	type Substance Root (Tape t) = Exactly
	substructure :: Lens
  (Substance 'Root (Tape t)) ((<:.>) (Tagged 'Root) (Tape t) a) a
substructure = ((<:.>) (Tagged 'Root) (Tape t) a
 -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T (->) Store Exactly ((<:.>) (Tagged 'Root) (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 'Root) (Tape t) a
  -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Tape t) a))
 -> P_Q_T (->) Store Exactly ((<:.>) (Tagged 'Root) (Tape t) a) a)
-> ((<:.>) (Tagged 'Root) (Tape t) a
    -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T (->) Store Exactly ((<:.>) (Tagged 'Root) (Tape t) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Root) (Tape t) a
zipper -> case T_U Covariant Covariant (:*:) 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 (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
      a
    -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (T_U Covariant Covariant (:*:) 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_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
  a
-> T_U Covariant Covariant (:*:) 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_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
   a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (T_U Covariant Covariant (:*:) 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 'Root) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (T_U Covariant Covariant (:*:) 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 'Root) (Tape t) a
zipper of
		 Exactly a
x :*: T_U Covariant Covariant (:*:) (Reverse t) t a
xs -> (((:*:) (Exactly a) :. (->) (Exactly a))
 > (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Exactly a) ((<:.>) (Tagged 'Root) (Tape t) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Exactly a) :. (->) (Exactly a))
  > (<:.>) (Tagged 'Root) (Tape t) a)
 -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Tape t) a))
-> (((:*:) (Exactly a) :. (->) (Exactly a))
    > (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Exactly a) ((<:.>) (Tagged 'Root) (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
x Exactly a
-> (Exactly a -> (<:.>) (Tagged 'Root) (Tape t) a)
-> ((:*:) (Exactly a) :. (->) (Exactly a))
   > (<:.>) (Tagged 'Root) (Tape t) a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged Zippable)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
  a
-> (<:.>) (Tagged 'Root) (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_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
   a
 -> (<:.>) (Tagged 'Root) (Tape t) a)
-> (Exactly a
    -> TU
         Covariant
         Covariant
         (Tagged Zippable)
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
         a)
-> Exactly a
-> (<:.>) (Tagged 'Root) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> 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 (Reverse t <:*:> t) a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
      a)
-> (Exactly a
    -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> Exactly a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse 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 ((Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> (Exactly a
    -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Exactly a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Exactly a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) (Reverse t) t a
xs)

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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
    -> (<:*:>) Exactly (Reverse t <:*:> t) a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
  (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
     (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)
  (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> (<:.>) (Tagged 'Left) (Tape t) a)
-> (Reverse t a
    -> TU
         Covariant
         Covariant
         (Tagged Zippable)
         (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)
     (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> t a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> (Reverse t a -> t a)
-> Reverse t a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
    -> (<:*:>) Exactly (Reverse t <:*:> t) a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
  (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
     (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)
  (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> (<:.>) (Tagged 'Right) (Tape t) a)
-> (t a
    -> TU
         Covariant
         Covariant
         (Tagged Zippable)
         (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)
     (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged Zippable)
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> (<:*:>)
         Exactly
         (Reverse t <:*:> t)
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> (<:*:>)
      Exactly
      (Reverse t <:*:> t)
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged Zippable)
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused :*: T_U (Reverse t (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d :*: t (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
     (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)
     (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused t (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d (t (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant t (Tape t) a
    -> t (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant t (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> Exactly
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged Zippable)
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> (<:*:>)
         Exactly
         (Reverse t <:*:> t)
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> (<:*:>)
      Exactly
      (Reverse t <:*:> t)
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> (<:*:>)
     Exactly
     (Reverse t <:*:> t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (TU
             Covariant
             Covariant
             (Tagged Zippable)
             (Exactly <:*:> (Reverse t <:*:> t))
             a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused :*: T_U (Reverse
  t
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
d :*: t (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
     (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)
     (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  a
focused (t (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> t (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall a b c. (a -> b -> c) -> b -> a -> c
% t (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
u) (t (TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> t (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
 -> t (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> Reverse
         t
         (TU
            Covariant
            Covariant
            (Tagged Zippable)
            (Exactly <:*:> (Reverse t <:*:> t))
            a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> t (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
new = Reverse t a
-> Lens
     (Reverse t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> Lens
     (Reverse t)
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> Reverse t a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a
      -> TU
           Covariant
           Covariant
           (Tagged Zippable)
           (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
new TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
   -> TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (Reverse t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
     (Exactly <:*:> (Reverse t <:*:> t))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
   (Exactly <:*:> (Reverse t <:*:> t))
   a
 -> t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
updated TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
new = t a
-> Lens
     t
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
         (Exactly <:*:> (Reverse t <:*:> t))
         a)
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> Lens
     t
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
     a
-> t a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      a
 -> TU
      Covariant
      Covariant
      (Tagged Zippable)
      (Exactly <:*:> (Reverse t <:*:> t))
      a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a
      -> TU
           Covariant
           Covariant
           (Tagged Zippable)
           (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
new TU
  Covariant
  Covariant
  (Tagged Zippable)
  (Exactly <:*:> (Reverse t <:*:> t))
  (TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     a
   -> TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (Exactly <:*:> (Reverse t <:*:> t))
        a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
      (Exactly <:*:> (Reverse t <:*:> t))
      (TU
         Covariant
         Covariant
         (Tagged Zippable)
         (Exactly <:*:> (Reverse t <:*:> t))
         a))
-> (<::>) (Tape t) (Tape t) a
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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)
  (Exactly <:*:> (Reverse t <:*:> t))
  (t a)
-> TU
     Covariant
     Covariant
     (Tagged Zippable)
     (Exactly <:*:> (Reverse t <:*:> t))
     (TU
        Covariant
        Covariant
        (Tagged Zippable)
        (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
=#-)