{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Binary where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Core.Morphism ((&), (%), (!)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), comap)) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Pattern.Object.Chain (Chain ((<=>))) import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False)) import Pandora.Paradigm.Primary.Object.Ordering (order) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:))) import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both)) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct) import Pandora.Paradigm.Schemes (TU (TU), T_ (T_), T_U (T_U), type (<:.>), type (<:*:>)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) import Pandora.Paradigm.Inventory.Store (Store (Store)) import Pandora.Paradigm.Inventory.Optics (type (:-.), (|>), (%~)) import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty) import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null)) import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Root)) import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve)) import Pandora.Paradigm.Structure.Ability.Insertable (Insertable (insert)) import Pandora.Paradigm.Structure.Ability.Rotatable (Rotatable (Rotational, rotation)) import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), sub) import Pandora.Paradigm.Structure.Ability.Zipper (Zipper) type Binary = Maybe <:.> Construction Wye rebalance :: Chain a => (Wye :. Construction Wye := a) -> Nonempty Binary a rebalance :: ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (Both Construction Wye a x Construction Wye a y) = a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a y Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & Construction Wye a -> Construction Wye a -> Construction Wye a -> Ordering -> Construction Wye a forall a. a -> a -> a -> Ordering -> a order (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a y) (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both Construction Wye a x (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a y)) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a x) (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a y)) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a x) (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) Construction Wye a y) instance (forall a . Chain a) => Insertable Binary where insert :: a -> Binary a -> Binary a insert a x (Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Primary Binary a Nothing) = Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((Wye :. Construction Wye) := a) -> Binary a) -> ((Wye :. Construction Wye) := a) -> Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Wye :. Construction Wye) := a forall a. Wye a End insert a x tree :: Binary a tree@(Binary a -> Primary Binary a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Just nonempty) = a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a nonempty Ordering -> (Ordering -> Binary a) -> Binary a forall a b. a -> (a -> b) -> b & Binary a -> Binary a -> Binary a -> Ordering -> Binary a forall a. a -> a -> a -> Ordering -> a order (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Left t => t a :-. Substructural 'Left t a sub @Left (Binary a -> Store (Binary a) (Binary a)) -> (Binary a -> Binary a) -> Binary a -> Binary a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src %~ a -> Binary a -> Binary a forall (t :: * -> *) a. Insertable t => a -> t a -> t a insert a x (Binary a -> Binary a) -> Binary a -> Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Binary a tree) Binary a tree (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Right t => t a :-. Substructural 'Right t a sub @Right (Binary a -> Store (Binary a) (Binary a)) -> (Binary a -> Binary a) -> Binary a -> Binary a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src %~ a -> Binary a -> Binary a forall (t :: * -> *) a. Insertable t => a -> t a -> t a insert a x (Binary a -> Binary a) -> Binary a -> Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Binary a tree) instance (forall a . Chain a) => Focusable Root Binary where type Focusing Root Binary a = Maybe a focusing :: Tagged 'Root (Binary a) :-. Focusing 'Root Binary a focusing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Root (Binary a) -> Binary a) -> Tagged 'Root (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Root (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Maybe (Construction Wye a) Nothing) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a))) -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe a forall a. Maybe a Nothing Maybe a -> (Maybe a -> Tagged 'Root (Binary a)) -> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a) forall s a. s -> a -> Product s a :*: Binary a -> Tagged 'Root (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Root (Binary a)) -> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Maybe (Construction Wye a) -> Binary a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Maybe (Construction Wye a) -> Binary a) -> (Maybe a -> Maybe (Construction Wye a)) -> Maybe a -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> Construction Wye a) -> Maybe a -> Maybe (Construction Wye a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b comap (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % (Wye :. Construction Wye) := a forall a. Wye a End) focusing (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Root (Binary a) -> Binary a) -> Tagged 'Root (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Root (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Just Construction Wye a x) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a))) -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a)) -> Store (Maybe a) (Tagged 'Root (Binary a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> Maybe a forall a. a -> Maybe a Just (a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a x) Maybe a -> (Maybe a -> Tagged 'Root (Binary a)) -> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Binary a) forall s a. s -> a -> Product s a :*: Binary a -> Tagged 'Root (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Root (Binary a)) -> (Maybe a -> Binary a) -> Maybe a -> Tagged 'Root (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Binary a) -> (Maybe a -> Construction Wye a) -> Maybe a -> Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> Construction Wye a) -> Construction Wye a -> Maybe a -> Construction Wye a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) (((Wye :. Construction Wye) := a) -> Construction Wye a forall a. Chain a => ((Wye :. Construction Wye) := a) -> Nonempty Binary a rebalance (((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> (Wye :. Construction Wye) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction Wye a x) instance Nullable Binary where null :: (Predicate :. Binary) := a null = (Binary a -> Boolean) -> (Predicate :. Binary) := a forall a. (a -> Boolean) -> Predicate a Predicate ((Binary a -> Boolean) -> (Predicate :. Binary) := a) -> (Binary a -> Boolean) -> (Predicate :. Binary) := a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ \case { TU Maybe (Construction Wye a) Nothing -> Boolean True ; Binary a _ -> Boolean False } instance Substructure Left Binary where type Substructural Left Binary a = Binary a substructure :: Tagged 'Left (Binary a) :-. Substructural 'Left Binary a substructure empty_tree :: Tagged 'Left (Binary a) empty_tree@(Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Left (Binary a) -> Binary a) -> Tagged 'Left (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Left (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Maybe (Construction Wye a) Nothing) = (((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Left (Binary a)) -> Store (Binary a) (Tagged 'Left (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Left (Binary a)) -> Store (Binary a) (Tagged 'Left (Binary a))) -> (((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Left (Binary a)) -> Store (Binary a) (Tagged 'Left (Binary a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Tagged 'Left (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract Tagged 'Left (Binary a) empty_tree Binary a -> (Binary a -> Tagged 'Left (Binary a)) -> ((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Left (Binary a) forall s a. s -> a -> Product s a :*: (!) Tagged 'Left (Binary a) empty_tree substructure (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Left (Binary a) -> Binary a) -> Tagged 'Left (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Left (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Just Construction Wye a tree) = Binary a -> Tagged 'Left (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Left (Binary a)) -> (Construction Wye a -> Binary a) -> Construction Wye a -> Tagged 'Left (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Tagged 'Left (Binary a)) -> Store (Binary a) (Construction Wye a) -> Store (Binary a) (Tagged 'Left (Binary a)) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Left t => t a :-. Substructural 'Left t a sub @Left (Construction Wye a -> Store (Maybe (Construction Wye a)) (Construction Wye a)) -> Lens (Maybe (Construction Wye a)) (Binary a) -> Lens (Construction Wye a) (Binary a) forall src old new. Lens src old -> Lens old new -> Lens src new |> Lens (Maybe (Construction Wye a)) (Binary a) forall a. Maybe (Construction Wye a) :-. Binary a can_be_empty) Construction Wye a tree instance Substructure Right Binary where type Substructural Right Binary a = Binary a substructure :: Tagged 'Right (Binary a) :-. Substructural 'Right Binary a substructure empty_tree :: Tagged 'Right (Binary a) empty_tree@(Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Right (Binary a) -> Binary a) -> Tagged 'Right (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Right (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Maybe (Construction Wye a) Nothing) = (((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Right (Binary a)) -> Store (Binary a) (Tagged 'Right (Binary a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Right (Binary a)) -> Store (Binary a) (Tagged 'Right (Binary a))) -> (((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Right (Binary a)) -> Store (Binary a) (Tagged 'Right (Binary a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Tagged 'Right (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract Tagged 'Right (Binary a) empty_tree Binary a -> (Binary a -> Tagged 'Right (Binary a)) -> ((:*:) (Binary a) :. (->) (Binary a)) := Tagged 'Right (Binary a) forall s a. s -> a -> Product s a :*: (!) Tagged 'Right (Binary a) empty_tree substructure (Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Binary a -> Maybe (Construction Wye a)) -> (Tagged 'Right (Binary a) -> Binary a) -> Tagged 'Right (Binary a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Right (Binary a) -> Binary a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Just Construction Wye a tree) = Binary a -> Tagged 'Right (Binary a) forall k (tag :: k) a. a -> Tagged tag a Tag (Binary a -> Tagged 'Right (Binary a)) -> (Construction Wye a -> Binary a) -> Construction Wye a -> Tagged 'Right (Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> Binary a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction Wye a -> Tagged 'Right (Binary a)) -> Store (Binary a) (Construction Wye a) -> Store (Binary a) (Tagged 'Right (Binary a)) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Right t => t a :-. Substructural 'Right t a sub @Right (Construction Wye a -> Store (Maybe (Construction Wye a)) (Construction Wye a)) -> Lens (Maybe (Construction Wye a)) (Binary a) -> Lens (Construction Wye a) (Binary a) forall src old new. Lens src old -> Lens old new -> Lens src new |> Lens (Maybe (Construction Wye a)) (Binary a) forall a. Maybe (Construction Wye a) :-. Binary a can_be_empty) Construction Wye a tree can_be_empty :: Maybe (Construction Wye a) :-. Binary a can_be_empty :: Maybe (Construction Wye a) :-. Binary a can_be_empty Maybe (Construction Wye a) maybe_tree = (((:*:) (Binary a) :. (->) (Binary a)) := Maybe (Construction Wye a)) -> Store (Binary a) (Maybe (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Binary a) :. (->) (Binary a)) := Maybe (Construction Wye a)) -> Store (Binary a) (Maybe (Construction Wye a))) -> (((:*:) (Binary a) :. (->) (Binary a)) := Maybe (Construction Wye a)) -> Store (Binary a) (Maybe (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe (Construction Wye a) -> Binary a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Maybe (Construction Wye a) maybe_tree Binary a -> (Binary a -> Maybe (Construction Wye a)) -> ((:*:) (Binary a) :. (->) (Binary a)) := Maybe (Construction Wye a) forall s a. s -> a -> Product s a :*: Binary a -> Maybe (Construction Wye a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run type instance Nonempty Binary = Construction Wye instance Focusable Root (Construction Wye) where type Focusing Root (Construction Wye) a = a focusing :: Tagged 'Root (Construction Wye a) :-. Focusing 'Root (Construction Wye) a focusing (Construction Wye a <-| Tagged 'Root forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Wye :. Construction Wye) := a xs) = (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a))) -> (((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a)) -> Store a (Tagged 'Root (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (a -> Tagged 'Root (Construction Wye a)) -> ((:*:) a :. (->) a) := Tagged 'Root (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Root (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Root (Construction Wye a)) -> (a -> Construction Wye a) -> a -> Tagged 'Root (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a) -> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a forall a b c. (a -> b -> c) -> b -> a -> c % (Wye :. Construction Wye) := a xs instance (forall a . Chain a) => Insertable (Construction Wye) where insert :: a -> Construction Wye a -> Construction Wye a insert a x Construction Wye a nonempty = let change :: Maybe (Construction Wye a) -> Maybe (Construction Wye a) change = Construction Wye a -> Maybe (Construction Wye a) forall a. a -> Maybe a Just (Construction Wye a -> Maybe (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Maybe (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Construction Wye a) -> Construction Wye a -> Maybe (Construction Wye a) -> Construction Wye a forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (a -> Construction Wye a -> Construction Wye a forall (t :: * -> *) a. Insertable t => a -> t a -> t a insert a x) (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye :. Construction Wye) := a forall a. Wye a End) in a x a -> a -> Ordering forall a. Chain a => a -> a -> Ordering <=> a <-| Construction Wye forall (t :: * -> *) a. Extractable t => a <-| t extract Construction Wye a nonempty Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a forall a b. a -> (a -> b) -> b & Construction Wye a -> Construction Wye a -> Construction Wye a -> Ordering -> Construction Wye a forall a. a -> a -> a -> Ordering -> a order (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Left t => t a :-. Substructural 'Left t a sub @Left (Construction Wye a -> Store (Maybe (Construction Wye a)) (Construction Wye a)) -> (Maybe (Construction Wye a) -> Maybe (Construction Wye a)) -> Construction Wye a -> Construction Wye a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src %~ Maybe (Construction Wye a) -> Maybe (Construction Wye a) change (Construction Wye a -> Construction Wye a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a nonempty) Construction Wye a nonempty (forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Right t => t a :-. Substructural 'Right t a sub @Right (Construction Wye a -> Store (Maybe (Construction Wye a)) (Construction Wye a)) -> (Maybe (Construction Wye a) -> Maybe (Construction Wye a)) -> Construction Wye a -> Construction Wye a forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src %~ Maybe (Construction Wye a) -> Maybe (Construction Wye a) change (Construction Wye a -> Construction Wye a) -> Construction Wye a -> Construction Wye a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a nonempty) instance Substructure Left (Construction Wye) where type Substructural Left (Construction Wye) a = Maybe :. Construction Wye := a substructure :: Tagged 'Left (Construction Wye a) :-. Substructural 'Left (Construction Wye) a substructure empty_tree :: Tagged 'Left (Construction Wye a) empty_tree@(Construction Wye a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ Wye (Construction Wye a) End) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe (Construction Wye a) forall a. Maybe a Nothing Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a) forall s a. s -> a -> Product s a :*: (Tagged 'Left (Construction Wye a) empty_tree Tagged 'Left (Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a) forall a b. a -> b -> a !) substructure (Construction Wye a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Left Construction Wye a lst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Maybe (Construction Wye a) forall a. a -> Maybe a Just Construction Wye a lst Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Left (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Left (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Wye (Construction Wye a) forall a. Wye a End substructure (Construction Wye a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Right Construction Wye a rst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe (Construction Wye a) forall a. Maybe a Nothing Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Left (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Left (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a)) -> Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a rst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Construction Wye a rst) substructure (Construction Wye a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Both Construction Wye a lst Construction Wye a rst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Left (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Maybe (Construction Wye a) forall a. a -> Maybe a Just Construction Wye a lst Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Left (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Left (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Left (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Left (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a)) -> Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a b c. (a -> b -> c) -> b -> a -> c % Construction Wye a rst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Construction Wye a rst) instance Substructure Right (Construction Wye) where type Substructural Right (Construction Wye) a = Maybe :. Construction Wye := a substructure :: Tagged 'Right (Construction Wye a) :-. Substructural 'Right (Construction Wye) a substructure emtpy_tree :: Tagged 'Right (Construction Wye a) emtpy_tree@(Construction Wye a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ Wye (Construction Wye a) End) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe (Construction Wye a) forall a. Maybe a Nothing Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a) forall s a. s -> a -> Product s a :*: (Tagged 'Right (Construction Wye a) emtpy_tree Tagged 'Right (Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a) forall a b. a -> b -> a !) substructure (Construction Wye a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Left Construction Wye a lst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Maybe (Construction Wye a) forall a. Maybe a Nothing Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Right (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Right (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both Construction Wye a lst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Construction Wye a lst) substructure (Construction Wye a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Right Construction Wye a rst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Maybe (Construction Wye a) forall a. a -> Maybe a Just Construction Wye a rst Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Right (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Right (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Right Wye (Construction Wye a) forall a. Wye a End substructure (Construction Wye a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Both Construction Wye a lst Construction Wye a rst)) = (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a))) -> (((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a)) -> Store (Maybe (Construction Wye a)) (Tagged 'Right (Construction Wye a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction Wye a -> Maybe (Construction Wye a) forall a. a -> Maybe a Just Construction Wye a rst Maybe (Construction Wye a) -> (Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a)) -> ((:*:) (Maybe (Construction Wye a)) :. (->) (Maybe (Construction Wye a))) := Tagged 'Right (Construction Wye a) forall s a. s -> a -> Product s a :*: Construction Wye a -> Tagged 'Right (Construction Wye a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction Wye a -> Tagged 'Right (Construction Wye a)) -> (Maybe (Construction Wye a) -> Construction Wye a) -> Maybe (Construction Wye a) -> Tagged 'Right (Construction Wye a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Wye (Construction Wye a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Wye (Construction Wye a) -> Construction Wye a) -> (Maybe (Construction Wye a) -> Wye (Construction Wye a)) -> Maybe (Construction Wye a) -> Construction Wye a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (Construction Wye a -> Wye (Construction Wye a)) -> Wye (Construction Wye a) -> Maybe (Construction Wye a) -> Wye (Construction Wye a) forall a e r. Monotonic a e => (a -> r) -> r -> e -> r resolve (Construction Wye a -> Construction Wye a -> Wye (Construction Wye a) forall a. a -> a -> Wye a Both Construction Wye a lst) (Construction Wye a -> Wye (Construction Wye a) forall a. a -> Wye a Left Construction Wye a lst) data Biforked a = Top | Leftward a | Rightward a type instance Zipper (Construction Wye) = Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye)) data Vertical a = Up a | Down a instance Rotatable Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where type Rotational Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a = Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a rotation :: Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Rotational 'Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construction Wye a focused :*: TU (TU (Leftward (Construct (T_ (a parent :*: TU (Just Construction Wye a rst))) Biforked (Construction Biforked (T_ Covariant Binary a)) next)))) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both Construction Wye a focused Construction Wye a rst) Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a :*: TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_ Covariant Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_ Covariant Binary a)) next) rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construction Wye a focused :*: TU (TU (Leftward (Construct (T_ (a parent :*: TU Maybe (Construction Wye a) Nothing)) Biforked (Construction Biforked (T_ Covariant Binary a)) next)))) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent (Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> Wye a Left Construction Wye a focused) Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a :*: TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_ Covariant Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_ Covariant Binary a)) next) rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construction Wye a focused :*: TU (TU (Rightward (Construct (T_ (a parent :*: TU (Just Construction Wye a lst))) Biforked (Construction Biforked (T_ Covariant Binary a)) next)))) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent (Construction Wye a -> Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> a -> Wye a Both Construction Wye a lst Construction Wye a focused) Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a :*: TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_ Covariant Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_ Covariant Binary a)) next) rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construction Wye a focused :*: TU (TU (Rightward (Construct (T_ (a parent :*: TU Maybe (Construction Wye a) Nothing)) Biforked (Construction Biforked (T_ Covariant Binary a)) next)))) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> ((Wye :. Construction Wye) := a) -> Construction Wye a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a parent (Construction Wye a -> (Wye :. Construction Wye) := a forall a. a -> Wye a Right Construction Wye a focused) Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a :*: TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Biforked (Construction Biforked (T_ Covariant Binary a)) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU Biforked (Construction Biforked (T_ Covariant Binary a)) next) rotation (Tagged 'Up ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> T_U (Construction Wye a _ :*: TU (TU Biforked (Construction Biforked (T_ Covariant Binary a)) Top))) = Rotational 'Up (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a forall a. Maybe a Nothing instance Rotatable (Down Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where type Rotational (Down Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a = Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a rotation :: Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Rotational ('Down 'Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Left Construction Wye a lst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a next)) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a (:*:) Construction Wye a lst (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall a. a -> Biforked a Leftward (Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_ Covariant Binary a -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a) -> (a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> TU Covariant Covariant Maybe (Construction Wye) a -> a :*: TU Covariant Covariant Maybe (Construction Wye) a forall s a. s -> a -> Product s a :*: ((Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Maybe :. Construction Wye) := a forall a. Maybe a Nothing) (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Biforked :. Construction Biforked) := T_ Covariant Binary a next rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Both Construction Wye a lst Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a next)) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a (:*:) Construction Wye a lst (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall a. a -> Biforked a Leftward (Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_ Covariant Binary a -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a) -> (a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> TU Covariant Covariant Maybe (Construction Wye) a -> a :*: TU Covariant Covariant Maybe (Construction Wye) a forall s a. s -> a -> Product s a :*: ((Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Construction Wye a -> (Maybe :. Construction Wye) := a forall a. a -> Maybe a Just Construction Wye a rst)) (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Biforked :. Construction Biforked) := T_ Covariant Binary a next rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ (Right Construction Wye a _) :*: TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a _) = Rotational ('Down 'Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a forall a. Maybe a Nothing rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Left) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ Wye (Construction Wye a) End :*: TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a _) = Rotational ('Down 'Left) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a forall a. Maybe a Nothing instance Rotatable (Down Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) where type Rotational (Down Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) a = Maybe :. (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant (Maybe <:.> Construction Wye))) := a rotation :: Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Rotational ('Down 'Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Right Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a next)) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a (:*:) Construction Wye a rst (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall a. a -> Biforked a Rightward (Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_ Covariant Binary a -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a) -> (a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> TU Covariant Covariant Maybe (Construction Wye) a -> a :*: TU Covariant Covariant Maybe (Construction Wye) a forall s a. s -> a -> Product s a :*: ((Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Maybe :. Construction Wye) := a forall a. Maybe a Nothing) (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Biforked :. Construction Biforked) := T_ Covariant Binary a next rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a x (Both Construction Wye a lst Construction Wye a rst) :*: TU (TU (Biforked :. Construction Biforked) := T_ Covariant Binary a next)) = (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall a. a -> Maybe a Just ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *) (a :: k). (t a :*: u a) -> T_U ct cu t u a T_U (Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Wye a -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall s a. s -> a -> Product s a (:*:) Construction Wye a rst (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a)) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> TU Covariant Covariant Biforked (Construction Biforked) (T_ Covariant Binary a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall a. a -> Biforked a Rightward (Construction Biforked (T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> (Biforked :. Construction Biforked) := T_ Covariant Binary a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . T_ Covariant Binary a -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Construction Biforked (T_ Covariant Binary a) forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall k (ct :: k) (t :: * -> *) a. (a :*: t a) -> T_ ct t a T_ ((a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a) -> (a :*: TU Covariant Covariant Maybe (Construction Wye) a) -> T_ Covariant Binary a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> TU Covariant Covariant Maybe (Construction Wye) a -> a :*: TU Covariant Covariant Maybe (Construction Wye) a forall s a. s -> a -> Product s a :*: ((Maybe :. Construction Wye) := a) -> TU Covariant Covariant Maybe (Construction Wye) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Construction Wye a -> (Maybe :. Construction Wye) := a forall a. a -> Maybe a Just Construction Wye a lst)) (((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a)) -> ((Biforked :. Construction Biforked) := T_ Covariant Binary a) -> Maybe ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Biforked :. Construction Biforked) := T_ Covariant Binary a next rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ (Left Construction Wye a _) :*: TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a _) = Rotational ('Down 'Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a forall a. Maybe a Nothing rotation ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a)) -> (Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> Product (Construction Wye a) (TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged ('Down 'Right) ((<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a) -> (<:*:>) (Construction Wye) ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary) a forall (t :: * -> *) a. Extractable t => a <-| t extract -> Construct a _ Wye (Construction Wye a) End :*: TU Covariant Covariant (Biforked <:.> Construction Biforked) (T_ Covariant Binary) a _) = Rotational ('Down 'Right) (Construction Wye <:*:> ((Biforked <:.> Construction Biforked) <:.> T_ Covariant Binary)) a forall a. Maybe a Nothing