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

module Pandora.Paradigm.Structure.Ability.Zipper where

import Pandora.Core.Functor (type (:=), type (:::))
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.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.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 :: * -> *) = Identity <:.:> Breadcrumbs structure := (:*:)

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

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t => Semimonoidal (<--) (:*:) (:*:) (Identity <:.:> t := (:*:)) where
	mult :: ((:=) (Identity <:.:> t) (:*:) a
 :*: (:=) (Identity <:.:> t) (:*:) b)
<-- (:=) (Identity <:.:> t) (:*:) (a :*: b)
mult = ((:=) (Identity <:.:> t) (:*:) (a :*: b)
 -> (:=) (Identity <:.:> t) (:*:) a
    :*: (:=) (Identity <:.:> t) (:*:) b)
-> ((:=) (Identity <:.:> t) (:*:) a
    :*: (:=) (Identity <:.:> t) (:*:) b)
   <-- (:=) (Identity <:.:> t) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((:=) (Identity <:.:> t) (:*:) (a :*: b)
  -> (:=) (Identity <:.:> t) (:*:) a
     :*: (:=) (Identity <:.:> t) (:*:) b)
 -> ((:=) (Identity <:.:> t) (:*:) a
     :*: (:=) (Identity <:.:> t) (:*:) b)
    <-- (:=) (Identity <:.:> t) (:*:) (a :*: b))
-> ((:=) (Identity <:.:> t) (:*:) (a :*: b)
    -> (:=) (Identity <:.:> t) (:*:) a
       :*: (:=) (Identity <:.:> t) (:*:) b)
-> ((:=) (Identity <:.:> t) (:*:) a
    :*: (:=) (Identity <:.:> t) (:*:) b)
   <-- (:=) (Identity <:.:> t) (:*:) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (Identity (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
			(Identity a :*: t a) -> (:=) (Identity <:.:> 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 -> Identity a
forall a. a -> Identity a
Identity a
x Identity a -> t a -> Identity a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
xs) (:=) (Identity <:.:> t) (:*:) a
-> (:=) (Identity <:.:> t) (:*:) b
-> (:=) (Identity <:.:> t) (:*:) a
   :*: (:=) (Identity <:.:> t) (:*:) b
forall s a. s -> a -> s :*: a
:*: (Identity b :*: t b) -> (:=) (Identity <:.:> 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 -> Identity b
forall a. a -> Identity a
Identity b
y Identity b -> t b -> Identity b :*: t b
forall s a. s -> a -> s :*: a
:*: t b
ys)

instance {-# OVERLAPS #-} Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (-->) (:*:) (:*:) (Identity <:.:> t := (:*:)) where
	unit :: Proxy (:*:)
-> (Unit (:*:) --> a) <-- (:=) (Identity <:.:> t) (:*:) a
unit Proxy (:*:)
_ = ((:=) (Identity <:.:> t) (:*:) a -> One --> a)
-> Flip (->) (One --> a) ((:=) (Identity <:.:> t) (:*:) a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((:=) (Identity <:.:> t) (:*:) a -> One --> a)
 -> Flip (->) (One --> a) ((:=) (Identity <:.:> t) (:*:) a))
-> ((:=) (Identity <:.:> t) (:*:) a -> One --> a)
-> Flip (->) (One --> a) ((:=) (Identity <:.:> t) (:*:) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (Identity 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 = Identity <:.:> (Reverse t <:.:> t := (:*:)) := (:*:)

-- 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) = Identity
	type Substance Root (Tape t) = Identity
	substructure :: Lens
  (Available 'Root (Tape t))
  ((<:.>) (Tagged 'Root) (Tape t) a)
  (Substance 'Root (Tape t) a)
substructure = ((<:.>) (Tagged 'Root) (Tape t) a
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (Tagged 'Root) (Tape t) a) (Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Root) (Tape t) a
  -> Store
       (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Root) (Tape t) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Tape t) a
    -> Store
         (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (Tagged 'Root) (Tape t) a) (Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Root) (Tape t) a
zipper -> case Tape t a
-> Identity 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
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape t a
-> Identity 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
		 Identity a
x :*: T_U Covariant Covariant (:*:) (Reverse t) t a
xs -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Root) (Tape t) a)
 -> Store
      (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Root) (Tape t) a)
-> Store (Identity (Identity a)) ((<:.>) (Tagged 'Root) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
x) Identity (Identity a)
-> (Identity (Identity a) -> (<:.>) (Tagged 'Root) (Tape t) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity 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)
-> (Identity (Identity a) -> Tape t a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity 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 ((Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
 -> Tape t a)
-> (Identity (Identity a)
    -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Identity (Identity a)
-> Tape t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> Identity 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) (Identity a
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> Identity 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
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Left (Tape t) where
	type Available Left (Tape t) = Identity
	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
      (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
       (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) (Tape t) a)
      (Reverse t a))
-> ((<:.>) (Tagged 'Left) (Tape t) a
    -> Store
         (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
-> Identity 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
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape t a
-> Identity 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
		Identity a
x :*: T_U (Reverse t a
ls :*: t a
rs) -> (((:*:) (Identity (Reverse t a)) :. (->) (Identity (Reverse t a)))
 := (<:.>) (Tagged 'Left) (Tape t) a)
-> Store
     (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Reverse t a)) :. (->) (Identity (Reverse t a)))
  := (<:.>) (Tagged 'Left) (Tape t) a)
 -> Store
      (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a))
-> (((:*:) (Identity (Reverse t a))
     :. (->) (Identity (Reverse t a)))
    := (<:.>) (Tagged 'Left) (Tape t) a)
-> Store
     (Identity (Reverse t a)) ((<:.>) (Tagged 'Left) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Reverse t a -> Identity (Reverse t a)
forall a. a -> Identity a
Identity Reverse t a
ls Identity (Reverse t a)
-> (Identity (Reverse t a) -> (<:.>) (Tagged 'Left) (Tape t) a)
-> ((:*:) (Identity (Reverse t a))
    :. (->) (Identity (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)
-> (Identity (Reverse t a) -> Tape t a)
-> Identity (Reverse t a)
-> (<:.>) (Tagged 'Left) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity 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 ((Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
 -> Tape t a)
-> (Identity (Reverse t a)
    -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Identity (Reverse t a)
-> Tape t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall s a. s -> a -> s :*: a
:*:) (T_U Covariant Covariant (:*:) (Reverse t) t a
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Identity (Reverse t a)
    -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Identity (Reverse t a)
-> Identity 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
. (Reverse t a :*: t a)
-> T_U Covariant Covariant (:*:) (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 ((Reverse t a :*: t a)
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Identity (Reverse t a) -> Reverse t a :*: t a)
-> Identity (Reverse t 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
. (Reverse t a -> t a -> Reverse t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
rs) (Reverse t a -> Reverse t a :*: t a)
-> (Identity (Reverse t a) -> Reverse t a)
-> Identity (Reverse t a)
-> Reverse t a :*: t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Reverse t a) -> Reverse t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Right (Tape t) where
	type Available Right (Tape t) = Identity
	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 (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (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 (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
 -> P_Q_T
      (->) Store Identity ((<:.>) (Tagged 'Right) (Tape t) a) (t a))
-> ((<:.>) (Tagged 'Right) (Tape t) a
    -> Store (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> P_Q_T
     (->) Store Identity ((<:.>) (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
-> Identity 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
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Tape t a
-> Identity 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
		Identity a
x :*: T_U (Reverse t a
ls :*: t a
rs) -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
 := (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
  := (<:.>) (Tagged 'Right) (Tape t) a)
 -> Store (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
    := (<:.>) (Tagged 'Right) (Tape t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Right) (Tape t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
rs Identity (t a)
-> (Identity (t a) -> (<:.>) (Tagged 'Right) (Tape t) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (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)
-> (Identity (t a) -> Tape t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Right) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Identity 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 ((Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
 -> Tape t a)
-> (Identity (t a)
    -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Identity (t a)
-> Tape t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a
forall s a. s -> a -> s :*: a
:*:) (T_U Covariant Covariant (:*:) (Reverse t) t a
 -> Identity a :*: T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Identity (t a)
    -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Identity (t a)
-> Identity 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
. (Reverse t a :*: t a)
-> T_U Covariant Covariant (:*:) (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 ((Reverse t a :*: t a)
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> (Identity (t a) -> Reverse t a :*: t a)
-> Identity (t 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
. (Reverse t a
ls Reverse t a -> t a -> Reverse t a :*: t a
forall s a. s -> a -> s :*: a
:*:) (t a -> Reverse t a :*: t a)
-> (Identity (t a) -> t a) -> Identity (t a) -> Reverse t a :*: t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Covariant (->) (->) t => Substructure Up (Tape t <::> Tape t) where
	type Available Up (Tape t <::> Tape t) = Identity
	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
      (Identity (TT Covariant Covariant t (Tape t) a))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
       (Identity (TT Covariant Covariant t (Tape t) a))
       ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
      (TT Covariant Covariant t (Tape t) a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> Store
         (Identity (TT Covariant Covariant t (Tape t) a))
         ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (:*:)
   Identity
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Identity
             ((Reverse t <:.:> t) := (:*:))
             a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
 -> Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Identity
             ((Reverse t <:.:> t) := (:*:))
             a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((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
		Identity T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
focused :*: T_U (Reverse
  t
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
d :*: t (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
u) ->
			(((:*:) (Identity (TT Covariant Covariant t (Tape t) a))
  :. (->) (Identity (TT Covariant Covariant t (Tape t) a)))
 := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (Identity (TT Covariant Covariant t (Tape t) a))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (TT Covariant Covariant t (Tape t) a))
   :. (->) (Identity (TT Covariant Covariant t (Tape t) a)))
  := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
 -> Store
      (Identity (TT Covariant Covariant t (Tape t) a))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> (((:*:) (Identity (TT Covariant Covariant t (Tape t) a))
     :. (->) (Identity (TT Covariant Covariant t (Tape t) a)))
    := (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (Identity (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
-> Identity (TT Covariant Covariant t (Tape t) a)
forall a. a -> Identity a
Identity (t (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
u) Identity (TT Covariant Covariant t (Tape t) a)
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> ((:*:) (Identity (TT Covariant Covariant t (Tape t) a))
    :. (->) (Identity (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)
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> Identity (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
   (:*:)
   Identity
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (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
. Identity
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall a. a -> Identity a
Identity T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
focused) (T_U
   Covariant
   Covariant
   (:*:)
   (Reverse t)
   t
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (TT Covariant Covariant t (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> t (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome Reverse
  t
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
d (t (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Reverse t)
      t
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> t (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (TT Covariant Covariant t (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
        (:*:)
        Identity
        ((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
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant t (Tape t) a)
    -> TT Covariant Covariant t (Tape t) a)
-> Identity (TT Covariant Covariant t (Tape t) a)
-> t (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (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) = Identity
	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
      (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
       (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
       ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Reverse t) (Tape t) a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> Store
         (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
         ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (:*:)
   Identity
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Identity
             ((Reverse t <:.:> t) := (:*:))
             a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
 -> Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U
             Covariant
             Covariant
             (:*:)
             Identity
             ((Reverse t <:.:> t) := (:*:))
             a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((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
		Identity T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
focused :*: T_U (Reverse
  t
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
d :*: t (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
u) -> 
			(((:*:) (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
  :. (->) (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)))
 := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (Identity (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 ((((:*:) (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
   :. (->) (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)))
  := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
 -> Store
      (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> (((:*:)
       (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
     :. (->) (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)))
    := (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (Identity (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
-> Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
forall a. a -> Identity a
Identity (Reverse
  t
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
d) Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> ((:*:)
      (Identity (TT Covariant Covariant (Reverse t) (Tape t) a))
    :. (->) (Identity (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)
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> Identity (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
   (:*:)
   Identity
   ((Reverse t <:.:> t) := (:*:))
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (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
. Identity
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
-> Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall a. a -> Identity a
Identity T_U
  Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
focused) (T_U
   Covariant
   Covariant
   (:*:)
   (Reverse t)
   t
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
-> t (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Reverse
   t
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> t (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Reverse t)
      t
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> t (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> Reverse
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall a b c. (a -> b -> c) -> b -> a -> c
% t (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
u) (Reverse
   t
   (T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Reverse t)
      t
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> Reverse
         t
         (T_U
            Covariant
            Covariant
            (:*:)
            Identity
            ((Reverse t <:.:> t) := (:*:))
            a))
-> Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse t)
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
        (:*:)
        Identity
        ((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
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a))
-> (Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
    -> TT Covariant Covariant (Reverse t) (Tape t) a)
-> Identity (TT Covariant Covariant (Reverse t) (Tape t) a)
-> Reverse
     t
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (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) = Identity
	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
      (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
       (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
       ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Tape t) (Reverse t) a))
-> ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a
    -> Store
         (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
         ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
  Identity
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
  (Reverse t a)
-> T_U
     Covariant Covariant (:*:) Identity ((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 (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
updated T_U
  Covariant
  Covariant
  (:*:)
  Identity
  ((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
      Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
      (Reverse t a)
 -> T_U
      Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
-> Lens
     Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
     (Reverse t a)
-> Reverse t a
-> T_U
     Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
-> T_U
     Covariant Covariant (:*:) Identity ((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 (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
      -> T_U
           Covariant
           Covariant
           (:*:)
           Identity
           ((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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
   -> T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
		(((:*:) (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
  :. (->) (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)))
 := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> Store
     (Identity (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 ((((:*:) (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
   :. (->) (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)))
  := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
 -> Store
      (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
      ((<:.>) (Tagged 'Left) (Tape t <::> Tape t) a))
-> (((:*:)
       (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
     :. (->) (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)))
    := (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> Store
     (Identity (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
-> Identity (TT Covariant Covariant (Tape t) (Reverse t) a)
forall a. a -> Identity a
Identity TT Covariant Covariant (Tape t) (Reverse t) a
target Identity (TT Covariant Covariant (Tape t) (Reverse t) a)
-> (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> (<:.>) (Tagged 'Left) (Tape t <::> Tape t) a)
-> ((:*:)
      (Identity (TT Covariant Covariant (Tape t) (Reverse t) a))
    :. (->) (Identity (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)
-> (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> (<::>) (Tape t) (Tape t) a)
-> Identity (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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)
-> (Identity (TT Covariant Covariant (Tape t) (Reverse t) a)
    -> TT Covariant Covariant (Tape t) (Reverse t) a)
-> Identity (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
. Identity (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) = Identity
	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
      (Identity (TT Covariant Covariant (Tape t) t a))
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
       (Identity (TT Covariant Covariant (Tape t) t a))
       ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
      (TT Covariant Covariant (Tape t) t a))
-> ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a
    -> Store
         (Identity (TT Covariant Covariant (Tape t) t a))
         ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (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
  Identity
  (T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     a)
  (t a)
-> T_U
     Covariant Covariant (:*:) Identity ((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 (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
updated T_U
  Covariant
  Covariant
  (:*:)
  Identity
  ((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
      Identity
      (T_U
         Covariant
         Covariant
         (:*:)
         Identity
         ((Reverse t <:.:> t) := (:*:))
         a)
      (t a)
 -> T_U
      Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
-> Lens
     Identity
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
     (t a)
-> t a
-> T_U
     Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
-> T_U
     Covariant Covariant (:*:) Identity ((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 (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Identity
      ((Reverse t <:.:> t) := (:*:))
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
      -> T_U
           Covariant
           Covariant
           (:*:)
           Identity
           ((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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (T_U
     Covariant Covariant (:*:) Identity ((Reverse t <:.:> t) := (:*:)) a
   -> T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((Reverse t <:.:> t) := (:*:))
        a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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
		(((:*:) (Identity (TT Covariant Covariant (Tape t) t a))
  :. (->) (Identity (TT Covariant Covariant (Tape t) t a)))
 := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> Store
     (Identity (TT Covariant Covariant (Tape t) t a))
     ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (TT Covariant Covariant (Tape t) t a))
   :. (->) (Identity (TT Covariant Covariant (Tape t) t a)))
  := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
 -> Store
      (Identity (TT Covariant Covariant (Tape t) t a))
      ((<:.>) (Tagged 'Right) (Tape t <::> Tape t) a))
-> (((:*:) (Identity (TT Covariant Covariant (Tape t) t a))
     :. (->) (Identity (TT Covariant Covariant (Tape t) t a)))
    := (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> Store
     (Identity (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
-> Identity (TT Covariant Covariant (Tape t) t a)
forall a. a -> Identity a
Identity TT Covariant Covariant (Tape t) t a
target Identity (TT Covariant Covariant (Tape t) t a)
-> (Identity (TT Covariant Covariant (Tape t) t a)
    -> (<:.>) (Tagged 'Right) (Tape t <::> Tape t) a)
-> ((:*:) (Identity (TT Covariant Covariant (Tape t) t a))
    :. (->) (Identity (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)
-> (Identity (TT Covariant Covariant (Tape t) t a)
    -> (<::>) (Tape t) (Tape t) a)
-> Identity (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
  (:*:)
  Identity
  ((Reverse t <:.:> t) := (:*:))
  (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Identity
     ((Reverse t <:.:> t) := (:*:))
     (T_U
        Covariant
        Covariant
        (:*:)
        Identity
        ((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)
-> (Identity (TT Covariant Covariant (Tape t) t a)
    -> TT Covariant Covariant (Tape t) t a)
-> Identity (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
. Identity (TT Covariant Covariant (Tape t) t a)
-> TT Covariant Covariant (Tape t) t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract