{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure.Some.Binary where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.Category ((.), ($), (/)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), comap)) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Functor.Avoidable (empty) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Pattern.Object.Chain (Chain ((<=>))) import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False)) import Pandora.Paradigm.Primary.Object.Ordering (order) import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator, Zero)) import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One)) import Pandora.Paradigm.Primary.Functor.Function ((!), (%), (&)) import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity)) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome) import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both)) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct) import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), type (<:.>), type (<:.:>)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) import Pandora.Paradigm.Inventory.State (State, modify) import Pandora.Paradigm.Inventory.Store (Store (Store)) import Pandora.Paradigm.Inventory.Optics (over) import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty) import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null)) import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Root)) import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Heighth), measure) import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve)) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate, Into, Insert), premorph, collate) import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), sub, substitute) import Pandora.Paradigm.Structure.Ability.Zipper (Zipper) type Binary = Maybe <:.> Construction Wye rebalance :: Chain a => (Wye :. Construction Wye := a) -> Nonempty Binary a rebalance :: ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Both Construction Wye a x Construction Wye a y) = a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a y Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & Construction Wye a -> Construction Wye a -> Construction Wye a -> Ordering -> Construction Wye a forall a. a -> a -> a -> Ordering -> a order (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a y (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a x (Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / ((Wye :. Construction Wye) := a) -> Nonempty Binary a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a y)) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a x (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / ((Wye :. Construction Wye) := a) -> Nonempty Binary a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) (Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / ((Wye :. Construction Wye) := a) -> Nonempty Binary a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a y)) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a x (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / ((Wye :. Construction Wye) := a) -> Nonempty Binary a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) (Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a y) instance (forall a . Chain a) => Morphable Insert Binary where type Morphing Insert Binary = Identity <:.:> Binary := (->) morphing :: (<:.>) (Tagged 'Insert) Binary a -> Morphing 'Insert Binary a morphing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Insert) Binary a -> Binary a) -> (<:.>) (Tagged 'Insert) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Insert) Binary a -> Binary a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Maybe (Construction Wye a) Nothing) = (Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity 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 ((Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity Binary a) -> (Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ \(Identity a x) -> Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((Wye :. Construction Wye) := a) -> Binary a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ (Wye :. Construction Wye) := a forall a. Wye a End morphing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Insert) Binary a -> Binary a) -> (<:.>) (Tagged 'Insert) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Insert) Binary a -> Binary a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Just Construction Wye a ne) = (Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity 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 ((Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity Binary a) -> (Identity a -> Binary a) -> T_U Covariant Covariant (->) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ \(Identity a x) -> Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> Construction Wye a -> Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a ne Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & Construction Wye a -> Construction Wye a -> Construction Wye a -> Ordering -> Construction Wye a forall a. a -> a -> a -> Ordering -> a order (Construction Wye a ne Construction Wye a -> (Construction Wye a -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & (Substructural 'Left (Construction Wye) a -> Substructural 'Left (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall k (f :: k) (t :: * -> *) a. Substructure f t => (Substructural f t a -> Substructural f t a) -> t a -> t a substitute @Left (a :=:=> Binary forall k (f :: k) (t :: * -> *) a. (Chain a, Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) => a :=:=> t collate @Insert a x)) Construction Wye a ne (Construction Wye a ne Construction Wye a -> (Construction Wye a -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & (Substructural 'Right (Construction Wye) a -> Substructural 'Right (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall k (f :: k) (t :: * -> *) a. Substructure f t => (Substructural f t a -> Substructural f t a) -> t a -> t a substitute @Right (a :=:=> Binary forall k (f :: k) (t :: * -> *) a. (Chain a, Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) => a :=:=> t collate @Insert a x)) instance (forall a . Chain a) => Focusable Root Binary where type Focusing Root Binary a = Maybe a focusing :: Tagged 'Root (Binary a) :-. Focusing 'Root Binary a focusing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Root (Binary a) -> Binary a) -> Tagged 'Root (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Root (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Maybe (Construction Wye a) Nothing) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a))) -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall (m :: * -> * -> *). Category m => m ~~> m $ Maybe a forall a. Maybe a Nothing Maybe a -> (Maybe a -> Tagged 'Root (Binary a)) -> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a) forall s a. s -> a -> Product s a :*: Binary a -> Tagged 'Root (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Root (Binary a)) -> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Maybe (Construction Wye a) -> Binary a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Maybe (Construction Wye a) -> Binary a) -> (Maybe a -> Maybe (Construction Wye a)) -> Maybe a -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> Construction Wye a) -> Maybe a -> Maybe (Construction Wye a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b comap (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % (Wye :. Construction Wye) := a forall a. Wye a End) focusing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Root (Binary a) -> Binary a) -> Tagged 'Root (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Root (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Just Construction Wye a x) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a))) -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall (m :: * -> * -> *). Category m => m ~~> m $ a -> Maybe a forall a. a -> Maybe a Just (a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a x) Maybe a -> (Maybe a -> Tagged 'Root (Binary a)) -> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a) forall s a. s -> a -> Product s a :*: Binary a -> Tagged 'Root (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Root (Binary a)) -> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> (Maybe a -> Construction Wye a) -> Maybe a -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> Construction Wye a) -> Construction Wye a -> Maybe a -> Construction Wye a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) instance Measurable Heighth Binary where type Measural Heighth Binary a = Numerator measurement :: Tagged 'Heighth (Binary a) -> Measural 'Heighth Binary a measurement (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Heighth (Binary a) -> Binary a) -> Tagged 'Heighth (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Just Construction Wye a bt) = Denumerator -> Numerator Numerator (Denumerator -> Numerator) -> Denumerator -> Numerator forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Measural 'Heighth (Construction Wye) a forall k (f :: k) (t :: * -> *) a. Measurable f t => t a -> Measural f t a measure @Heighth Construction Wye a bt measurement (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Heighth (Binary a) -> Binary a) -> Tagged 'Heighth (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Maybe (Construction Wye a) Nothing) = Numerator Measural 'Heighth Binary a Zero instance Nullable Binary where null :: (Predicate :. Binary) := a null = (Binary a -> Boolean) -> (Predicate :. Binary) := a forall a. (a -> Boolean) -> Predicate a Predicate ((Binary a -> Boolean) -> (Predicate :. Binary) := a) -> (Binary a -> Boolean) -> (Predicate :. Binary) := a forall (m :: * -> * -> *). Category m => m ~~> m $ \case { TU Maybe (Construction Wye a) Nothing -> Boolean True ; Binary a _ -> Boolean False } instance Substructure Left Binary where type Substructural Left Binary = Binary substructure :: Lens ((<:.>) (Tagged 'Left) Binary a) (Substructural 'Left Binary a) substructure empty_tree :: (<:.>) (Tagged 'Left) Binary a empty_tree@(TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Left) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a) -> (<:.>) (Tagged 'Left) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) Binary a -> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a)) -> (<:.>) (Tagged 'Left) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) Binary a -> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Maybe (Construction Wye a) Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) Binary a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) Binary a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) Binary a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract ((<:.>) (Tagged 'Left) Binary a -> Primary (Tagged 'Left <:.> Binary) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) (Tagged 'Left) Binary a empty_tree) TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) Binary a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) Binary a forall s a. s -> a -> Product s a :*: (!) (<:.>) (Tagged 'Left) Binary a empty_tree substructure (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Left) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a) -> (<:.>) (Tagged 'Left) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) Binary a -> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a)) -> (<:.>) (Tagged 'Left) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) Binary a -> Tagged 'Left (TU Covariant Covariant Maybe (Construction Wye) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Just Construction Wye a tree) = TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) Binary a) -> (Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> (<:.>) (Tagged 'Left) Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Left) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) (Construction Wye a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) Binary a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Lens (Construction Wye a) (Substructural 'Left (Construction Wye) a) forall k (f :: k) (t :: * -> *). Substructure f t => t :~. Substructural f t sub @Left Construction Wye a tree instance Substructure Right Binary where type Substructural Right Binary = Binary substructure :: Lens ((<:.>) (Tagged 'Right) Binary a) (Substructural 'Right Binary a) substructure empty_tree :: (<:.>) (Tagged 'Right) Binary a empty_tree@(TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Right) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a) -> (<:.>) (Tagged 'Right) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a)) -> (<:.>) (Tagged 'Right) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Maybe (Construction Wye a) Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) Binary a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) Binary a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) Binary a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract ((<:.>) (Tagged 'Right) Binary a -> Primary (Tagged 'Right <:.> Binary) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) (Tagged 'Right) Binary a empty_tree) TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) Binary a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) Binary a forall s a. s -> a -> Product s a :*: (!) (<:.>) (Tagged 'Right) Binary a empty_tree substructure (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction Wye) a -> Maybe (Construction Wye a)) -> ((<:.>) (Tagged 'Right) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a) -> (<:.>) (Tagged 'Right) Binary a -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction Wye) a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a)) -> (<:.>) (Tagged 'Right) Binary a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Just Construction Wye a tree) = TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) Binary a) -> (Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> (<:.>) (Tagged 'Right) Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Right) Binary a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) (Construction Wye a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) Binary a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Lens (Construction Wye a) (Substructural 'Right (Construction Wye) a) forall k (f :: k) (t :: * -> *). Substructure f t => t :~. Substructural f t sub @Right Construction Wye a tree binary :: forall t a . (Traversable t, Chain a) => t a -> Binary a binary :: t a -> Binary a binary t a struct = (Binary a :*: t (Binary a)) -> Binary a forall a b. (a :*: b) -> a attached ((Binary a :*: t (Binary a)) -> Binary a) -> (Binary a :*: t (Binary a)) -> Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ forall a. Interpreted (State (Binary a)) => State (Binary a) a -> Primary (State (Binary a)) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run @(State (Binary a)) (State (Binary a) (t (Binary a)) -> ((->) (Binary a) :. (:*:) (Binary a)) := t (Binary a)) -> Binary a -> State (Binary a) (t (Binary a)) -> Binary a :*: t (Binary a) forall a b c. (a -> b -> c) -> b -> a -> c % Binary a forall (t :: * -> *) a. Avoidable t => t a empty (State (Binary a) (t (Binary a)) -> Binary a :*: t (Binary a)) -> State (Binary a) (t (Binary a)) -> Binary a :*: t (Binary a) forall (m :: * -> * -> *). Category m => m ~~> m $ t a struct t a -> (a -> State (Binary a) (Binary a)) -> State (Binary a) (t (Binary a)) forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> forall s (t :: * -> *). Stateful s t => (s -> s) -> t s forall (t :: * -> *). Stateful (Binary a) t => (Binary a -> Binary a) -> t (Binary a) modify @(Binary a) ((Binary a -> Binary a) -> State (Binary a) (Binary a)) -> (a -> Binary a -> Binary a) -> a -> State (Binary a) (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Binary a -> Binary a insert' where insert' :: a -> Binary a -> Binary a insert' :: a -> Binary a -> Binary a insert' a x (Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Primary Binary a Nothing) = Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((Wye :. Construction Wye) := a) -> Binary a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *). Category m => m ~~> m $ (Wye :. Construction Wye) := a forall a. Wye a End insert' a x tree :: Binary a tree@(Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Just nonempty) = a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a nonempty Ordering -> (Ordering -> Binary a) -> Binary a forall a b. a -> (a -> b) -> b & Binary a -> Binary a -> Binary a -> Ordering -> Binary a forall a. a -> a -> a -> Ordering -> a order (Binary a tree Binary a -> (Binary a -> Binary a) -> Binary a forall a b. a -> (a -> b) -> b & (Substructural 'Left Binary a -> Substructural 'Left Binary a) -> Binary a -> Binary a forall k (f :: k) (t :: * -> *) a. Substructure f t => (Substructural f t a -> Substructural f t a) -> t a -> t a substitute @Left (a -> Binary a -> Binary a insert' a x)) Binary a tree (Binary a tree Binary a -> (Binary a -> Binary a) -> Binary a forall a b. a -> (a -> b) -> b & (Substructural 'Right Binary a -> Substructural 'Right Binary a) -> Binary a -> Binary a forall k (f :: k) (t :: * -> *) a. Substructure f t => (Substructural f t a -> Substructural f t a) -> t a -> t a substitute @Right (a -> Binary a -> Binary a insert' a x)) type instance Nonempty Binary = Construction Wye instance Morphable (Into Binary) (Construction Wye) where type Morphing (Into Binary) (Construction Wye) = Binary morphing :: (<:.>) (Tagged ('Into Binary)) (Construction Wye) a -> Morphing ('Into Binary) (Construction Wye) a morphing = Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a) -> ((<:.>) (Tagged ('Into Binary)) (Construction Wye) a -> Construction Wye a) -> (<:.>) (Tagged ('Into Binary)) (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Into Binary)) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph instance (forall a . Chain a) => Morphable Insert (Construction Wye) where type Morphing Insert (Construction Wye) = Identity <:.:> Construction Wye := (->) morphing :: (<:.>) (Tagged 'Insert) (Construction Wye) a -> Morphing 'Insert (Construction Wye) a morphing ((<:.>) (Tagged 'Insert) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construction Wye a xs) = (Identity a -> Construction Wye a) -> T_U Covariant Covariant (->) Identity (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 ((Identity a -> Construction Wye a) -> T_U Covariant Covariant (->) Identity (Construction Wye) a) -> (Identity a -> Construction Wye a) -> T_U Covariant Covariant (->) Identity (Construction Wye) a forall (m :: * -> * -> *). Category m => m ~~> m $ \(Identity a x) -> let change :: TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a change = Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Construction Wye a) -> Construction Wye a -> ((Maybe :. Construction Wye) := a) -> Construction Wye a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (a :=:=> Construction Wye forall k (f :: k) (t :: * -> *) a. (Chain a, Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) => a :=:=> t collate @Insert a x) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye :. Construction Wye) := a forall a. Wye a End) (((Maybe :. Construction Wye) := a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run in a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <:= Construction Wye forall (t :: * -> *) a. Extractable t => a <:= t extract Construction Wye a xs Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & Construction Wye a -> Construction Wye a -> Construction Wye a -> Ordering -> Construction Wye a forall a. a -> a -> a -> Ordering -> a order (Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src over (Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a) -> Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / forall k (f :: k) (t :: * -> *). Substructure f t => t :~. Substructural f t forall (t :: * -> *). Substructure 'Left t => t :~. Substructural 'Left t sub @Left ((TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a change (Construction Wye a -> Construction Wye a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a xs) Construction Wye a xs (Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src over (Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a) -> Lens (Construction Wye a) (TU Covariant Covariant Maybe (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / forall k (f :: k) (t :: * -> *). Substructure f t => t :~. Substructural f t forall (t :: * -> *). Substructure 'Right t => t :~. Substructural 'Right t sub @Right ((TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / TU Covariant Covariant Maybe (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a change (Construction Wye a -> Construction Wye a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a xs) instance Focusable Root (Construction Wye) where type Focusing Root (Construction Wye) a = a focusing :: Tagged 'Root (Construction Wye a) :-. Focusing 'Root (Construction Wye) a focusing (Construction Wye a <:= Tagged 'Root forall (t :: * -> *) a. Extractable t => a <:= t extract -> Construct a x (Wye :. Construction Wye) := a xs) = (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a))) -> (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a)) forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> (a -> Tagged 'Root (Construction Wye a)) -> ((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Root (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Root (Construction Wye a)) -> (a -> Construction Wye a) -> a -> Tagged 'Root (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % (Wye :. Construction Wye) := a xs instance Measurable Heighth (Construction Wye) where type Measural Heighth (Construction Wye) a = Denumerator measurement :: Tagged 'Heighth (Construction Wye a) -> Measural 'Heighth (Construction Wye) a measurement (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a) -> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a) -> Tagged 'Heighth (Construction Wye a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. Extractable t => a <:= t extract -> (Wye :. Construction Wye) := a End) = Denumerator Measural 'Heighth (Construction Wye) a One measurement (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a) -> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a) -> Tagged 'Heighth (Construction Wye a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Left Construction Wye a lst) = Denumerator One Denumerator -> Denumerator -> Denumerator forall a. Semigroup a => a -> a -> a + Construction Wye a -> Measural 'Heighth (Construction Wye) a forall k (f :: k) (t :: * -> *) a. Measurable f t => t a -> Measural f t a measure @Heighth Construction Wye a lst measurement (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a) -> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a) -> Tagged 'Heighth (Construction Wye a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Right Construction Wye a rst) = Denumerator One Denumerator -> Denumerator -> Denumerator forall a. Semigroup a => a -> a -> a + Construction Wye a -> Measural 'Heighth (Construction Wye) a forall k (f :: k) (t :: * -> *) a. Measurable f t => t a -> Measural f t a measure @Heighth Construction Wye a rst measurement (Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct (Construction Wye a -> (Wye :. Construction Wye) := a) -> (Tagged 'Heighth (Construction Wye a) -> Construction Wye a) -> Tagged 'Heighth (Construction Wye a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Heighth (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. Extractable t => a <:= t extract -> Both Construction Wye a lst Construction Wye a rst) = Denumerator One Denumerator -> Denumerator -> Denumerator forall a. Semigroup a => a -> a -> a + let (Denumerator lm :*: Denumerator rm) = Construction Wye a -> Measural 'Heighth (Construction Wye) a forall k (f :: k) (t :: * -> *) a. Measurable f t => t a -> Measural f t a measure @Heighth Construction Wye a lst Denumerator -> Denumerator -> Product Denumerator Denumerator forall s a. s -> a -> Product s a :*: Construction Wye a -> Measural 'Heighth (Construction Wye) a forall k (f :: k) (t :: * -> *) a. Measurable f t => t a -> Measural f t a measure @Heighth Construction Wye a rst in Denumerator lm Denumerator -> Denumerator -> Ordering forall a. Chain a => a -> a -> Ordering <=> Denumerator rm Ordering -> (Ordering -> Denumerator) -> Denumerator forall a b. a -> (a -> b) -> b & Denumerator -> Denumerator -> Denumerator -> Ordering -> Denumerator forall a. a -> a -> a -> Ordering -> a order Denumerator rm Denumerator lm Denumerator lm instance Substructure Left (Construction Wye) where type Substructural Left (Construction Wye) = Binary substructure :: Lens ((<:.>) (Tagged 'Left) (Construction Wye) a) (Substructural 'Left (Construction Wye) a) substructure empty_tree :: (<:.>) (Tagged 'Left) (Construction Wye) a empty_tree@(Construction Wye a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a)) -> (<:.>) (Tagged 'Left) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a _ Wye (Construction Wye a) End) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a forall (t :: * -> *) a. Avoidable t => t a empty TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a forall s a. s -> a -> Product s a :*: ((<:.>) (Tagged 'Left) (Construction Wye) a empty_tree (<:.>) (Tagged 'Left) (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall a b. a -> b -> a !) substructure (Construction Wye a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a)) -> (<:.>) (Tagged 'Left) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Left Construction Wye a lst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a lst TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Wye (Construction Wye a) forall a. Wye a End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run substructure (Construction Wye a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a)) -> (<:.>) (Tagged 'Left) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Right Construction Wye a rst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a forall (t :: * -> *) a. Avoidable t => t a empty TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a)) -> Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a rst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Construction Wye a rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run substructure (Construction Wye a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Left) -> ((<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a)) -> (<:.>) (Tagged 'Left) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Left) (Construction Wye) a -> Tagged 'Left (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Both Construction Wye a lst Construction Wye a rst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Left) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a lst TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Left) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Left) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a)) -> Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a rst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Construction Wye a rst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run instance Substructure Right (Construction Wye) where type Substructural Right (Construction Wye) = Binary substructure :: Lens ((<:.>) (Tagged 'Right) (Construction Wye) a) (Substructural 'Right (Construction Wye) a) substructure emtpy_tree :: (<:.>) (Tagged 'Right) (Construction Wye) a emtpy_tree@(Construction Wye a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a)) -> (<:.>) (Tagged 'Right) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a _ Wye (Construction Wye a) End) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a forall (t :: * -> *) a. Avoidable t => t a empty TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a forall s a. s -> a -> Product s a :*: ((<:.>) (Tagged 'Right) (Construction Wye) a emtpy_tree (<:.>) (Tagged 'Right) (Construction Wye) a -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall a b. a -> b -> a !) substructure (Construction Wye a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a)) -> (<:.>) (Tagged 'Right) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Left Construction Wye a lst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant Maybe (Construction Wye) a forall (t :: * -> *) a. Avoidable t => t a empty TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both Construction Wye a lst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Construction Wye a lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run substructure (Construction Wye a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a)) -> (<:.>) (Tagged 'Right) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Right Construction Wye a rst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a rst TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Wye (Construction Wye a) forall a. Wye a End (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run substructure (Construction Wye a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Wye a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a)) -> (<:.>) (Tagged 'Right) (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) (Construction Wye) a -> Tagged 'Right (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (Both Construction Wye a lst Construction Wye a rst)) = (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a)) -> (((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a) -> Store (TU Covariant Covariant Maybe (Construction Wye) a) ((<:.>) (Tagged 'Right) (Construction Wye) a) forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Maybe (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a rst TU Covariant Covariant Maybe (Construction Wye) a -> (TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> ((:*:) (TU Covariant Covariant Maybe (Construction Wye) a) :. (->) (TU Covariant Covariant Maybe (Construction Wye) a)) := (<:.>) (Tagged 'Right) (Construction Wye) a forall s a. s -> a -> Product s a :*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a) -> TU Covariant Covariant Maybe (Construction Wye) a -> (<:.>) (Tagged 'Right) (Construction Wye) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a)) -> TU Covariant Covariant Maybe (Construction Wye) a -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> ((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both Construction Wye a lst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Construction Wye a lst) (((Maybe :. Construction Wye) := a) -> Wye (Construction Wye a)) -> (TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a -> Wye (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction Wye) a -> (Maybe :. Construction Wye) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run data Biforked a = Top | Leftward a | Rightward a instance Covariant Biforked where a -> b _ <$> :: (a -> b) -> Biforked a -> Biforked b <$> Biforked a Top = Biforked b forall a. Biforked a Top a -> b f <$> Leftward a l = b -> Biforked b forall a. a -> Biforked a Leftward (b -> Biforked b) -> b -> Biforked b forall (m :: * -> * -> *). Category m => m ~~> m $ a -> b f a l a -> b f <$> Rightward a r = b -> Biforked b forall a. a -> Biforked a Rightward (b -> Biforked b) -> b -> Biforked b forall (m :: * -> * -> *). Category m => m ~~> m $ a -> b f a r type Bifurcation = Biforked <:.> Construction Biforked type Bicursor = Identity <:.:> Binary := (:*:) type instance Zipper (Construction Wye) = Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:) data Vertical a = Up a | Down a instance Morphable (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where type Morphing (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) = Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) morphing :: (<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Morphing ('Rotate 'Up) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construction Wye a focused :*: TU (TU (Rightward (Construct (T_U (Identity a parent :*: Binary a rest)) Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) next)))) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *). Category m => m ~~> m / a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent ((Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve ((Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> (Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both Construction Wye a focused (((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> Wye a Left Construction Wye a focused (((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run Binary a rest) (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *). Category m => m ~~> m / TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) next) morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construction Wye a focused :*: TU (TU (Rightward (Construct (T_U (Identity a parent :*: Binary a rest)) Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) next)))) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *). Category m => m ~~> m / a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent ((Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve ((Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> (Construction Wye a -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a) -> Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a focused (((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> ((Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> Wye a Right Construction Wye a focused (((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a) -> ((Maybe :. Construction Wye) := a) -> (Wye :. Construction Wye) := a forall (m :: * -> * -> *). Category m => m ~~> m / Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run Binary a rest) (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *). Category m => m ~~> m / TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) next) morphing ((<:.>) (Tagged ('Rotate 'Up)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> T_U (Construction Wye a _ :*: TU (TU Biforked (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) Top))) = Morphing ('Rotate 'Up) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: * -> *) a. Avoidable t => t a empty instance Morphable (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where type Morphing (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) = Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) morphing :: (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Morphing ('Rotate ('Down 'Left)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Left Construction Wye a lst) :*: TU (TU (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next)) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome Construction Wye a lst (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall a. a -> Biforked a Leftward (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_U Covariant Covariant (:*:) Identity Binary a -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a x (Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / Binary a forall (t :: * -> *) a. Avoidable t => t a empty) (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Both Construction Wye a lst Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next)) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome Construction Wye a lst (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall a. a -> Biforked a Leftward (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_U Covariant Covariant (:*:) Identity Binary a -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a x (Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a rst) (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a _ (Right Construction Wye a _) :*: TU Covariant Covariant Bifurcation Bicursor a _) = Morphing ('Rotate ('Down 'Left)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: * -> *) a. Avoidable t => t a empty morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Left))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a _ Wye (Construction Wye a) End :*: TU Covariant Covariant Bifurcation Bicursor a _) = Morphing ('Rotate ('Down 'Left)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: * -> *) a. Avoidable t => t a empty instance Morphable (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where type Morphing (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) = Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) morphing :: (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Morphing ('Rotate ('Down 'Right)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Right Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next)) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome Construction Wye a rst (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall a. a -> Biforked a Rightward (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_U Covariant Covariant (:*:) Identity Binary a -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a x (Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / Binary a forall (t :: * -> *) a. Avoidable t => t a empty) (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Both Construction Wye a lst Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next)) = (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome Construction Wye a rst (TU Covariant Covariant Bifurcation Bicursor a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Bifurcation Bicursor a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a)) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_U Covariant Covariant (:*:) Identity Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall a. a -> Biforked a Rightward (Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a)) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_U Covariant Covariant (:*:) Identity Binary a -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> Construction Biforked (T_U Covariant Covariant (:*:) Identity Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Identity a -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / a -> Identity a forall a. a -> Identity a Identity a x (Binary a -> T_U Covariant Covariant (:*:) Identity Binary a) -> Binary a -> T_U Covariant Covariant (:*:) Identity Binary a forall (m :: * -> * -> *). Category m => m ~~> m / Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift Construction Wye a lst) (((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a) -> ((Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a) -> TU Covariant Covariant Maybe ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (m :: * -> * -> *). Category m => m ~~> m $ (Biforked :. Construction Biforked) := T_U Covariant Covariant (:*:) Identity Binary a next morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a _ (Left Construction Wye a _) :*: TU Covariant Covariant Bifurcation Bicursor a _) = Morphing ('Rotate ('Down 'Right)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: * -> *) a. Avoidable t => t a empty morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a)) -> ((<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a) -> (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> Product (Construction Wye a) (TU Covariant Covariant Bifurcation Bicursor a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Rotate ('Down 'Right))) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a -> (:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a _ Wye (Construction Wye a) End :*: TU Covariant Covariant Bifurcation Bicursor a _) = Morphing ('Rotate ('Down 'Right)) ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)) a forall (t :: * -> *) a. Avoidable t => t a empty