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

import Pandora.Core.Functor (type (:.), type (>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant ((<-|-), (<-|-|-))
import Pandora.Pattern.Functor.Contravariant ((>-|-))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Transformer.Hoistable ((/|\))
import Pandora.Pattern.Object.Setoid (Setoid ((==), (!=), (?=)))
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic (extract, empty, (>-||-))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>), attached)
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic (extract, point)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True))
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.Functor.Tagged (Tagged)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
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.Controlflow.Effect.Interpreted (run, unite, (<~), (=#-), (<~~~~))
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), Vertical (Up, Down), premorph, find)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure)
	, Segment (Root, Rest, Forest), sub, tagstruct)
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (pop, push))
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 Prefixed Rose k a -> (Rose :. (:*:) k) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Prefixed Rose k a -> (Rose :. (:*:) k) > a)
-> Prefixed 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
-> Prefixed 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) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Up Forest) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = List <::> Tape Roses
	substructure :: Lens
  (Substance
     ('Up 'Forest)
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses
                          <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  ((<:.>)
     (Tagged ('Up 'Forest))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Up 'Forest))
   (Tagged (Zippable structure)
    <:.> (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
   a
 -> Store
      ((<::>) List (Tape Roses) a)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> P_Q_T
     (->)
     Store
     (List <::> Tape Roses)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
    (Tagged (Zippable structure)
     <:.> (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
    a
  -> Store
       ((<::>) List (Tape Roses) a)
       ((<:.>)
          (Tagged ('Up 'Forest))
          (Tagged (Zippable structure)
           <:.> (Exactly
                 <:*:> (Roses
                        <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
          a))
 -> P_Q_T
      (->)
      Store
      (List <::> Tape Roses)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Up 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a
    -> Store
         ((<::>) List (Tape Roses) a)
         ((<:.>)
            (Tagged ('Up 'Forest))
            (Tagged (Zippable structure)
             <:.> (Exactly
                   <:*:> (Roses
                          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
            a))
-> P_Q_T
     (->)
     Store
     (List <::> Tape Roses)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
  (Tagged (Zippable structure)
   <:.> (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)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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 :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (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))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
-> Store
     ((<::>) List (Tape Roses) a)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
 -> Store
      ((<::>) List (Tape Roses) a)
      ((<:.>)
         (Tagged ('Up 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> (((:*:) ((<::>) List (Tape Roses) a)
     :. (->) ((<::>) List (Tape Roses) a))
    > (<:.>)
        (Tagged ('Up 'Forest))
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
        a)
-> Store
     ((<::>) List (Tape Roses) a)
     ((<:.>)
        (Tagged ('Up 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
-> ((:*:) ((<::>) List (Tape Roses) a)
    :. (->) ((<::>) List (Tape Roses) a))
   > (<:.>)
       (Tagged ('Up 'Forest))
       (Tagged (Zippable structure)
        <:.> (Exactly
              <:*:> (Roses
                     <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
       a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> (<:.>)
     (Tagged ('Up 'Forest))
     (Tagged (Zippable structure)
      <:.> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> (<:.>)
      (Tagged ('Up 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> ((<::>) List (Tape Roses) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> (<::>) List (Tape Roses) a
-> (<:.>)
     (Tagged ('Up 'Forest))
     (Tagged (Zippable structure)
      <:.> (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (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
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Down Forest) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
	substructure :: Lens
  (Substance
     ('Down 'Forest)
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses
                          <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  ((<:.>)
     (Tagged ('Down 'Forest))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Down 'Forest))
   (Tagged (Zippable structure)
    <:.> (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
   a
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
    (Tagged (Zippable structure)
     <:.> (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
    a
  -> Store
       (Roses a)
       ((<:.>)
          (Tagged ('Down 'Forest))
          (Tagged (Zippable structure)
           <:.> (Exactly
                 <:*:> (Roses
                        <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
          a))
 -> P_Q_T
      (->)
      Store
      Roses
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Down 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a
    -> Store
         (Roses a)
         ((<:.>)
            (Tagged ('Down 'Forest))
            (Tagged (Zippable structure)
             <:.> (Exactly
                   <:*:> (Roses
                          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
            a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
  (Tagged (Zippable structure)
   <:.> (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)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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 :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (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))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Down 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> (((:*:) (Roses a) :. (->) (Roses a))
    > (<:.>)
        (Tagged ('Down 'Forest))
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
        a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Down 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
-> ((:*:) (Roses a) :. (->) (Roses a))
   > (<:.>)
       (Tagged ('Down 'Forest))
       (Tagged (Zippable structure)
        <:.> (Exactly
              <:*:> (Roses
                     <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
       a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> (<:.>)
     (Tagged ('Down 'Forest))
     (Tagged (Zippable structure)
      <:.> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> (<:.>)
      (Tagged ('Down 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> (Roses a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> Roses a
-> (<:.>)
     (Tagged ('Down 'Forest))
     (Tagged (Zippable structure)
      <:.> (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (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
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Left Forest) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Reverse Roses
	substructure :: Lens
  (Substance
     ('Left 'Forest)
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses
                          <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  ((<:.>)
     (Tagged ('Left 'Forest))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Left 'Forest))
   (Tagged (Zippable structure)
    <:.> (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
   a
 -> Store
      (Reverse Roses a)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> P_Q_T
     (->)
     Store
     (Reverse Roses)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
    (Tagged (Zippable structure)
     <:.> (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
    a
  -> Store
       (Reverse Roses a)
       ((<:.>)
          (Tagged ('Left 'Forest))
          (Tagged (Zippable structure)
           <:.> (Exactly
                 <:*:> (Roses
                        <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
          a))
 -> P_Q_T
      (->)
      Store
      (Reverse Roses)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Left 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a
    -> Store
         (Reverse Roses a)
         ((<:.>)
            (Tagged ('Left 'Forest))
            (Tagged (Zippable structure)
             <:.> (Exactly
                   <:*:> (Roses
                          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
            a))
-> P_Q_T
     (->)
     Store
     (Reverse Roses)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
  (Tagged (Zippable structure)
   <:.> (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)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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 :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (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))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
-> Store
     (Reverse Roses a)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
 -> Store
      (Reverse Roses a)
      ((<:.>)
         (Tagged ('Left 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> (((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
    > (<:.>)
        (Tagged ('Left 'Forest))
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
        a)
-> Store
     (Reverse Roses a)
     ((<:.>)
        (Tagged ('Left 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
-> ((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
   > (<:.>)
       (Tagged ('Left 'Forest))
       (Tagged (Zippable structure)
        <:.> (Exactly
              <:*:> (Roses
                     <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
       a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> (<:.>)
     (Tagged ('Left 'Forest))
     (Tagged (Zippable structure)
      <:.> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> (<:.>)
      (Tagged ('Left 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> (Reverse Roses a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> Reverse Roses a
-> (<:.>)
     (Tagged ('Left 'Forest))
     (Tagged (Zippable structure)
      <:.> (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (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
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
	type Substance (Right Forest) (Tagged (Zippable structure) <:.> Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
	substructure :: Lens
  (Substance
     ('Right 'Forest)
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses
                          <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
  ((<:.>)
     (Tagged ('Right 'Forest))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
  a
substructure = ((<:.>)
   (Tagged ('Right 'Forest))
   (Tagged (Zippable structure)
    <:.> (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
   a
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
    (Tagged (Zippable structure)
     <:.> (Exactly
           <:*:> (Roses
                  <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
    a
  -> Store
       (Roses a)
       ((<:.>)
          (Tagged ('Right 'Forest))
          (Tagged (Zippable structure)
           <:.> (Exactly
                 <:*:> (Roses
                        <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
          a))
 -> P_Q_T
      (->)
      Store
      Roses
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
      a)
-> ((<:.>)
      (Tagged ('Right 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a
    -> Store
         (Roses a)
         ((<:.>)
            (Tagged ('Right 'Forest))
            (Tagged (Zippable structure)
             <:.> (Exactly
                   <:*:> (Roses
                          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
            a))
-> P_Q_T
     (->)
     Store
     Roses
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
  (Tagged (Zippable structure)
   <:.> (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)
-> (TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
         a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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 :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          Roses
          (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
          a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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))
  (Tagged (Zippable structure)
   <:.> (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))
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
 -> Store
      (Roses a)
      ((<:.>)
         (Tagged ('Right 'Forest))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a))
-> (((:*:) (Roses a) :. (->) (Roses a))
    > (<:.>)
        (Tagged ('Right 'Forest))
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
        a)
-> Store
     (Roses a)
     ((<:.>)
        (Tagged ('Right 'Forest))
        (Tagged (Zippable structure)
         <:.> (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))
         (Tagged (Zippable structure)
          <:.> (Exactly
                <:*:> (Roses
                       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
         a)
-> ((:*:) (Roses a) :. (->) (Roses a))
   > (<:.>)
       (Tagged ('Right 'Forest))
       (Tagged (Zippable structure)
        <:.> (Exactly
              <:*:> (Roses
                     <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
       a
forall s a. s -> a -> s :*: a
:*: TU
  Covariant
  Covariant
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> (<:.>)
     (Tagged ('Right 'Forest))
     (Tagged (Zippable structure)
      <:.> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> (<:.>)
      (Tagged ('Right 'Forest))
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> (Roses a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable structure))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> Roses a
-> (<:.>)
     (Tagged ('Right 'Forest))
     (Tagged (Zippable structure)
      <:.> (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (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
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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 (Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)))) (Construction List) where
	type Morphing (Into (Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)))) (Construction List) =
		Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))
	morphing :: (<::>)
  (Tagged
     ('Into
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses
                             <:*:> (Roses <:*:> (List <::> Tape Roses))))))))
  (Construction List)
  a
-> Morphing
     ('Into
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses
                             <:*:> (Roses <:*:> (List <::> Tape Roses)))))))
     (Construction List)
     a
morphing (<::>)
  (Tagged
     ('Into
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses
                             <:*:> (Roses <:*:> (List <::> Tape Roses))))))))
  (Construction List)
  a
nonempty_rose_tree = case (<::>)
  (Tagged
     ('Into
        (Tagged (Zippable structure)
         <:.> (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
        (Tagged (Zippable structure)
         <:.> (Exactly
               <:*:> (Roses
                      <:*:> (Reverse Roses
                             <:*:> (Roses <:*:> (List <::> Tape Roses))))))))
  (Construction List)
  a
nonempty_rose_tree of
		Construct a
x (List :. Construction List) > a
xs -> T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> 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
<:*:> ((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) (Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) where
	type Morphing (Rotate Up) (Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) =
		Maybe <::> (Tagged (Zippable structure) <:.> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)))
	morphing :: (<::>)
  (Tagged ('Rotate 'Up))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> Morphing
     ('Rotate 'Up)
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a
morphing ((<::>)
  (Tagged ('Rotate 'Up))
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree) = case forall e. Stack List => State (Popping List e) (Maybe e)
forall (t :: * -> *) e. Stack t => State (Popping t e) (Maybe e)
pop @List State
  (List
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a))
  (Maybe
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a))
-> ((->)
      (List
         (TU
            Covariant
            Covariant
            (Tagged (Zippable Roses))
            (Exactly <:*:> (Reverse Roses <:*:> Roses))
            a))
    :. (:*:)
         (List
            (TU
               Covariant
               Covariant
               (Tagged (Zippable Roses))
               (Exactly <:*:> (Reverse Roses <:*:> Roses))
               a)))
   > Maybe
       (TU
          Covariant
          Covariant
          (Tagged (Zippable Roses))
          (Exactly <:*:> (Reverse Roses <:*:> Roses))
          a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (<::>) List (Tape Roses) a
-> List
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens
  (List <::> Tape Roses)
  ((<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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)
   ((<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
   a
 -> (<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
 -> (<::>) List (Tape Roses) a)
-> Lens
     (List <::> Tape Roses)
     ((<:.>)
        (Tagged (Zippable structure))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
-> (<:.>)
     (Tagged (Zippable structure))
     (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) ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> (<::>) List (Tape Roses) a)
-> (<:.>)
     (Tagged (Zippable structure))
     (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)
<-- (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree) of
		-- TODO: Traversable for Maybe up over Product
		List
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
parents :*: Just TU
  Covariant
  Covariant
  (Tagged (Zippable Roses))
  (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
  ((<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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
   ((<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
   a
 -> (<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
 -> Exactly a)
-> Lens
     Exactly
     ((<:.>)
        (Tagged (Zippable structure))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
-> (<:.>)
     (Tagged (Zippable structure))
     (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 ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Exactly a)
-> (<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree 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
  ((<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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
   ((<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
   a
 -> (<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
 -> Roses a)
-> Lens
     Roses
     ((<:.>)
        (Tagged (Zippable structure))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
-> (<:.>)
     (Tagged (Zippable structure))
     (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) ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Roses a)
-> (<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree 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)
  ((<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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)
   ((<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
   a
 -> (<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
 -> Reverse Roses a)
-> Lens
     (Reverse Roses)
     ((<:.>)
        (Tagged (Zippable structure))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
-> (<:.>)
     (Tagged (Zippable structure))
     (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) ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Reverse Roses a)
-> (<:.>)
     (Tagged (Zippable structure))
     (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)
<-- (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree 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
  ((<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a)
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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
   ((<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a)
   a
 -> (<:.>)
      (Tagged (Zippable structure))
      (Exactly
       <:*:> (Roses
              <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
      a
 -> Roses a)
-> Lens
     Roses
     ((<:.>)
        (Tagged (Zippable structure))
        (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
        a)
     a
-> (<:.>)
     (Tagged (Zippable structure))
     (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) ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> Roses a)
-> (<:.>)
     (Tagged (Zippable structure))
     (Exactly
      <:*:> (Roses
             <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
nonempty_rose_tree in
			(<:.>)
  (Tagged (Zippable structure))
  (Exactly
   <:*:> (Roses
          <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
  a
-> TT
     Covariant
     Covariant
     Maybe
     (Tagged (Zippable structure)
      <:.> (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 ((<:.>)
   (Tagged (Zippable structure))
   (Exactly
    <:*:> (Roses
           <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
   a
 -> TT
      Covariant
      Covariant
      Maybe
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> (T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Roses
       <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
      a
    -> (<:.>)
         (Tagged (Zippable structure))
         (Exactly
          <:*:> (Roses
                 <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
         a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> TT
     Covariant
     Covariant
     Maybe
     (Tagged (Zippable structure)
      <:.> (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
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Roses
   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
  a
-> (<:.>)
     (Tagged (Zippable structure))
     (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
 -> TT
      Covariant
      Covariant
      Maybe
      (Tagged (Zippable structure)
       <:.> (Exactly
             <:*:> (Roses
                    <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
      a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Roses
      <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
     a
-> TT
     Covariant
     Covariant
     Maybe
     (Tagged (Zippable structure)
      <:.> (Exactly
            <:*:> (Roses
                   <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Lens
  Exactly
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Exactly
   (TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a)
   a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a
 -> Exactly a)
-> Lens
     Exactly
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable Roses))
   (Exactly <:*:> (Reverse Roses <:*:> Roses))
   a
 -> Exactly a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TU
  Covariant
  Covariant
  (Tagged (Zippable Roses))
  (Exactly <:*:> (Reverse Roses <:*:> Roses))
  a
parent
				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
<:*:> ((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)
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Reverse Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Reverse Roses)
   (TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a)
   a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a
 -> Reverse Roses a)
-> Lens
     (Reverse Roses)
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable Roses))
   (Exactly <:*:> (Reverse Roses <:*:> Roses))
   a
 -> Reverse Roses a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TU
  Covariant
  Covariant
  (Tagged (Zippable Roses))
  (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
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
  a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   Roses
   (TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a)
   a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable Roses))
      (Exactly <:*:> (Reverse Roses <:*:> Roses))
      a
 -> Roses a)
-> Lens
     Roses
     (TU
        Covariant
        Covariant
        (Tagged (Zippable Roses))
        (Exactly <:*:> (Reverse Roses <:*:> Roses))
        a)
     a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (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 (TU
   Covariant
   Covariant
   (Tagged (Zippable Roses))
   (Exactly <:*:> (Reverse Roses <:*:> Roses))
   a
 -> Roses a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TU
  Covariant
  Covariant
  (Tagged (Zippable Roses))
  (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
<:*:> List
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite List
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
parents
		List
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
_ :*: Maybe
  (TU
     Covariant
     Covariant
     (Tagged (Zippable Roses))
     (Exactly <:*:> (Reverse Roses <:*:> Roses))
     a)
Nothing -> Morphing
  ('Rotate 'Up)
  (Tagged (Zippable structure)
   <:.> (Exactly
         <:*:> (Roses
                <:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
  a
forall (t :: * -> *) a. Emptiable t => t a
empty