{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}

module Pandora.Paradigm.Structure.Ability.Zipper where

import Pandora.Core.Functor (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.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 ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic ((<-*-))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
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.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))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, 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)

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

type Zipper (structure :: * -> *) = 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 -> One --> a)
-> Flip (->) (One --> a) ((:=) (Exactly <:.:> t) (:*:) a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((:=) (Exactly <:.:> t) (:*:) a -> One --> a)
 -> Flip (->) (One --> a) ((:=) (Exactly <:.:> t) (:*:) a))
-> ((:=) (Exactly <:.:> t) (:*:) a -> One --> a)
-> Flip (->) (One --> a) ((:=) (Exactly <:.:> t) (:*:) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (Exactly a
x :*: t a
_)) -> (One -> a) -> 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 = Exactly <:.:> (Reverse t <:.:> t := (:*:)) := (:*:)

instance 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 = Exactly a -> (:=) (Reverse t <:.:> t) (:*:) a -> Tape t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Exactly a -> (:=) (Reverse t <:.:> t) (:*:) a -> Tape t a)
-> Exactly a -> (:=) (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 ((:=) (Reverse t <:.:> t) (:*:) a -> Tape t a)
-> (:=) (Reverse t <:.:> t) (:*:) a -> Tape t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse t a -> t a -> (:=) (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 -> (:=) (Reverse t <:.:> t) (:*:) a)
-> Reverse t a -> t a -> (:=) (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 -> (:=) (Reverse t <:.:> t) (:*:) a)
-> t a -> (:=) (Reverse t <:.:> t) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# t a
right

-- TODO: It's too fragile to define such an instance without any hints about zippers?
-- Should we wrap Zipper in Tagged Zippable?
instance Covariant (->) (->) t => Substructure Root (Tape t) where
	type Available Root (Tape t) = Exactly
	type Substance Root (Tape t) = Exactly
	substructure :: Lens
  (Available 'Root (Tape t))
  ((<:.>) (Tagged 'Root) (Tape t) a)
  (Substance 'Root (Tape t) a)
substructure = ((<:.>) (Tagged 'Root) (Tape t) a
 -> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Root) (Tape t) a) (Exactly 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 (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a))
 -> P_Q_T
      (->) Store Exactly ((<:.>) (Tagged 'Root) (Tape t) a) (Exactly a))
-> ((<:.>) (Tagged 'Root) (Tape t) a
    -> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Root) (Tape t) a) (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Root) (Tape t) a
zipper -> case Tape 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 (Tape t a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape 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 -> Tape 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 (Exactly a)) :. (->) (Exactly (Exactly a)))
 := (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
  := (<:.>) (Tagged 'Root) (Tape t) a)
 -> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> (((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
    := (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Exactly (Exactly a)) ((<:.>) (Tagged 'Root) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Exactly (Exactly a)
forall a. a -> Exactly a
Exactly (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x) Exactly (Exactly a)
-> (Exactly (Exactly a) -> (<:.>) (Tagged 'Root) (Tape t) a)
-> ((:*:) (Exactly (Exactly a)) :. (->) (Exactly (Exactly a)))
   := (<:.>) (Tagged 'Root) (Tape t) a
forall s a. s -> a -> s :*: a
:*: Tape 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 (Tape t a -> (<:.>) (Tagged 'Root) (Tape t) a)
-> (Exactly (Exactly a) -> Tape t a)
-> Exactly (Exactly a)
-> (<:.>) (Tagged 'Root) (Tape 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)
-> Tape 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)
 -> Tape t a)
-> (Exactly (Exactly a)
    -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Exactly (Exactly a)
-> Tape 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) (Exactly a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Exactly (Exactly a) -> Exactly a)
-> Exactly (Exactly 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
. Exactly (Exactly a) -> Exactly a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Left (Tape t) where
	type Available Left (Tape t) = Exactly
	type Substance Left (Tape t) = Reverse t
	substructure :: Lens
  (Available 'Left (Tape t))
  ((<:.>) (Tagged 'Left) (Tape t) a)
  (Substance 'Left (Tape t) a)
substructure = ((<:.>) (Tagged 'Left) (Tape t) a
 -> Store
      (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Left) (Tape t) a) (Reverse t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Tape t) a
  -> Store
       (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Left) (Tape t) a)
      (Reverse t a))
-> ((<:.>) (Tagged 'Left) (Tape t) a
    -> Store
         (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Left) (Tape t) a) (Reverse t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) (Tape t) a
zipper -> case Tape 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 (Tape t a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape 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 -> Tape 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) -> (((:*:) (Exactly (Reverse t a)) :. (->) (Exactly (Reverse t a)))
 := (<:.>) (Tagged 'Left) (Tape t) a)
-> Store (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (Reverse t a)) :. (->) (Exactly (Reverse t a)))
  := (<:.>) (Tagged 'Left) (Tape t) a)
 -> Store
      (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> (((:*:) (Exactly (Reverse t a)) :. (->) (Exactly (Reverse t a)))
    := (<:.>) (Tagged 'Left) (Tape t) a)
-> Store (Exactly (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse t a -> Exactly (Reverse t a)
forall a. a -> Exactly a
Exactly Reverse t a
ls Exactly (Reverse t a)
-> (Exactly (Reverse t a) -> (<:.>) (Tagged 'Left) (Tape t) a)
-> ((:*:) (Exactly (Reverse t a)) :. (->) (Exactly (Reverse t a)))
   := (<:.>) (Tagged 'Left) (Tape t) a
forall s a. s -> a -> s :*: a
:*: Tape 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 (Tape t a -> (<:.>) (Tagged 'Left) (Tape t) a)
-> (Exactly (Reverse t a) -> Tape t a)
-> Exactly (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 -> Tape t a
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) a
x (t a -> t a -> Tape t a) -> t a -> t a -> Tape t a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a -> Tape t a)
-> (Exactly (Reverse t a) -> t a)
-> Exactly (Reverse t a)
-> Tape 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 (Reverse t a -> t a)
-> (Exactly (Reverse t a) -> Reverse t a)
-> Exactly (Reverse t a)
-> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (Reverse t a) -> Reverse t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
		-- Exactly x :*: T_U (ls :*: rs) -> Store ! Exactly ls :*: lift . T_U . (Exactly x :*:) . T_U . (:*: rs) . extract

instance Covariant (->) (->) t => Substructure Right (Tape t) where
	type Available Right (Tape t) = Exactly
	type Substance Right (Tape t) = t
	substructure :: Lens
  (Available 'Right (Tape t))
  ((<:.>) (Tagged 'Right) (Tape t) a)
  (Substance 'Right (Tape t) a)
substructure = ((<:.>) (Tagged 'Right) (Tape t) a
 -> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Right) (Tape t) a) (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) (Tape t) a
  -> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
 -> P_Q_T
      (->) Store Exactly ((<:.>) (Tagged 'Right) (Tape t) a) (t a))
-> ((<:.>) (Tagged 'Right) (Tape t) a
    -> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T
     (->) Store Exactly ((<:.>) (Tagged 'Right) (Tape t) a) (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) (Tape t) a
zipper -> case Tape 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 (Tape t a
 -> Exactly a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape 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 -> Tape 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) -> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
 := (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
  := (<:.>) (Tagged 'Right) (Tape t) a)
 -> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> (((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
    := (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (Exactly (t a)) ((<:.>) (Tagged 'Right) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Exactly (t a)
forall a. a -> Exactly a
Exactly t a
rs Exactly (t a)
-> (Exactly (t a) -> (<:.>) (Tagged 'Right) (Tape t) a)
-> ((:*:) (Exactly (t a)) :. (->) (Exactly (t a)))
   := (<:.>) (Tagged 'Right) (Tape t) a
forall s a. s -> a -> s :*: a
:*: Tape 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 (Tape t a -> (<:.>) (Tagged 'Right) (Tape t) a)
-> (Exactly (t a) -> Tape t a)
-> Exactly (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 -> Tape t a
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) a
x t a
ls (t a -> Tape t a)
-> (Exactly (t a) -> t a) -> Exactly (t a) -> Tape t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Up (Tape t <::> Tape t) where
	type Available Up (Tape t <::> Tape t) = Exactly
	type Substance Up (Tape t <::> Tape t) = t <::> Tape t
	substructure :: Lens
  (Available 'Up (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
  (Substance 'Up (Tape t <::> Tape t) a)
substructure = ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Store
      (Exactly (TT Covariant Covariant t (Tape t) a))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     (TT Covariant Covariant t (Tape t) a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
  -> Store
       (Exactly (TT Covariant Covariant t (Tape t) a))
       ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
      (TT Covariant Covariant t (Tape t) a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> Store
         (Exactly (TT Covariant Covariant t (Tape t) a))
         ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     (TT Covariant Covariant t (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
x -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant Covariant (:*:) Exactly ((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) := (:*:))
   (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Exactly
             ((Reverse t <:.:> t) := (:*:))
             a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (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
. TT Covariant Covariant (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) 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
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         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
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (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
. Tagged 'Up (TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Up (TT Covariant Covariant (Tape t) (Tape t) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> Tagged 'Up (TT Covariant Covariant (Tape t) (Tape t) a))
-> (<:.>) (Tagged 'Up) (Tape 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
. (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Tagged 'Up (TT Covariant Covariant (Tape t) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Exactly
             ((Reverse t <:.:> t) := (:*:))
             a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant Covariant (:*:) 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 T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
focused :*: T_U (Reverse t (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
d :*: t (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
u) ->
			(((:*:) (Exactly (TT Covariant Covariant t (Tape t) a))
  :. (->) (Exactly (TT Covariant Covariant t (Tape t) a)))
 := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant t (Tape t) a))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (TT Covariant Covariant t (Tape t) a))
   :. (->) (Exactly (TT Covariant Covariant t (Tape t) a)))
  := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
 -> Store
      (Exactly (TT Covariant Covariant t (Tape t) a))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> (((:*:) (Exactly (TT Covariant Covariant t (Tape t) a))
     :. (->) (Exactly (TT Covariant Covariant t (Tape t) a)))
    := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant t (Tape t) a))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant t (Tape t) a
-> Exactly (TT Covariant Covariant t (Tape t) a)
forall a. a -> Exactly a
Exactly (t (T_U
     Covariant Covariant (:*:) 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 (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
u) Exactly (TT Covariant Covariant t (Tape t) a)
-> (Exactly (TT Covariant Covariant t (Tape t) a)
    -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> ((:*:) (Exactly (TT Covariant Covariant t (Tape t) a))
    :. (->) (Exactly (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)
-> (Exactly (TT Covariant Covariant t (Tape t) a)
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> Exactly (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) 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 (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (Exactly (TT Covariant Covariant t (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Exactly (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
. T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
focused t (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
d (t (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Exactly (TT Covariant Covariant t (Tape t) a)
    -> t (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Exactly (TT Covariant Covariant t (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (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
. TT Covariant Covariant t (Tape t) a
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant t (Tape t) a
 -> t (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Exactly (TT Covariant Covariant t (Tape t) a)
    -> TT Covariant Covariant t (Tape t) a)
-> Exactly (TT Covariant Covariant t (Tape t) a)
-> t (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 (TT Covariant Covariant t (Tape t) a)
-> TT Covariant Covariant t (Tape t) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Down (Tape t <::> Tape t) where
	type Available Down (Tape t <::> Tape t) = Exactly
	type Substance Down (Tape t <::> Tape t) = Reverse t <::> Tape t
	substructure :: Lens
  (Available 'Down (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
  (Substance 'Down (Tape t <::> Tape t) a)
substructure = ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Store
      (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Reverse t) (Tape t) a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
  -> Store
       (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
       ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Reverse t) (Tape t) a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> Store
         (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
         ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Reverse t) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
ii -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant Covariant (:*:) Exactly ((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) := (:*:))
   (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Exactly
             ((Reverse t <:.:> t) := (:*:))
             a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (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
. TT Covariant Covariant (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) 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
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         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
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (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
. Tagged 'Down (TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Down (TT Covariant Covariant (Tape t) (Tape t) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> Tagged 'Down (TT Covariant Covariant (Tape t) (Tape t) a))
-> (<:.>) (Tagged 'Down) (Tape 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
. (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Tagged 'Down (TT Covariant Covariant (Tape t) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Exactly
             ((Reverse t <:.:> t) := (:*:))
             a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant Covariant (:*:) 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 T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
focused :*: T_U (Reverse
  t
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
d :*: t (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
u) ->
			(((:*:) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
  :. (->) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)))
 := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (Exactly (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 ((((:*:) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
   :. (->) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)))
  := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
 -> Store
      (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> (((:*:)
       (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
     :. (->) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)))
    := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant (Reverse t) (Tape t) a
-> Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
forall a. a -> Exactly a
Exactly (Reverse
  t
  (T_U
     Covariant Covariant (:*:) 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
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
d) Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> ((:*:) (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a))
    :. (->) (Exactly (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)
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> Exactly (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) 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 (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Exactly (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
. (T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) T_U
  Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
focused (t (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> t (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall a b c. (a -> b -> c) -> b -> a -> c
% t (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
u) (t (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> t (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (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
. Reverse
  t
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> t (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Reverse
   t
   (T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
 -> t (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> Reverse
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Exactly
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
-> t (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
. TT Covariant Covariant (Reverse t) (Tape t) a
-> Reverse
     t
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant (Reverse t) (Tape t) a
 -> Reverse
      t
      (T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> TT Covariant Covariant (Reverse t) (Tape t) a)
-> Exactly (TT Covariant Covariant (Reverse t) (Tape t) a)
-> Reverse
     t
     (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 (TT Covariant Covariant (Reverse t) (Tape t) a)
-> TT Covariant Covariant (Reverse t) (Tape t) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure Left (Tape t <::> Tape t) where
	type Available Left (Tape t <::> Tape t) = Exactly
	type Substance Left (Tape t <::> Tape t) = Tape t <::> Reverse t
	substructure :: Lens
  (Available 'Left (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
  (Substance 'Left (Tape t <::> Tape t) a)
substructure = ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
 -> Store
      (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Tape t) (Reverse t) a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
  -> Store
       (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
       ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Tape t) (Reverse t) a))
-> ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
    -> Store
         (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
         ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Tape t) (Reverse t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
ii ->
		let target :: TT Covariant Covariant (Tape t) (Reverse t) a
target = (Lens
  Exactly
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
  (Reverse t a)
-> T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> Reverse t a
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Convex Lens) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left) (T_U
   Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     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 (TT Covariant Covariant (Tape t) (Reverse t)) a)
-> (<::>) (Tape t) (Tape t) a
-> TT Covariant Covariant (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 '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 'Left) (Tape t <::> Tape t) a
ii) in
		let updated :: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
updated T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
new = (forall e r. Settable (Convex Lens) => Setting (Convex Lens) e r
forall k (i :: k) e r. Settable i => Setting i e r
set @(Convex Lens) (Reverse t a
 -> Lens
      Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
      (Reverse t a)
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> Lens
     Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
     (Reverse t a)
-> Reverse t a
-> T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> T_U
     Covariant Covariant (:*:) 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)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left) (Reverse t a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
      -> T_U
           Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
   -> T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) 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
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged '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 'Left) (Tape t <::> Tape t) a
ii) in
		(((:*:) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
  :. (->) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)))
 := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
     ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
   :. (->) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)))
  := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
 -> Store
      (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> (((:*:)
       (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
     :. (->) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)))
    := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
     ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant (Tape t) (Reverse t) a
-> Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
forall a. a -> Exactly a
Exactly TT Covariant Covariant (Tape t) (Reverse t) a
target Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
-> (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> ((:*:) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a))
    :. (->) (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)))
   := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged '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 'Left) (Tape t <::> Tape t) a)
-> (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> (<::>) (Tape t) (Tape t) a)
-> Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
-> (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (TT Covariant Covariant (Tape t) (Reverse t)) a
-> Primary (Tape t <::> Tape t) a
T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
updated (Primary (TT Covariant Covariant (Tape t) (Reverse t)) a
 -> Primary (Tape t <::> Tape t) a)
-> TT Covariant Covariant (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)
=#-) (TT Covariant Covariant (Tape t) (Reverse t) a
 -> (<::>) (Tape t) (Tape t) a)
-> (Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> TT Covariant Covariant (Tape t) (Reverse t) a)
-> Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
-> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (TT Covariant Covariant (Tape t) (Reverse t) a)
-> TT Covariant Covariant (Tape t) (Reverse t) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure Right (Tape t <::> Tape t) where
	type Available Right (Tape t <::> Tape t) = Exactly
	type Substance Right (Tape t <::> Tape t) = Tape t <::> t
	substructure :: Lens
  (Available 'Right (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
  (Substance 'Right (Tape t <::> Tape t) a)
substructure = ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
 -> Store
      (Exactly (TT Covariant Covariant (Tape t) t a))
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Tape t) t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
  -> Store
       (Exactly (TT Covariant Covariant (Tape t) t a))
       ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Exactly
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Tape t) t a))
-> ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
    -> Store
         (Exactly (TT Covariant Covariant (Tape t) t a))
         ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Exactly
     ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
     (TT Covariant Covariant (Tape t) t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
ii ->
		let target :: TT Covariant Covariant (Tape t) t a
target = (Lens
  Exactly
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
  (t a)
-> T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> t a
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Convex Lens) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right) (T_U
   Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     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 (TT Covariant Covariant (Tape t) t) a)
-> (<::>) (Tape t) (Tape t) a
-> TT Covariant Covariant (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 '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 'Right) (Tape t <::> Tape t) a
ii in
		let updated :: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
updated T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (t a)
new = (forall e r. Settable (Convex Lens) => Setting (Convex Lens) e r
forall k (i :: k) e r. Settable i => Setting i e r
set @(Convex Lens) (t a
 -> Lens
      Exactly
      (T_U
         Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
      (t a)
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> Lens
     Exactly
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
     (t a)
-> t a
-> T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
-> T_U
     Covariant Covariant (:*:) 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)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right) (t a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
      -> T_U
           Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a
   -> T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) 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
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged '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 'Right) (Tape t <::> Tape t) a
ii) in
		(((:*:) (Exactly (TT Covariant Covariant (Tape t) t a))
  :. (->) (Exactly (TT Covariant Covariant (Tape t) t a)))
 := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant (Tape t) t a))
     ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Exactly (TT Covariant Covariant (Tape t) t a))
   :. (->) (Exactly (TT Covariant Covariant (Tape t) t a)))
  := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
 -> Store
      (Exactly (TT Covariant Covariant (Tape t) t a))
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> (((:*:) (Exactly (TT Covariant Covariant (Tape t) t a))
     :. (->) (Exactly (TT Covariant Covariant (Tape t) t a)))
    := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> Store
     (Exactly (TT Covariant Covariant (Tape t) t a))
     ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant (Tape t) t a
-> Exactly (TT Covariant Covariant (Tape t) t a)
forall a. a -> Exactly a
Exactly TT Covariant Covariant (Tape t) t a
target Exactly (TT Covariant Covariant (Tape t) t a)
-> (Exactly (TT Covariant Covariant (Tape t) t a)
    -> (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> ((:*:) (Exactly (TT Covariant Covariant (Tape t) t a))
    :. (->) (Exactly (TT Covariant Covariant (Tape t) t a)))
   := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged '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 'Right) (Tape t <::> Tape t) a)
-> (Exactly (TT Covariant Covariant (Tape t) t a)
    -> (<::>) (Tape t) (Tape t) a)
-> Exactly (TT Covariant Covariant (Tape t) t a)
-> (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (TT Covariant Covariant (Tape t) t) a
-> Primary (Tape t <::> Tape t) a
T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  ((Reverse t <:.:> t) := (:*:))
  (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Exactly ((Reverse t <:.:> t) := (:*:)) a)
updated (Primary (TT Covariant Covariant (Tape t) t) a
 -> Primary (Tape t <::> Tape t) a)
-> TT Covariant Covariant (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)
=#-) (TT Covariant Covariant (Tape t) t a -> (<::>) (Tape t) (Tape t) a)
-> (Exactly (TT Covariant Covariant (Tape t) t a)
    -> TT Covariant Covariant (Tape t) t a)
-> Exactly (TT Covariant Covariant (Tape t) t a)
-> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (TT Covariant Covariant (Tape t) t a)
-> TT Covariant Covariant (Tape t) t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract