{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure.Some.Binary where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), comap))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (empty)
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (order)
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator, Zero))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor.Function ((!), (%), (&))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), type (<:.>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.State (State, modify)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (over)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Root))
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Heighth), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable ((+=)))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate, Into))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), sub, substitute)
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)

type Binary = Maybe <:.> Construction Wye

rebalance :: Chain a => (Wye :. Construction Wye := a) -> Nonempty Binary a
rebalance :: ((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (Both Construction Wye a
x Construction Wye a
y) = a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
y Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a
forall a b. a -> (a -> b) -> b
& Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall a. a -> a -> a -> Ordering -> a
order
	(a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
y) (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both Construction Wye a
x (((Wye :. Construction Wye) := a) -> Construction Wye a
forall a.
Chain a =>
((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
y))
	(a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
x) (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both (((Wye :. Construction Wye) := a) -> Construction Wye a
forall a.
Chain a =>
((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
x) (((Wye :. Construction Wye) := a) -> Construction Wye a
forall a.
Chain a =>
((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
y))
	(a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
x) (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both (((Wye :. Construction Wye) := a) -> Construction Wye a
forall a.
Chain a =>
((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
x) Construction Wye a
y)

instance (forall a . Chain a) => Insertable Binary where
	a
x += :: a -> Binary a -> Binary a
+= (Binary a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Primary Binary a
Nothing) = Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> Binary a)
-> (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a)
-> Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Wye :. Construction Wye) := a) -> Binary a)
-> ((Wye :. Construction Wye) := a) -> Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Wye :. Construction Wye) := a
forall a. Wye a
End
	a
x += tree :: Binary a
tree@(Binary a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just nonempty) = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
nonempty Ordering -> (Ordering -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& Binary a -> Binary a -> Binary a -> Ordering -> Binary a
forall a. a -> a -> a -> Ordering -> a
order
		(Binary a
tree Binary a -> (Binary a -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& (Substructural 'Left Binary a -> Substructural 'Left Binary a)
-> Binary a -> Binary a
forall k (f :: k) (t :: * -> *) a.
Substructure f t =>
(Substructural f t a -> Substructural f t a) -> t a -> t a
substitute @Left (a
x a -> Binary a -> Binary a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+=)) Binary a
tree (Binary a
tree Binary a -> (Binary a -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& (Substructural 'Right Binary a -> Substructural 'Right Binary a)
-> Binary a -> Binary a
forall k (f :: k) (t :: * -> *) a.
Substructure f t =>
(Substructural f t a -> Substructural f t a) -> t a -> t a
substitute @Right (a
x a -> Binary a -> Binary a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+=))

instance (forall a . Chain a) => Focusable Root Binary where
	type Focusing Root Binary a = Maybe a
	focusing :: Tagged 'Root (Binary a) :-. Focusing 'Root Binary a
focusing (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> (Tagged 'Root (Binary a) -> Binary a)
-> Tagged 'Root (Binary a)
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Root (Binary a) -> Binary a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction Wye a)
Nothing) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
-> Store (Maybe a) (Tagged 'Root (Binary a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
 -> Store (Maybe a) (Tagged 'Root (Binary a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
-> Store (Maybe a) (Tagged 'Root (Binary a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe a
forall a. Maybe a
Nothing Maybe a
-> (Maybe a -> Tagged 'Root (Binary a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)
forall s a. s -> a -> Product s a
:*: Binary a -> Tagged 'Root (Binary a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Binary a -> Tagged 'Root (Binary a))
-> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Maybe (Construction Wye a) -> Binary 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 (Maybe (Construction Wye a) -> Binary a)
-> (Maybe a -> Maybe (Construction Wye a)) -> Maybe a -> Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction Wye a) -> Maybe a -> Maybe (Construction Wye a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Wye :. Construction Wye) := a
forall a. Wye a
End)
	focusing (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> (Tagged 'Root (Binary a) -> Binary a)
-> Tagged 'Root (Binary a)
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Root (Binary a) -> Binary a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Wye a
x) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
-> Store (Maybe a) (Tagged 'Root (Binary a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
 -> Store (Maybe a) (Tagged 'Root (Binary a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a))
-> Store (Maybe a) (Tagged 'Root (Binary a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Maybe a
forall a. a -> Maybe a
Just (a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
x) Maybe a
-> (Maybe a -> Tagged 'Root (Binary a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)
forall s a. s -> a -> Product s a
:*: Binary a -> Tagged 'Root (Binary a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Binary a -> Tagged 'Root (Binary a))
-> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> Binary a)
-> (Maybe a -> Construction Wye a) -> Maybe a -> Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction Wye a)
-> Construction Wye a -> Maybe a -> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
x) (((Wye :. Construction Wye) := a) -> Construction Wye a
forall a.
Chain a =>
((Wye :. Construction Wye) := a) -> Nonempty Binary a
rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
x)

instance Measurable Heighth Binary where
	type Measural Heighth Binary a = Numerator
	measurement :: Tagged 'Heighth (Binary a) -> Measural 'Heighth Binary a
measurement (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> (Tagged 'Heighth (Binary a) -> Binary a)
-> Tagged 'Heighth (Binary a)
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Binary a) -> Binary a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Wye a
bt) = Denumerator -> Numerator
Numerator (Denumerator -> Numerator) -> Denumerator -> Numerator
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a -> Measural 'Heighth (Construction Wye) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Heighth Construction Wye a
bt
	measurement (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> (Tagged 'Heighth (Binary a) -> Binary a)
-> Tagged 'Heighth (Binary a)
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Binary a) -> Binary a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction Wye a)
Nothing) = Numerator
Measural 'Heighth Binary a
Zero

instance Nullable Binary where
	null :: (Predicate :. Binary) := a
null = (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Binary a -> Boolean) -> (Predicate :. Binary) := a)
-> (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \case { TU Maybe (Construction Wye a)
Nothing -> Boolean
True ; Binary a
_ -> Boolean
False }

instance Substructure Left Binary where
	type Substructural Left Binary = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Left) Binary a) (Substructural 'Left Binary a)
substructure empty_tree :: (<:.>) (Tagged 'Left) Binary a
empty_tree@(TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) a
 -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Left) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Wye) a
 <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) Binary a
    -> Tagged
         'Left (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Left) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) Binary a
-> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Maybe (Construction Wye a)
Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) Binary a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) Binary a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract ((<:.>) (Tagged 'Left) Binary a
-> Primary (Tagged 'Left <:.> Binary) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Left) Binary a
empty_tree) TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) Binary a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) Binary a
forall s a. s -> a -> Product s a
:*: (!) (<:.>) (Tagged 'Left) Binary a
empty_tree
	substructure (TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) a
 -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Left) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Wye) a
 <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) Binary a
    -> Tagged
         'Left (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Left) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) Binary a
-> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just Construction Wye a
tree) = TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Left) Binary a)
-> (Construction Wye a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     (Construction Wye a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens
  (Construction Wye a) (Substructural 'Left (Construction Wye) a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
sub @Left Construction Wye a
tree

instance Substructure Right Binary where
	type Substructural Right Binary = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Right) Binary a) (Substructural 'Right Binary a)
substructure empty_tree :: (<:.>) (Tagged 'Right) Binary a
empty_tree@(TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) a
 -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Right) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Wye) a
 <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) Binary a
    -> Tagged
         'Right (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Right) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) Binary a
-> Tagged
     'Right (TU Covariant Covariant Maybe (Construction Wye) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Maybe (Construction Wye a)
Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) Binary a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) Binary a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) Binary a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract ((<:.>) (Tagged 'Right) Binary a
-> Primary (Tagged 'Right <:.> Binary) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Right) Binary a
empty_tree) TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) Binary a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) Binary a
forall s a. s -> a -> Product s a
:*: (!) (<:.>) (Tagged 'Right) Binary a
empty_tree
	substructure (TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) a
 -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Right) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Wye) a
 <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) Binary a
    -> Tagged
         'Right (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Right) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) Binary a
-> Tagged
     'Right (TU Covariant Covariant Maybe (Construction Wye) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just Construction Wye a
tree) = TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Right) Binary a)
-> (Construction Wye a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     (Construction Wye a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) Binary a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens
  (Construction Wye a) (Substructural 'Right (Construction Wye) a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
sub @Right Construction Wye a
tree

binary :: forall t a . (Traversable t, Chain a) => t a -> Binary a
binary :: t a -> Binary a
binary t a
struct = (Binary a :*: t ()) -> Binary a
forall a b. (a :*: b) -> a
attached ((Binary a :*: t ()) -> Binary a)
-> (Binary a :*: t ()) -> Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ forall a.
Interpreted (State (Binary a)) =>
State (Binary a) a -> Primary (State (Binary a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Binary a)) (State (Binary a) (t ())
 -> ((->) (Binary a) :. (:*:) (Binary a)) := t ())
-> Binary a -> State (Binary a) (t ()) -> Binary a :*: t ()
forall a b c. (a -> b -> c) -> b -> a -> c
% Binary a
forall (t :: * -> *) a. Avoidable t => t a
empty (State (Binary a) (t ()) -> Binary a :*: t ())
-> State (Binary a) (t ()) -> Binary a :*: t ()
forall (m :: * -> * -> *). Category m => m ~~> m
$ t a
struct t a -> (a -> State (Binary a) ()) -> State (Binary a) (t ())
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> forall s (t :: * -> *). Stateful s t => (s -> s) -> t ()
forall (t :: * -> *).
Stateful (Binary a) t =>
(Binary a -> Binary a) -> t ()
modify @(Binary a) ((Binary a -> Binary a) -> State (Binary a) ())
-> (a -> Binary a -> Binary a) -> a -> State (Binary a) ()
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Binary a -> Binary a
insert' where

	insert' :: a -> Binary a -> Binary a
	insert' :: a -> Binary a -> Binary a
insert' a
x (Binary a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Primary Binary a
Nothing) = Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> Binary a)
-> (((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a)
-> Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Wye :. Construction Wye) := a) -> Binary a)
-> ((Wye :. Construction Wye) := a) -> Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Wye :. Construction Wye) := a
forall a. Wye a
End
	insert' a
x tree :: Binary a
tree@(Binary a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just nonempty) = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
nonempty Ordering -> (Ordering -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& Binary a -> Binary a -> Binary a -> Ordering -> Binary a
forall a. a -> a -> a -> Ordering -> a
order
		(Binary a
tree Binary a -> (Binary a -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& (Substructural 'Left Binary a -> Substructural 'Left Binary a)
-> Binary a -> Binary a
forall k (f :: k) (t :: * -> *) a.
Substructure f t =>
(Substructural f t a -> Substructural f t a) -> t a -> t a
substitute @Left (a -> Binary a -> Binary a
insert' a
x)) Binary a
tree (Binary a
tree Binary a -> (Binary a -> Binary a) -> Binary a
forall a b. a -> (a -> b) -> b
& (Substructural 'Right Binary a -> Substructural 'Right Binary a)
-> Binary a -> Binary a
forall k (f :: k) (t :: * -> *) a.
Substructure f t =>
(Substructural f t a -> Substructural f t a) -> t a -> t a
substitute @Right (a -> Binary a -> Binary a
insert' a
x))

type instance Nonempty Binary = Construction Wye

instance Morphable (Into Binary) (Construction Wye) where
	type Morphing (Into Binary) (Construction Wye) = Binary
	morphing :: (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Morphing ('Into Binary) (Construction Wye) a
morphing = Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a
 -> TU Covariant Covariant Maybe (Construction Wye) a)
-> ((<:.>) (Tagged ('Into Binary)) (Construction Wye) a
    -> Construction Wye a)
-> (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a <:= Tagged ('Into Binary)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged ('Into Binary))
-> ((<:.>) (Tagged ('Into Binary)) (Construction Wye) a
    -> Tagged ('Into Binary) (Construction Wye a))
-> (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Tagged ('Into Binary) (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Focusable Root (Construction Wye) where
	type Focusing Root (Construction Wye) a = a
	focusing :: Tagged 'Root (Construction Wye a)
:-. Focusing 'Root (Construction Wye) a
focusing (Construction Wye a <:= Tagged 'Root
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Construct a
x (Wye :. Construction Wye) := a
xs) = (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a))
-> Store a (Tagged 'Root (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a))
 -> Store a (Tagged 'Root (Construction Wye a)))
-> (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a))
-> Store a (Tagged 'Root (Construction Wye a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
x a
-> (a -> Tagged 'Root (Construction Wye a))
-> ((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)
forall s a. s -> a -> Product s a
:*: Construction Wye a -> Tagged 'Root (Construction Wye a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Root (Construction Wye a))
-> (a -> Construction Wye a)
-> a
-> Tagged 'Root (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Wye :. Construction Wye) := a
xs

instance (forall a . Chain a) => Insertable (Construction Wye) where
	a
x += :: a -> Construction Wye a -> Construction Wye a
+= Construction Wye a
b = let change :: TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
change = Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a
 -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> ((Maybe :. Construction Wye) := a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a
x a -> Construction Wye a -> Construction Wye a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
+=) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye :. Construction Wye) := a
forall a. Wye a
End) (((Maybe :. Construction Wye) := a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run in
		a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
b Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a
forall a b. a -> (a -> b) -> b
& Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall a. a -> a -> a -> Ordering -> a
order (Lens
  (Construction Wye a)
  (TU Covariant Covariant Maybe (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
over (forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
forall (t :: * -> *).
Substructure 'Left t =>
t :~. Substructural 'Left t
sub @Left) TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
change (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
b) Construction Wye a
b (Lens
  (Construction Wye a)
  (TU Covariant Covariant Maybe (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
over (forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
forall (t :: * -> *).
Substructure 'Right t =>
t :~. Substructural 'Right t
sub @Right) TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
change (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
b)

instance Measurable Heighth (Construction Wye) where
	type Measural Heighth (Construction Wye) a = Denumerator
	measurement :: Tagged 'Heighth (Construction Wye a)
-> Measural 'Heighth (Construction Wye) a
measurement (Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a)
-> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a)
-> Tagged 'Heighth (Construction Wye a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> (Wye :. Construction Wye) := a
End) = Denumerator
Measural 'Heighth (Construction Wye) a
One
	measurement (Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a)
-> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a)
-> Tagged 'Heighth (Construction Wye a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Left Construction Wye a
lst) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+ Construction Wye a -> Measural 'Heighth (Construction Wye) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Heighth Construction Wye a
lst
	measurement (Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a)
-> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a)
-> Tagged 'Heighth (Construction Wye a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Right Construction Wye a
rst) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+ Construction Wye a -> Measural 'Heighth (Construction Wye) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Heighth Construction Wye a
rst
	measurement (Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a)
-> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a)
-> Tagged 'Heighth (Construction Wye a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Heighth (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Both Construction Wye a
lst Construction Wye a
rst) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+
		let (Denumerator
lm :*: Denumerator
rm) = Construction Wye a -> Measural 'Heighth (Construction Wye) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Heighth Construction Wye a
lst Denumerator -> Denumerator -> Product Denumerator Denumerator
forall s a. s -> a -> Product s a
:*: Construction Wye a -> Measural 'Heighth (Construction Wye) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Heighth Construction Wye a
rst
		in Denumerator
lm Denumerator -> Denumerator -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> Denumerator
rm Ordering -> (Ordering -> Denumerator) -> Denumerator
forall a b. a -> (a -> b) -> b
& Denumerator
-> Denumerator -> Denumerator -> Ordering -> Denumerator
forall a. a -> a -> a -> Ordering -> a
order Denumerator
rm Denumerator
lm Denumerator
lm

instance Substructure Left (Construction Wye) where
	type Substructural Left (Construction Wye) = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Left) (Construction Wye) a)
  (Substructural 'Left (Construction Wye) a)
substructure empty_tree :: (<:.>) (Tagged 'Left) (Construction Wye) a
empty_tree@(Construction Wye a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Tagged 'Left (Construction Wye a))
-> (<:.>) (Tagged 'Left) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ Wye (Construction Wye a)
End) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((<:.>) (Tagged 'Left) (Construction Wye) a
empty_tree (<:.>) (Tagged 'Left) (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall a b. a -> b -> a
!)
	substructure (Construction Wye a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Tagged 'Left (Construction Wye a))
-> (<:.>) (Tagged 'Left) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Left Construction Wye a
lst)) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Wye (Construction Wye a)
forall a. Wye a
End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
	substructure (Construction Wye a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Tagged 'Left (Construction Wye a))
-> (<:.>) (Tagged 'Left) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Right Construction Wye a
rst)) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
	substructure (Construction Wye a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Tagged 'Left (Construction Wye a))
-> (<:.>) (Tagged 'Left) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Substructure Right (Construction Wye) where
	type Substructural Right (Construction Wye) = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Right) (Construction Wye) a)
  (Substructural 'Right (Construction Wye) a)
substructure emtpy_tree :: (<:.>) (Tagged 'Right) (Construction Wye) a
emtpy_tree@(Construction Wye a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Tagged 'Right (Construction Wye a))
-> (<:.>) (Tagged 'Right) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ Wye (Construction Wye a)
End) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((<:.>) (Tagged 'Right) (Construction Wye) a
emtpy_tree (<:.>) (Tagged 'Right) (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall a b. a -> b -> a
!)
	substructure (Construction Wye a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Tagged 'Right (Construction Wye a))
-> (<:.>) (Tagged 'Right) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Left Construction Wye a
lst)) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
	substructure (Construction Wye a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Tagged 'Right (Construction Wye a))
-> (<:.>) (Tagged 'Right) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Right Construction Wye a
rst)) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Wye (Construction Wye a)
forall a. Wye a
End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
	substructure (Construction Wye a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Right)
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Tagged 'Right (Construction Wye a))
-> (<:.>) (Tagged 'Right) (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) =
		 (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

data Biforked a = Top | Leftward a | Rightward a

instance Covariant Biforked where
	a -> b
_ <$> :: (a -> b) -> Biforked a -> Biforked b
<$> Biforked a
Top = Biforked b
forall a. Biforked a
Top
	a -> b
f <$> Leftward a
l = b -> Biforked b
forall a. a -> Biforked a
Leftward (b -> Biforked b) -> b -> Biforked b
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> b
f a
l
	a -> b
f <$> Rightward a
r = b -> Biforked b
forall a. a -> Biforked a
Rightward (b -> Biforked b) -> b -> Biforked b
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> b
f a
r

type instance Zipper (Construction Wye) = T_U Covariant Covariant (Construction Wye) (:*:)
	((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye))

data Vertical a = Up a | Down a

instance Morphable (Rotate Up) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye))) where
	type Morphing (Rotate Up) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
		= Maybe <:.> (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
	morphing :: (<:.>)
  (Tagged ('Rotate 'Up))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Morphing
     ('Rotate 'Up)
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate 'Up))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate 'Up))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate 'Up)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate 'Up))
-> ((<:.>)
      (Tagged ('Rotate 'Up))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate 'Up)
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate 'Up))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate 'Up))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate 'Up)
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_U (Identity a
parent :*: (<:.>) Maybe (Construction Wye) a
rest)) Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
next)))) =
		T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
parent ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both Construction Wye a
focused) (Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> Wye a
Left Construction Wye a
focused) (((Maybe :. Construction Wye) := a)
 -> (Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (<:.>) Maybe (Construction Wye) a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) Maybe (Construction Wye) a
rest) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
next)
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate 'Up))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate 'Up))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate 'Up)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate 'Up))
-> ((<:.>)
      (Tagged ('Rotate 'Up))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate 'Up)
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate 'Up))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate 'Up))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate 'Up)
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_U (Identity a
parent :*: (<:.>) Maybe (Construction Wye) a
rest)) Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
next)))) =
		T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
parent ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> (Wye :. Construction Wye) := a)
-> Construction Wye a
-> Construction Wye a
-> (Wye :. Construction Wye) := a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
focused) (Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> Wye a
Right Construction Wye a
focused) (((Maybe :. Construction Wye) := a)
 -> (Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (<:.>) Maybe (Construction Wye) a -> Primary Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) Maybe (Construction Wye) a
rest) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
next)
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate 'Up)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate 'Up))
-> ((<:.>)
      (Tagged ('Rotate 'Up))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate 'Up)
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate 'Up))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate 'Up))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate 'Up)
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> T_U (Construction Wye a
_ :*: TU (TU Biforked
  (Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
Top))) = Morphing
  ('Rotate 'Up)
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable (Rotate (Down Left)) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye))) where
	type Morphing (Rotate (Down Left)) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
		= Maybe <:.> (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
	morphing :: (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Morphing
     ('Rotate ('Down 'Left))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Left))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Left)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Left))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Left))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Left Construction Wye a
lst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next)) =
		T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> T_U
      Covariant
      Covariant
      (Construction Wye)
      (:*:)
      ((Biforked <:.> Construction Biforked)
       <:.> T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
lst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Identity (:*:) Binary a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
 -> (Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Construction
         Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant Identity (:*:) Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
 -> T_U Covariant Covariant Identity (:*:) Binary a)
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (<:.>) Maybe (Construction Wye) a
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
forall s a. s -> a -> Product s a
:*: (<:.>) Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Left))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Left)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Left))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Left))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next)) =
		T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> T_U
      Covariant
      Covariant
      (Construction Wye)
      (:*:)
      ((Biforked <:.> Construction Biforked)
       <:.> T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
lst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Identity (:*:) Binary a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
 -> (Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Construction
         Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant Identity (:*:) Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
 -> T_U Covariant Covariant Identity (:*:) Binary a)
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (<:.>) Maybe (Construction Wye) a
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Left))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Left)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Left))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Left))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ (Right Construction Wye a
_) :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary)
  a
_) = Morphing
  ('Rotate ('Down 'Left))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
forall (t :: * -> *) a. Avoidable t => t a
empty
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Left))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Left)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Left))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Left))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ Wye (Construction Wye a)
End :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary)
  a
_) = Morphing
  ('Rotate ('Down 'Left))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable (Rotate (Down Right)) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye))) where
	type Morphing (Rotate (Down Right)) (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
		= Maybe <:.> (T_U Covariant Covariant (Construction Wye) (:*:) ((Biforked <:.> Construction Biforked) <:.> T_U Covariant Covariant Identity (:*:) (Maybe <:.> Construction Wye)))
	morphing :: (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Morphing
     ('Rotate ('Down 'Right))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Right))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Right)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Right))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Right))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Right Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next)) = T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> T_U
      Covariant
      Covariant
      (Construction Wye)
      (:*:)
      ((Biforked <:.> Construction Biforked)
       <:.> T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
rst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Identity (:*:) Binary a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
 -> (Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Construction
         Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant Identity (:*:) Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
 -> T_U Covariant Covariant Identity (:*:) Binary a)
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (<:.>) Maybe (Construction Wye) a
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
forall s a. s -> a -> Product s a
:*: (<:.>) Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Right))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Right)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Right))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Right))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next)) = T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product
  (Construction Wye a)
  (TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
 -> T_U
      Covariant
      Covariant
      (Construction Wye)
      (:*:)
      ((Biforked <:.> Construction Biforked)
       <:.> T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
rst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     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 (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary)
      a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary 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 (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Identity (:*:) Binary a))
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Identity (:*:) Binary a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Identity (:*:) Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
 -> (Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Identity (:*:) Binary a)
    -> Construction
         Biforked (T_U Covariant Covariant Identity (:*:) Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant Identity (:*:) Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Identity (:*:) Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall k k k k k (ct :: k) (cu :: k) (t :: k -> k)
       (p :: k -> k -> *) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu t p u a
T_U (Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
 -> T_U Covariant Covariant Identity (:*:) Binary a)
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
-> T_U Covariant Covariant Identity (:*:) Binary a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (<:.>) Maybe (Construction Wye) a
-> Product (Identity a) ((<:.>) Maybe (Construction Wye) a)
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Identity (:*:) Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a)
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Identity (:*:) Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Identity (:*:) Binary a
next
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Right))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Right)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Right))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Right))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ (Left Construction Wye a
_) :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary)
  a
_) = Morphing
  ('Rotate ('Down 'Right))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
forall (t :: * -> *) a. Avoidable t => t a
empty
	morphing (T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_U Covariant Covariant Identity (:*:) Binary)
         a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary)
         a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (Construction Wye)
  (:*:)
  ((Biforked <:.> Construction Biforked)
   <:.> T_U Covariant Covariant Identity (:*:) Binary)
  a
<:= Tagged ('Rotate ('Down 'Right))
forall (t :: * -> *) a. Extractable t => a <:= t
extract (T_U
   Covariant
   Covariant
   (Construction Wye)
   (:*:)
   ((Biforked <:.> Construction Biforked)
    <:.> T_U Covariant Covariant Identity (:*:) Binary)
   a
 <:= Tagged ('Rotate ('Down 'Right)))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      (T_U
         Covariant
         Covariant
         (Construction Wye)
         (:*:)
         ((Biforked <:.> Construction Biforked)
          <:.> T_U Covariant Covariant Identity (:*:) Binary))
      a
    -> Tagged
         ('Rotate ('Down 'Right))
         (T_U
            Covariant
            Covariant
            (Construction Wye)
            (:*:)
            ((Biforked <:.> Construction Biforked)
             <:.> T_U Covariant Covariant Identity (:*:) Binary)
            a))
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary))
     a
-> T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
-> Tagged
     ('Rotate ('Down 'Right))
     (T_U
        Covariant
        Covariant
        (Construction Wye)
        (:*:)
        ((Biforked <:.> Construction Biforked)
         <:.> T_U Covariant Covariant Identity (:*:) Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
_ Wye (Construction Wye a)
End :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_U Covariant Covariant Identity (:*:) Binary)
  a
_) = Morphing
  ('Rotate ('Down 'Right))
  (T_U
     Covariant
     Covariant
     (Construction Wye)
     (:*:)
     ((Biforked <:.> Construction Biforked)
      <:.> T_U Covariant Covariant Identity (:*:) Binary))
  a
forall (t :: * -> *) a. Avoidable t => t a
empty