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

module Pandora.Paradigm.Structure.Binary where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Morphism ((&), (%), (!))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), comap))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Transformer.Liftable (lift)
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.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
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_ (T_), T_U (T_U), type (<:.>), type (<:*:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (type (:-.), (|>), (%~))
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.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Insertable (Insertable (insert))
import Pandora.Paradigm.Structure.Ability.Rotatable (Rotatable (Rotational, rotation))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), sub)
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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
	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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ (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
		(forall k (f :: * -> k) (t :: * -> *) a.
Substructure f t =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Left t =>
t a :-. Substructural 'Left t a
sub @Left (Binary a -> Store (Binary a) (Binary a))
-> (Binary a -> Binary a) -> Binary a -> Binary a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
%~ a -> Binary a -> Binary a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x (Binary a -> Binary a) -> Binary a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Binary a
tree) Binary a
tree (forall k (f :: * -> k) (t :: * -> *) a.
Substructure f t =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Right t =>
t a :-. Substructural 'Right t a
sub @Right (Binary a -> Store (Binary a) (Binary a))
-> (Binary a -> Binary a) -> Binary a -> Binary a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
%~ a -> Binary a -> Binary a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x (Binary a -> Binary a) -> Binary a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Binary a
tree)

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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a -> (Wye :. Construction Wye) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Wye a
x)

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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ \case { TU Maybe (Construction Wye a)
Nothing -> Boolean
True ; Binary a
_ -> Boolean
False }

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

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

can_be_empty :: Maybe (Construction Wye a) :-. Binary a
can_be_empty :: Maybe (Construction Wye a) :-. Binary a
can_be_empty Maybe (Construction Wye a)
maybe_tree = (((:*:) (Binary a) :. (->) (Binary a))
 := Maybe (Construction Wye a))
-> Store (Binary a) (Maybe (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Binary a) :. (->) (Binary a))
  := Maybe (Construction Wye a))
 -> Store (Binary a) (Maybe (Construction Wye a)))
-> (((:*:) (Binary a) :. (->) (Binary a))
    := Maybe (Construction Wye a))
-> Store (Binary a) (Maybe (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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)
maybe_tree Binary a
-> (Binary a -> Maybe (Construction Wye a))
-> ((:*:) (Binary a) :. (->) (Binary a))
   := Maybe (Construction Wye a)
forall s a. s -> a -> Product s a
:*: Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

type instance Nonempty Binary = Construction Wye

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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
	insert :: a -> Construction Wye a -> Construction Wye a
insert a
x Construction Wye a
nonempty = let change :: Maybe (Construction Wye a) -> Maybe (Construction Wye a)
change = Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just (Construction Wye a -> Maybe (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> 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 -> Construction Wye a -> Construction Wye a
forall (t :: * -> *) a. Insertable t => a -> t a -> t a
insert a
x) (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) 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
nonempty 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 (forall k (f :: * -> k) (t :: * -> *) a.
Substructure f t =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Left t =>
t a :-. Substructural 'Left t a
sub @Left (Construction Wye a
 -> Store (Maybe (Construction Wye a)) (Construction Wye a))
-> (Maybe (Construction Wye a) -> Maybe (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
%~ Maybe (Construction Wye a) -> Maybe (Construction Wye a)
change (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a
nonempty) Construction Wye a
nonempty (forall k (f :: * -> k) (t :: * -> *) a.
Substructure f t =>
t a :-. Substructural f t a
forall (t :: * -> *) a.
Substructure 'Right t =>
t a :-. Substructural 'Right t a
sub @Right (Construction Wye a
 -> Store (Maybe (Construction Wye a)) (Construction Wye a))
-> (Maybe (Construction Wye a) -> Maybe (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
%~ Maybe (Construction Wye a) -> Maybe (Construction Wye a)
change (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a
nonempty)

instance Substructure Left (Construction Wye) where
	type Substructural Left (Construction Wye) a = Maybe :. Construction Wye := a
	substructure :: 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 -> Construct a
_ Wye (Construction Wye a)
End) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Left (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Left (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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)
-> 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 -> Construct a
x (Left Construction Wye a
lst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Left (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
lst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Left (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Left (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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
	substructure (Construction Wye a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Right Construction Wye a
rst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Left (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Left (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Left (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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)
	substructure (Construction Wye a <-| Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Left (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Left (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
lst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Left (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Left (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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)

instance Substructure Right (Construction Wye) where
	type Substructural Right (Construction Wye) a = Maybe :. Construction Wye := a
	substructure :: 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 -> Construct a
_ Wye (Construction Wye a)
End) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Right (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Right (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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)
-> 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 -> Construct a
x (Left Construction Wye a
lst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Right (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Right (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Right (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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)
	substructure (Construction Wye a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Right Construction Wye a
rst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Right (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
rst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Right (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Right (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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
	substructure (Construction Wye a <-| Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst)) = (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := Tagged 'Right (Construction Wye a))
 -> Store
      (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := Tagged 'Right (Construction Wye a))
-> Store
     (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
rst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> Tagged 'Right (Construction Wye a))
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Wye a -> Tagged 'Right (Construction Wye a))
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> 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)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> 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)

data Biforked a = Top | Leftward a | Rightward a

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

data Vertical a = Up a | Down a

instance Rotatable Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where
	type Rotational Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a
		= Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a
	rotation :: Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> Rotational
     'Up
     (Construction Wye
      <:*:> ((Biforked <:.> Construction Biforked)
             <:.> T_ Covariant Binary))
     a
rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      'Up
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     'Up
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Wye a
focused :*: TU (TU (Leftward (Construct (T_ (a
parent :*: TU (Just Construction Wye a
rst))) Biforked (Construction Biforked (T_ Covariant Binary a))
next)))) =
		(<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both Construction Wye a
focused Construction Wye a
rst) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
next)
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      'Up
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     'Up
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Wye a
focused :*: TU (TU (Leftward (Construct (T_ (a
parent :*: TU Maybe (Construction Wye a)
Nothing)) Biforked (Construction Biforked (T_ Covariant Binary a))
next)))) =
		(<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
forall a. a -> Wye a
Left Construction Wye a
focused) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
next)
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      'Up
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     'Up
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_ (a
parent :*: TU (Just Construction Wye a
lst))) Biforked (Construction Biforked (T_ Covariant Binary a))
next)))) =
		(<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both Construction Wye a
lst Construction Wye a
focused) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
next)
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      'Up
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     'Up
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_ (a
parent :*: TU Maybe (Construction Wye a)
Nothing)) Biforked (Construction Biforked (T_ Covariant Binary a))
next)))) =
		(<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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
forall a. a -> Wye a
Right Construction Wye a
focused) Construction Wye a
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
:*: TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a))
next)
	rotation (Tagged
  'Up
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> T_U (Construction Wye a
_ :*: TU (TU Biforked (Construction Biforked (T_ Covariant Binary a))
Top))) = Rotational
  'Up
  (Construction Wye
   <:*:> ((Biforked <:.> Construction Biforked)
          <:.> T_ Covariant Binary))
  a
forall a. Maybe a
Nothing

instance Rotatable (Down Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where
	type Rotational (Down Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a
		= Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a
	rotation :: Tagged
  ('Down 'Left)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> Rotational
     ('Down 'Left)
     (Construction Wye
      <:*:> ((Biforked <:.> Construction Biforked)
             <:.> T_ Covariant Binary))
     a
rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Left)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Left)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Left)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Left Construction Wye a
lst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a
next)) = (<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> (<:*:>)
      (Construction Wye)
      ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_ Covariant Binary)
            a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
lst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant 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_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_ Covariant Binary a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Biforked (T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall a. a -> Biforked a
Leftward (Construction Biforked (T_ Covariant Binary a)
 -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Construction Biforked (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_ Covariant Binary a
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Construction Biforked (T_ Covariant Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a
T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
 -> T_ Covariant Binary a)
-> (a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
x a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> a :*: TU Covariant Covariant Maybe (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) 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
forall a. Maybe a
Nothing) (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Biforked :. Construction Biforked) := T_ Covariant Binary a
next
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Left)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Left)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Left)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a
next)) = (<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> (<:*:>)
      (Construction Wye)
      ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_ Covariant Binary)
            a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
lst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant 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_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_ Covariant Binary a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Biforked (T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall a. a -> Biforked a
Leftward (Construction Biforked (T_ Covariant Binary a)
 -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Construction Biforked (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_ Covariant Binary a
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Construction Biforked (T_ Covariant Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a
T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
 -> T_ Covariant Binary a)
-> (a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
x a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> a :*: TU Covariant Covariant Maybe (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Construction Wye a -> (Maybe :. Construction Wye) := a
forall a. a -> Maybe a
Just Construction Wye a
rst)) (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Biforked :. Construction Biforked) := T_ Covariant Binary a
next
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Left)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Left)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Left)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
_ (Right Construction Wye a
_) :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_ Covariant Binary)
  a
_) = Rotational
  ('Down 'Left)
  (Construction Wye
   <:*:> ((Biforked <:.> Construction Biforked)
          <:.> T_ Covariant Binary))
  a
forall a. Maybe a
Nothing
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Left)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Left)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Left)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
_ Wye (Construction Wye a)
End :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_ Covariant Binary)
  a
_) = Rotational
  ('Down 'Left)
  (Construction Wye
   <:*:> ((Biforked <:.> Construction Biforked)
          <:.> T_ Covariant Binary))
  a
forall a. Maybe a
Nothing

instance Rotatable (Down Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where
	type Rotational (Down Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a
		= Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a
	rotation :: Tagged
  ('Down 'Right)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> Rotational
     ('Down 'Right)
     (Construction Wye
      <:*:> ((Biforked <:.> Construction Biforked)
             <:.> T_ Covariant Binary))
     a
rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Right)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Right)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Right)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Right Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a
next)) = (<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> (<:*:>)
      (Construction Wye)
      ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_ Covariant Binary)
            a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
rst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant 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_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_ Covariant Binary a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Biforked (T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall a. a -> Biforked a
Rightward (Construction Biforked (T_ Covariant Binary a)
 -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Construction Biforked (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_ Covariant Binary a
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Construction Biforked (T_ Covariant Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a
T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
 -> T_ Covariant Binary a)
-> (a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
x a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> a :*: TU Covariant Covariant Maybe (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) 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
forall a. Maybe a
Nothing) (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Biforked :. Construction Biforked) := T_ Covariant Binary a
next
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Right)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Right)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Right)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a
next)) = (<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall a. a -> Maybe a
Just ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U (Product
   (Construction Wye a)
   (TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
 -> (<:*:>)
      (Construction Wye)
      ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Product
         (Construction Wye a)
         (TU
            Covariant
            Covariant
            (Biforked <:.> Construction Biforked)
            (T_ Covariant Binary)
            a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant 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_ Covariant Binary)
     a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall s a. s -> a -> Product s a
(:*:) Construction Wye a
rst (TU
   Covariant
   Covariant
   (Biforked <:.> Construction Biforked)
   (T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant 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_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      (Biforked <:.> Construction Biforked)
      (T_ Covariant Binary)
      a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     (Biforked <:.> Construction Biforked)
     (T_ Covariant Binary)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant 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_ Covariant Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_ Covariant Binary a))
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_ Covariant Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Biforked (T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall a. a -> Biforked a
Rightward (Construction Biforked (T_ Covariant Binary a)
 -> (Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
    -> Construction Biforked (T_ Covariant Binary a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> (Biforked :. Construction Biforked) := T_ Covariant Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_ Covariant Binary a
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Construction Biforked (T_ Covariant Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a
T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a)
 -> T_ Covariant Binary a)
-> (a :*: TU Covariant Covariant Maybe (Construction Wye) a)
-> T_ Covariant Binary a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
x a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> a :*: TU Covariant Covariant Maybe (Construction Wye) a
forall s a. s -> a -> Product s a
:*: ((Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Construction Wye a -> (Maybe :. Construction Wye) := a
forall a. a -> Maybe a
Just Construction Wye a
lst)) (((Biforked :. Construction Biforked) := T_ Covariant Binary a)
 -> Maybe
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a))
-> ((Biforked :. Construction Biforked) := T_ Covariant Binary a)
-> Maybe
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (Biforked :. Construction Biforked) := T_ Covariant Binary a
next
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Right)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Right)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Right)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
_ (Left Construction Wye a
_) :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_ Covariant Binary)
  a
_) = Rotational
  ('Down 'Right)
  (Construction Wye
   <:*:> ((Biforked <:.> Construction Biforked)
          <:.> T_ Covariant Binary))
  a
forall a. Maybe a
Nothing
	rotation ((<:*:>)
  (Construction Wye)
  ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
  a
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:*:>)
   (Construction Wye)
   ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
   a
 -> Product
      (Construction Wye a)
      (TU
         Covariant
         Covariant
         (Biforked <:.> Construction Biforked)
         (T_ Covariant Binary)
         a))
-> (Tagged
      ('Down 'Right)
      ((<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
    -> (<:*:>)
         (Construction Wye)
         ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
         a)
-> Tagged
     ('Down 'Right)
     ((<:*:>)
        (Construction Wye)
        ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
        a)
-> Product
     (Construction Wye a)
     (TU
        Covariant
        Covariant
        (Biforked <:.> Construction Biforked)
        (T_ Covariant Binary)
        a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged
  ('Down 'Right)
  ((<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a)
-> (<:*:>)
     (Construction Wye)
     ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)
     a
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
_ Wye (Construction Wye a)
End :*: TU
  Covariant
  Covariant
  (Biforked <:.> Construction Biforked)
  (T_ Covariant Binary)
  a
_) = Rotational
  ('Down 'Right)
  (Construction Wye
   <:*:> ((Biforked <:.> Construction Biforked)
          <:.> T_ Covariant Binary))
  a
forall a. Maybe a
Nothing