{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.Binary where
import Pandora.Core.Functor (type (:=), type (:=>), type (:::))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bindable ((=<<))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Paradigm.Primary ()
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), type (:*:), attached, twosome)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), (&))
import Pandora.Paradigm.Primary.Algebraic (($$$>-), (<-*-), extract)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Ordering (order)
import Pandora.Paradigm.Primary.Functor (Comparison)
import Pandora.Paradigm.Primary.Functor.Convergence (Convergence (Convergence))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), P_Q_T (P_Q_T), type (<:.>), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (=||))
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (over, view)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), morph, premorph
, Morph (Rotate, Into, Insert, Lookup, Vary, Key, Element), Vertical (Up, Down), lookup, vary)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure), Segment (Root), sub)
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))
type Binary = Maybe <:.> Construction Wye
instance {-# OVERLAPS #-} Traversable (->) (->) (Construction Wye) where
a -> u b
f <<- :: (a -> u b) -> Construction Wye a -> u (Construction Wye b)
<<- (Construct a
x (Left Construction Wye a
l)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> Wye a
Left (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
l)
a -> u b
f <<- (Construct a
x (Right Construction Wye a
r)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> Wye a
Right (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
r)
a -> u b
f <<- (Construct a
x (Both Construction Wye a
l Construction Wye a
r)) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u b
-> u (((Wye :. Construction Wye) := b) -> Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x u (((Wye :. Construction Wye) := b) -> Construction Wye b)
-> u ((Wye :. Construction Wye) := b) -> u (Construction Wye b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (Construction Wye b
-> Construction Wye b -> (Wye :. Construction Wye) := b
forall a. a -> a -> Wye a
Both (Construction Wye b
-> Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b)
-> u (Construction Wye b -> (Wye :. Construction Wye) := b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
l u (Construction Wye b -> (Wye :. Construction Wye) := b)
-> u (Construction Wye b) -> u ((Wye :. Construction Wye) := b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t,
Semimonoidal (Straight (->)) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- a -> u b
f (a -> u b) -> Construction Wye a -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- Construction Wye a
r)
a -> u b
f <<- (Construct a
x Wye (Construction Wye a)
End) = b -> ((Wye :. Construction Wye) := b) -> Construction Wye b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((Wye :. Construction Wye) := b) -> Construction Wye b)
-> ((Wye :. Construction Wye) := b) -> b -> Construction Wye b
forall a b c. (a -> b -> c) -> b -> a -> c
% (Wye :. Construction Wye) := b
forall a. Wye a
End (b -> Construction Wye b) -> u b -> u (Construction Wye b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> a -> u b
f a
x
instance Morphable Insert Binary where
type Morphing Insert Binary = (Identity <:.:> Comparison := (:*:)) <:.:> Binary := (->)
morphing :: (<:.>) (Tagged 'Insert) Binary a -> Morphing 'Insert Binary a
morphing (<:.>) (Tagged 'Insert) Binary a
binary = case TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a)
-> TU Covariant Covariant Maybe (Construction Wye) a
-> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Insert) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph (<:.>) (Tagged 'Insert) Binary a
binary of
(Maybe :. Construction Wye) := a
Nothing -> (T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Comparison a
_)) -> Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x
Just Construction Wye a
non_empty_binary -> (T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
Binary
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Convergence a -> a -> Ordering
f)) ->
let continue :: Construction Wye a -> Construction Wye a
continue Construction Wye a
xs = T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Nonempty Binary a -> Morphing 'Insert (Nonempty Binary) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
struct ~> Morphing mod struct
morph @Insert @(Nonempty Binary) Nonempty Binary a
Construction Wye a
xs (T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a
-> Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Identity a
-> Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity a
x (Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Comparison a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (a -> a -> Ordering) -> Comparison a
forall r a. (a -> a -> r) -> Convergence r a
Convergence a -> a -> Ordering
f in
let 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> ((Maybe :. Construction Wye) := a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Construction Wye a
continue (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) in
Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> a -> Ordering
f a
x (a -> Ordering) -> a -> Ordering
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye a
non_empty_binary Ordering -> (Ordering -> Construction Wye a) -> Construction Wye a
forall a b. a -> (a -> b) -> b
& Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall a. a -> a -> a -> Ordering -> a
order (Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
non_empty_binary
# over (sub @Left) change non_empty_binary
# over (sub @Right) change non_empty_binary
instance Nullable Binary where
null :: (Predicate :. Binary) := a
null = (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Binary a -> Boolean) -> (Predicate :. Binary) := a)
-> (Binary a -> Boolean) -> (Predicate :. Binary) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case { TU Maybe (Construction Wye a)
Nothing -> Boolean
True ; Binary a
_ -> Boolean
False }
instance Substructure Left Binary where
type Available Left Binary = Maybe
type Substance Left Binary = Construction Wye
substructure :: Lens
(Available 'Left Binary)
((<:.>) (Tagged 'Left) Binary a)
(Substance 'Left Binary a)
substructure = ((<:.>) (Tagged 'Left) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) Binary a)
(Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) Binary a)
(Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) Binary a)
(Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) Binary a
bintree -> case TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Left) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Left) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Left) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Left) Binary a -> Maybe (Construction Wye a))
-> (<:.>) (Tagged 'Left) Binary a -> Maybe (Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) Binary a
bintree of
Maybe (Construction Wye a)
Nothing -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall (m :: * -> * -> *) a b. Category m => 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) Binary a)
-> ((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) Binary a
forall s a. s -> a -> s :*: a
:*: TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a)
-> (Maybe (Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe (Construction Wye a)
-> 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
Just Construction Wye a
tree -> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Left) Binary a)
-> (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Left) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Wye a -> (<:.>) (Tagged 'Left) Binary a)
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Left) Binary a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> P_Q_T (->) Store Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left) Construction Wye a
tree
instance Substructure Right Binary where
type Available Right Binary = Maybe
type Substance Right Binary = Construction Wye
substructure :: Lens
(Available 'Right Binary)
((<:.>) (Tagged 'Right) Binary a)
(Substance 'Right Binary a)
substructure = ((<:.>) (Tagged 'Right) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) Binary a)
(Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) Binary a)
(Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) Binary a)
(Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) Binary a
bintree -> case TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) a
-> Maybe (Construction Wye a))
-> ((<:.>) (Tagged 'Right) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> (<:.>) (Tagged 'Right) Binary a
-> Maybe (Construction Wye a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a)
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (TU Covariant Covariant Maybe (Construction Wye) a)
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> ((<:.>) (Tagged 'Right) Binary a
-> Tagged
'Right (TU Covariant Covariant Maybe (Construction Wye) a))
-> (<:.>) (Tagged 'Right) Binary a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) Binary a
-> Tagged
'Right (TU Covariant Covariant Maybe (Construction Wye) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<:.>) (Tagged 'Right) Binary a -> Maybe (Construction Wye a))
-> (<:.>) (Tagged 'Right) Binary a -> Maybe (Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) Binary a
bintree of
Maybe (Construction Wye a)
Nothing -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) Binary a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall (m :: * -> * -> *) a b. Category m => 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) Binary a)
-> ((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) Binary a
forall s a. s -> a -> s :*: a
:*: TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a)
-> (Maybe (Construction Wye a)
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe (Construction Wye a)
-> 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
Just Construction Wye a
tree -> TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TU Covariant Covariant Maybe (Construction Wye) a
-> (<:.>) (Tagged 'Right) Binary a)
-> (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> Construction Wye a
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Liftable (->) t, Covariant (->) (->) u) =>
u a -> t u a
lift @(->) (Construction Wye a -> (<:.>) (Tagged 'Right) Binary a)
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
-> Store
(Maybe (Construction Wye a)) ((<:.>) (Tagged 'Right) Binary a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> P_Q_T (->) Store Maybe (Construction Wye a) (Construction Wye a)
-> Construction Wye a
-> Store (Maybe (Construction Wye a)) (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right) Construction Wye a
tree
type instance Nonempty Binary = Construction Wye
instance Morphable (Into Binary) (Construction Wye) where
type Morphing (Into Binary) (Construction Wye) = Binary
morphing :: (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Morphing ('Into Binary) (Construction Wye) a
morphing = Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a)
-> ((<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Construction Wye a)
-> (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into Binary)) (Construction Wye) a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph
instance Morphable Insert (Construction Wye) where
type Morphing Insert (Construction Wye) = (Identity <:.:> Comparison := (:*:)) <:.:> Construction Wye := (->)
morphing :: (<:.>) (Tagged 'Insert) (Construction Wye) a
-> Morphing 'Insert (Construction Wye) a
morphing ((<:.>) (Tagged 'Insert) (Construction Wye) a -> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construction Wye a
nonempty_list) = (T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a)
-> (T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U (Identity a
x :*: Convergence a -> a -> Ordering
f)) ->
let continue :: Construction Wye a -> Construction Wye a
continue Construction Wye a
xs = T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U
Covariant
Covariant
(->)
(T_U Covariant Covariant (:*:) Identity Comparison)
(Construction Wye)
a
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Nonempty Binary a -> Morphing 'Insert (Nonempty Binary) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
struct ~> Morphing mod struct
morph @Insert @(Nonempty Binary) Nonempty Binary a
Construction Wye a
xs (T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a)
-> T_U Covariant Covariant (:*:) Identity Comparison a
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Identity a
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> Identity a
forall a. a -> Identity a
Identity a
x (Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a)
-> Convergence Ordering a
-> T_U Covariant Covariant (:*:) Identity Comparison a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (a -> a -> Ordering) -> Convergence Ordering a
forall r a. (a -> a -> r) -> Convergence r a
Convergence a -> a -> Ordering
f in
let 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> Maybe (Construction Wye a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Construction Wye a
continue (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) in
Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall a. a -> a -> a -> Ordering -> a
order (Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a)
-> Construction Wye a
-> Construction Wye a
-> Construction Wye a
-> Ordering
-> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
nonempty_list
# over (sub @Left) change nonempty_list
# over (sub @Right) change nonempty_list
# f x (extract nonempty_list)
instance Substructure Root (Construction Wye) where
type Available Root (Construction Wye) = Identity
type Substance Root (Construction Wye) = Identity
substructure :: Lens
(Available 'Root (Construction Wye))
((<:.>) (Tagged 'Root) (Construction Wye) a)
(Substance 'Root (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Root) (Construction Wye) a
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Root) (Construction Wye) a)
(Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Root) (Construction Wye) a
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Root) (Construction Wye) a)
(Identity a))
-> ((<:.>) (Tagged 'Root) (Construction Wye) a
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Root) (Construction Wye) a)
(Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Construction Wye) a
bintree -> case (<:.>) (Tagged 'Root) (Construction Wye) a -> Construction Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Root) (Construction Wye) a
bintree of
Construct a
x (Wye :. Construction Wye) := a
xs -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Root) (Construction Wye) a)
-> Store
(Identity (Identity a))
((<:.>) (Tagged 'Root) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
x) Identity (Identity a)
-> (Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Root) (Construction Wye) a
forall s a. s -> a -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Root) (Construction Wye) a)
-> (Identity (Identity a) -> Construction Wye a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Wye :. Construction Wye) := a) -> Construction Wye a)
-> ((Wye :. Construction Wye) := a) -> a -> Construction Wye a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Wye :. Construction Wye) := a
xs) (a -> Construction Wye a)
-> (Identity (Identity a) -> a)
-> Identity (Identity a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Substructure Left (Construction Wye) where
type Available Left (Construction Wye) = Maybe
type Substance Left (Construction Wye) = Construction Wye
substructure :: Lens
(Available 'Left (Construction Wye))
((<:.>) (Tagged 'Left) (Construction Wye) a)
(Substance 'Left (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Left) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) (Construction Wye) a)
(Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) (Construction Wye) a)
(Construction Wye a))
-> ((<:.>) (Tagged 'Left) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Left) (Construction Wye) a)
(Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Left) (Construction Wye) a
bintree -> case Tagged 'Left (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Left (Construction Wye a) -> Construction Wye a)
-> Tagged 'Left (Construction Wye a) -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Construction Wye) a
-> Tagged 'Left (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Left) (Construction Wye) a
bintree of
Construct a
x Wye (Construction Wye a)
End -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> Maybe (Construction Wye a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x)
Construct a
x (Left Construction Wye a
lst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Wye (Construction Wye a)
forall a. Wye a
End
Construct a
x (Right Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst)
Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Left) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Left) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Left) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Left) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
-> Wye (Construction Wye a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
rst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Construction Wye a
rst)
instance Substructure Right (Construction Wye) where
type Available Right (Construction Wye) = Maybe
type Substance Right (Construction Wye) = Construction Wye
substructure :: Lens
(Available 'Right (Construction Wye))
((<:.>) (Tagged 'Right) (Construction Wye) a)
(Substance 'Right (Construction Wye) a)
substructure = ((<:.>) (Tagged 'Right) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) (Construction Wye) a)
(Construction Wye a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) (Construction Wye) a)
(Construction Wye a))
-> ((<:.>) (Tagged 'Right) (Construction Wye) a
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> P_Q_T
(->)
Store
Maybe
((<:.>) (Tagged 'Right) (Construction Wye) a)
(Construction Wye a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Right) (Construction Wye) a
bintree -> case Tagged 'Right (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (Construction Wye a) -> Construction Wye a)
-> Tagged 'Right (Construction Wye a) -> Construction Wye a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) (Construction Wye) a
-> Tagged 'Right (Construction Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Right) (Construction Wye) a
bintree of
Construct a
x Wye (Construction Wye a)
End -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Construction Wye a)
-> Construction Wye a
-> Maybe (Construction Wye a)
-> Construction Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Construction Wye a -> Wye (Construction Wye a))
-> Construction Wye a
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x)
Construct a
x (Left Construction Wye a
lst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst)
Construct a
x (Right Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Right Wye (Construction Wye a)
forall a. Wye a
End
Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a))
-> (((:*:) (Maybe (Construction Wye a))
:. (->) (Maybe (Construction Wye a)))
:= (<:.>) (Tagged 'Right) (Construction Wye) a)
-> Store
(Maybe (Construction Wye a))
((<:.>) (Tagged 'Right) (Construction Wye) a)
forall (m :: * -> * -> *) a b. Category m => 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 -> s :*: a
:*: Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye a -> (<:.>) (Tagged 'Right) (Construction Wye) a)
-> (Maybe (Construction Wye a) -> Construction Wye a)
-> Maybe (Construction Wye a)
-> (<:.>) (Tagged 'Right) (Construction Wye) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Wye (Construction Wye a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye (Construction Wye a) -> Construction Wye a)
-> (Maybe (Construction Wye a) -> Wye (Construction Wye a))
-> Maybe (Construction Wye a)
-> Construction Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction Wye a -> Wye (Construction Wye a))
-> Wye (Construction Wye a)
-> Maybe (Construction Wye a)
-> Wye (Construction Wye a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction Wye a
-> Construction Wye a -> Wye (Construction Wye a)
forall a. a -> a -> Wye a
Both Construction Wye a
lst) (Construction Wye a -> Wye (Construction Wye a)
forall a. a -> Wye a
Left Construction Wye a
lst)
instance Chain k => Morphable (Lookup Key) (Prefixed Binary k) where
type Morphing (Lookup Key) (Prefixed Binary k) = (->) k <:.> Maybe
morphing :: (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Morphing ('Lookup 'Key) (Prefixed Binary k) a
morphing (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction Wye (k :*: a))
Nothing) = (((->) k :. Maybe) := a) -> TU Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) k :. Maybe) := a)
-> TU Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) := a)
-> TU Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \k
_ -> Maybe a
forall a. Maybe a
Nothing
morphing (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just Construction Wye (k :*: a)
tree) = (((->) k :. Maybe) := a) -> TU Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) k :. Maybe) := a)
-> TU Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) := a)
-> TU Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \k
key ->
let root :: k :*: a
root = Construction Wye (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye (k :*: a)
tree in k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (k :*: a) -> k
forall a b. (a :*: b) -> a
attached k :*: a
root Ordering -> (Ordering -> Maybe a) -> Maybe a
forall a b. a -> (a -> b) -> b
& Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall a. a -> a -> a -> Ordering -> a
order (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (k :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract k :*: a
root)
(k -> Prefixed (Construction Wye) k a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key k
key (Prefixed (Construction Wye) k a -> Maybe a)
-> (Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a)
-> Construction Wye (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (k :*: a) -> Maybe a)
-> Maybe (Construction Wye (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a))
forall (available :: * -> *) source target.
Lens available source target -> source -> available target
view (Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a)))
-> Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye (k :*: a)
tree)
(k -> Prefixed (Construction Wye) k a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key k
key (Prefixed (Construction Wye) k a -> Maybe a)
-> (Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a)
-> Construction Wye (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a) -> Prefixed (Construction Wye) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (k :*: a) -> Maybe a)
-> Maybe (Construction Wye (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a))
forall (available :: * -> *) source target.
Lens available source target -> source -> available target
view (Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> Lens
Maybe (Construction Wye (k :*: a)) (Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Right structure)
:= Available 'Right structure
sub @Right (Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a)))
-> Construction Wye (k :*: a) -> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye (k :*: a)
tree)
instance Chain k => Morphable (Vary Element) (Prefixed Binary k) where
type Morphing (Vary Element) (Prefixed Binary k) = ((:*:) k <:.> Identity) <:.:> Prefixed Binary k := (->)
morphing :: (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Morphing ('Vary 'Element) (Prefixed Binary k) a
morphing (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction Wye (k :*: a))
Nothing) = (TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a)
-> (TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (k
key :*: Identity a
value)) -> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Prefixed Binary k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Prefixed Binary k a)
-> ((k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (k :*: a)
-> Prefixed Binary k a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((k :*: a) -> Construction Wye (k :*: a))
-> (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (k :*: a) -> Construction Wye (k :*: a)
forall a. a :=> Nonempty Binary
leaf ((k :*: a) -> Prefixed Binary k a)
-> (k :*: a) -> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ k
key k -> a -> k :*: a
forall s a. s -> a -> s :*: a
:*: a
value
morphing (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Maybe (Construction Wye (k :*: a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Binary k a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just Construction Wye (k :*: a)
tree) = (TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
(t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a)
-> (TU Covariant Covariant ((:*:) k) Identity a
-> Prefixed Binary k a)
-> T_U
Covariant
Covariant
(->)
(TU Covariant Covariant ((:*:) k) Identity)
(Prefixed Binary k)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (k
key :*: Identity a
value)) ->
let continue :: Maybe (Construction Wye (k :*: a))
-> Maybe (Construction Wye (k :*: a))
continue = ((k -> a -> Prefixed Binary k a -> Prefixed Binary k a
forall a (mod :: a) key value (struct :: * -> *).
Morphed
('Vary mod)
struct
((((:*:) key <:.> Identity) <:.:> struct) := (->)) =>
key -> value -> struct value -> struct value
vary @Element @k @_ @(Prefixed Binary _) k
key a
value (Prefixed Binary k a -> Prefixed Binary k a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
=||) (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> Maybe (Construction Wye (k :*: a))
-> Maybe (Construction Wye (k :*: a))
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
=||)
in let root :: k :*: a
root = Construction Wye (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Wye (k :*: a)
tree in TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Prefixed Binary k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
-> Prefixed Binary k a)
-> (Construction Wye (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a))
-> Construction Wye (k :*: a)
-> Prefixed Binary k a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (k :*: a)
-> TU Covariant Covariant Maybe (Construction Wye) (k :*: a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction Wye (k :*: a) -> Prefixed Binary k a)
-> Construction Wye (k :*: a) -> Prefixed Binary k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (k :*: a) -> k
forall a b. (a :*: b) -> a
attached k :*: a
root Ordering
-> (Ordering -> Construction Wye (k :*: a))
-> Construction Wye (k :*: a)
forall a b. a -> (a -> b) -> b
& Construction Wye (k :*: a)
-> Construction Wye (k :*: a)
-> Construction Wye (k :*: a)
-> Ordering
-> Construction Wye (k :*: a)
forall a. a -> a -> a -> Ordering -> a
order
# over (sub @Root) ($$$>- value) tree
# over (sub @Left) continue tree
# over (sub @Right) continue tree
instance Chain key => Morphable (Lookup Key) (Prefixed (Construction Wye) key) where
type Morphing (Lookup Key) (Prefixed (Construction Wye) key) = (->) key <:.> Maybe
morphing :: (<:.>) (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Morphing ('Lookup 'Key) (Prefixed (Construction Wye) key) a
morphing (Prefixed (Construction Wye) key a -> Construction Wye (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed (Construction Wye) key a -> Construction Wye (key :*: a))
-> ((<:.>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Prefixed (Construction Wye) key a)
-> (<:.>)
(Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Construction Wye (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed (Construction Wye) key) a
-> Prefixed (Construction Wye) key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct key :*: a
x (Wye :. Construction Wye) := (key :*: a)
xs) = (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) := a)
-> TU Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \key
key ->
key
key key -> key -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (key :*: a) -> key
forall a b. (a :*: b) -> a
attached key :*: a
x Ordering -> (Ordering -> Maybe a) -> Maybe a
forall a b. a -> (a -> b) -> b
& Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall a. a -> a -> a -> Ordering -> a
order (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (key :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract key :*: a
x)
(key -> Prefixed (Construction Wye) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Wye) key a -> Maybe a)
-> (Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a)
-> Identity (Construction Wye (key :*: a))
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a)
-> (Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a))
-> Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity (Construction Wye (key :*: a)) -> Maybe a)
-> Maybe (Identity (Construction Wye (key :*: a))) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (available :: * -> *) source target.
Lens available source target -> source -> available target
view (Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a))))
-> Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a))))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs)
(key -> Prefixed (Construction Wye) key a -> Maybe a
forall a1 (mod :: a1) key (struct :: * -> *) a2.
Morphed ('Lookup mod) struct ((->) key <:.> Maybe) =>
key -> struct a2 -> Maybe a2
lookup @Key key
key (Prefixed (Construction Wye) key a -> Maybe a)
-> (Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a)
-> Identity (Construction Wye (key :*: a))
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (Construction Wye (key :*: a) -> Prefixed (Construction Wye) key a)
-> (Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a))
-> Identity (Construction Wye (key :*: a))
-> Prefixed (Construction Wye) key a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Construction Wye (key :*: a))
-> Construction Wye (key :*: a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity (Construction Wye (key :*: a)) -> Maybe a)
-> Maybe (Identity (Construction Wye (key :*: a))) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (available :: * -> *) source target.
Lens available source target -> source -> available target
view (Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a))))
-> Lens
Maybe
((Wye :. Construction Wye) := (key :*: a))
(Identity (Construction Wye (key :*: a)))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
(structure #=@ Substance segment structure)
:= Available segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
(structure #=@ Substance 'Left structure)
:= Available 'Left structure
sub @Left (((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a))))
-> ((Wye :. Construction Wye) := (key :*: a))
-> Maybe (Identity (Construction Wye (key :*: a)))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Wye :. Construction Wye) := (key :*: a)
xs)
data Biforked a = Top | Leftward a | Rightward a
instance Covariant (->) (->) Biforked where
a -> b
_ <$> :: (a -> b) -> Biforked a -> Biforked b
<$> Biforked a
Top = Biforked b
forall a. Biforked a
Top
a -> b
f <$> Leftward a
l = b -> Biforked b
forall a. a -> Biforked a
Leftward (b -> Biforked b) -> b -> Biforked b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
l
a -> b
f <$> Rightward a
r = b -> Biforked b
forall a. a -> Biforked a
Rightward (b -> Biforked b) -> b -> Biforked b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
r
type Bifurcation = Biforked <:.> Construction Biforked
type Bicursor = Identity <:.:> Binary := (:*:)
type instance Zipper (Construction Wye) (Up ::: Down Left ::: Down Right) =
Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)
instance Morphable (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
type Morphing (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
= Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
morphing :: (<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Morphing
('Rotate 'Up)
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_U (Identity a
parent :*: Binary a
rest)) Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)))) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
parent ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> (Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both Construction Wye a
focused (((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> Wye a
Left Construction Wye a
focused (((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Binary a -> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Binary a
rest) (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construction Wye a
focused :*: TU (TU (Rightward (Construct (T_U (Identity a
parent :*: Binary a
rest)) Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)))) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
parent ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve ((Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> (Construction Wye a -> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> a -> Wye a
Both (Construction Wye a
-> Construction Wye a -> (Wye :. Construction Wye) := a)
-> Construction Wye a
-> Construction Wye a
-> (Wye :. Construction Wye) := a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Wye a
focused (((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> ((Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Wye a -> (Wye :. Construction Wye) := a
forall a. a -> Wye a
Right Construction Wye a
focused (((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a)
-> ((Maybe :. Construction Wye) := a)
-> (Wye :. Construction Wye) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Binary a -> (Maybe :. Construction Wye) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Binary a
rest) (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
next)
morphing ((<:.>)
(Tagged ('Rotate 'Up))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> T_U (Construction Wye a
_ :*: TU (TU Biforked
(Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
Top))) = ((Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a
forall a. Maybe a
Nothing
instance Morphable (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
type Morphing (Rotate (Down Left)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
= Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
morphing :: (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Morphing
('Rotate ('Down 'Left))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Left Construction Wye a
lst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next)) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome Construction Wye a
lst (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (((Maybe :. Construction Wye) := a)
-> 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_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next)) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome Construction Wye a
lst (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Leftward (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift Construction Wye a
rst) (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ (Right Construction Wye a
_) :*: TU Covariant Covariant Bifurcation Bicursor a
_) = ((Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a
forall a. Maybe a
Nothing
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Left)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ Wye (Construction Wye a)
End :*: TU Covariant Covariant Bifurcation Bicursor a
_) = ((Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a
forall a. Maybe a
Nothing
instance Morphable (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
type Morphing (Rotate (Down Right)) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
= Maybe <:.> (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
morphing :: (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Morphing
('Rotate ('Down 'Right))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Right Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next)) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome Construction Wye a
rst (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (((Maybe :. Construction Wye) := a)
-> 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_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) :*: TU (TU (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next)) =
(:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Wye a
-> TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome Construction Wye a
rst (TU Covariant Covariant Bifurcation Bicursor a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a)
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a))
-> (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Biforked
(Construction Biforked)
(T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
forall a. a -> Biforked a
Rightward (Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> T_U Covariant Covariant (:*:) Identity Binary a
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Identity a
-> TU Covariant Covariant Maybe (Construction Wye) a
-> T_U Covariant Covariant (:*:) Identity Binary a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a -> Identity a
forall a. a -> Identity a
Identity a
x) (Construction Wye a
-> TU Covariant Covariant Maybe (Construction Wye) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift Construction Wye a
lst) (((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a))
-> ((Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a)
-> Construction
Biforked (T_U Covariant Covariant (:*:) Identity Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Biforked :. Construction Biforked)
:= T_U Covariant Covariant (:*:) Identity Binary a
next
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ (Left Construction Wye a
_) :*: TU Covariant Covariant Bifurcation Bicursor a
_) = ((Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a
forall a. Maybe a
Nothing
morphing ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a)
-> ((<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a)
-> (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> Construction Wye a
:*: TU Covariant Covariant Bifurcation Bicursor a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>)
(Tagged ('Rotate ('Down 'Right)))
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
-> (:=)
(Construction Wye <:.:> (Bifurcation <:.> Bicursor)) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct a
_ Wye (Construction Wye a)
End :*: TU Covariant Covariant Bifurcation Bicursor a
_) = ((Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a)
-> TU
Covariant
Covariant
Maybe
((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:))
a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe
:. ((Construction Wye <:.:> (Bifurcation <:.> Bicursor)) := (:*:)))
:= a
forall a. Maybe a
Nothing
leaf :: a :=> Nonempty Binary
leaf :: a :=> Nonempty Binary
leaf a
x = a -> ((Wye :. Construction Wye) := a) -> Construction Wye a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Wye :. Construction Wye) := a
forall a. Wye a
End