{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.Rose where

import Pandora.Core.Functor (type (:.), type (>>>))
import Pandora.Core.Interpreted (run, unite, (<~))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), identity)
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant ((<-|-))
import Pandora.Pattern.Functor.Contravariant ((>-|-))
import Pandora.Pattern.Functor.Traversable ((<<-))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((?=)))
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>), attached)
import Pandora.Paradigm.Algebraic.Functor (extract, point, empty)
import Pandora.Paradigm.Primary.Auxiliary (Vertical (Up, Down), Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (equate)
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse)
import Pandora.Paradigm.Schemes (TU (TU), TT (TT), T_U (T_U), P_Q_T (P_Q_T),  type (<::>), type (<:.>))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (view)
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Into, Rotate, Lookup, Element, Key), premorph, find)
import Pandora.Paradigm.Structure.Modification.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root, Rest, Forest), sub)
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (pop))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed)
import Pandora.Paradigm.Structure.Modification.Tape (Tape)
import Pandora.Paradigm.Structure.Some.List (List)

type Rose = Maybe <:.> Construction List

--------------------------------------- Non-empty rose tree ----------------------------------------

type instance Nonempty Rose = Construction List

--------------------------------------- Prefixed rose tree -----------------------------------------

instance Setoid k => Morphable (Lookup Key) (Prefixed Rose k) where
	type Morphing (Lookup Key) (Prefixed Rose k) = (->) (Nonempty List k) <:.> Maybe
	morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Morphing ('Lookup 'Key) (Prefixed Rose k) a
morphing (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree = case TT Covariant Covariant Rose ((:*:) k) a -> (Rose :. (:*:) k) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Rose ((:*:) k) a
 -> (Rose :. (:*:) k) >>> a)
-> TT Covariant Covariant Rose ((:*:) k) a
-> (Rose :. (:*:) k) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> TT Covariant Covariant Rose ((:*:) k) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree of
		TU Maybe (Construction List (k :*: a))
Nothing -> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) >>> a) -> TU ct cu t u a
TU ((((->) (Construction Maybe k) :. Maybe) >>> a)
 -> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Maybe a -> ((->) (Construction Maybe k) :. Maybe) >>> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant Maybe a
forall a. Maybe a
Nothing
		TU (Just Construction List (k :*: a)
tree) -> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) >>> a) -> TU ct cu t u a
TU ((((->) (Construction Maybe k) :. Maybe) >>> a)
 -> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> Construction List (k :*: a) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree (Construction Maybe k -> Construction List (k :*: a) -> Maybe a)
-> Construction List (k :*: a)
-> ((->) (Construction Maybe k) :. Maybe) >>> a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction List (k :*: a)
tree

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
--instance Setoid k => Morphable (Vary Element) (Prefixed Rose k) where
--	type Morphing (Vary Element) (Prefixed Rose k) = ((:*:) (Nonempty List k) <:.> Exactly) <:.:> Prefixed Rose k > (->)
--	morphing (run . run . premorph -> Nothing) = T_U ! \(TU (Construct key _ :*: Exactly value)) -> Prefixed . lift ! Construct (key :*: value) empty
--	morphing (run . run . premorph -> Just (Construct focused subtree)) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed . lift ! attached focused == key ? Construct (key :*: value) subtree ! Construct focused subtree
--		Construct key (Just keys) -> Prefixed . lift ! attached focused != key ? Construct focused subtree
--			! Construct focused ! vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value -#=!> subtree

---------------------------------- Non-empty prefixed rose tree ------------------------------------

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
--instance Setoid k => Morphable (Vary Element) (Prefixed (Construction List) k) where
--	type Morphing (Vary Element) (Prefixed (Construction List) k) =
--		((:*:) (Nonempty List k) <:.> Exactly) <:.:> Prefixed (Construction List) k > (->)
--	morphing (run . premorph -> Construct x (TU Nothing)) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed ! attached x == key ? Construct (key :*: value) empty ! Construct x empty
--		Construct _ (Just _) -> Prefixed ! Construct x (TU Nothing)
--	morphing (run . premorph -> Construct x (TU (Just subtree))) = T_U ! \(TU (breadcrumbs :*: Exactly value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed ! attached x != key ? Construct x # lift subtree
--			! Construct (key :*: value) (lift subtree)
--		Construct key (Just keys) -> Prefixed ! attached x != key ? Construct x # lift subtree
--			! Construct (key :*: value) . lift ! vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value -#=!> subtree

find_rose_sub_tree :: forall k a . Setoid k => Nonempty List k -> Nonempty Rose >>> k :*: a -> Maybe a
find_rose_sub_tree :: Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree (Construct k ks) Nonempty Rose >>> (k :*: a)
tree = k
k k -> k -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?= (k :*: a) -> k
forall a b. (a :*: b) -> a
attached (Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree)
	(Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- case (Maybe :. Construction Maybe) >>> k
ks of
		Just Construction Maybe k
keys -> Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree Nonempty List k
Construction Maybe k
keys (Construction List (k :*: a) -> Maybe a)
-> Maybe (Construction List (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Nonempty List k -> (Maybe :. Nonempty Rose) >>> (k :*: a)
subtree Nonempty List k
Construction Maybe k
keys
		(Maybe :. Construction Maybe) >>> k
Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (k :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((k :*: a) -> a) -> (k :*: a) -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree
	(Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Maybe a
forall a. Maybe a
Nothing where

	subtree :: Nonempty List k -> Maybe :. Nonempty Rose >>> k :*: a
	subtree :: Nonempty List k -> (Maybe :. Nonempty Rose) >>> (k :*: a)
subtree Nonempty List k
keys = forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed
  ('Find mod) struct ((Predicate <:.:> result) >>>>>> (->)) =>
Predicate a2 -> struct a2 -> result a2
forall (struct :: * -> *) (result :: * -> *) a2.
Morphed
  ('Find 'Element) struct ((Predicate <:.:> result) >>>>>> (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element
		(Predicate (Construction List (k :*: a))
 -> List (Construction List (k :*: a))
 -> Maybe (Construction List (k :*: a)))
-> Predicate (Construction List (k :*: a))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k)
-> (Construction List (k :*: a) -> k :*: a)
-> Construction List (k :*: a)
-> k
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
			(Construction List (k :*: a) -> k)
-> Predicate k -> Predicate (Construction List (k :*: a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
>-|- k :=> Predicate
forall a. Setoid a => a :=> Predicate
equate (k :=> Predicate) -> k :=> Predicate
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> k
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty List k
Construction Maybe k
keys
		(List (Construction List (k :*: a))
 -> Maybe (Construction List (k :*: a)))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Construction List (k :*: a) -> List (Construction List (k :*: a))
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree

------------------------------ Non-empty rose tree zipper -----------------------------

type Roses = List <::> Construction List

instance Zippable (Construction List) where
	type Breadcrumbs (Construction List) = Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)

-- TODO: Try to use substructure @Right . substructure @Right . substructure @Right . substructure @Right here
instance Substructure (Up Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Up Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = List <::> Tape Roses
	substructure :: Lens
  (Substance
     ('Up 'Forest)
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  ((<:.>)
     (Tagged ('Up 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Up 'Forest))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Store
      ((<::>) List (Tape Roses) a)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> P_Q_T
     (->)
     Store
     (List <::> Tape Roses)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
    (Tagged ('Up 'Forest))
    (Exactly
     <:*:> (Roses
            <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
    a
  -> Store
       ((<::>) List (Tape Roses) a)
       ((<:.>)
          (Tagged ('Up 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a))
 -> P_Q_T
      (->)
      Store
      (List <::> Tape Roses)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Up 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> Store
         ((<::>) List (Tape Roses) a)
         ((<:.>)
            (Tagged ('Up 'Forest))
            (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
            a))
-> P_Q_T
     (->)
     Store
     (List <::> Tape Roses)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
  (Tagged ('Up 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged ('Up 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
  (Tagged ('Up 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper of
		Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: T_U (Roses a
right :*: (<::>) List (Tape Roses) a
up))) ->
			(((:*:) ((<::>) List (Tape Roses) a)
  :. (->) ((<::>) List (Tape Roses) a))
 >>> (<:.>)
       (Tagged ('Up 'Forest))
       (Exactly
        <:*:> (Roses
               <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
       a)
-> Store
     ((<::>) List (Tape Roses) a)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) ((<::>) List (Tape Roses) a)
   :. (->) ((<::>) List (Tape Roses) a))
  >>> (<:.>)
        (Tagged ('Up 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
 -> Store
      ((<::>) List (Tape Roses) a)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> (((:*:) ((<::>) List (Tape Roses) a)
     :. (->) ((<::>) List (Tape Roses) a))
    >>> (<:.>)
          (Tagged ('Up 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a)
-> Store
     ((<::>) List (Tape Roses) a)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) List (Tape Roses) a
up (<::>) List (Tape Roses) a
-> ((<::>) List (Tape Roses) a
    -> (<:.>)
         (Tagged ('Up 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> ((:*:) ((<::>) List (Tape Roses) a)
    :. (->) ((<::>) List (Tape Roses) a))
   >>> (<:.>)
         (Tagged ('Up 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a
forall s a. s -> a -> s :*: a
:*: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> (<:.>)
     (Tagged ('Up 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> (<:.>)
      (Tagged ('Up 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> ((<::>) List (Tape Roses) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> (<::>) List (Tape Roses) a
-> (<:.>)
     (Tagged ('Up 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   Roses
   (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
-> ((<::>) List (Tape Roses) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a)
-> (<::>) List (Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   (Reverse Roses)
   (Roses <:*:> (List <::> Tape Roses))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Roses
      (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
      a)
-> ((<::>) List (Tape Roses) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Reverse Roses)
         (Roses <:*:> (List <::> Tape Roses))
         a)
-> (<::>) List (Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
left Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Reverse Roses)
      (Roses <:*:> (List <::> Tape Roses))
      a)
-> ((<::>) List (Tape Roses) a
    -> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a)
-> (<::>) List (Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
right Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>)

-- TODO: Try to use substructure @Left . substructure @Right here
instance Substructure (Down Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Down Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
	substructure :: Lens
  (Substance
     ('Down 'Forest)
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  ((<:.>)
     (Tagged ('Down 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Down 'Forest))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
    (Tagged ('Down 'Forest))
    (Exactly
     <:*:> (Roses
            <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
    a
  -> Store
       (Roses a)
       ((<:.>)
          (Tagged ('Down 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a))
 -> P_Q_T
      (->)
      Store
      Roses
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Down 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> Store
         (Roses a)
         ((<:.>)
            (Tagged ('Down 'Forest))
            (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
            a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
  (Tagged ('Down 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged ('Down 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
  (Tagged ('Down 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper of
		Exactly a
x :*: T_U (Roses a
down :*: (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
rest) ->
			(((:*:) (Roses a) :. (->) (Roses a))
 >>> (<:.>)
       (Tagged ('Down 'Forest))
       (Exactly
        <:*:> (Roses
               <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
       a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Roses a) :. (->) (Roses a))
  >>> (<:.>)
        (Tagged ('Down 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> (((:*:) (Roses a) :. (->) (Roses a))
    >>> (<:.>)
          (Tagged ('Down 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Roses a
down Roses a
-> (Roses a
    -> (<:.>)
         (Tagged ('Down 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> ((:*:) (Roses a) :. (->) (Roses a))
   >>> (<:.>)
         (Tagged ('Down 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a
forall s a. s -> a -> s :*: a
:*: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> (<:.>)
     (Tagged ('Down 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> (<:.>)
      (Tagged ('Down 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> (Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> Roses a
-> (<:.>)
     (Tagged ('Down 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   Roses
   (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
-> (Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a)
-> Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
-> (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
rest)

-- TODO: Try to use substructure @Left . substructure @Right . substructure @Right here
instance Substructure (Left Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Left Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Reverse Roses
	substructure :: Lens
  (Substance
     ('Left 'Forest)
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  ((<:.>)
     (Tagged ('Left 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Left 'Forest))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Store
      (Reverse Roses a)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> P_Q_T
     (->)
     Store
     (Reverse Roses)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
    (Tagged ('Left 'Forest))
    (Exactly
     <:*:> (Roses
            <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
    a
  -> Store
       (Reverse Roses a)
       ((<:.>)
          (Tagged ('Left 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a))
 -> P_Q_T
      (->)
      Store
      (Reverse Roses)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Left 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> Store
         (Reverse Roses a)
         ((<:.>)
            (Tagged ('Left 'Forest))
            (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
            a))
-> P_Q_T
     (->)
     Store
     (Reverse Roses)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
  (Tagged ('Left 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged ('Left 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
  (Tagged ('Left 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper of
		Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: (<:*:>) Roses (List <::> Tape Roses) a
rest)) ->
			(((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
 >>> (<:.>)
       (Tagged ('Left 'Forest))
       (Exactly
        <:*:> (Roses
               <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
       a)
-> Store
     (Reverse Roses a)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
  >>> (<:.>)
        (Tagged ('Left 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
 -> Store
      (Reverse Roses a)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> (((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
    >>> (<:.>)
          (Tagged ('Left 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a)
-> Store
     (Reverse Roses a)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Reverse Roses a
left Reverse Roses a
-> (Reverse Roses a
    -> (<:.>)
         (Tagged ('Left 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> ((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
   >>> (<:.>)
         (Tagged ('Left 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a
forall s a. s -> a -> s :*: a
:*: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> (<:.>)
     (Tagged ('Left 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> (<:.>)
      (Tagged ('Left 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> (Reverse Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> Reverse Roses a
-> (<:.>)
     (Tagged ('Left 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   Roses
   (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
-> (Reverse Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a)
-> Reverse Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   (Reverse Roses)
   (Roses <:*:> (List <::> Tape Roses))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Roses
      (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
      a)
-> (Reverse Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Reverse Roses)
         (Roses <:*:> (List <::> Tape Roses))
         a)
-> Reverse Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
-> (<:*:>) Roses (List <::> Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<:*:>) Roses (List <::> Tape Roses) a
rest)

-- TODO: Try to use substructure  @Left . substructure @Right . substructure @Right . substructure @Right here
instance Substructure (Right Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Right Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
	substructure :: Lens
  (Substance
     ('Right 'Forest)
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  ((<:.>)
     (Tagged ('Right 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Right 'Forest))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
    (Tagged ('Right 'Forest))
    (Exactly
     <:*:> (Roses
            <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
    a
  -> Store
       (Roses a)
       ((<:.>)
          (Tagged ('Right 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a))
 -> P_Q_T
      (->)
      Store
      Roses
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Right 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> Store
         (Roses a)
         ((<:.>)
            (Tagged ('Right 'Forest))
            (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
            a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
  (Tagged ('Right 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged ('Right 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
  (Tagged ('Right 'Forest))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
zipper of
		Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: T_U (Roses a
right :*: (<::>) List (Tape Roses) a
rest))) ->
			(((:*:) (Roses a) :. (->) (Roses a))
 >>> (<:.>)
       (Tagged ('Right 'Forest))
       (Exactly
        <:*:> (Roses
               <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
       a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Roses a) :. (->) (Roses a))
  >>> (<:.>)
        (Tagged ('Right 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a))
-> (((:*:) (Roses a) :. (->) (Roses a))
    >>> (<:.>)
          (Tagged ('Right 'Forest))
          (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
          a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Roses a
right Roses a
-> (Roses a
    -> (<:.>)
         (Tagged ('Right 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> ((:*:) (Roses a) :. (->) (Roses a))
   >>> (<:.>)
         (Tagged ('Right 'Forest))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a
forall s a. s -> a -> s :*: a
:*: T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> (<:.>)
     (Tagged ('Right 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> (<:.>)
      (Tagged ('Right 'Forest))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> (Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> Roses a
-> (<:.>)
     (Tagged ('Right 'Forest))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   Roses
   (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
-> (Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Roses
         (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
         a)
-> Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
   Covariant
   Covariant
   (:*:)
   (Reverse Roses)
   (Roses <:*:> (List <::> Tape Roses))
   a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Roses
      (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
      a)
-> (Roses a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Reverse Roses)
         (Roses <:*:> (List <::> Tape Roses))
         a)
-> Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
left Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Reverse Roses)
      (Roses <:*:> (List <::> Tape Roses))
      a)
-> (Roses a
    -> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a)
-> Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<::>) List (Tape Roses) a
rest)

instance Morphable (Into (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) (Construction List) where
	type Morphing (Into (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) (Construction List) =
		Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)
	morphing :: (<::>)
  (Tagged
     ('Into
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses
                       <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  (Construction List)
  a
-> Morphing
     ('Into
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     (Construction List)
     a
morphing (<::>)
  (Tagged
     ('Into
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses
                       <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  (Construction List)
  a
nonempty_rose_tree = case (<::>)
  (Tagged
     ('Into
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses
                       <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  (Construction List)
  a
-> Construction List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged
     ('Into
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses
                       <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  (Construction List)
  a
nonempty_rose_tree of
		Construct a
x (List :. Construction List) >>> a
xs -> a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   >>>>>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (List :. Construction List) >>> a
xs Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Reverse Roses a
forall (t :: * -> *) a. Emptiable t => t a
empty Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Roses a
forall (t :: * -> *) a. Emptiable t => t a
empty Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<::>) List (Tape Roses) a
forall (t :: * -> *) a. Emptiable t => t a
empty

instance Morphable (Rotate Up) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Morphing (Rotate Up) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) =
		Maybe <::> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))
	morphing :: (<::>)
  (Tagged ('Rotate 'Up))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> Morphing
     ('Rotate 'Up)
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
morphing ((<::>)
  (Tagged ('Rotate 'Up))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z) = ((Maybe
  :. (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
 >>> a)
-> TT
     Covariant
     Covariant
     Maybe
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     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 (((Maybe
   :. (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  >>> a)
 -> TT
      Covariant
      Covariant
      Maybe
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> ((Maybe
     :. (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
    >>> a)
-> TT
     Covariant
     Covariant
     Maybe
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (TT
   Covariant
   Covariant
   Maybe
   (Construction Maybe)
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
 :*: T_U
       Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
restruct ((TT
    Covariant
    Covariant
    Maybe
    (Construction Maybe)
    (T_U
       Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
  :*: T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
-> Maybe
     (TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (T_U
           Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
      :*: T_U
            Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (Maybe
    :. (Exactly
        <:*:> (Roses
               <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
   >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- forall a. Category (->) => a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity @(->) (Maybe
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
 -> Maybe
      (T_U
         Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> (TT
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (T_U
         Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
    :*: Maybe
          (T_U
             Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> Maybe
     (TT
        Covariant
        Covariant
        Maybe
        (Construction Maybe)
        (T_U
           Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
      :*: T_U
            Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- forall e. Stack List => (State < List e) < Topping List e
forall (structure :: * -> *) e.
Stack structure =>
(State < structure e) < Topping structure e
pop @List State
  (TT
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
  (Maybe
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> ((->)
      (TT
         Covariant
         Covariant
         Maybe
         (Construction Maybe)
         (T_U
            Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
    :. (:*:)
         (TT
            Covariant
            Covariant
            Maybe
            (Construction Maybe)
            (T_U
               Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)))
   >>> Maybe
         (T_U
            Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (<::>) List (Tape Roses) a
-> TT
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens
  (List <::> Tape Roses)
  ((<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a)
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> (<::>) List (Tape Roses) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (List <::> Tape Roses)
   ((<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
   a
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
 -> (<::>) List (Tape Roses) a)
-> Lens
     (List <::> Tape Roses)
     ((<:*:>)
        Exactly
        (Roses
         <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
        a)
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Up 'Forest) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Up 'Forest) structure
sub @(Up Forest) ((<:*:>)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> (<::>) List (Tape Roses) a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z) where

		-- TODO: Add type declaration
		restruct :: (TT
   Covariant
   Covariant
   Maybe
   (Construction Maybe)
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
 :*: T_U
       Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
restruct (TT
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
parents :*: T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent) =
			let child_node :: a
child_node = Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a) -> Exactly a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  Exactly
  ((<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a)
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Exactly
   ((<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
   a
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
 -> Exactly a)
-> Lens
     Exactly
     ((<:*:>)
        Exactly
        (Roses
         <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
        a)
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root ((<:*:>)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Exactly a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z in
			let central_children :: (List :. Construction List) >>> a
central_children = Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  Roses
  ((<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a)
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Roses
   ((<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
   a
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
 -> Roses a)
-> Lens
     Roses
     ((<:*:>)
        Exactly
        (Roses
         <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
        a)
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Down 'Forest) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Down 'Forest) structure
sub @(Down Forest) ((<:*:>)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Roses a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z in
			let left_children :: (List :. Construction List) >>> a
left_children = forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Reverse Roses a -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Reverse Roses a -> Roses a) -> Reverse Roses a -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  (Reverse Roses)
  ((<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a)
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Reverse Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Reverse Roses)
   ((<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
   a
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
 -> Reverse Roses a)
-> Lens
     (Reverse Roses)
     ((<:*:>)
        Exactly
        (Roses
         <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
        a)
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Left 'Forest) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Forest) structure
sub @(Left Forest) ((<:*:>)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Reverse Roses a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z in
			let right_children :: (List :. Construction List) >>> a
right_children = Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  Roses
  ((<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a)
  a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Roses
   ((<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a)
   a
 -> (<:*:>)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
 -> Roses a)
-> Lens
     Roses
     ((<:*:>)
        Exactly
        (Roses
         <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
        a)
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Right 'Forest) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Forest) structure
sub @(Right Forest) ((<:*:>)
   Exactly
   (Roses
    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
   a
 -> Roses a)
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
z in
			Lens
  Exactly
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Exactly
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> Exactly a)
-> Lens
     Exactly
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
     a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root (T_U
   Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> Exactly a)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
				Exactly a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
-> (<:*:>)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (((List :. Construction List) >>> a) -> Roses a)
-> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (List :. Construction List) >>> a
left_children ((List :. Construction List) >>> a)
-> ((List :. Construction List) >>> a)
-> (List :. Construction List) >>> a
forall a. Semigroup a => a -> a -> a
+ Construction List a -> (List :. Construction List) >>> a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> ((List :. Construction List) >>> a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
child_node (List :. Construction List) >>> a
central_children) ((List :. Construction List) >>> a)
-> ((List :. Construction List) >>> a)
-> (List :. Construction List) >>> a
forall a. Semigroup a => a -> a -> a
+ (List :. Construction List) >>> a
right_children
				Roses a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
-> T_U
     Covariant
     Covariant
     (:*:)
     Roses
     (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Lens
  (Reverse Roses)
  (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
  a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Reverse Roses)
   (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
   a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
 -> Reverse Roses a)
-> Lens
     (Reverse Roses)
     (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
     a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
 -> Reverse Roses a)
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  (Reverse Roses <:*:> Roses)
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Reverse Roses <:*:> Roses)
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> Lens
     (Reverse Roses <:*:> Roses)
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
     a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U
   Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
				Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse Roses)
     (Roses <:*:> (List <::> Tape Roses))
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Lens
  Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
 -> Roses a)
-> Lens
     Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a)
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  (Reverse Roses <:*:> Roses)
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
  a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Reverse Roses <:*:> Roses)
   (T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
   a
 -> T_U
      Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> Lens
     (Reverse Roses <:*:> Roses)
     (T_U
        Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
     a
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U
   Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
 -> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
				Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> TT
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite TT
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (T_U
     Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
parents