{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Ability.Substructure where

import Pandora.Core.Interpreted (run, unite, (<~), (=#-))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|-|-)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (type (@>>>), view, replace)
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic.Functor ((>-||-), extract, empty)
import Pandora.Paradigm.Primary.Auxiliary (Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.TT (type (<::>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))

type Substructured segment source target = (Substructure segment source, Substance segment source ~ target)

class Substructure segment (structure :: * -> *) where
	type Substance segment structure :: * -> *
	substructure :: (Tagged segment <:.> structure) @>>> Substance segment structure

	sub :: (Covariant (->) (->) structure) => structure @>>> Substance segment structure
	sub = (structure a -> TU Covariant Covariant (Tagged segment) structure a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (structure a
 -> TU Covariant Covariant (Tagged segment) structure a)
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store (Substance segment structure a) (structure a))
-> structure a
-> Store (Substance segment structure a) (structure a)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Contravariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p b c) (p a c)
>-||-) ((TU Covariant Covariant (Tagged segment) structure a
  -> Store (Substance segment structure a) (structure a))
 -> structure a
 -> Store (Substance segment structure a) (structure a))
-> ((TU Covariant Covariant (Tagged segment) structure a
     -> Store
          (Substance segment structure a)
          (TU Covariant Covariant (Tagged segment) structure a))
    -> TU Covariant Covariant (Tagged segment) structure a
    -> Store (Substance segment structure a) (structure a))
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store
         (Substance segment structure a)
         (TU Covariant Covariant (Tagged segment) structure a))
-> structure a
-> Store (Substance segment structure a) (structure a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *) a.
(Lowerable (->) t, Covariant (->) (->) u) =>
t u a -> u a
lower @(->) (TU Covariant Covariant (Tagged segment) structure a
 -> structure a)
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store
         (Substance segment structure a)
         (TU Covariant Covariant (Tagged segment) structure a))
-> TU Covariant Covariant (Tagged segment) structure a
-> Store (Substance segment structure a) (structure a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|-) (Primary
   (P_Q_T
      (->)
      Store
      (Substance segment structure)
      (TU Covariant Covariant (Tagged segment) structure a))
   a
 -> Primary
      (P_Q_T (->) Store (Substance segment structure) (structure a)) a)
-> ((->)
    < P_Q_T
        (->)
        Store
        (Substance segment structure)
        (TU Covariant Covariant (Tagged segment) structure a)
        a)
   < P_Q_T (->) Store (Substance segment structure) (structure a) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- Substructure segment structure =>
(Tagged segment <:.> structure) @>>> Substance segment structure
forall k (segment :: k) (structure :: * -> *).
Substructure segment structure =>
(Tagged segment <:.> structure) @>>> Substance segment structure
substructure @segment @structure

tagstruct :: Covariant (->) (->) structure => (Tagged segment <:.> structure) @>>> structure
tagstruct :: (Tagged segment <:.> structure) @>>> structure
tagstruct = ((<:.>) (Tagged segment) structure a
 -> Store (structure a) ((<:.>) (Tagged segment) structure a))
-> P_Q_T
     (->) Store structure ((<:.>) (Tagged segment) structure 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 segment) structure a
  -> Store (structure a) ((<:.>) (Tagged segment) structure a))
 -> P_Q_T
      (->) Store structure ((<:.>) (Tagged segment) structure a) a)
-> ((<:.>) (Tagged segment) structure a
    -> Store (structure a) ((<:.>) (Tagged segment) structure a))
-> P_Q_T
     (->) Store structure ((<:.>) (Tagged segment) structure a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (((:*:) (structure a) :. (->) (structure a))
 >>> (<:.>) (Tagged segment) structure a)
-> Store (structure a) ((<:.>) (Tagged segment) structure a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (structure a) :. (->) (structure a))
  >>> (<:.>) (Tagged segment) structure a)
 -> Store (structure a) ((<:.>) (Tagged segment) structure a))
-> ((<:.>) (Tagged segment) structure a
    -> ((:*:) (structure a) :. (->) (structure a))
       >>> (<:.>) (Tagged segment) structure a)
-> (<:.>) (Tagged segment) structure a
-> Store (structure a) ((<:.>) (Tagged segment) structure a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (structure a
-> (structure a -> (<:.>) (Tagged segment) structure a)
-> ((:*:) (structure a) :. (->) (structure a))
   >>> (<:.>) (Tagged segment) structure a
forall s a. s -> a -> s :*: a
:*: structure a -> (<:.>) (Tagged segment) structure a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift) (structure a
 -> ((:*:) (structure a) :. (->) (structure a))
    >>> (<:.>) (Tagged segment) structure a)
-> ((<:.>) (Tagged segment) structure a -> structure a)
-> (<:.>) (Tagged segment) structure a
-> ((:*:) (structure a) :. (->) (structure a))
   >>> (<:.>) (Tagged segment) structure a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged segment) structure a -> structure a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower

instance (Covariant (->) (->) t, Covariant (->) (->) u) => Substructure Left (t <:*:> u) where
	type Substance Left (t <:*:> u) = t
	substructure :: Lens
  (Substance 'Left (t <:*:> u))
  ((<:.>) (Tagged 'Left) (t <:*:> u) a)
  a
substructure = ((<:.>) (Tagged 'Left) (t <:*:> u) a
 -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) 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) (t <:*:> u) a
  -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
 -> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) a) a)
-> ((<:.>) (Tagged 'Left) (t <:*:> u) a
    -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> P_Q_T (->) Store t ((<:.>) (Tagged 'Left) (t <:*:> u) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Left) (t <:*:> u) a
x -> case T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U Covariant Covariant (:*:) t u a -> t a :*: u a)
-> T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Left) (t <:*:> u) a
-> T_U Covariant Covariant (:*:) t u a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (t <:*:> u) a
x of
		t a
ls :*: u a
rs -> (((:*:) (t a) :. (->) (t a))
 >>> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (t a) :. (->) (t a))
  >>> (<:.>) (Tagged 'Left) (t <:*:> u) a)
 -> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a))
-> (((:*:) (t a) :. (->) (t a))
    >>> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> Store (t a) ((<:.>) (Tagged 'Left) (t <:*:> u) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t a
ls t a
-> (t a -> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> ((:*:) (t a) :. (->) (t a))
   >>> (<:.>) (Tagged 'Left) (t <:*:> u) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t u a
-> (<:.>) (Tagged 'Left) (t <:*:> u) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t u a
 -> (<:.>) (Tagged 'Left) (t <:*:> u) a)
-> (t a -> T_U Covariant Covariant (:*:) t u a)
-> t a
-> (<:.>) (Tagged 'Left) (t <:*:> u) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> u a -> T_U Covariant Covariant (:*:) t u a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> u a
rs)

instance (Covariant (->) (->) t, Covariant (->) (->) u) => Substructure Right (t <:*:> u) where
	type Substance Right (t <:*:> u) = u
	substructure :: Lens
  (Substance 'Right (t <:*:> u))
  ((<:.>) (Tagged 'Right) (t <:*:> u) a)
  a
substructure = ((<:.>) (Tagged 'Right) (t <:*:> u) a
 -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) 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) (t <:*:> u) a
  -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
 -> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) a) a)
-> ((<:.>) (Tagged 'Right) (t <:*:> u) a
    -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> P_Q_T (->) Store u ((<:.>) (Tagged 'Right) (t <:*:> u) a) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Right) (t <:*:> u) a
x -> case T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U Covariant Covariant (:*:) t u a -> t a :*: u a)
-> T_U Covariant Covariant (:*:) t u a -> t a :*: u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Right) (t <:*:> u) a
-> T_U Covariant Covariant (:*:) t u a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) (t <:*:> u) a
x of
		t a
ls :*: u a
rs -> (((:*:) (u a) :. (->) (u a))
 >>> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (u a) :. (->) (u a))
  >>> (<:.>) (Tagged 'Right) (t <:*:> u) a)
 -> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a))
-> (((:*:) (u a) :. (->) (u a))
    >>> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> Store (u a) ((<:.>) (Tagged 'Right) (t <:*:> u) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- u a
rs u a
-> (u a -> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> ((:*:) (u a) :. (->) (u a))
   >>> (<:.>) (Tagged 'Right) (t <:*:> u) a
forall s a. s -> a -> s :*: a
:*: T_U Covariant Covariant (:*:) t u a
-> (<:.>) (Tagged 'Right) (t <:*:> u) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U Covariant Covariant (:*:) t u a
 -> (<:.>) (Tagged 'Right) (t <:*:> u) a)
-> (u a -> T_U Covariant Covariant (:*:) t u a)
-> u a
-> (<:.>) (Tagged 'Right) (t <:*:> u) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a
ls t a -> u a -> T_U Covariant Covariant (:*:) t u a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>)

data Segment a = Tree a | Root a | Rest a | Branch a | Ancestors a | Children a | Siblings a | Forest a | Medium a

data Location a = Focused a

instance Covariant (->) (->) t => Substructure Root (Exactly <:*:> t) where
	type Substance Root (Exactly <:*:> t) = Exactly
	substructure :: Lens
  (Substance 'Root (Exactly <:*:> t))
  ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a)
  a
substructure = ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly t a)
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a))
-> (<:.>) (Tagged 'Root) (Exactly <:*:> t) a
-> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Contravariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p b c) (p a c)
>-||-) ((T_U Covariant Covariant (:*:) Exactly t a
  -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a))
 -> (<:.>) (Tagged 'Root) (Exactly <:*:> t) a
 -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a))
-> ((T_U Covariant Covariant (:*:) Exactly t a
     -> Store (Exactly a) (T_U Covariant Covariant (:*:) Exactly t a))
    -> T_U Covariant Covariant (:*:) Exactly t a
    -> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a))
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (Exactly a) (T_U Covariant Covariant (:*:) Exactly t a))
-> (<:.>) (Tagged 'Root) (Exactly <:*:> t) a
-> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) 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 @(->) (T_U Covariant Covariant (:*:) Exactly t a
 -> (<:.>) (Tagged 'Root) (Exactly <:*:> t) a)
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (Exactly a) (T_U Covariant Covariant (:*:) Exactly t a))
-> T_U Covariant Covariant (:*:) Exactly t a
-> Store (Exactly a) ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|-) (Primary
   (P_Q_T
      (->) Store Exactly (T_U Covariant Covariant (:*:) Exactly t a))
   a
 -> Primary
      (P_Q_T
         (->) Store Exactly ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a))
      a)
-> ((->)
    < P_Q_T
        (->) Store Exactly (T_U Covariant Covariant (:*:) Exactly t a) a)
   < P_Q_T
       (->) Store Exactly ((<:.>) (Tagged 'Root) (Exactly <:*:> t) a) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u 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

instance Covariant (->) (->) t => Substructure Rest (Exactly <:*:> t) where
	type Substance Rest (Exactly <:*:> t) = t
	substructure :: Lens
  (Substance 'Rest (Exactly <:*:> t))
  ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a)
  a
substructure = ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly t a)
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a))
-> (<:.>) (Tagged 'Rest) (Exactly <:*:> t) a
-> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Contravariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p b c) (p a c)
>-||-) ((T_U Covariant Covariant (:*:) Exactly t a
  -> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a))
 -> (<:.>) (Tagged 'Rest) (Exactly <:*:> t) a
 -> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a))
-> ((T_U Covariant Covariant (:*:) Exactly t a
     -> Store (t a) (T_U Covariant Covariant (:*:) Exactly t a))
    -> T_U Covariant Covariant (:*:) Exactly t a
    -> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a))
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (t a) (T_U Covariant Covariant (:*:) Exactly t a))
-> (<:.>) (Tagged 'Rest) (Exactly <:*:> t) a
-> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) 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 @(->) (T_U Covariant Covariant (:*:) Exactly t a
 -> (<:.>) (Tagged 'Rest) (Exactly <:*:> t) a)
-> (T_U Covariant Covariant (:*:) Exactly t a
    -> Store (t a) (T_U Covariant Covariant (:*:) Exactly t a))
-> T_U Covariant Covariant (:*:) Exactly t a
-> Store (t a) ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|-) (Primary
   (P_Q_T (->) Store t (T_U Covariant Covariant (:*:) Exactly t a)) a
 -> Primary
      (P_Q_T (->) Store t ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a)) a)
-> ((->)
    < P_Q_T (->) Store t (T_U Covariant Covariant (:*:) Exactly t a) a)
   < P_Q_T (->) Store t ((<:.>) (Tagged 'Rest) (Exactly <:*:> t) a) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u 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

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

instance (Covariant (->) (->) t, Substructure i t) => Substructure (i Branch) (Construction t) where
	type Substance (i Branch) (Construction t) = Substance i t <::> Construction t
	substructure :: Lens
  (Substance (i 'Branch) (Construction t))
  ((<:.>) (Tagged (i 'Branch)) (Construction t) a)
  a
substructure = ((<:.>) (Tagged (i 'Branch)) (Construction t) a
 -> Store
      ((<::>) (Substance i t) (Construction t) a)
      ((<:.>) (Tagged (i 'Branch)) (Construction t) a))
-> P_Q_T
     (->)
     Store
     (Substance i t <::> Construction t)
     ((<:.>) (Tagged (i 'Branch)) (Construction t) 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 (i 'Branch)) (Construction t) a
  -> Store
       ((<::>) (Substance i t) (Construction t) a)
       ((<:.>) (Tagged (i 'Branch)) (Construction t) a))
 -> P_Q_T
      (->)
      Store
      (Substance i t <::> Construction t)
      ((<:.>) (Tagged (i 'Branch)) (Construction t) a)
      a)
-> ((<:.>) (Tagged (i 'Branch)) (Construction t) a
    -> Store
         ((<::>) (Substance i t) (Construction t) a)
         ((<:.>) (Tagged (i 'Branch)) (Construction t) a))
-> P_Q_T
     (->)
     Store
     (Substance i t <::> Construction t)
     ((<:.>) (Tagged (i 'Branch)) (Construction t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged (i 'Branch)) (Construction t) a
source -> case (<:.>) (Tagged (i 'Branch)) (Construction t) a -> Construction t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged (i 'Branch)) (Construction t) a
source of
		Construct a
x (t :. Construction t) >>> a
xs -> (((:*:) ((<::>) (Substance i t) (Construction t) a)
  :. (->) ((<::>) (Substance i t) (Construction t) a))
 >>> (<:.>) (Tagged (i 'Branch)) (Construction t) a)
-> Store
     ((<::>) (Substance i t) (Construction t) a)
     ((<:.>) (Tagged (i 'Branch)) (Construction t) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) ((<::>) (Substance i t) (Construction t) a)
   :. (->) ((<::>) (Substance i t) (Construction t) a))
  >>> (<:.>) (Tagged (i 'Branch)) (Construction t) a)
 -> Store
      ((<::>) (Substance i t) (Construction t) a)
      ((<:.>) (Tagged (i 'Branch)) (Construction t) a))
-> (((:*:) ((<::>) (Substance i t) (Construction t) a)
     :. (->) ((<::>) (Substance i t) (Construction t) a))
    >>> (<:.>) (Tagged (i 'Branch)) (Construction t) a)
-> Store
     ((<::>) (Substance i t) (Construction t) a)
     ((<:.>) (Tagged (i 'Branch)) (Construction t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Substance i t :. Construction t) >>> a)
-> (<::>) (Substance i t) (Construction t) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (Lens
  (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
-> ((t :. Construction t) >>> a)
-> (Substance i t :. Construction t) >>> a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
   (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
 -> ((t :. Construction t) >>> a)
 -> (Substance i t :. Construction t) >>> a)
-> Lens
     (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
-> ((t :. Construction t) >>> a)
-> (Substance i t :. Construction t) >>> 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 i structure, Covariant (->) (->) structure) =>
structure @>>> Substance i structure
sub @i (((t :. Construction t) >>> a)
 -> (Substance i t :. Construction t) >>> a)
-> ((t :. Construction t) >>> a)
-> (Substance i t :. Construction t) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (t :. Construction t) >>> a
xs) (<::>) (Substance i t) (Construction t) a
-> ((<::>) (Substance i t) (Construction t) a
    -> (<:.>) (Tagged (i 'Branch)) (Construction t) a)
-> ((:*:) ((<::>) (Substance i t) (Construction t) a)
    :. (->) ((<::>) (Substance i t) (Construction t) a))
   >>> (<:.>) (Tagged (i 'Branch)) (Construction t) a
forall s a. s -> a -> s :*: a
:*: \(<::>) (Substance i t) (Construction t) a
target ->
			Construction t a -> (<:.>) (Tagged (i 'Branch)) (Construction t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction t a
 -> (<:.>) (Tagged (i 'Branch)) (Construction t) a)
-> Construction t a
-> (<:.>) (Tagged (i 'Branch)) (Construction t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> ((t :. Construction t) >>> a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (((t :. Construction t) >>> a) -> Construction t a)
-> ((t :. Construction t) >>> a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Substance i t :. Construction t) >>> a)
-> Lens
     (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
-> ((t :. Construction t) >>> a)
-> (t :. Construction t) >>> a
forall (i :: * -> *) source target.
i target -> Lens i source target -> source -> source
replace (((Substance i t :. Construction t) >>> a)
 -> Lens
      (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
 -> ((t :. Construction t) >>> a)
 -> (t :. Construction t) >>> a)
-> ((Substance i t :. Construction t) >>> a)
-> Lens
     (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
-> ((t :. Construction t) >>> a)
-> (t :. Construction t) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<::>) (Substance i t) (Construction t) a
-> (Substance i t :. Construction t) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (<::>) (Substance i t) (Construction t) a
target (Lens
   (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
 -> ((t :. Construction t) >>> a) -> (t :. Construction t) >>> a)
-> Lens
     (Substance i t) ((t :. Construction t) >>> a) (Construction t a)
-> ((t :. Construction t) >>> a)
-> (t :. Construction t) >>> 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 i structure, Covariant (->) (->) structure) =>
structure @>>> Substance i structure
sub @i (((t :. Construction t) >>> a) -> (t :. Construction t) >>> a)
-> ((t :. Construction t) >>> a) -> (t :. Construction t) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (t :. Construction t) >>> a
xs

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