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