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

module Pandora.Paradigm.Structure.Some.Binary where

import Pandora.Core.Functor (type (:.), type (:=), type (:=>))
import Pandora.Pattern.Category (identity, (.), ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), ($$>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (empty)
import Pandora.Pattern.Functor.Bindable ((>>=))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Paradigm.Primary ()
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (order)
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator, Zero))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor (Comparison)
import Pandora.Paradigm.Primary.Functor.Convergence (Convergence (Convergence))
import Pandora.Paradigm.Primary.Functor.Function ((%), (&))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), PQ_ (PQ_), type (<:.>), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (over, view)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Heighth), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
	, Morph (Rotate, Into, Insert, Lookup, Vary, Key, Element), Vertical (Up, Down), morph, premorph, lookup)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Root), sub)
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))

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
	# Construct (extract x) (Both # rebalance (deconstruct x) # rebalance (deconstruct y))
	# Construct (extract y) (Both # x # rebalance (deconstruct y))
	# Construct (extract x) (Both # rebalance (deconstruct x) # y)

instance Morphable Insert Binary where
	type Morphing Insert Binary = (Identity <:.:> Comparison := (:*:)) <:.:> Binary := (->)
	morphing :: (<:.>) (Tagged 'Insert) Binary a -> Morphing 'Insert Binary a
morphing (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Insert) Binary a -> Binary a)
-> (<:.>) (Tagged 'Insert) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Insert) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction Wye a)
Nothing) = (T_U Covariant Covariant Product Identity Comparison a -> Binary a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     Binary
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant Product Identity Comparison a
  -> Binary a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant Product Identity Comparison)
      Binary
      a)
-> (T_U Covariant Covariant Product Identity Comparison a
    -> Binary a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     Binary
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Comparison a
_)) -> Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> Binary a) -> Construction Wye a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x
	morphing (Binary a -> Maybe (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Binary a -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Insert) Binary a -> Binary a)
-> (<:.>) (Tagged 'Insert) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Insert) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just Construction Wye a
ne) = (T_U Covariant Covariant Product Identity Comparison a -> Binary a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     Binary
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant Product Identity Comparison a
  -> Binary a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant Product Identity Comparison)
      Binary
      a)
-> (T_U Covariant Covariant Product Identity Comparison a
    -> Binary a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     Binary
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Convergence a -> a -> Ordering
f)) ->
		let continue :: Binary a -> Binary a
continue Binary a
xs = T_U
  Covariant
  Covariant
  (->)
  (T_U Covariant Covariant Product Identity Comparison)
  Binary
  a
-> T_U Covariant Covariant Product Identity Comparison a
-> Binary a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (->)
   (T_U Covariant Covariant Product Identity Comparison)
   Binary
   a
 -> T_U Covariant Covariant Product Identity Comparison a
 -> Binary a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     Binary
     a
-> T_U Covariant Covariant Product Identity Comparison a
-> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Binary a -> Morphing 'Insert Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
struct ~> Morphing mod struct
morph @Insert Binary a
xs (T_U Covariant Covariant Product Identity Comparison a -> Binary a)
-> T_U Covariant Covariant Product Identity Comparison a
-> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a
-> Comparison a
-> T_U Covariant Covariant Product Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (Identity a
 -> Comparison a
 -> T_U Covariant Covariant Product Identity Comparison a)
-> Identity a
-> Comparison a
-> T_U Covariant Covariant Product Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity a
x (Comparison a
 -> T_U Covariant Covariant Product Identity Comparison a)
-> Comparison a
-> T_U Covariant Covariant Product Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (a -> a -> Ordering) -> Comparison a
forall r a. (a -> a -> r) -> Convergence r a
Convergence a -> a -> Ordering
f
		in Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> Binary a) -> Construction Wye a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> a -> Ordering
f a
x (a -> Ordering) -> a -> Ordering
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye a
ne 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 (Construction Wye a
 -> Construction Wye a
 -> Construction Wye a
 -> Ordering
 -> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
ne (Construction Wye a
 -> Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Lens (Construction Wye a) (Binary a)
-> (Binary a -> Binary a)
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
over (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Left t, Covariant t) =>
t :~. Substructural 'Left t
sub @Left) Binary a -> Binary a
continue Construction Wye a
ne (Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a -> Ordering -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Lens (Construction Wye a) (Binary a)
-> (Binary a -> Binary a)
-> Construction Wye a
-> Construction Wye a
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
over (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Right t, Covariant t) =>
t :~. Substructural 'Right t
sub @Right) Binary a -> Binary a
continue Construction Wye a
ne

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

instance Nullable Binary where
	null :: (Predicate :. Binary) := a
null = (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Binary a -> Boolean) -> (Predicate :. Binary) := a)
-> (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall (m :: * -> * -> *) a b. Category m => 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 = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Left) Binary a) (Substructural 'Left Binary a)
substructure = ((<:.>) (Tagged 'Left) Binary a
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) Binary a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) Binary a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Left) Binary a
  -> Store
       (TU Covariant Covariant Maybe (Construction Wye) a)
       ((<:.>) (Tagged 'Left) Binary a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Left) Binary a)
      (TU Covariant Covariant Maybe (Construction Wye) a))
-> ((<:.>) (Tagged 'Left) Binary a
    -> Store
         (TU Covariant Covariant Maybe (Construction Wye) a)
         ((<:.>) (Tagged 'Left) Binary a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) Binary a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) Binary a
bintree -> case TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) a
 -> (Maybe :. Construction Wye) := a)
-> ((<:.>) (Tagged 'Left) Binary a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Left) Binary a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Wye) a
 <:= Tagged 'Left)
-> ((<:.>) (Tagged 'Left) Binary a
    -> Tagged
         'Left (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Left) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) Binary a
-> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) (Tagged 'Left) Binary a
 -> (Maybe :. Construction Wye) := a)
-> (<:.>) (Tagged 'Left) Binary a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) Binary a
bintree of
		(Maybe :. Construction Wye) := a
Nothing -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) Binary a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) Binary a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) Binary a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) Binary a
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Left) Binary a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) a. Category m => m a a
identity
		Just Construction Wye a
tree -> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Left) Binary a)
-> (Construction Wye a
    -> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) Binary a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     (Construction Wye a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) Binary a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> PQ_
  (->)
  Store
  (Construction Wye a)
  (TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     (Construction Wye a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Left t, Covariant t) =>
t :~. Substructural 'Left t
sub @Left) Construction Wye a
tree

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

-------------------------------------- Non-empty binary tree ---------------------------------------

type instance Nonempty Binary = Construction Wye

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

instance Morphable Insert (Construction Wye) where
	type Morphing Insert (Construction Wye) = (Identity <:.:> Comparison := (:*:)) <:.:> Construction Wye := (->)
	morphing :: (<:.>) (Tagged 'Insert) (Construction Wye) a
-> Morphing 'Insert (Construction Wye) a
morphing ((<:.>) (Tagged 'Insert) (Construction Wye) a -> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construction Wye a
nonempty_list) = (T_U Covariant Covariant Product Identity Comparison a
 -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     (Construction Wye)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant Product Identity Comparison a
  -> Construction Wye a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant Product Identity Comparison)
      (Construction Wye)
      a)
-> (T_U Covariant Covariant Product Identity Comparison a
    -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     (Construction Wye)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Convergence a -> a -> Ordering
f)) ->
		let continue :: Construction Wye a -> Construction Wye a
continue Construction Wye a
xs = T_U
  Covariant
  Covariant
  (->)
  (T_U Covariant Covariant Product Identity Comparison)
  (Construction Wye)
  a
-> T_U Covariant Covariant Product Identity Comparison a
-> Construction Wye a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (->)
   (T_U Covariant Covariant Product Identity Comparison)
   (Construction Wye)
   a
 -> T_U Covariant Covariant Product Identity Comparison a
 -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant Product Identity Comparison)
     (Construction Wye)
     a
-> T_U Covariant Covariant Product Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Nonempty Binary a -> Morphing 'Insert (Nonempty Binary) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
struct ~> Morphing mod struct
morph @Insert @(Nonempty Binary) Nonempty Binary a
Construction Wye a
xs (T_U Covariant Covariant Product Identity Comparison a
 -> Construction Wye a)
-> T_U Covariant Covariant Product Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant Product Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (Identity a
 -> Convergence Ordering a
 -> T_U Covariant Covariant Product Identity Comparison a)
-> Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant Product Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity a
x (Convergence Ordering a
 -> T_U Covariant Covariant Product Identity Comparison a)
-> Convergence Ordering a
-> T_U Covariant Covariant Product Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (a -> a -> Ordering) -> Convergence Ordering a
forall r a. (a -> a -> r) -> Convergence r a
Convergence a -> a -> Ordering
f in
		let change :: TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
change = Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a
 -> TU Covariant Covariant Maybe (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> ((Maybe :. Construction Wye) := a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Construction Wye a
continue (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) (((Maybe :. Construction Wye) := a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run in
		Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall a. a -> a -> a -> Ordering -> a
order (Construction Wye a
 -> Construction Wye a
 -> Construction Wye a
 -> Ordering
 -> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
nonempty_list
			# over (sub @Left) change nonempty_list
			# over (sub @Right) change nonempty_list
			# f x (extract nonempty_list)

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

instance Substructure Root (Construction Wye) where
	type Substructural Root (Construction Wye) = Identity
	substructure :: Lens
  ((<:.>) (Tagged 'Root) (Construction Wye) a)
  (Substructural 'Root (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Root) (Construction Wye) a
 -> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
     (Identity a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Root) (Construction Wye) a
  -> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Root) (Construction Wye) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Construction Wye) a
    -> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Construction Wye) a
bintree -> case (<:.>) (Tagged 'Root) (Construction Wye) a -> Construction Wye a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower (<:.>) (Tagged 'Root) (Construction Wye) a
bintree of
		Construct a
x (Wye :. Construction Wye) := a
xs -> (((:*:) (Identity a) :. (->) (Identity a))
 := (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a))
  := (<:.>) (Tagged 'Root) (Construction Wye) a)
 -> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> (((:*:) (Identity a) :. (->) (Identity a))
    := (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store (Identity a) ((<:.>) (Tagged 'Root) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> ((:*:) (Identity a) :. (->) (Identity a))
   := (<:.>) (Tagged 'Root) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> (Identity a -> Construction Wye a)
-> Identity 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) (a -> Construction Wye a)
-> (Identity a -> a) -> Identity a -> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => a <:= t
extract

instance Substructure Left (Construction Wye) where
	type Substructural Left (Construction Wye) = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Left) (Construction Wye) a)
  (Substructural 'Left (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Left) (Construction Wye) a
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Left) (Construction Wye) a
  -> Store
       (TU Covariant Covariant Maybe (Construction Wye) a)
       ((<:.>) (Tagged 'Left) (Construction Wye) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Left) (Construction Wye) a)
      (TU Covariant Covariant Maybe (Construction Wye) a))
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Store
         (TU Covariant Covariant Maybe (Construction Wye) a)
         ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Construction Wye) a
bintree -> case Construction Wye a <:= Tagged 'Left
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Left)
-> Construction Wye a <:= Tagged 'Left
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Construction Wye) a
-> Primary (Tagged 'Left <:.> Construction Wye) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Left) (Construction Wye) a
bintree of
		Construct a
x Wye (Construction Wye a)
End -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (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 -> 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)
-> (Construction Wye a -> Wye (Construction Wye a))
-> 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)
forall a. a -> Wye a
Left) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) (((Maybe :. Construction Wye) := a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Left Construction Wye a
lst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Wye (Construction Wye a)
forall a. Wye a
End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Right Construction Wye a
rst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Substructure Right (Construction Wye) where
	type Substructural Right (Construction Wye) = Binary
	substructure :: Lens
  ((<:.>) (Tagged 'Right) (Construction Wye) a)
  (Substructural 'Right (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Right) (Construction Wye) a
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ (((<:.>) (Tagged 'Right) (Construction Wye) a
  -> Store
       (TU Covariant Covariant Maybe (Construction Wye) a)
       ((<:.>) (Tagged 'Right) (Construction Wye) a))
 -> PQ_
      (->)
      Store
      ((<:.>) (Tagged 'Right) (Construction Wye) a)
      (TU Covariant Covariant Maybe (Construction Wye) a))
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Store
         (TU Covariant Covariant Maybe (Construction Wye) a)
         ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> PQ_
     (->)
     Store
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
     (TU Covariant Covariant Maybe (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) (Construction Wye) a
bintree -> case Construction Wye a <:= Tagged 'Right
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Wye a <:= Tagged 'Right)
-> Construction Wye a <:= Tagged 'Right
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) (Construction Wye) a
-> Primary (Tagged 'Right <:.> Construction Wye) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Right) (Construction Wye) a
bintree of
		Construct a
x Wye (Construction Wye a)
End -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (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 -> 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)
-> (Construction Wye a -> Wye (Construction Wye a))
-> 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)
forall a. a -> Wye a
Right) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) (((Maybe :. Construction Wye) := a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Left Construction Wye a
lst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Right Construction Wye a
rst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Wye (Construction Wye a)
forall a. Wye a
End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Wye) a)
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Wye) a)
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst TU Covariant Covariant Maybe (Construction Wye) a
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Wye) a))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> Product s a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> Wye (Construction Wye a))
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> ((Maybe :. Construction Wye) := a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a))
-> (TU Covariant Covariant Maybe (Construction Wye) a
    -> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> Wye (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

-------------------------------------- Prefixed binary tree ----------------------------------------

instance Chain k => Morphable (Lookup Key) (Prefixed Binary k) where
	type Morphing (Lookup Key) (Prefixed Binary k) = (->) k <:.> Maybe
	morphing :: (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Morphing ('Lookup 'Key) (Prefixed Binary k) a
morphing (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Maybe (Construction Wye (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Maybe (Construction Wye (Product k a)))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Maybe (Construction Wye (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Binary k a
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction Wye (Product k a))
Nothing) = Maybe a -> TU Covariant Covariant ((->) k) Maybe a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Maybe a
forall a. Maybe a
Nothing
	morphing (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Maybe (Construction Wye (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Maybe (Construction Wye (Product k a)))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Maybe (Construction Wye (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Binary k a
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just Construction Wye (Product k a)
tree) = (((->) k :. Maybe) := a) -> TU Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) k :. Maybe) := a)
 -> TU Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) := a)
-> TU Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \k
key ->
		let root :: Product k a
root = Product k a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye (Product k a)
tree in k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> Product k a -> k
forall a b. (a :*: b) -> a
attached Product k a
root Ordering -> (Ordering -> Maybe a) -> Maybe a
forall a b. a -> (a -> b) -> b
& Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall a. a -> a -> a -> Ordering -> a
order (Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a)
-> Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Maybe a
forall a. a -> Maybe a
Just (a <:= Product k
forall (t :: * -> *) a. Extractable t => a <:= t
extract Product k a
root)
			# lookup @Key key (Prefixed $ view # sub @Left # tree)
			# lookup @Key key (Prefixed $ view # sub @Right # tree)

instance Chain k => Morphable (Vary Element) (Prefixed Binary k) where
	type Morphing (Vary Element) (Prefixed Binary k) = (Product k <:.> Identity) <:.:> Prefixed Binary k := (->)
	morphing :: (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Morphing ('Vary 'Element) (Prefixed Binary k) a
morphing (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Maybe (Construction Wye (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Maybe (Construction Wye (Product k a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Maybe (Construction Wye (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Binary k a
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction Wye (Product k a))
Nothing) = (TU Covariant Covariant (Product k) Identity a
 -> Prefixed Binary k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product k) Identity)
     (Prefixed Binary k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU Covariant Covariant (Product k) Identity a
  -> Prefixed Binary k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product k) Identity)
      (Prefixed Binary k)
      a)
-> (TU Covariant Covariant (Product k) Identity a
    -> Prefixed Binary k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product k) Identity)
     (Prefixed Binary k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (k
key :*: Identity a
value)) -> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Prefixed Binary k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Prefixed Binary k a)
-> (Product k a
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> Product k a
-> Prefixed Binary k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye (Product k a)
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye (Product k a)
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> (Product k a -> Construction Wye (Product k a))
-> Product k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product k a -> Construction Wye (Product k a)
forall a. a :=> Nonempty Binary
leaf (Product k a -> Prefixed Binary k a)
-> Product k a -> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ k
key k -> a -> Product k a
forall s a. s -> a -> Product s a
:*: a
value
	morphing (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Maybe (Construction Wye (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Maybe (Construction Wye (Product k a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Maybe (Construction Wye (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Binary k a
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just Construction Wye (Product k a)
tree) = (TU Covariant Covariant (Product k) Identity a
 -> Prefixed Binary k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product k) Identity)
     (Prefixed Binary k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU Covariant Covariant (Product k) Identity a
  -> Prefixed Binary k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product k) Identity)
      (Prefixed Binary k)
      a)
-> (TU Covariant Covariant (Product k) Identity a
    -> Prefixed Binary k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product k) Identity)
     (Prefixed Binary k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (k
key :*: Identity a
value)) ->
		let continue :: TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
continue TU Covariant Covariant Maybe (Construction Wye) (Product k a)
xs = Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Binary k a
 -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U
  Covariant
  Covariant
  (->)
  (TU Covariant Covariant (Product k) Identity)
  (Prefixed Binary k)
  a
-> TU Covariant Covariant (Product k) Identity a
-> Prefixed Binary k a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U
   Covariant
   Covariant
   (->)
   (TU Covariant Covariant (Product k) Identity)
   (Prefixed Binary k)
   a
 -> TU Covariant Covariant (Product k) Identity a
 -> Prefixed Binary k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product k) Identity)
     (Prefixed Binary k)
     a
-> TU Covariant Covariant (Product k) Identity a
-> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Prefixed Binary k a
-> Morphing ('Vary 'Element) (Prefixed Binary k) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
struct ~> Morphing mod struct
morph @(Vary Element) (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Prefixed Binary k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed TU Covariant Covariant Maybe (Construction Wye) (Product k a)
xs) (TU Covariant Covariant (Product k) Identity a
 -> Prefixed Binary k a)
-> TU Covariant Covariant (Product k) Identity a
-> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Product k (Identity a)
-> TU Covariant Covariant (Product k) Identity 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 (k
key k -> Identity a -> Product k (Identity a)
forall s a. s -> a -> Product s a
:*: a -> Identity a
forall a. a -> Identity a
Identity a
value)
		in let root :: Product k a
root = Product k a <:= Construction Wye
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Wye (Product k a)
tree in TU Covariant Covariant Maybe (Construction Wye) (Product k a)
-> Prefixed Binary k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction Wye) (Product k a)
 -> Prefixed Binary k a)
-> (Construction Wye (Product k a)
    -> TU Covariant Covariant Maybe (Construction Wye) (Product k a))
-> Construction Wye (Product k a)
-> Prefixed Binary k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye (Product k a)
-> TU Covariant Covariant Maybe (Construction Wye) (Product k a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Wye (Product k a) -> Prefixed Binary k a)
-> Construction Wye (Product k a) -> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> Product k a -> k
forall a b. (a :*: b) -> a
attached Product k a
root Ordering
-> (Ordering -> Construction Wye (Product k a))
-> Construction Wye (Product k a)
forall a b. a -> (a -> b) -> b
& Construction Wye (Product k a)
-> Construction Wye (Product k a)
-> Construction Wye (Product k a)
-> Ordering
-> Construction Wye (Product k a)
forall a. a -> a -> a -> Ordering -> a
order
			# over (sub @Root) ($$> value) tree # over (sub @Left) continue tree # over (sub @Right) continue tree

---------------------------------- Prefixed non-empty binary tree ----------------------------------

instance Chain key => Morphable (Lookup Key) (Prefixed (Construction Wye) key) where
	type Morphing (Lookup Key) (Prefixed (Construction Wye) key) = (->) key <:.> Maybe
	morphing :: (<:.>) (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Morphing ('Lookup 'Key) (Prefixed (Construction Wye) key) a
morphing (Prefixed (Construction Wye) key a -> Construction Wye (key :*: a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed (Construction Wye) key a -> Construction Wye (key :*: a))
-> ((<:.>)
      (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
    -> Prefixed (Construction Wye) key a)
-> (<:.>)
     (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Construction Wye (key :*: a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Prefixed (Construction Wye) key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct key :*: a
x (Wye :. Construction Wye) := (key :*: a)
xs) = (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) key :. Maybe) := a)
 -> TU Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \key
key ->
		key
key key -> key -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (key :*: a) -> key
forall a b. (a :*: b) -> a
attached key :*: a
x Ordering -> (Ordering -> Maybe a) -> Maybe a
forall a b. a -> (a -> b) -> b
& Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall a. a -> a -> a -> Ordering -> a
order (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a <:= Product key
forall (t :: * -> *) a. Extractable t => a <:= t
extract key :*: a
x)
			(Lens
  ((Wye :. Construction Wye) := (key :*: a))
  (Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall src tgt. Lens src tgt -> src -> tgt
view (Lens
   ((Wye :. Construction Wye) := (key :*: a))
   (Maybe (Construction Wye (key :*: a)))
 -> ((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Construction Wye (key :*: a)))
-> Lens
     ((Wye :. Construction Wye) := (key :*: a))
     (Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Left t, Covariant t) =>
t :~. Substructural 'Left t
sub @Left (((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs Maybe (Construction Wye (key :*: a))
-> (Construction Wye (key :*: a) -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= key -> Prefixed (Construction Wye) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Wye) key a -> Maybe a)
-> (Construction Wye (key :*: a)
    -> Prefixed (Construction Wye) key a)
-> Construction Wye (key :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed)
			(Lens
  ((Wye :. Construction Wye) := (key :*: a))
  (Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall src tgt. Lens src tgt -> src -> tgt
view (Lens
   ((Wye :. Construction Wye) := (key :*: a))
   (Maybe (Construction Wye (key :*: a)))
 -> ((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Construction Wye (key :*: a)))
-> Lens
     ((Wye :. Construction Wye) := (key :*: a))
     (Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (f :: k) (t :: * -> *).
(Substructure f t, Covariant t) =>
t :~. Substructural f t
forall (t :: * -> *).
(Substructure 'Right t, Covariant t) =>
t :~. Substructural 'Right t
sub @Right (((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Construction Wye (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs Maybe (Construction Wye (key :*: a))
-> (Construction Wye (key :*: a) -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= key -> Prefixed (Construction Wye) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Wye) key a -> Maybe a)
-> (Construction Wye (key :*: a)
    -> Prefixed (Construction Wye) key a)
-> Construction Wye (key :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed)

-------------------------------------- Zipper of binary tree ---------------------------------------

data Biforked a = Top | Leftward a | Rightward a

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

type Bifurcation = Biforked <:.> Construction Biforked

type Bicursor = Identity <:.:> Binary := (:*:)

type instance Zipper (Construction Wye) = Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)

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

instance Morphable (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
	type Morphing (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
		= Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
	morphing :: (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> Morphing
     ('Rotate ('Down 'Left))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Left Construction Wye a
lst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next)) =
		(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome Construction Wye a
lst (TU Covariant Covariant Bifurcation Bicursor a
 -> (:=)
      (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Product Identity Binary a)
 -> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Product Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Product Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Product Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant Product Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> Binary a -> T_U Covariant Covariant Product Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) Binary a
forall (t :: * -> *) a. Avoidable t => t a
empty (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next)) =
		(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome Construction Wye a
lst (TU Covariant Covariant Bifurcation Bicursor a
 -> (:=)
      (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Product Identity Binary a)
 -> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Product Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Product Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Product Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant Product Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> Binary a -> T_U Covariant Covariant Product Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
rst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ (Right Construction Wye a
_) :*: TU Covariant Covariant Bifurcation Bicursor a
_) = Morphing
  ('Rotate ('Down 'Left))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
forall (t :: * -> *) a. Avoidable t => t a
empty
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Left)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Left)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Left)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ Wye (Construction Wye a)
End :*: TU Covariant Covariant Bifurcation Bicursor a
_) = Morphing
  ('Rotate ('Down 'Left))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
	type Morphing (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
		= Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
	morphing :: (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> Morphing
     ('Rotate ('Down 'Right))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Right Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next)) =
		(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome Construction Wye a
rst (TU Covariant Covariant Bifurcation Bicursor a
 -> (:=)
      (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Product Identity Binary a)
 -> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Product Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Product Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Product Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant Product Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> Binary a -> T_U Covariant Covariant Product Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) Binary a
forall (t :: * -> *) a. Avoidable t => t a
empty (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next)) =
		(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome Construction Wye a
rst (TU Covariant Covariant Bifurcation Bicursor a
 -> (:=)
      (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant Product Identity Binary a)
 -> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> TU
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant Product Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant Product Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant Product Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant Product Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant Product Identity Binary a)
 -> TU
      Covariant
      Covariant
      Maybe
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
-> TU
     Covariant
     Covariant
     Maybe
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant Product Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> T_U Covariant Covariant Product Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> Binary a -> T_U Covariant Covariant Product Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u Product a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a -> Binary a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Wye a
lst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant Product Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant Product Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant Product Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant Product Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant Product Identity Binary a
next
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ (Left Construction Wye a
_) :*: TU Covariant Covariant Bifurcation Bicursor a
_) = Morphing
  ('Rotate ('Down 'Right))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
forall (t :: * -> *) a. Avoidable t => t a
empty
	morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=)
   (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
 -> Product
      (Construction Wye a)
      (TU Covariant Covariant Bifurcation Bicursor a))
-> ((<:.>)
      (Tagged ('Rotate ('Down 'Right)))
      ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
      a
    -> (:=)
         (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a)
-> (<:.>)
     (Tagged ('Rotate ('Down 'Right)))
     ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
     a
-> Product
     (Construction Wye a)
     (TU Covariant Covariant Bifurcation Bicursor a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>)
  (Tagged ('Rotate ('Down 'Right)))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
-> (:=)
     (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) Product a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ Wye (Construction Wye a)
End :*: TU Covariant Covariant Bifurcation Bicursor a
_) = Morphing
  ('Rotate ('Down 'Right))
  ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := Product)
  a
forall (t :: * -> *) a. Avoidable t => t a
empty

leaf :: a :=> Nonempty Binary
leaf :: a :=> Nonempty Binary
leaf 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