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

import Pandora.Core.Functor (type (~>), type (>), type (<), type (:=>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), (-->), (--->))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|-|-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bindable (Bindable ((===<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), type (:*:), type (<:*:>), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), (&), (.:..))
import Pandora.Paradigm.Primary.Algebraic ((<-*-), (<-*--), (<-*-*-), extract, point, empty)
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.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Primary (twosome)
import Pandora.Paradigm.Schemes (TT (TT), T_U (T_U), P_Q_T (P_Q_T), type (<::>), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (<~))
import Pandora.Paradigm.Inventory.Ability.Gettable (get)
import Pandora.Paradigm.Inventory.Ability.Settable (set)
import Pandora.Paradigm.Inventory.Ability.Modifiable (modify)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (Lens, Obscure, view, replace, mutate)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), morph, premorph
	, Morph (Rotate, Into, Insert, Lookup, Key), Vertical (Up, Down), Horizontal (Leftward, Rightward), lookup)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root), sub)
import Pandora.Paradigm.Structure.Ability.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))

type Binary = Maybe <::> Construction (Maybe <:*:> Maybe)

-- instance {-# OVERLAPS #-} Traversable (->) (->) (Construction Wye) where
	-- f <<- Construct x (Left l) = Construct <-|-- f x <-*-- Left <-|- f <<- l
	-- f <<- Construct x (Right r) = Construct <-|-- f x <-*-- Right <-|- f <<- r
	-- f <<- Construct x (Both l r) = Construct <-|-- f x <-*-- Both <-|- f <<- l <-*- f <<- r
	-- f <<- Construct x End = Construct % End <-|- f x

-- instance {-# OVERLAPS #-} Traversable (->) (->) (Construction (Maybe <:*:> Maybe)) where
	-- f <<- Construct x branches = Construct <-|- f x <-*- (f <<- branches :: _)

	-- f <<- Construct x (Left l) = Construct <-|-- f x <-*-- Left <-|- f <<- l
	-- f <<- Construct x (Right r) = Construct <-|-- f x <-*-- Right <-|- f <<- r
	-- f <<- Construct x (Both l r) = Construct <-|-- f x <-*-- Both <-|- f <<- l <-*- f <<- r
	-- f <<- Construct x (Nothing <:*:> Nothing) = Construct % (Nothing <:*:> Nothing) <-|- f x

--rebalance :: Chain a => (Wye :. Construction Wye > a) -> Nonempty Binary a
--rebalance (Both x y) = extract x <=> extract y & order
--	# Construct (extract x) (Both # rebalance (deconstruct x) # rebalance (deconstruct y))
--	# Construct (extract y) (Both # x # rebalance (deconstruct y))
--	# Construct (extract x) (Both # rebalance (deconstruct x) # y)

-- instance Morphable Insert Binary where
	-- type Morphing Insert Binary = (Exactly <:.:> Comparison > (:*:)) <:.:> Binary > (->)
	-- morphing struct = case run ---> premorph struct of
		-- Nothing -> T_U <-- \(T_U (Exactly x :*: _)) -> lift <-- leaf x
		-- Just binary -> T_U <-- \(T_U (Exactly x :*: Convergence f)) ->
			-- let continue xs = run <-- morph @Insert @(Nonempty Binary) xs <--- twosome <-- Exactly x <-- Convergence f in
			-- let step = iff @Just <-|-|- get @(Obscure Lens) <-*-*- modify @(Obscure Lens) continue <-*-*- set @(Obscure Lens) <-- leaf x in
			-- lift <---- order binary
				-- <--- step <-- sub @Left <-- binary
				-- <--- step <-- sub @Right <-- binary
				-- <--- f x <-- extract binary

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

instance Substructure Right Binary where
	type Substance Right Binary = Binary
	substructure :: Lens (Substance 'Right Binary) ((<:.>) (Tagged 'Right) Binary a) a
substructure = ((<:.>) (Tagged 'Right) Binary a
 -> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T (->) Store Binary ((<:.>) (Tagged 'Right) Binary a) 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 (Binary a) ((<:.>) (Tagged 'Right) Binary a))
 -> P_Q_T (->) Store Binary ((<:.>) (Tagged 'Right) Binary a) a)
-> ((<:.>) (Tagged 'Right) Binary a
    -> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a))
-> P_Q_T (->) Store Binary ((<:.>) (Tagged 'Right) Binary a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Right) Binary a
struct -> case Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) > a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) > a)
-> ((<:.>) (Tagged 'Right) Binary a -> Binary a)
-> (<:.>) (Tagged 'Right) Binary a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tagged 'Right (Binary a) -> Binary a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (Binary a) -> Binary a)
-> ((<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (Binary a))
-> (<:.>) (Tagged 'Right) Binary a
-> Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Right) Binary a -> Tagged 'Right (Binary a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<:.>) (Tagged 'Right) Binary a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) > a)
-> (<:.>) (Tagged 'Right) Binary a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
---> (<:.>) (Tagged 'Right) Binary a
struct of
		(Maybe :. Construction (Maybe <:*:> Maybe)) > a
Nothing -> (((:*:) (Binary a) :. (->) (Binary a))
 > (<:.>) (Tagged 'Right) Binary a)
-> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:) (Binary a) :. (->) (Binary a))
  > (<:.>) (Tagged 'Right) Binary a)
 -> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a))
-> (((:*:) (Binary a) :. (->) (Binary a))
    > (<:.>) (Tagged 'Right) Binary a)
-> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a
forall (t :: * -> *) a. Emptiable t => t a
empty Binary a
-> (Binary a -> (<:.>) (Tagged 'Right) Binary a)
-> ((:*:) (Binary a) :. (->) (Binary a))
   > (<:.>) (Tagged 'Right) Binary a
forall s a. s -> a -> s :*: a
:*: Binary a -> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Binary a -> (<:.>) (Tagged 'Right) Binary a)
-> (Binary a -> Binary a)
-> Binary a
-> (<:.>) (Tagged 'Right) Binary a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary a -> Binary a -> Binary a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant Binary a
forall (t :: * -> *) a. Emptiable t => t a
empty
		Just Construction (Maybe <:*:> Maybe) a
tree -> Binary a -> (<:.>) (Tagged 'Right) Binary a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Binary a -> (<:.>) (Tagged 'Right) Binary a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) 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 (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Right) Binary a)
-> Store (Binary a) (Construction (Maybe <:*:> Maybe) a)
-> Store (Binary a) ((<:.>) (Tagged 'Right) Binary a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right P_Q_T (->) Store Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Store (Binary a) (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ Construction (Maybe <:*:> Maybe) a
tree

-------------------------------------- Non-empty binary tree ---------------------------------------

type instance Nonempty Binary = Construction (Maybe <:*:> Maybe)

instance Morphable (Into Binary) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Into Binary) (Construction (Maybe <:*:> Maybe)) = Binary
	morphing :: (<::>) (Tagged ('Into Binary)) (Construction (Maybe <:*:> Maybe)) a
-> Morphing ('Into Binary) (Construction (Maybe <:*:> Maybe)) a
morphing = Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> ((<::>)
      (Tagged ('Into Binary)) (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> (<::>)
     (Tagged ('Into Binary)) (Construction (Maybe <:*:> Maybe)) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Binary)) (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) 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) = (Exactly <:.:> Comparison > (:*:)) <:.:> Construction Wye > (->)
	-- morphing (premorph -> struct) = T_U <-- \(T_U (Exactly x :*: Convergence f)) ->
		-- let continue xs = run <--- morph @Insert @(Nonempty Binary) xs <---- twosome <--- Exactly x <--- Convergence f in
		-- let step = iff @Just <-|-|- (run .:.. view) <-*-*- mutate continue <-*-*- replace (leaf x) in
		-- order struct
			-- <---- step <--- sub @Left <--- struct
			-- <---- step <--- sub @Right <--- struct
			-- <---- f x <--- extract struct

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

instance Substructure Left (Construction (Maybe <:*:> Maybe)) where
	type Substance Left (Construction (Maybe <:*:> Maybe)) = Binary
	substructure :: Lens
  (Substance 'Left (Construction (Maybe <:*:> Maybe)))
  ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
  a
substructure = ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> P_Q_T
     (->)
     Store
     Binary
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
     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 (Maybe <:*:> Maybe)) a
  -> Store
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
       ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
 -> P_Q_T
      (->)
      Store
      Binary
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
      a)
-> ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
    -> Store
         (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
         ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> P_Q_T
     (->)
     Store
     Binary
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
struct -> case Tagged 'Left (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Left (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> Tagged 'Left (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
---> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
-> Tagged 'Left (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
struct of
		Construct a
x (T_U (Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing :*: Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. Maybe a
Nothing TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (Construction (Maybe <:*:> Maybe) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
left) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Just Construction (Maybe <:*:> Maybe) a
lst :*: Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. a -> Maybe a
Just Construction (Maybe <:*:> Maybe) a
lst) TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
left T_U
  Covariant
  Covariant
  (:*:)
  Maybe
  Maybe
  (Construction (Maybe <:*:> Maybe) a)
forall k k (ct :: k) (cu :: k) a. T_U ct cu (:*:) Maybe Maybe a
end (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing :*: Just Construction (Maybe <:*:> Maybe) a
rst)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. Maybe a
Nothing TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> a -> T_U ct cu (:*:) Maybe Maybe a
both (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction (Maybe <:*:> Maybe) a
rst) (Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
right Construction (Maybe <:*:> Maybe) a
rst) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Just Construction (Maybe <:*:> Maybe) a
lst :*: Just Construction (Maybe <:*:> Maybe) a
rst)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. a -> Maybe a
Just Construction (Maybe <:*:> Maybe) a
lst) TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Left) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> a -> T_U ct cu (:*:) Maybe Maybe a
both (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction (Maybe <:*:> Maybe) a
rst) (Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
right Construction (Maybe <:*:> Maybe) a
rst) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance Substructure Right (Construction (Maybe <:*:> Maybe)) where
	type Substance Right (Construction (Maybe <:*:> Maybe)) = Binary
	substructure :: Lens
  (Substance 'Right (Construction (Maybe <:*:> Maybe)))
  ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
  a
substructure = ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> P_Q_T
     (->)
     Store
     Binary
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
     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 (Maybe <:*:> Maybe)) a
  -> Store
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
       ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
 -> P_Q_T
      (->)
      Store
      Binary
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
      a)
-> ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
    -> Store
         (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
         ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> P_Q_T
     (->)
     Store
     Binary
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
struct -> case Tagged 'Right (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Right (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> Tagged 'Right (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
-> Tagged 'Right (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
struct of
		Construct a
x (T_U (Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing :*: Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. Maybe a
Nothing TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (Construction (Maybe <:*:> Maybe) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
right) (a :=> Nonempty Binary
forall a. a :=> Nonempty Binary
leaf a
x) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Just Construction (Maybe <:*:> Maybe) a
lst :*: Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. Maybe a
Nothing TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> a -> T_U ct cu (:*:) Maybe Maybe a
both Construction (Maybe <:*:> Maybe) a
lst) (Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
left Construction (Maybe <:*:> Maybe) a
lst) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Maybe (Construction (Maybe <:*:> Maybe) a)
Nothing :*: Just Construction (Maybe <:*:> Maybe) a
rst)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. a -> Maybe a
Just Construction (Maybe <:*:> Maybe) a
rst) TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
right T_U
  Covariant
  Covariant
  (:*:)
  Maybe
  Maybe
  (Construction (Maybe <:*:> Maybe) a)
forall k k (ct :: k) (cu :: k) a. T_U ct cu (:*:) Maybe Maybe a
end (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		Construct a
x (T_U (Just Construction (Maybe <:*:> Maybe) a
lst :*: Just Construction (Maybe <:*:> Maybe) a
rst)) -> (((:*:)
    (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
  :. (->)
       (TT
          Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
 > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall s a. (((:*:) s :. (->) s) > a) -> Store s a
Store ((((:*:)
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
   :. (->)
        (TT
           Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
  > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
 -> Store
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
      ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a))
-> (((:*:)
       (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     :. (->)
          (TT
             Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
    > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> Store
     (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
     ((<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe (Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT (Construction (Maybe <:*:> Maybe) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall a. a -> Maybe a
Just Construction (Maybe <:*:> Maybe) a
rst) TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> ((:*:)
      (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
    :. (->)
         (TT
            Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a))
   > (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall s a. s -> a -> s :*: a
:*: Construction (Maybe <:*:> Maybe) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) a
 -> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Construction (Maybe <:*:> Maybe) a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (<:.>) (Tagged 'Right) (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x (T_U
   Covariant
   Covariant
   (:*:)
   Maybe
   Maybe
   (Construction (Maybe <:*:> Maybe) a)
 -> Construction (Maybe <:*:> Maybe) a)
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Maybe
         Maybe
         (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
-> Maybe (Construction (Maybe <:*:> Maybe) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> a -> T_U ct cu (:*:) Maybe Maybe a
both Construction (Maybe <:*:> Maybe) a
lst) (Construction (Maybe <:*:> Maybe) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall k k a (ct :: k) (cu :: k).
a -> T_U ct cu (:*:) Maybe Maybe a
left Construction (Maybe <:*:> Maybe) a
lst) (Maybe (Construction (Maybe <:*:> Maybe) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Maybe
      Maybe
      (Construction (Maybe <:*:> Maybe) a))
-> (TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
    -> Maybe (Construction (Maybe <:*:> Maybe) a))
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Maybe
     Maybe
     (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> Maybe (Construction (Maybe <:*:> Maybe) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

-------------------------------------- Prefixed binary tree ----------------------------------------

instance Chain k => Morphable (Lookup Key) (Prefixed Binary k) where
	type Morphing (Lookup Key) (Prefixed Binary k) = (->) k <::> Maybe
	morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Morphing ('Lookup 'Key) (Prefixed Binary k) a
morphing (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
struct = case TT
  Covariant
  Covariant
  Maybe
  (Construction (Maybe <:*:> Maybe))
  (k :*: a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT
   Covariant
   Covariant
   Maybe
   (Construction (Maybe <:*:> Maybe))
   (k :*: a)
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> TT
         Covariant
         Covariant
         Maybe
         (Construction (Maybe <:*:> Maybe))
         (k :*: a))
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Prefixed Binary k a
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Prefixed Binary k a
 -> TT
      Covariant
      Covariant
      Maybe
      (Construction (Maybe <:*:> Maybe))
      (k :*: a))
-> ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
    -> Prefixed Binary k a)
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> Prefixed Binary k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph ((<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a))
-> (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<::>) (Tagged ('Lookup 'Key)) (Prefixed Binary k) a
struct of
		(Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
Nothing -> (((->) k :. Maybe) > a) -> TT Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT ((((->) k :. Maybe) > a)
 -> TT Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) > a)
-> TT Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \k
_ -> Maybe a
forall a. Maybe a
Nothing
		Just Construction (Maybe <:*:> Maybe) (k :*: a)
tree -> (((->) k :. Maybe) > a) -> TT Covariant Covariant ((->) k) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT ((((->) k :. Maybe) > a)
 -> TT Covariant Covariant ((->) k) Maybe a)
-> (((->) k :. Maybe) > a)
-> TT Covariant Covariant ((->) k) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \k
key ->
			k
key k -> k -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k) -> (k :*: a) -> k
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction (Maybe <:*:> Maybe) (k :*: a)
tree 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
				(Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a)
-> Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- 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) -> a) -> (k :*: a) -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> Construction (Maybe <:*:> Maybe) (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction (Maybe <:*:> Maybe) (k :*: a)
tree
				(Maybe a -> Maybe a -> Ordering -> Maybe a)
-> Maybe a -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- k -> Prefixed (Construction (Maybe <:*:> Maybe)) 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 (Maybe <:*:> Maybe)) k a -> Maybe a)
-> (Construction (Maybe <:*:> Maybe) (k :*: a)
    -> Prefixed (Construction (Maybe <:*:> Maybe)) k a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) (k :*: a)
-> Prefixed (Construction (Maybe <:*:> Maybe)) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) > a) -> Prefixed t k a
Prefixed (Construction (Maybe <:*:> Maybe) (k :*: a) -> Maybe a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a))
-> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT
  Covariant
  Covariant
  Maybe
  (Construction (Maybe <:*:> Maybe))
  (k :*: a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
 -> Construction (Maybe <:*:> Maybe) (k :*: a)
 -> TT
      Covariant
      Covariant
      Maybe
      (Construction (Maybe <:*:> Maybe))
      (k :*: a))
-> Lens
     Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (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
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (Construction (Maybe <:*:> Maybe) (k :*: a)
 -> TT
      Covariant
      Covariant
      Maybe
      (Construction (Maybe <:*:> Maybe))
      (k :*: a))
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) (k :*: a)
tree)
				(Maybe a -> Ordering -> Maybe a) -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- k -> Prefixed (Construction (Maybe <:*:> Maybe)) 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 (Maybe <:*:> Maybe)) k a -> Maybe a)
-> (Construction (Maybe <:*:> Maybe) (k :*: a)
    -> Prefixed (Construction (Maybe <:*:> Maybe)) k a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) (k :*: a)
-> Prefixed (Construction (Maybe <:*:> Maybe)) k a
forall (t :: * -> *) k a. ((t :. (:*:) k) > a) -> Prefixed t k a
Prefixed (Construction (Maybe <:*:> Maybe) (k :*: a) -> Maybe a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a))
-> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT
  Covariant
  Covariant
  Maybe
  (Construction (Maybe <:*:> Maybe))
  (k :*: a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) > (k :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
 -> Construction (Maybe <:*:> Maybe) (k :*: a)
 -> TT
      Covariant
      Covariant
      Maybe
      (Construction (Maybe <:*:> Maybe))
      (k :*: a))
-> Lens
     Binary (Construction (Maybe <:*:> Maybe) (k :*: a)) (k :*: a)
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (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
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (Construction (Maybe <:*:> Maybe) (k :*: a)
 -> TT
      Covariant
      Covariant
      Maybe
      (Construction (Maybe <:*:> Maybe))
      (k :*: a))
-> Construction (Maybe <:*:> Maybe) (k :*: a)
-> TT
     Covariant
     Covariant
     Maybe
     (Construction (Maybe <:*:> Maybe))
     (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) (k :*: a)
tree)

-- instance Chain k => Morphable (Vary Element) (Prefixed Binary k) where
	-- type Morphing (Vary Element) (Prefixed Binary k) = ((:*:) k <::> Exactly) <:.:> Prefixed Binary k > (->)
	-- morphing struct = case run . run . premorph ! struct of
		-- Nothing -> T_U ! \(TT (key :*: Exactly value)) -> Prefixed . lift . leaf ! key :*: value
		-- Just tree -> T_U ! \(TT (key :*: Exactly value)) ->
			-- let continue = ((vary @Element @k @_ @(Prefixed Binary _) key value -#=) -#=) in
			-- Prefixed . lift ! key <=> attached (extract tree) & order
				-- # over (sub @Root) (!!!>- value) tree
				-- # over (sub @Left) continue tree
				-- # over (sub @Right) continue tree

---------------------------------- Prefixed non-empty binary tree ----------------------------------

instance Chain key => Morphable (Lookup Key) (Prefixed < Construction (Maybe <:*:> Maybe) < key) where
	type Morphing (Lookup Key) (Prefixed < Construction (Maybe <:*:> Maybe) < key) = (->) key <::> Maybe
	morphing :: (<::>)
  (Tagged ('Lookup 'Key))
  ((Prefixed < Construction (Maybe <:*:> Maybe)) < key)
  a
-> Morphing
     ('Lookup 'Key)
     ((Prefixed < Construction (Maybe <:*:> Maybe)) < key)
     a
morphing ((<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a
-> Construction (Maybe <:*:> Maybe) (key :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a
 -> Construction (Maybe <:*:> Maybe) (key :*: a))
-> ((<::>)
      (Tagged ('Lookup 'Key))
      ((Prefixed < Construction (Maybe <:*:> Maybe)) < key)
      a
    -> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a)
-> (<::>)
     (Tagged ('Lookup 'Key))
     ((Prefixed < Construction (Maybe <:*:> Maybe)) < key)
     a
-> Construction (Maybe <:*:> Maybe) (key :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Lookup 'Key))
  ((Prefixed < Construction (Maybe <:*:> Maybe)) < key)
  a
-> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construct key :*: a
x ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
> (key :*: a)
xs) = (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') > a) -> TT ct ct' t t' a
TT ((((->) key :. Maybe) > a)
 -> TT Covariant Covariant ((->) key) Maybe a)
-> (((->) key :. Maybe) > a)
-> TT Covariant Covariant ((->) key) Maybe a
forall (m :: * -> * -> *) 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
			(Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a)
-> Maybe a -> Maybe a -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- 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
			(Maybe a -> Maybe a -> Ordering -> Maybe a)
-> Maybe a -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- key
-> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) 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 (Maybe <:*:> Maybe)) key a
 -> Maybe a)
-> (Construction (Maybe <:*:> Maybe) (key :*: a)
    -> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a)
-> Construction (Maybe <:*:> Maybe) (key :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) (key :*: a)
-> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) > a) -> Prefixed t k a
Prefixed (Construction (Maybe <:*:> Maybe) (key :*: a) -> Maybe a)
-> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe
   (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
   (Construction (Maybe <:*:> Maybe) (key :*: a))
 -> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     > (key :*: a))
 -> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)))
-> Lens
     Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
      > (key :*: a))
     (Construction (Maybe <:*:> Maybe) (key :*: a))
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
-> Maybe (Construction (Maybe <:*:> Maybe) (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
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
  > (key :*: a))
 -> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)))
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
-> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
> (key :*: a)
xs
			(Maybe a -> Ordering -> Maybe a) -> Maybe a -> Ordering -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- key
-> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) 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 (Maybe <:*:> Maybe)) key a
 -> Maybe a)
-> (Construction (Maybe <:*:> Maybe) (key :*: a)
    -> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a)
-> Construction (Maybe <:*:> Maybe) (key :*: a)
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) (key :*: a)
-> (<) (Prefixed < Construction (Maybe <:*:> Maybe)) key a
forall (t :: * -> *) k a. ((t :. (:*:) k) > a) -> Prefixed t k a
Prefixed (Construction (Maybe <:*:> Maybe) (key :*: a) -> Maybe a)
-> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< forall e r. Gettable (Obscure Lens) => Getting (Obscure Lens) e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @(Obscure Lens) (Lens
   Maybe
   (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
   (Construction (Maybe <:*:> Maybe) (key :*: a))
 -> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     > (key :*: a))
 -> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)))
-> Lens
     Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
      > (key :*: a))
     (Construction (Maybe <:*:> Maybe) (key :*: a))
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
-> Maybe (Construction (Maybe <:*:> Maybe) (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
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
  > (key :*: a))
 -> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a)))
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    > (key :*: a))
-> Maybe (Construction (Maybe <:*:> Maybe) (key :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
> (key :*: a)
xs

-------------------------------------- Zipper of binary tree ---------------------------------------
	{-
data Biforked a = Top | Horizontal (Horizontal a)

instance Covariant (->) (->) Biforked where
	_ <-|- Top = Top
	f <-|- Horizontal (Leftward l) = Horizontal . Leftward <-- f l
	f <-|- Horizontal (Rightward r) = Horizontal . Rightward <-- f r

instance Traversable (->) (->) Biforked where
	_ <<- Top = point Top
	f <<- Horizontal (Leftward l) = Horizontal . Leftward <-|- f l
	f <<- Horizontal (Rightward r) = Horizontal . Rightward <-|- f r

type Bifurcation = Biforked <::> Construction Biforked

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

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

_focused_part_to_nonempty_binary_tree :: (Exactly <:.:> Wye <::> Construction Wye > (:*:)) ~> Construction Wye
_focused_part_to_nonempty_binary_tree (T_U (Exactly x :*: xs)) = Construct x <-- run xs

instance Morphable (Rotate Up) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:)) where
	type Morphing (Rotate Up) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:))
		= Maybe <::> ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> Bifurcation <::> Bicursor > (:*:))
	morphing struct = case run ---> premorph struct of
		focused :*: TT (TT (Horizontal (Rightward (Construct (T_U (Exactly parent :*: rest)) next)))) ->
			lift . (twosome % TT (TT next)) . twosome (Exactly parent) . TT <---- resolve
				<--- Both <-- _focused_part_to_nonempty_binary_tree focused
				<--- Left <-- _focused_part_to_nonempty_binary_tree focused
				<--- run rest
		focused :*: TT (TT (Horizontal (Leftward (Construct (T_U (Exactly parent :*: rest)) next)))) ->
			lift . (twosome % TT (TT next)) . twosome (Exactly parent) . TT <---- resolve
				<--- Both % _focused_part_to_nonempty_binary_tree focused
				<--- Right <-- _focused_part_to_nonempty_binary_tree focused
				<--- run rest
		_ -> TT Nothing

_nonempty_binary_tree_to_focused_part :: Construction Wye ~> Exactly <:.:> Wye <::> Construction Wye > (:*:)
_nonempty_binary_tree_to_focused_part (Construct x xs) = twosome <--- Exactly x <--- TT xs

instance Morphable (Rotate > Down Left) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:)) where
	type Morphing (Rotate > Down Left) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:))
		= Maybe <::> ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> Bifurcation <::> Bicursor > (:*:))
	morphing struct = case run ---> premorph struct of
		T_U (Exactly x :*: TT (Left lst)) :*: TT (TT next) ->
			lift . twosome (_nonempty_binary_tree_to_focused_part lst)
				. TT . TT . Horizontal . Leftward <---- Construct 
					<--- twosome <-- Exactly x <-- TT Nothing 
					<--- next
		T_U (Exactly x :*: TT (Both lst rst)) :*: TT (TT next) ->
			lift . twosome (_nonempty_binary_tree_to_focused_part lst)
				. TT . TT . Horizontal . Leftward <---- Construct
					<--- twosome <-- Exactly x <-- lift rst 
					<--- next
		_ -> TT Nothing

instance Morphable (Rotate > Down Right) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:)) where
	type Morphing (Rotate > Down Right) ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> (Bifurcation <::> Bicursor) > (:*:))
		= Maybe <::> ((Exactly <:.:> Wye <::> Construction Wye > (:*:)) <:.:> Bifurcation <::> Bicursor > (:*:))
	morphing struct = case run ---> premorph struct of
		T_U (Exactly x :*: TT (Right rst)) :*: TT (TT next) ->
			lift . twosome (_nonempty_binary_tree_to_focused_part rst)
				. TT . TT . Horizontal . Rightward <---- Construct (twosome <--- Exactly x <--- TT Nothing) next
		T_U (Exactly x :*: TT (Both lst rst)) :*: TT (TT next) ->
			lift . twosome (_nonempty_binary_tree_to_focused_part rst)
				. TT . TT . Horizontal . Rightward <---- Construct (twosome <--- Exactly x <--- lift lst) next
		_ -> TT Nothing
-}

leaf :: a :=> Nonempty Binary
leaf :: a :=> Nonempty Binary
leaf a
x = a
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) > a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) > a) -> Construction t a
Construct a
x ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) > a
forall k k (ct :: k) (cu :: k) a. T_U ct cu (:*:) Maybe Maybe a
end

left :: a -> T_U ct cu (:*:) Maybe Maybe a
left a
x = (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe 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 ((Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a)
-> (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a -> Maybe a -> Maybe a :*: Maybe a
forall s a. s -> a -> s :*: a
:*: Maybe a
forall a. Maybe a
Nothing
right :: a -> T_U ct cu (:*:) Maybe Maybe a
right a
x = (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe 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 ((Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a)
-> (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe a
forall a. Maybe a
Nothing Maybe a -> Maybe a -> Maybe a :*: Maybe a
forall s a. s -> a -> s :*: a
:*: a -> Maybe a
forall a. a -> Maybe a
Just a
x
both :: a -> a -> T_U ct cu (:*:) Maybe Maybe a
both a
x a
y = (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe 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 ((Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a)
-> (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a -> Maybe a -> Maybe a :*: Maybe a
forall s a. s -> a -> s :*: a
:*: a -> Maybe a
forall a. a -> Maybe a
Just a
y
end :: T_U ct cu (:*:) Maybe Maybe a
end = (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe 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 ((Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a)
-> (Maybe a :*: Maybe a) -> T_U ct cu (:*:) Maybe Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Maybe a
forall a. Maybe a
Nothing Maybe a -> Maybe a -> Maybe a :*: Maybe a
forall s a. s -> a -> s :*: a
:*: Maybe a
forall a. Maybe a
Nothing