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

import Pandora.Core.Functor (type (~>), type (:=), type (:=>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|-|-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bindable ((=<<))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), type (:*:), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), (&))
import Pandora.Paradigm.Primary.Algebraic ((!!!>-), (<-*-), (<-*-*-), extract, point)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (order)
import Pandora.Paradigm.Primary.Functor (Comparison)
import Pandora.Paradigm.Primary.Functor.Convergence (Convergence (Convergence))
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.Wye (Wye (End, Left, Right, Both))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Primary (twosome)
import Pandora.Paradigm.Schemes (TT (TT), T_U (T_U), P_Q_T (P_Q_T), type (<::>), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Conditional ((?))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!), (=||))
import Pandora.Paradigm.Inventory.Ability.Gettable (get)
import Pandora.Paradigm.Inventory.Ability.Settable (set)
import Pandora.Paradigm.Inventory.Ability.Modifiable (modify)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Convex, Obscure)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), morph, premorph
	, Morph (Rotate, Into, Insert, Lookup, Vary, Key, Element), Vertical (Up, Down), lookup, vary)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure), Segment (Root), sub)
import Pandora.Paradigm.Structure.Ability.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))

type Binary = Maybe <::> Construction Wye

instance {-# OVERLAPS #-} Traversable (->) (->) (Construction Wye) where
	a -> u b
f <<- :: (a -> u b) -> Construction Wye a -> u (Construction Wye b)
<<- (Construct a
x (Left Construction Wye a
l)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> Wye a
Left (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
l)
	a -> u b
f <<- (Construct a
x (Right Construction Wye a
r)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> Wye a
Right (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
r)
	a -> u b
f <<- (Construct a
x (Both Construction Wye a
l Construction Wye a
r)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b
-> Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> a -> Wye a
Both (Construction Wye b
 -> Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b)
-> u (Construction Wye b -> (Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
l u (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
r)
	a -> u b
f <<- (Construct a
x Wye (Construction Wye a)
End) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> ((Wye :. Construction Wye) := b) -> b -> Construction Wye b
forall a b c. (a -> b -> c) -> b -> a -> c
% (Wye :. Construction Wye) := b
forall a. Wye a
End (b -> Construction Wye b) -> u b -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
x

--rebalance :: Chain a => (Wye :. Construction Wye := a) -> Nonempty Binary a
--rebalance (Both x y) = extract x <=> extract y & 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 (<::>) (Tagged 'Insert) Binary a
struct = case TT Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Wye) a
 -> (Maybe :. Construction Wye) := a)
-> TT Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) (Tagged 'Insert) Binary a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged 'Insert) Binary a
struct of
		(Maybe :. Construction Wye) := a
Nothing -> (T_U Covariant Covariant (:*:) Identity Comparison a
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a
  -> TT Covariant Covariant Maybe (Construction Wye) a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant (:*:) Identity Comparison)
      Binary
      a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
    -> TT Covariant Covariant Maybe (Construction Wye) a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) Identity Comparison)
     Binary
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (Identity a
x :*: Comparison a
_)) -> Construction Wye a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> TT Covariant Covariant Maybe (Construction Wye) 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
		Just Construction Wye a
struct -> (T_U Covariant Covariant (:*:) Identity Comparison a
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a
  -> TT Covariant Covariant Maybe (Construction Wye) a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant (:*:) Identity Comparison)
      Binary
      a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
    -> TT Covariant Covariant Maybe (Construction Wye) a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) Identity Comparison)
     Binary
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (Identity a
x :*: Convergence a -> a -> Ordering
f)) -> forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Wye a
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!
			let continue :: Construction Wye a -> Construction Wye a
continue Construction Wye a
xs = T_U
  Covariant
  Covariant
  (->)
  (T_U Covariant Covariant (:*:) Identity Comparison)
  (Construction Wye)
  a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (->)
   (T_U Covariant Covariant (:*:) Identity Comparison)
   (Construction Wye)
   a
 -> T_U Covariant Covariant (:*:) Identity Comparison a
 -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) Identity Comparison)
     (Construction Wye)
     a
-> T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a
 -> Construction Wye a)
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a
-> Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
 -> Comparison a
 -> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Identity a
-> Comparison a
-> T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a)
-> Comparison a
-> T_U Covariant Covariant (:*:) 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
			let step :: Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step = ((Maybe :. Construction Wye) := a)
-> Construction Wye a -> Construction Wye a -> Construction Wye a
forall clause a. Conditional clause => clause -> a -> a -> a
(?) (((Maybe :. Construction Wye) := a)
 -> Construction Wye a -> Construction Wye a -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> (Maybe :. Construction Wye) := a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a
 -> Construction Wye a
 -> Construction Wye a
 -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (Straight (->)) (:*:) (:*:) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- (Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @(Obscure Lens) Construction Wye a -> Construction Wye a
continue (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (Straight (->)) (:*:) (:*:) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- Construction Wye a
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall k (i :: k) e r. Settable i => Setting i e r
set @(Obscure Lens) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) 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
struct (Construction Wye a
 -> Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
struct (Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a -> Ordering -> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
struct (Ordering -> Construction Wye a) -> Ordering -> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> a -> Ordering
f a
x (a -> Ordering) -> a -> Ordering
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye a
struct

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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case { TT Maybe (Construction Wye a)
Nothing -> Boolean
True ; Binary a
_ -> Boolean
False }

instance Substructure Left Binary where
	type Available Left Binary = Maybe
	type Substance Left Binary = Construction Wye
	substructure :: Lens
  (Available 'Left Binary)
  ((<:.>) (Tagged 'Left) Binary a)
  (Substance 'Left Binary a)
substructure = ((<:.>) (Tagged 'Left) Binary a
 -> Store
      (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Left) Binary a)
     (Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) Binary a
  -> Store
       (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
 -> P_Q_T
      (->)
      Store
      Maybe
      ((<:.>) (Tagged 'Left) Binary a)
      (Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a
    -> Store
         (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Left) Binary a)
     (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) Binary a
struct -> case Binary a -> Maybe (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Binary a -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a -> Binary a)
-> (<:.>) (Tagged 'Left) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) Binary a -> Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (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
struct of
		Maybe (Construction Wye a)
Nothing -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Left) Binary a)
 -> Store
      (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Left) Binary a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a) -> (<:.>) (Tagged 'Left) Binary a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Left) Binary a
forall s a. s -> a -> s :*: a
:*: Binary a -> (<:.>) (Tagged 'Left) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Binary a -> (<:.>) (Tagged 'Left) Binary a)
-> (Maybe (Construction Wye a) -> Binary a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe (Construction Wye a) -> Binary a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT
		Just Construction Wye a
tree -> Binary a -> (<:.>) (Tagged 'Left) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Binary a -> (<:.>) (Tagged 'Left) Binary a)
-> (Construction Wye a -> Binary a)
-> Construction Wye a
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Wye a -> (<:.>) (Tagged 'Left) Binary a)
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- P_Q_T (->) Store Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left) Construction Wye a
tree

instance Substructure Right Binary where
	type Available Right Binary = Maybe
	type Substance Right Binary = Construction Wye
	substructure :: Lens
  (Available 'Right Binary)
  ((<:.>) (Tagged 'Right) Binary a)
  (Substance 'Right Binary a)
substructure = ((<:.>) (Tagged 'Right) Binary a
 -> Store
      (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Right) Binary a)
     (Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) Binary a
  -> Store
       (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
 -> P_Q_T
      (->)
      Store
      Maybe
      ((<:.>) (Tagged 'Right) Binary a)
      (Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
    -> Store
         (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Right) Binary a)
     (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) Binary a
struct -> case TT Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Wye) a
 -> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
    -> TT Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Right) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tagged 'Right (TT Covariant Covariant Maybe (Construction Wye) a)
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (TT Covariant Covariant Maybe (Construction Wye) a)
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> ((<:.>) (Tagged 'Right) Binary a
    -> Tagged
         'Right (TT Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Right) Binary a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) Binary a
-> Tagged
     'Right (TT Covariant Covariant Maybe (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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
struct of
		Maybe (Construction Wye a)
Nothing -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Right) Binary a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Right) Binary a)
 -> Store
      (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Right) Binary a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a) -> (<:.>) (Tagged 'Right) Binary a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Right) Binary a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Right) Binary a)
-> (Maybe (Construction Wye a)
    -> TT Covariant Covariant Maybe (Construction Wye) a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe (Construction Wye a)
-> TT Covariant Covariant Maybe (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT
		Just Construction Wye a
tree -> TT Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant Maybe (Construction Wye) a
 -> (<:.>) (Tagged 'Right) Binary a)
-> (Construction Wye a
    -> TT Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Wye a -> (<:.>) (Tagged 'Right) Binary a)
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
-> Store
     (Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- P_Q_T (->) Store Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
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
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a
 -> TT Covariant Covariant Maybe (Construction Wye) a)
-> ((<::>) (Tagged ('Into Binary)) (Construction Wye) a
    -> Construction Wye a)
-> (<::>) (Tagged ('Into Binary)) (Construction Wye) a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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
struct) = (T_U Covariant Covariant (:*:) Identity Comparison a
 -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a
  -> Construction Wye a)
 -> T_U
      Covariant
      Covariant
      (->)
      (T_U Covariant Covariant (:*:) Identity Comparison)
      (Construction Wye)
      a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
    -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) Identity Comparison)
     (Construction Wye)
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 (:*:) Identity Comparison)
  (Construction Wye)
  a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (->)
   (T_U Covariant Covariant (:*:) Identity Comparison)
   (Construction Wye)
   a
 -> T_U Covariant Covariant (:*:) Identity Comparison a
 -> Construction Wye a)
-> T_U
     Covariant
     Covariant
     (->)
     (T_U Covariant Covariant (:*:) Identity Comparison)
     (Construction Wye)
     a
-> T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a
 -> Construction Wye a)
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
 -> Convergence Ordering a
 -> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) 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 (:*:) Identity Comparison a)
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) 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 step :: Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step = Maybe (Construction Wye a)
-> Construction Wye a -> Construction Wye a -> Construction Wye a
forall clause a. Conditional clause => clause -> a -> a -> a
(?) (Maybe (Construction Wye a)
 -> Construction Wye a -> Construction Wye a -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> Maybe (Construction Wye a))
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a
 -> Construction Wye a
 -> Construction Wye a
 -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (Straight (->)) (:*:) (:*:) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- (Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @(Obscure Lens) Construction Wye a -> Construction Wye a
continue (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a -> Construction Wye a)
-> (Lens Maybe (Construction Wye a) (Construction Wye a)
    -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (Straight (->)) (:*:) (:*:) t,
 Semimonoidal (Straight (->)) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- Construction Wye a
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall k (i :: k) e r. Settable i => Setting i e r
set @(Obscure Lens) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) 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
struct (Construction Wye a
 -> Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
struct (Construction Wye a -> Ordering -> Construction Wye a)
-> Construction Wye a -> Ordering -> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a -> Construction Wye a
step (Lens Maybe (Construction Wye a) (Construction Wye a)
 -> Construction Wye a -> Construction Wye a)
-> Lens Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right (Construction Wye a -> Construction Wye a)
-> Construction Wye a -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
struct (Ordering -> Construction Wye a) -> Ordering -> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> a -> Ordering
f a
x (a -> Ordering) -> a -> Ordering
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye a
struct

instance Substructure Root (Construction Wye) where
	type Available Root (Construction Wye) = Identity
	type Substance Root (Construction Wye) = Identity
	substructure :: Lens
  (Available 'Root (Construction Wye))
  ((<:.>) (Tagged 'Root) (Construction Wye) a)
  (Substance 'Root (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Root) (Construction Wye) a
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
     (Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Root) (Construction Wye) a
  -> Store
       (Identity (Identity a))
       ((<:.>) (Tagged 'Root) (Construction Wye) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Root) (Construction Wye) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Construction Wye) a
    -> Store
         (Identity (Identity a))
         ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
     (Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Root) (Construction Wye) a
struct -> case (<:.>) (Tagged 'Root) (Construction Wye) a -> Construction Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) (Construction Wye) a
struct of
		Construct a
x (Wye :. Construction Wye) := a
xs -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Root) (Construction Wye) a)
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Construction Wye) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
x) Identity (Identity a)
-> (Identity (Identity a)
    -> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Root) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> (Identity (Identity a) -> Construction Wye a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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 (Identity a) -> a)
-> Identity (Identity a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract

instance Substructure Left (Construction Wye) where
	type Available Left (Construction Wye) = Maybe
	type Substance Left (Construction Wye) = Construction Wye
	substructure :: Lens
  (Available 'Left (Construction Wye))
  ((<:.>) (Tagged 'Left) (Construction Wye) a)
  (Substance 'Left (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Left) (Construction Wye) a
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
     (Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Construction Wye) a
  -> Store
       (Maybe (Construction Wye a))
       ((<:.>) (Tagged 'Left) (Construction Wye) a))
 -> P_Q_T
      (->)
      Store
      Maybe
      ((<:.>) (Tagged 'Left) (Construction Wye) a)
      (Construction Wye a))
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
    -> Store
         (Maybe (Construction Wye a))
         ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
     (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) (Construction Wye) a
struct -> case Tagged 'Left (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Left (Construction Wye a) -> Construction Wye a)
-> Tagged 'Left (Construction Wye a) -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Left) (Construction Wye) a
struct of
		Construct a
x Wye (Construction Wye a)
End -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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.
Semigroupoid 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)
		Construct a
x (Left Construction Wye a
lst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
lst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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
		Construct a
x (Right Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Left) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
lst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Left) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
 -> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst)

instance Substructure Right (Construction Wye) where
	type Available Right (Construction Wye) = Maybe
	type Substance Right (Construction Wye) = Construction Wye
	substructure :: Lens
  (Available 'Right (Construction Wye))
  ((<:.>) (Tagged 'Right) (Construction Wye) a)
  (Substance 'Right (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Right) (Construction Wye) a
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
     (Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) (Construction Wye) a
  -> Store
       (Maybe (Construction Wye a))
       ((<:.>) (Tagged 'Right) (Construction Wye) a))
 -> P_Q_T
      (->)
      Store
      Maybe
      ((<:.>) (Tagged 'Right) (Construction Wye) a)
      (Construction Wye a))
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
    -> Store
         (Maybe (Construction Wye a))
         ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> P_Q_T
     (->)
     Store
     Maybe
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
     (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) (Construction Wye) a
struct -> case Tagged 'Right (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (Construction Wye a) -> Construction Wye a)
-> Tagged 'Right (Construction Wye a) -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Right) (Construction Wye) a
struct of
		Construct a
x Wye (Construction Wye a)
End -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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.
Semigroupoid 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)
		Construct a
x (Left Construction Wye a
lst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Construction Wye a)
forall a. Maybe a
Nothing Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
		Construct a
x (Right Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
rst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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
		Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
  :. (->) (Maybe (Construction Wye a)))
 := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
   :. (->) (Maybe (Construction Wye a)))
  := (<:.>) (Tagged 'Right) (Construction Wye) a)
 -> Store
      (Maybe (Construction Wye a))
      ((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
     :. (->) (Maybe (Construction Wye a)))
    := (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
     (Maybe (Construction Wye a))
     ((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a -> Maybe (Construction Wye a)
forall a. a -> Maybe a
Just Construction Wye a
rst Maybe (Construction Wye a)
-> (Maybe (Construction Wye a)
    -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> ((:*:) (Maybe (Construction Wye a))
    :. (->) (Maybe (Construction Wye a)))
   := (<:.>) (Tagged 'Right) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)

-------------------------------------- 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 (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
struct = case TT Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TT Covariant Covariant Maybe (Construction Wye) (k :*: a)
 -> (Maybe :. Construction Wye) := (k :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> TT Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TT Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Binary k a
 -> TT Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TT Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid 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 ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
 -> (Maybe :. Construction Wye) := (k :*: a))
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
struct of
		(Maybe :. Construction Wye) := (k :*: a)
Nothing -> (((->) k :. Maybe) := a) -> TT Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT ((((->) k :. Maybe) := a)
 -> TT Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) := a)
-> TT Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \k
_ -> Maybe a
forall a. Maybe a
Nothing
		Just Construction Wye (k :*: a)
tree -> (((->) k :. Maybe) := a) -> TT Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT ((((->) k :. Maybe) := a)
 -> TT Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) := a)
-> TT Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \k
key ->
			let root :: k :*: a
root = Construction Wye (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye (k :*: a)
tree in k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (k :*: a) -> k
forall a b. (a :*: b) -> a
attached 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 (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (k :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract k :*: a
root)
				(k -> Prefixed (Construction Wye) k a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <::> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key k
key (Prefixed (Construction Wye) k a -> Maybe a)
-> (Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a)
-> Construction Wye (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (k :*: a) -> Maybe a)
-> ((Maybe :. Construction Wye) := (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
 -> Construction Wye (k :*: a)
 -> (Maybe :. Construction Wye) := (k :*: a))
-> Lens
     Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (Construction Wye (k :*: a)
 -> (Maybe :. Construction Wye) := (k :*: a))
-> Construction Wye (k :*: a)
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye (k :*: a)
tree)
				(k -> Prefixed (Construction Wye) k a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <::> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key k
key (Prefixed (Construction Wye) k a -> Maybe a)
-> (Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a)
-> Construction Wye (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (k :*: a) -> Maybe a)
-> ((Maybe :. Construction Wye) := (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
 -> Construction Wye (k :*: a)
 -> (Maybe :. Construction Wye) := (k :*: a))
-> Lens
     Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right (Construction Wye (k :*: a)
 -> (Maybe :. Construction Wye) := (k :*: a))
-> Construction Wye (k :*: a)
-> (Maybe :. Construction Wye) := (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye (k :*: a)
tree)

-- instance Chain k => Morphable (Vary Element) (Prefixed Binary k) where
	-- type Morphing (Vary Element) (Prefixed Binary k) = ((:*:) k <::> Identity) <:.:> Prefixed Binary k := (->)
	-- morphing struct = case run . run . premorph ! struct of
		-- Nothing -> T_U ! \(TT (key :*: Identity value)) -> Prefixed . lift . leaf ! key :*: value
		-- Just tree -> T_U ! \(TT (key :*: Identity value)) ->
			-- let continue = ((vary @Element @k @_ @(Prefixed Binary _) key value =||) =||) in
			-- Prefixed . lift ! key <=> attached (extract tree) & 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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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.
Semigroupoid 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)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) := a)
 -> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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)
# (key :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract key :*: a
x)
			(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)
-> (Identity (Construction Wye (key :*: a))
    -> Prefixed (Construction Wye) key a)
-> Identity (Construction Wye (key :*: a))
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a)
-> (Identity (Construction Wye (key :*: a))
    -> Construction Wye (key :*: a))
-> Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity (Construction Wye (key :*: a)) -> Maybe a)
-> Maybe (Identity (Construction Wye (key :*: a))) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe
   ((Wye :. Construction Wye) := (key :*: a))
   (Identity (Construction Wye (key :*: a)))
 -> ((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Identity (Construction Wye (key :*: a))))
-> Lens
     Maybe
     ((Wye :. Construction Wye) := (key :*: a))
     (Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Identity (Construction Wye (key :*: a))))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs)
			(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)
-> (Identity (Construction Wye (key :*: a))
    -> Prefixed (Construction Wye) key a)
-> Identity (Construction Wye (key :*: a))
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a)
-> (Identity (Construction Wye (key :*: a))
    -> Construction Wye (key :*: a))
-> Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity (Construction Wye (key :*: a)) -> Maybe a)
-> Maybe (Identity (Construction Wye (key :*: a))) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe
   ((Wye :. Construction Wye) := (key :*: a))
   (Identity (Construction Wye (key :*: a)))
 -> ((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Identity (Construction Wye (key :*: a))))
-> Lens
     Maybe
     ((Wye :. Construction Wye) := (key :*: a))
     (Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (((Wye :. Construction Wye) := (key :*: a))
 -> Maybe (Identity (Construction Wye (key :*: a))))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs)

-------------------------------------- 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> b
f a
r

instance Traversable (->) (->) Biforked where
	a -> u b
_ <<- :: (a -> u b) -> Biforked a -> u (Biforked b)
<<- Biforked a
Top = Biforked b -> u (Biforked b)
forall (t :: * -> *) a. Pointable t => a -> t a
point Biforked b
forall a. Biforked a
Top
	a -> u b
f <<- Leftward a
l = b -> Biforked b
forall a. a -> Biforked a
Leftward (b -> Biforked b) -> u b -> u (Biforked b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
l
	a -> u b
f <<- Rightward a
r = b -> Biforked b
forall a. a -> Biforked a
Rightward (b -> Biforked b) -> u b -> u (Biforked b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
r

type Bifurcation = Biforked <::> Construction Biforked

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

instance Zippable (Construction Wye) where
	type Breadcrumbs (Construction Wye) = (Wye <::> Construction Wye) <:.:> (Bifurcation <::> Bicursor) := (:*:)

_focused_part_to_nonempty_binary_tree :: (Identity <:.:> Wye <::> Construction Wye := (:*:)) ~> Construction Wye
_focused_part_to_nonempty_binary_tree :: (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a
-> Construction Wye a
_focused_part_to_nonempty_binary_tree (T_U (Identity a
x :*: (<::>) Wye (Construction Wye) a
xs)) = 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)
-> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>) Wye (Construction Wye) a -> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<::>) Wye (Construction Wye) a
xs

instance Morphable (Rotate Up) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:)) where
	type Morphing (Rotate Up) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:))
		= Maybe <::> ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> Bifurcation <::> Bicursor := (:*:))
	morphing :: (<::>)
  (Tagged ('Rotate 'Up))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> Morphing
     ('Rotate 'Up)
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
morphing (<::>)
  (Tagged ('Rotate 'Up))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct = case T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> T_U
      Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
    :*: TT Covariant Covariant Bifurcation Bicursor a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>)
  (Tagged ('Rotate 'Up))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Rotate 'Up))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct of
		T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
focused :*: TT (TT (Rightward (Construct (T_U (Identity a
parent :*: Binary a
rest)) Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next))) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (((Wye :. Construction Wye) := a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> ((Wye :. Construction Wye) := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (T_U
   Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
 -> TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)) (T_U
   Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (((Wye :. Construction Wye) := a)
    -> T_U
         Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a)
-> ((Wye :. Construction Wye) := a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a
-> TT Covariant Covariant Wye (Construction Wye) a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
parent) (TT Covariant Covariant Wye (Construction Wye) a
 -> T_U
      Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a)
-> (((Wye :. Construction Wye) := a)
    -> TT Covariant Covariant Wye (Construction Wye) a)
-> ((Wye :. Construction Wye) := a)
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Wye :. Construction Wye) := a)
-> TT Covariant Covariant Wye (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Wye :. Construction Wye) := a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> ((Wye :. Construction Wye) := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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
				# Both (_focused_part_to_nonempty_binary_tree focused)
				# Left (_focused_part_to_nonempty_binary_tree focused)
				# run rest
		T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
focused :*: TT (TT (Leftward (Construct (T_U (Identity a
parent :*: Binary a
rest)) Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next))) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (((Wye :. Construction Wye) := a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> ((Wye :. Construction Wye) := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (T_U
   Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
 -> TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT Biforked
  (Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)) (T_U
   Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (((Wye :. Construction Wye) := a)
    -> T_U
         Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a)
-> ((Wye :. Construction Wye) := a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a
-> TT Covariant Covariant Wye (Construction Wye) a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
parent) (TT Covariant Covariant Wye (Construction Wye) a
 -> T_U
      Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a)
-> (((Wye :. Construction Wye) := a)
    -> TT Covariant Covariant Wye (Construction Wye) a)
-> ((Wye :. Construction Wye) := a)
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Wye :. Construction Wye) := a)
-> TT Covariant Covariant Wye (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Wye :. Construction Wye) := a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> ((Wye :. Construction Wye) := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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
				# Both % _focused_part_to_nonempty_binary_tree focused
				# Right (_focused_part_to_nonempty_binary_tree focused)
				# run rest
		T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
:*: TT Covariant Covariant Bifurcation Bicursor a
_ -> ((Maybe
  :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:)))
 := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe
 :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      <:.:> (Bifurcation <::> Bicursor))
     := (:*:)))
:= a
forall a. Maybe a
Nothing

_nonempty_binary_tree_to_focused_part :: Construction Wye ~> Identity <:.:> Wye <::> Construction Wye := (:*:)
_nonempty_binary_tree_to_focused_part :: Construction Wye a
-> (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a
_nonempty_binary_tree_to_focused_part (Construct a
x (Wye :. Construction Wye) := a
xs) = Identity a
-> (<::>) Wye (Construction Wye) a
-> (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
 -> (<::>) Wye (Construction Wye) a
 -> (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a)
-> Identity a
-> (<::>) Wye (Construction Wye) a
-> (:=) (Identity <:.:> (Wye <::> 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 ((<::>) Wye (Construction Wye) a
 -> (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a)
-> (<::>) Wye (Construction Wye) a
-> (:=) (Identity <:.:> (Wye <::> Construction Wye)) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# ((Wye :. Construction Wye) := a) -> (<::>) Wye (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Wye :. Construction Wye) := a
xs

instance Morphable (Rotate (Down Left)) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:)) where
	type Morphing (Rotate (Down Left)) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:))
		= Maybe <::> ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> Bifurcation <::> Bicursor := (:*:))
	morphing :: (<::>)
  (Tagged ('Rotate ('Down 'Left)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> Morphing
     ('Rotate ('Down 'Left))
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
morphing (<::>)
  (Tagged ('Rotate ('Down 'Left)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct = case T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> T_U
      Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
    :*: TT Covariant Covariant Bifurcation Bicursor a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>)
  (Tagged ('Rotate ('Down 'Left)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Rotate ('Down 'Left)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct of
		T_U (Identity a
x :*: TT (Left Construction Wye a
lst)) :*: TT (TT (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
Construction Wye
~> ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
_nonempty_binary_tree_to_focused_part Construction Wye a
lst)
				(TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (TT
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TT Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (((Maybe :. Construction Wye) := a)
-> TT Covariant Covariant Maybe (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Wye) := a
forall a. Maybe a
Nothing) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
		T_U (Identity a
x :*: TT (Both Construction Wye a
lst Construction Wye a
rst)) :*: TT (TT (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
Construction Wye
~> ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
_nonempty_binary_tree_to_focused_part Construction Wye a
lst)
				(TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (TT
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
   Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TT Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift Construction Wye a
rst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
		T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
:*: TT Covariant Covariant Bifurcation Bicursor a
_ -> ((Maybe
  :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:)))
 := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe
 :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      <:.:> (Bifurcation <::> Bicursor))
     := (:*:)))
:= a
forall a. Maybe a
Nothing

instance Morphable (Rotate (Down Right)) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:)) where
	type Morphing (Rotate (Down Right)) ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> (Bifurcation <::> Bicursor) := (:*:))
		= Maybe <::> ((Identity <:.:> Wye <::> Construction Wye := (:*:)) <:.:> Bifurcation <::> Bicursor := (:*:))
	morphing :: (<::>)
  (Tagged ('Rotate ('Down 'Right)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> Morphing
     ('Rotate ('Down 'Right))
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
morphing (<::>)
  (Tagged ('Rotate ('Down 'Right)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct = case T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> T_U
      Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
    :*: TT Covariant Covariant Bifurcation Bicursor a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
   :*: TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<::>)
  (Tagged ('Rotate ('Down 'Right)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
  (Tagged ('Rotate ('Down 'Right)))
  ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
    <:.:> (Bifurcation <::> Bicursor))
   := (:*:))
  a
struct of
		T_U (Identity a
x :*: TT (Right Construction Wye a
rst)) :*: TT (TT (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
Construction Wye
~> ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
_nonempty_binary_tree_to_focused_part Construction Wye a
rst)
				(TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (TT
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TT Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (((Maybe :. Construction Wye) := a)
-> TT Covariant Covariant Maybe (Construction Wye) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe :. Construction Wye) := a
forall a. Maybe a
Nothing) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
		T_U (Identity a
x :*: TT (Both Construction Wye a
lst Construction Wye a
rst)) :*: TT (TT (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next) ->
			T_U
  Covariant
  Covariant
  (:*:)
  ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
  (Bifurcation <::> Bicursor)
  a
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
   Covariant
   Covariant
   (:*:)
   ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
   (Bifurcation <::> Bicursor)
   a
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
         (Bifurcation <::> Bicursor)
         a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
-> TT Covariant Covariant Bifurcation Bicursor a
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> T_U
     Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
Construction Wye
~> ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
_nonempty_binary_tree_to_focused_part Construction Wye a
rst)
				(TT Covariant Covariant Bifurcation Bicursor a
 -> T_U
      Covariant
      Covariant
      (:*:)
      ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      (Bifurcation <::> Bicursor)
      a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT Covariant Covariant Bifurcation Bicursor a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> T_U
     Covariant
     Covariant
     (:*:)
     ((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
     (Bifurcation <::> Bicursor)
     a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT
  Covariant
  Covariant
  Biforked
  (Construction Biforked)
  (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (TT
   Covariant
   Covariant
   Biforked
   (Construction Biforked)
   (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT Covariant Covariant Bifurcation Bicursor a)
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> TT
         Covariant
         Covariant
         Biforked
         (Construction Biforked)
         (T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
 := T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Biforked
      (Construction Biforked)
      (T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
    -> (Biforked :. Construction Biforked)
       := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Biforked
     (Construction Biforked)
     (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
  Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
   := T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
   Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
 -> TT
      Covariant
      Covariant
      Maybe
      ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
        <:.:> (Bifurcation <::> Bicursor))
       := (:*:))
      a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
 -> ((Biforked :. Construction Biforked)
     := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TT Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a
-> TT Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift Construction Wye a
lst) (((Biforked :. Construction Biforked)
  := T_U Covariant Covariant (:*:) Identity Binary a)
 -> Construction
      Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
    := T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
     Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
		T_U
  Covariant Covariant (:*:) Identity (Wye <::> Construction Wye) a
:*: TT Covariant Covariant Bifurcation Bicursor a
_ -> ((Maybe
  :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:)))
 := a)
-> TT
     Covariant
     Covariant
     Maybe
     ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
       <:.:> (Bifurcation <::> Bicursor))
      := (:*:))
     a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') := a) -> TT ct ct' t t' a
TT (Maybe
 :. ((((Identity <:.:> (Wye <::> Construction Wye)) := (:*:))
      <:.:> (Bifurcation <::> Bicursor))
     := (:*:)))
:= a
forall a. Maybe a
Nothing

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