diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -437,6 +437,26 @@
 * Remove `Focusable` ability if favor of `Structure` typeclass
 * Define `<$$`, `<$$$`, `<$$$$`, `$$>`, `$$$>`, `$$$$>` infix operators in `Covariant` typeclass
 * Define `<$||=`, `<$$||=`, `<$$$||=`, `<$$$$||=` infix operators in `Interpreted` typeclass
-* Define `=||$>`, =||$$>`, `=||$$$>`, `=||$$$$>` infix operators in `Interpreted` typeclass
+* Define `=||$>`, `=||$$>`, `=||$$$>`, `=||$$$$>` infix operators in `Interpreted` typeclass
 
 # 0.4.2
+* Rename `>-<` method of `Invariant` typeclass to `<$<`
+* Define `P_T` joint schema exclusively for `Prism` type
+* Define `Prism` type and its `preview` method
+* Redefine `Lens` type as `Optics` on `Identity`
+* Define `#=@` type operator as synonymous for `Optics`
+* Redefine `Substructure` typeclass with polymorphic `Optics`
+* Generalize optical `view`, `set`, `over` methods
+* Change `Substructured` constraint type according to new `Substructure` definition
+* Define `:::` - type operator for almost anything higher kinded
+* Redefine `Zipper` - add possible moves to type definition
+* Define experimental `Fastenable` type family to have it as `Constraint`
+* Remove `:~.` type operator in `Optics` module
+* Rename `Optics` type synonymous to `Lens`
+* Define `PTU` joint schema
+* Define `P_Q_T` joint schema
+* Redefine `Lens` type synonymous and use `P_Q_T` joint schema
+* Define `Convex` and `Obscure` type families for `Lens`
+* Change `Substructured` constraint - add paramater for `Available`
+* Define experimental `Impliable` typeclass
+* Remove `:-.` type operator in `Optics` module
diff --git a/Pandora/Core.hs b/Pandora/Core.hs
--- a/Pandora/Core.hs
+++ b/Pandora/Core.hs
@@ -1,3 +1,4 @@
 module Pandora.Core (module Exports) where
 
+import Pandora.Core.Impliable as Exports
 import Pandora.Core.Functor as Exports
diff --git a/Pandora/Core/Functor.hs b/Pandora/Core/Functor.hs
--- a/Pandora/Core/Functor.hs
+++ b/Pandora/Core/Functor.hs
@@ -3,6 +3,7 @@
 infixr 0 :=, <:=, :=>, :=:=>, ~>
 infixr 1 .:, :.
 infixr 2 ::|:., ::|.:, ::|::
+infixr 9 :::
 
 -- | Parameter application
 type (:=) t a = t a
@@ -29,3 +30,6 @@
 type (::|:.) p a b = p (p a b) b
 type (::|.:) p a b = p a (p a b)
 type (::|::) p a b = p (p a b) (p a b)
+
+-- Type operator for anything higher kinded
+data (:::) t u :: k -> k' -> *
diff --git a/Pandora/Core/Impliable.hs b/Pandora/Core/Impliable.hs
new file mode 100644
--- /dev/null
+++ b/Pandora/Core/Impliable.hs
@@ -0,0 +1,5 @@
+module Pandora.Core.Impliable where
+
+class Impliable result where
+	type Arguments result = args | args -> result
+	imply :: Arguments result
diff --git a/Pandora/Paradigm/Inventory.hs b/Pandora/Paradigm/Inventory.hs
--- a/Pandora/Paradigm/Inventory.hs
+++ b/Pandora/Paradigm/Inventory.hs
@@ -13,10 +13,12 @@
 
 import Pandora.Core.Functor (type (~>))
 import Pandora.Pattern.Category ((.), ($), (#), identity)
+import Pandora.Pattern.Functor.Covariant (Covariant)
 import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
 import Pandora.Pattern.Functor.Extractable (extract)
 import Pandora.Pattern.Functor.Bivariant ((<->))
 import Pandora.Paradigm.Primary.Functor.Function ((!), (%))
+import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
 import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
 import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
 import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt)
@@ -36,14 +38,14 @@
 	x -| f = Environment $ x -| f . Equipment
 	x |- g = run x |- run . g
 
-zoom :: Stateful bg t => Lens bg ls -> State ls ~> t
-zoom lens less = let restruct f v = f <-> identity $ run less v
+zoom :: Stateful bg t => Lens Identity bg ls -> State ls ~> t
+zoom lens less = let restruct to = (to . Identity <-> identity) . run less . extract @Identity
 	in adapt . State $ (|- restruct) . run . run lens
 
-(=<>) :: Stateful src t => src :-. tgt -> tgt -> t src
+(=<>) :: Stateful src t => Lens mode src tgt -> mode tgt -> t src
 lens =<> new = modify $ set lens new
 
-(~<>) :: Stateful src t => src :-. tgt -> (tgt -> tgt) -> t src
+(~<>) :: Covariant mode => Stateful src t => Lens mode src tgt -> (mode tgt -> mode tgt) -> t src
 lens ~<> f = modify $ over lens f
 
 magnify :: forall bg ls t . (Accessible ls bg, Stateful bg t) => t ls
diff --git a/Pandora/Paradigm/Inventory/Optics.hs b/Pandora/Paradigm/Inventory/Optics.hs
--- a/Pandora/Paradigm/Inventory/Optics.hs
+++ b/Pandora/Paradigm/Inventory/Optics.hs
@@ -2,44 +2,73 @@
 
 module Pandora.Paradigm.Inventory.Optics where
 
-import Pandora.Pattern.Category (Category (identity, (.), ($)))
-import Pandora.Pattern.Functor.Covariant ((<$))
+import Pandora.Core.Impliable (Impliable (Arguments, imply))
+import Pandora.Pattern.Category (Category (identity, (.), ($), (#)))
+import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$)))
 import Pandora.Pattern.Functor.Extractable (Extractable (extract))
+import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
+import Pandora.Pattern.Functor.Divariant ((>->))
 import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
 import Pandora.Pattern.Object.Setoid (Setoid ((==)))
-import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (run))
+import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
+import Pandora.Paradigm.Primary.Functor.Function ((!), (%))
+import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
 import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
+import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
 import Pandora.Paradigm.Primary.Object.Boolean ((?))
 import Pandora.Paradigm.Inventory.Store (Store (Store), position, look, retrofit)
-import Pandora.Paradigm.Schemes.PQ_ (PQ_ (PQ_))
+import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
+import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)
 
-infixr 0 :-.
-infixr 0 :~.
+infixl 2 #=@
 
-type (:-.) src tgt = Lens src tgt
+type Lens = P_Q_T (->) Store
 
--- Reference to taret within some source
-type Lens = PQ_ (->) Store
+instance Invariant (Flip (Lens available) tgt) where
+	f <$< g = \(Flip (P_Q_T lens)) -> Flip . P_Q_T $ g >-> (f <$>) $ lens
 
-instance Category Lens where
-	identity = PQ_ $ \src -> Store $ src :*: identity
-	PQ_ to . PQ_ from = PQ_ $ \src -> src <$ (to . position $ from src)
+type family Convex lens where
+	Convex Lens = Lens Identity
 
+instance Category (Lens Identity) where
+	identity = imply @(Convex Lens _ _) identity ((%) (!))
+	P_Q_T to . P_Q_T from = P_Q_T $ \source -> source <$ (to . extract @Identity . position $ from source)
+
+instance Impliable (P_Q_T (->) Store Identity source target) where
+	type Arguments (P_Q_T (->) Store Identity source target) =
+		(source -> target) -> (source -> target -> source) -> Lens Identity source target
+	imply getter setter = P_Q_T $ \source -> Store $ Identity # getter source :*: setter source . extract
+
+type family Obscure lens where
+	Obscure Lens = Lens Maybe
+
+instance Impliable (P_Q_T (->) Store Maybe source target) where
+	type Arguments (P_Q_T (->) Store Maybe source target) =
+		(source -> Maybe target) -> (source -> Maybe target -> source) -> Lens Maybe source target
+	imply getter setter = P_Q_T $ \source -> Store $ getter source :*: setter source
+
+instance Category (Lens Maybe) where
+	identity = imply @(Obscure Lens _ _) # Just # resolve identity
+	P_Q_T to . P_Q_T from = P_Q_T $ \source -> case position # from source of
+		Nothing -> Store $ Nothing :*: (source !)
+		Just between -> source <$ to between
+
 -- Lens as natural transformation
-type (:~.) src tgt = forall a . Lens (src a) (tgt a)
+type (#=@) source target available = forall a . Lens available (source a) (target a)
 
--- | Get the target of a lens
-view :: Lens src tgt -> src -> tgt
-view lens = position . run lens
+-- | Get focused target value
+view :: Lens available source target -> source -> available target
+view lens = position @_ @(Store _) . run lens
 
--- | Replace the target of a lens
-set :: Lens src tgt -> tgt -> src -> src
+-- Replace focused target value with new value
+set :: Lens available source target -> available target -> source -> source
 set lens new = look new . run lens
 
--- | Modify the target of a lens
-over :: Lens src tgt -> (tgt -> tgt) -> src -> src
+-- | Modify focused target value
+over :: Covariant available => Lens available source target -> (available target -> available target) -> source -> source
 over lens f = extract . retrofit f . run lens
 
 -- | Representable based lens
-represent :: (Representable t, Setoid (Representation t)) => Representation t -> t a :-. a
-represent r = PQ_ $ \x -> Store $ r <#> x :*: \new -> tabulate (\r' -> r' == r ? new $ r' <#> x)
+represent :: forall t a . (Representable t, Setoid (Representation t)) => Representation t -> Convex Lens (t a) a
+represent r = imply @(Convex Lens (t a) a) (r <#>) (\source target -> tabulate $ \r' -> r' == r ? target $ r' <#> source)
diff --git a/Pandora/Paradigm/Inventory/State.hs b/Pandora/Paradigm/Inventory/State.hs
--- a/Pandora/Paradigm/Inventory/State.hs
+++ b/Pandora/Paradigm/Inventory/State.hs
@@ -5,6 +5,7 @@
 import Pandora.Core.Functor (type (:.), type (:=))
 import Pandora.Pattern.Category (identity, (.), ($))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
+import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
 import Pandora.Pattern.Functor.Pointable (Pointable (point))
 import Pandora.Pattern.Functor.Applicative (Applicative ((<*>), (*>)))
 import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
@@ -12,8 +13,10 @@
 import Pandora.Pattern.Functor.Monad (Monad)
 import Pandora.Pattern.Functor.Adjoint ((-|), (|-), ($|-))
 import Pandora.Pattern.Functor.Bivariant ((<->))
+import Pandora.Pattern.Functor.Divariant ((>->))
+import Pandora.Paradigm.Primary.Transformer (Flip)
 import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
-import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite), Schematic)
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (||=)), Schematic)
 import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
 import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>))
 import Pandora.Paradigm.Primary.Functor (Product ((:*:)), type (:*:), delta)
@@ -34,6 +37,9 @@
 	x >>= f = State $ run x $|- run . f
 
 instance Monad (State s) where
+
+instance Invariant (Flip State r) where
+	f <$< g = ((g >-> (f <-> identity) ||=) ||=)
 
 instance Interpreted (State s) where
 	type Primary (State s) a = (->) s :. (:*:) s := a
diff --git a/Pandora/Paradigm/Inventory/Store.hs b/Pandora/Paradigm/Inventory/Store.hs
--- a/Pandora/Paradigm/Inventory/Store.hs
+++ b/Pandora/Paradigm/Inventory/Store.hs
@@ -5,15 +5,19 @@
 import Pandora.Core (type (:.), type (:=), type (<:=), type (~>))
 import Pandora.Pattern.Category (identity, (.), ($))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>), (.#..)))
+import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
 import Pandora.Pattern.Functor.Extractable (Extractable (extract))
 import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
 import Pandora.Pattern.Functor.Comonad (Comonad)
+import Pandora.Pattern.Functor.Bivariant ((<->))
+import Pandora.Pattern.Functor.Divariant ((>->))
 import Pandora.Pattern.Functor.Adjoint ((-|), (|-))
 import Pandora.Paradigm.Primary.Functor.Function ((%))
 import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
 import Pandora.Paradigm.Primary.Functor ()
+import Pandora.Paradigm.Primary.Transformer.Flip (Flip)
 import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
-import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite), Schematic)
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (||=)), Schematic)
 import Pandora.Paradigm.Controlflow.Effect.Transformer.Comonadic (Comonadic (bring), (:<) (TC))
 import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>))
 
@@ -30,6 +34,9 @@
 	Store x =>> f = Store $ f <$$> Store .#.. (-| identity) <$> x
 
 instance Comonad (Store s) where
+
+instance Invariant (Flip Store r) where
+	f <$< g = ((f <-> (g >-> identity) ||=) ||=)
 
 instance Interpreted (Store s) where
 	type Primary (Store s) a = (:*:) s :. (->) s := a
diff --git a/Pandora/Paradigm/Primary.hs b/Pandora/Paradigm/Primary.hs
--- a/Pandora/Paradigm/Primary.hs
+++ b/Pandora/Paradigm/Primary.hs
@@ -16,10 +16,10 @@
 import Pandora.Pattern.Transformer.Lowerable (lower)
 import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
 import Pandora.Paradigm.Inventory.Store (Store (Store))
-import Pandora.Paradigm.Schemes (TU (TU), PQ_ (PQ_), type (<:.>), type (<:.:>))
+import Pandora.Paradigm.Schemes (TU (TU), P_Q_T (P_Q_T), type (<:.>), type (<:.:>))
 import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
 import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Into), premorph)
-import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure))
+import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure))
 
 instance Category (Flip (->)) where
 	identity = Flip identity
@@ -94,17 +94,19 @@
 	morphing (run . premorph -> Nothing :*: Nothing) = End
 
 instance Substructure Left Wye where
-	type Substructural Left Wye = Maybe
-	substructure = PQ_ $ \new -> case lower new of
-		End -> Store $ Nothing :*: lift . resolve Left End
-		Left x -> Store $ Just x :*: lift . resolve Left End
-		Right y -> Store $ Nothing :*: (lift # Right y !)
-		Both x y -> Store $ Just x :*: lift . resolve (Both % y) (Right y)
+	type Available Left Wye = Maybe
+	type Substance Left Wye = Identity
+	substructure = P_Q_T $ \new -> case lower new of
+		End -> Store $ Nothing :*: lift . resolve Left End . (extract <$>)
+		Left x -> Store $ Just (Identity x) :*: lift . resolve Left End . (extract <$>)
+		Right y -> Store $ Nothing :*: (lift # Right y !) . (extract <$>)
+		Both x y -> Store $ Just (Identity x) :*: lift . resolve (Both % y) (Right y) . (extract <$>)
 
 instance Substructure Right Wye where
-	type Substructural Right Wye = Maybe
-	substructure = PQ_ $ \new -> case lower new of
-		End -> Store $ Nothing :*: lift . resolve Right End
-		Left x -> Store $ Nothing :*: (lift # Left x !)
-		Right y -> Store $ Just y :*: lift . resolve Right End
-		Both x y -> Store $ Just y :*: lift . resolve (Both x) (Left x)
+	type Available Right Wye = Maybe
+	type Substance Right Wye = Identity
+	substructure = P_Q_T $ \new -> case lower new of
+		End -> Store $ Nothing :*: lift . resolve Right End . (extract <$>)
+		Left x -> Store $ Nothing :*: (lift # Left x !) . (extract <$>)
+		Right y -> Store $ Just (Identity y) :*: lift . resolve Right End . (extract <$>)
+		Both x y -> Store $ Just (Identity y) :*: lift . resolve (Both x) (Left x) . (extract <$>)
diff --git a/Pandora/Paradigm/Primary/Functor/Constant.hs b/Pandora/Paradigm/Primary/Functor/Constant.hs
--- a/Pandora/Paradigm/Primary/Functor/Constant.hs
+++ b/Pandora/Paradigm/Primary/Functor/Constant.hs
@@ -3,7 +3,7 @@
 import Pandora.Pattern.Category (($))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
 import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<)))
-import Pandora.Pattern.Functor.Invariant (Invariant ((>-<)))
+import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
 import Pandora.Pattern.Functor.Pointable (Pointable (point))
 import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
 import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->)))
@@ -27,7 +27,7 @@
 	_ >$< Constant x = Constant x
 
 instance Invariant (Constant a) where
-	_ >-< _ = \(Constant x) -> Constant x
+	_ <$< _ = \(Constant x) -> Constant x
 
 instance Traversable (Constant a) where
 	Constant x ->> _ = point $ Constant x
diff --git a/Pandora/Paradigm/Primary/Functor/Endo.hs b/Pandora/Paradigm/Primary/Functor/Endo.hs
--- a/Pandora/Paradigm/Primary/Functor/Endo.hs
+++ b/Pandora/Paradigm/Primary/Functor/Endo.hs
@@ -1,7 +1,7 @@
 module Pandora.Paradigm.Primary.Functor.Endo where
 
 import Pandora.Pattern.Category (identity, (.), (#))
-import Pandora.Pattern.Functor.Invariant (Invariant ((>-<)))
+import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
 import Pandora.Pattern.Functor.Divariant ((>->))
 import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
 import Pandora.Pattern.Object.Monoid (Monoid (zero))
@@ -16,7 +16,7 @@
 	unite = Endo
 
 instance Invariant Endo where
-	f >-< g = (g >-> f ||=)
+	f <$< g = (g >-> f ||=)
 
 instance Semigroup (Endo a) where
 	Endo f + Endo g = Endo # g . f
diff --git a/Pandora/Paradigm/Primary/Functor/Product.hs b/Pandora/Paradigm/Primary/Functor/Product.hs
--- a/Pandora/Paradigm/Primary/Functor/Product.hs
+++ b/Pandora/Paradigm/Primary/Functor/Product.hs
@@ -1,6 +1,9 @@
 module Pandora.Paradigm.Primary.Functor.Product where
 
+import Pandora.Core.Functor (type (:=))
+import Pandora.Pattern.Category (($), (#))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
+import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
 import Pandora.Pattern.Functor.Extractable (Extractable (extract))
 import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
 import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
@@ -23,7 +26,7 @@
 type (:*:) = Product
 
 instance Covariant (Product s) where
-	f <$> x = attached x :*: f (extract x)
+	f <$> x = attached x :*: f # extract x
 
 instance Extractable (Product a) where
 	extract ~(_ :*: y) = y
@@ -63,8 +66,11 @@
 instance (Lattice s, Lattice a) => Lattice (s :*: a) where
 
 instance (Group s, Group a) => Group (s :*: a) where
-	invert x = invert (attached x) :*: invert (extract x)
+	invert x = invert # attached x :*: invert # extract x
 
+instance {-# OVERLAPS #-} Applicative t => Applicative (t <:.:> t := (:*:)) where
+	T_U (lfs :*: rfs) <*> T_U (ls :*: rs) = T_U $ lfs <*> ls :*: rfs <*> rs
+
 delta :: a -> a :*: a
 delta x = x :*: x
 
@@ -75,4 +81,4 @@
 attached ~(x :*: _) = x
 
 twosome :: t a -> u a -> (<:.:>) t u (:*:) a
-twosome x y = T_U (x :*: y)
+twosome x y = T_U $ x :*: y
diff --git a/Pandora/Paradigm/Primary/Transformer/Tap.hs b/Pandora/Paradigm/Primary/Transformer/Tap.hs
--- a/Pandora/Paradigm/Primary/Transformer/Tap.hs
+++ b/Pandora/Paradigm/Primary/Transformer/Tap.hs
@@ -1,5 +1,6 @@
 module Pandora.Paradigm.Primary.Transformer.Tap where
 
+import Pandora.Core.Functor (type (:=))
 import Pandora.Pattern.Category ((.), ($), (#))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
 import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
@@ -10,9 +11,18 @@
 import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
 import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
 import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
+import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
 import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
 import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
+import Pandora.Paradigm.Inventory.Store (Store (Store))
 import Pandora.Paradigm.Primary.Functor.Function ((%))
+import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
+import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:))
+import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
+import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
+import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
+import Pandora.Paradigm.Structure.Ability.Substructure
+	(Substructure (Available, Substance, substructure), Segment (Root))
 
 data Tap t a = Tap a (t a)
 
@@ -42,3 +52,21 @@
 
 instance Hoistable Tap where
 	f /|\ Tap x xs = Tap x # f xs
+
+instance Covariant t => Substructure Root (Tap (t <:.:> t := (:*:))) where
+	type Available Root (Tap (t <:.:> t := (:*:))) = Identity
+	type Substance Root (Tap (t <:.:> t := (:*:))) = Identity
+	substructure = P_Q_T $ \zipper -> case lower zipper of
+		Tap x xs -> Store $ Identity (Identity x) :*: lift . (Tap % xs) . extract . extract
+
+instance Covariant t => Substructure Left (Tap (t <:.:> t := (:*:))) where
+	type Available Left (Tap (t <:.:> t := (:*:))) = Identity
+	type Substance Left (Tap (t <:.:> t := (:*:))) = t
+	substructure = P_Q_T $ \zipper -> case lower zipper of
+		Tap x (T_U (future :*: past)) -> Store $ Identity future :*: lift . Tap x . T_U . (:*: past) . extract
+
+instance Covariant t => Substructure Right (Tap (t <:.:> t := (:*:))) where
+	type Available Right (Tap (t <:.:> t := (:*:))) = Identity
+	type Substance Right (Tap (t <:.:> t := (:*:))) = t
+	substructure = P_Q_T $ \zipper -> case lower zipper of
+		Tap x (T_U (future :*: past)) -> Store $ Identity past :*: lift . Tap x . T_U . (future :*:) . extract
diff --git a/Pandora/Paradigm/Schemes.hs b/Pandora/Paradigm/Schemes.hs
--- a/Pandora/Paradigm/Schemes.hs
+++ b/Pandora/Paradigm/Schemes.hs
@@ -3,6 +3,9 @@
 module Pandora.Paradigm.Schemes (module Exports) where
 
 import Pandora.Paradigm.Schemes.PQ_ as Exports
+import Pandora.Paradigm.Schemes.P_Q_T as Exports
+import Pandora.Paradigm.Schemes.P_T as Exports
+import Pandora.Paradigm.Schemes.PTU as Exports
 import Pandora.Paradigm.Schemes.U_T as Exports
 import Pandora.Paradigm.Schemes.T_U as Exports
 import Pandora.Paradigm.Schemes.UTU as Exports
diff --git a/Pandora/Paradigm/Schemes/PTU.hs b/Pandora/Paradigm/Schemes/PTU.hs
new file mode 100644
--- /dev/null
+++ b/Pandora/Paradigm/Schemes/PTU.hs
@@ -0,0 +1,10 @@
+module Pandora.Paradigm.Schemes.PTU where
+
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
+
+newtype PTU p t u a b = PTU (p (t a) (u b))
+
+instance Interpreted (PTU p t u a) where
+	type Primary (PTU p t u a) b = p (t a) (u b)
+	run ~(PTU x) = x
+	unite = PTU
diff --git a/Pandora/Paradigm/Schemes/P_Q_T.hs b/Pandora/Paradigm/Schemes/P_Q_T.hs
new file mode 100644
--- /dev/null
+++ b/Pandora/Paradigm/Schemes/P_Q_T.hs
@@ -0,0 +1,10 @@
+module Pandora.Paradigm.Schemes.P_Q_T where
+
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
+
+newtype P_Q_T (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) (a :: *) (b :: *) = P_Q_T (p a (q (t b) a))
+
+instance Interpreted (P_Q_T p q t a) where
+	type Primary (P_Q_T p q t a) b = (p a (q (t b) a))
+	run ~(P_Q_T x) = x
+	unite = P_Q_T
diff --git a/Pandora/Paradigm/Schemes/P_T.hs b/Pandora/Paradigm/Schemes/P_T.hs
new file mode 100644
--- /dev/null
+++ b/Pandora/Paradigm/Schemes/P_T.hs
@@ -0,0 +1,10 @@
+module Pandora.Paradigm.Schemes.P_T where
+
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
+
+newtype P_T p t a b = P_T (p (t a) b)
+
+instance Interpreted (P_T p t a) where
+	type Primary (P_T p t a) b = p (t a) b
+	run ~(P_T x) = x
+	unite = P_T
diff --git a/Pandora/Paradigm/Structure.hs b/Pandora/Paradigm/Structure.hs
--- a/Pandora/Paradigm/Structure.hs
+++ b/Pandora/Paradigm/Structure.hs
@@ -7,6 +7,7 @@
 import Pandora.Paradigm.Structure.Modification as Exports
 import Pandora.Paradigm.Structure.Some as Exports
 
+import Pandora.Core.Functor (type (:=))
 import Pandora.Pattern.Category (($), (.), (#))
 import Pandora.Pattern.Functor.Covariant (Covariant (comap))
 import Pandora.Pattern.Functor.Extractable (extract)
@@ -18,16 +19,18 @@
 import Pandora.Paradigm.Inventory.Optics ()
 import Pandora.Paradigm.Inventory.Store (Store (Store))
 import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
+import Pandora.Paradigm.Primary.Functor.Function ((%))
 import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
 import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
 import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
-import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
+import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
 import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End))
 import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
 import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
 import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
 import Pandora.Paradigm.Schemes.TU (type (<:.>))
-import Pandora.Paradigm.Schemes.PQ_ (PQ_ (PQ_))
+import Pandora.Paradigm.Schemes.T_U ( type (<:.:>))
+import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
 
 instance Monotonic s a => Monotonic s (s :*: a) where
 	reduce f r x = reduce f # f (attached x) r # extract x
@@ -36,9 +39,10 @@
 	null = Predicate $ \case { Just _ -> True ; _ -> False }
 
 instance Covariant t => Substructure Tail (Tap t) where
-	type Substructural Tail (Tap t) = t
-	substructure = PQ_ $ \tap -> case extract # run tap of
-		Tap x xs -> Store $ xs :*: lift . Tap x
+	type Available Tail (Tap t) = Identity
+	type Substance Tail (Tap t) = t
+	substructure = P_Q_T $ \tap -> case extract # run tap of
+		Tap x xs -> Store $ Identity xs :*: lift . Tap x . extract
 
 instance Morphable (Into (Preorder (Construction Maybe))) (Construction Wye) where
 	type Morphing (Into (Preorder (Construction Maybe))) (Construction Wye) = Construction Maybe
@@ -66,20 +70,34 @@
 	morphing (premorph -> xs) = comap (into @(o ds)) ||= xs
 
 instance Substructure Left (Flip Product a) where
-	type Substructural Left (Flip Product a) = Identity
-	substructure = PQ_ $ \product -> case run # lower product of
-		s :*: x -> Store $ Identity s :*: lift . Flip . (:*: x) . extract
+	type Available Left (Flip Product a) = Identity
+	type Substance Left (Flip Product a) = Identity
+	substructure = P_Q_T $ \product -> case run # lower product of
+		s :*: x -> Store $ Identity (Identity s) :*: lift . Flip . (:*: x) . extract . extract
 
 instance Substructure Right (Product s) where
-	type Substructural Right (Product s) = Identity
-	substructure = PQ_ $ \product -> case lower product of
-		s :*: x -> Store $ Identity x :*: lift . (s :*:) . extract
+	type Available Right (Product s) = Identity
+	type Substance Right (Product s) = Identity
+	substructure = P_Q_T $ \product -> case lower product of
+		s :*: x -> Store $ Identity (Identity x) :*: lift . (s :*:) . extract . extract
 
 instance Accessible s (s :*: a) where
-	access = PQ_ $ \(s :*: x) -> Store $ s :*: (:*: x)
+	access = P_Q_T $ \(s :*: x) -> Store $ Identity s :*: (:*: x) . extract
 
 instance Accessible a (s :*: a) where
-	access = PQ_ $ \(s :*: x) -> Store $ x :*: (s :*:)
+	access = P_Q_T $ \(s :*: x) -> Store $ Identity x :*: (s :*:) . extract
 
 instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
 	access = access @b . access @a
+
+instance Covariant t => Substructure Left (t <:.:> t := (:*:)) where
+	type Available Left (t <:.:> t := (:*:)) = Identity
+	type Substance Left (t <:.:> t := (:*:)) = t
+	substructure = P_Q_T $ \x -> case run # lower x of
+		ls :*: rs -> Store $ Identity ls :*: lift . (twosome % rs) . extract
+
+instance Covariant t => Substructure Right (t <:.:> t := (:*:)) where
+	type Available Right (t <:.:> t := (:*:)) = Identity
+	type Substance Right (t <:.:> t := (:*:)) = t
+	substructure = P_Q_T $ \x -> case run # lower x of
+		ls :*: rs -> Store $ Identity rs :*: lift . (twosome ls) . extract
diff --git a/Pandora/Paradigm/Structure/Ability/Accessible.hs b/Pandora/Paradigm/Structure/Ability/Accessible.hs
--- a/Pandora/Paradigm/Structure/Ability/Accessible.hs
+++ b/Pandora/Paradigm/Structure/Ability/Accessible.hs
@@ -1,6 +1,7 @@
 module Pandora.Paradigm.Structure.Ability.Accessible where
 
-import Pandora.Paradigm.Inventory.Optics (type (:-.))
+import Pandora.Paradigm.Primary.Functor.Identity (Identity)
+import Pandora.Paradigm.Inventory.Optics (Lens)
 
-class Accessible tgt src where
-	access :: src :-. tgt
+class Accessible target source where
+	access :: Lens Identity source target
diff --git a/Pandora/Paradigm/Structure/Ability/Substructure.hs b/Pandora/Paradigm/Structure/Ability/Substructure.hs
--- a/Pandora/Paradigm/Structure/Ability/Substructure.hs
+++ b/Pandora/Paradigm/Structure/Ability/Substructure.hs
@@ -3,22 +3,25 @@
 
 module Pandora.Paradigm.Structure.Ability.Substructure where
 
+import Pandora.Core.Functor (type (:=))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
 import Pandora.Pattern.Functor.Divariant ((>->))
 import Pandora.Pattern.Transformer.Liftable (lift)
 import Pandora.Pattern.Transformer.Lowerable (lower)
 import Pandora.Paradigm.Controlflow.Effect.Interpreted ((||=))
-import Pandora.Paradigm.Inventory.Optics (type (:~.))
+import Pandora.Paradigm.Inventory.Optics (type (#=@))
 import Pandora.Paradigm.Primary.Functor.Tagged (Tagged)
 import Pandora.Paradigm.Schemes.TU (type (<:.>))
 
-class Substructure f t where
-	type Substructural (f :: k) (t :: * -> *) :: * -> *
-	substructure :: Tagged f <:.> t :~. Substructural f t
+data Segment a = Root a | Tail a
 
-	sub :: Covariant t => t :~. Substructural f t
-	sub = lift >-> (lower <$>) ||= substructure @f @t
+type Substructured segment source available target = (Substructure segment source,
+	Substance segment source ~ target, Available segment source ~ available)
 
-data Segment a = Root a | Tail a
+class Substructure segment (structure :: * -> *) where
+	type Available segment structure :: * -> *
+	type Substance segment structure :: * -> *
+	substructure :: (Tagged segment <:.> structure) #=@ Substance segment structure := Available segment structure
 
-type Substructured i source target = (Substructure i source, Substructural i source ~ target)
+	sub :: Covariant structure => structure #=@ Substance segment structure := Available segment structure
+	sub = lift >-> (lower <$>) ||= substructure @segment @structure
diff --git a/Pandora/Paradigm/Structure/Ability/Zipper.hs b/Pandora/Paradigm/Structure/Ability/Zipper.hs
--- a/Pandora/Paradigm/Structure/Ability/Zipper.hs
+++ b/Pandora/Paradigm/Structure/Ability/Zipper.hs
@@ -1,3 +1,10 @@
 module Pandora.Paradigm.Structure.Ability.Zipper where
 
-type family Zipper (s :: * -> *) = (r :: * -> *) | r -> s
+import Pandora.Core.Functor (type (:::))
+import Pandora.Paradigm.Structure.Ability.Morphable (Morphable, Morph (Rotate))
+
+type family Zipper (structure :: * -> *) (moves :: k) = (result :: * -> *) | result -> structure
+
+type family Fastenable structure rs where
+	Fastenable structure (r ::: rs) = (Morphable (Rotate r) structure, Fastenable structure rs)
+	Fastenable structure r = Morphable (Rotate r) structure
diff --git a/Pandora/Paradigm/Structure/Some/Binary.hs b/Pandora/Paradigm/Structure/Some/Binary.hs
--- a/Pandora/Paradigm/Structure/Some/Binary.hs
+++ b/Pandora/Paradigm/Structure/Some/Binary.hs
@@ -2,9 +2,9 @@
 
 module Pandora.Paradigm.Structure.Some.Binary where
 
-import Pandora.Core.Functor (type (:.), type (:=), type (:=>))
-import Pandora.Pattern.Category (identity, (.), ($), (#))
-import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), ($$>)))
+import Pandora.Core.Functor (type (:.), type (:=), type (:=>), type (:::))
+import Pandora.Pattern.Category ((.), ($), (#))
+import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), ($$$>)))
 import Pandora.Pattern.Functor.Extractable (extract)
 import Pandora.Pattern.Functor.Avoidable (empty)
 import Pandora.Pattern.Functor.Bindable ((>>=))
@@ -26,17 +26,17 @@
 import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
 import Pandora.Paradigm.Primary.Functor.Wye (Wye (End, Left, Right, Both))
 import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
-import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), PQ_ (PQ_), type (<:.>), type (<:.:>))
-import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
+import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), P_Q_T (P_Q_T), type (<:.>), type (<:.:>))
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (=||))
 import Pandora.Paradigm.Inventory.Store (Store (Store))
 import Pandora.Paradigm.Inventory.Optics (over, view)
 import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
 import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
 import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Heighth), measure)
 import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (resolve))
-import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
-	, Morph (Rotate, Into, Insert, Lookup, Vary, Key, Element), Vertical (Up, Down), morph, premorph, lookup)
-import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Root), sub)
+import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), morph, premorph
+	, Morph (Rotate, Into, Insert, Lookup, Vary, Key, Element), Vertical (Up, Down), lookup, vary)
+import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure), Segment (Root), sub)
 import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
 import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))
 
@@ -52,8 +52,11 @@
 	type Morphing Insert Binary = (Identity <:.:> Comparison := (:*:)) <:.:> Binary := (->)
 	morphing (run . premorph -> Nothing) = T_U $ \(T_U (Identity x :*: _)) -> lift $ leaf x
 	morphing (run . premorph -> Just ne) = T_U $ \(T_U (Identity x :*: Convergence f)) ->
-		let continue xs = run # morph @Insert xs $ twosome # Identity x # Convergence f
-		in lift $ f x # extract ne & order # ne # over (sub @Left) continue ne # over (sub @Right) continue ne
+		let continue xs = run # morph @Insert @(Nonempty Binary) xs $ twosome # Identity x # Convergence f in
+		let change = Just . resolve continue (leaf x) in
+		lift $ f x # extract ne & order # ne
+			# over (sub @Left) change ne
+			# over (sub @Right) change ne
 
 instance Measurable Heighth Binary where
 	type Measural Heighth Binary a = Numerator
@@ -64,15 +67,17 @@
 	null = Predicate $ \case { TU Nothing -> True ; _ -> False }
 
 instance Substructure Left Binary where
-	type Substructural Left Binary = Binary
-	substructure = PQ_ $ \bintree -> case run . extract . run # bintree of
-		Nothing -> Store $ empty :*: lift . identity
+	type Available Left Binary = Maybe
+	type Substance Left Binary = Construction Wye
+	substructure = P_Q_T $ \bintree -> case run . lower # bintree of
+		Nothing -> Store $ Nothing :*: lift . TU
 		Just tree -> lift . lift <$> run (sub @Left) tree
 
 instance Substructure Right Binary where
-	type Substructural Right Binary = Binary
-	substructure = PQ_ $ \bintree -> case run . extract . run # bintree of
-		Nothing -> Store $ empty :*: lift . identity
+	type Available Right Binary = Maybe
+	type Substance Right Binary = Construction Wye
+	substructure = P_Q_T $ \bintree -> case run . extract . run # bintree of
+		Nothing -> Store $ Nothing :*: lift . TU
 		Just tree -> lift . lift <$> run (sub @Right) tree
 
 -------------------------------------- Non-empty binary tree ---------------------------------------
@@ -87,7 +92,7 @@
 	type Morphing Insert (Construction Wye) = (Identity <:.:> Comparison := (:*:)) <:.:> Construction Wye := (->)
 	morphing (premorph -> nonempty_list) = T_U $ \(T_U (Identity x :*: Convergence f)) ->
 		let continue xs = run # morph @Insert @(Nonempty Binary) xs $ twosome # Identity x # Convergence f in
-		let change = lift . resolve continue (leaf x) . run in
+		let change = Just . resolve continue (leaf x) in
 		order # nonempty_list
 			# over (sub @Left) change nonempty_list
 			# over (sub @Right) change nonempty_list
@@ -103,25 +108,28 @@
 		in lm <=> rm & order lm rm lm
 
 instance Substructure Root (Construction Wye) where
-	type Substructural Root (Construction Wye) = Identity
-	substructure = PQ_ $ \bintree -> case lower bintree of
-		Construct x xs -> Store $ Identity x :*: lift . (Construct % xs) . extract
+	type Available Root (Construction Wye) = Identity
+	type Substance Root (Construction Wye) = Identity
+	substructure = P_Q_T $ \bintree -> case lower bintree of
+		Construct x xs -> Store $ Identity (Identity x) :*: lift . (Construct % xs) . extract . extract
 
 instance Substructure Left (Construction Wye) where
-	type Substructural Left (Construction Wye) = Binary
-	substructure = PQ_ $ \bintree -> case extract # run bintree of
-		Construct x End -> Store $ empty :*: lift . resolve (Construct x . Left) (leaf x) . run
-		Construct x (Left lst) -> Store $ lift lst :*: lift . Construct x . resolve Left End . run
-		Construct x (Right rst) -> Store $ empty :*: lift . Construct x . resolve (Both % rst) (Right rst) . run
-		Construct x (Both lst rst) -> Store $ lift lst :*: lift . Construct x . resolve (Both % rst) (Right rst) . run
+	type Available Left (Construction Wye) = Maybe
+	type Substance Left (Construction Wye) = Construction Wye
+	substructure = P_Q_T $ \bintree -> case extract # run bintree of
+		Construct x End -> Store $ Nothing :*: lift . resolve (Construct x . Left) (leaf x)
+		Construct x (Left lst) -> Store $ Just lst :*: lift . Construct x . resolve Left End
+		Construct x (Right rst) -> Store $ Nothing :*: lift . Construct x . resolve (Both % rst) (Right rst)
+		Construct x (Both lst rst) -> Store $ Just lst :*: lift . Construct x . resolve (Both % rst) (Right rst)
 
 instance Substructure Right (Construction Wye) where
-	type Substructural Right (Construction Wye) = Binary
-	substructure = PQ_ $ \bintree -> case extract # run bintree of
-		Construct x End -> Store $ empty :*: lift . resolve (Construct x . Right) (leaf x) . run
-		Construct x (Left lst) -> Store $ empty :*: lift . Construct x . resolve (Both lst) (Left lst) . run
-		Construct x (Right rst) -> Store $ lift rst :*: lift . Construct x . resolve Right End . run
-		Construct x (Both lst rst) -> Store $ lift rst :*: lift . Construct x . resolve (Both lst) (Left lst) . run
+	type Available Right (Construction Wye) = Maybe
+	type Substance Right (Construction Wye) = Construction Wye
+	substructure = P_Q_T $ \bintree -> case extract # run bintree of
+		Construct x End -> Store $ Nothing :*: lift . resolve (Construct x . Right) (leaf x)
+		Construct x (Left lst) -> Store $ Nothing :*: lift . Construct x . resolve (Both lst) (Left lst)
+		Construct x (Right rst) -> Store $ Just rst :*: lift . Construct x . resolve Right End
+		Construct x (Both lst rst) -> Store $ Just rst :*: lift . Construct x . resolve (Both lst) (Left lst)
 
 -------------------------------------- Prefixed binary tree ----------------------------------------
 
@@ -129,17 +137,19 @@
 	type Morphing (Lookup Key) (Prefixed Binary k) = (->) k <:.> Maybe
 	morphing (run . run . premorph -> Nothing) = lift Nothing
 	morphing (run . run . premorph -> Just tree) = TU $ \key ->
-		let root = extract tree in key <=> attached root & order # Just (extract root)
-			# lookup @Key key (Prefixed $ view # sub @Left # tree)
-			# lookup @Key key (Prefixed $ view # sub @Right # tree)
+		let root = extract tree in key <=> attached root & order (Just # extract root)
+			(view # sub @Left # tree >>= lookup @Key key . Prefixed)
+			(view # sub @Right # tree >>= lookup @Key key . Prefixed)
 
 instance Chain k => Morphable (Vary Element) (Prefixed Binary k) where
 	type Morphing (Vary Element) (Prefixed Binary k) = (Product k <:.> Identity) <:.:> Prefixed Binary k := (->)
 	morphing (run . run . premorph -> Nothing) = T_U $ \(TU (key :*: Identity value)) -> Prefixed . lift . leaf $ key :*: value
 	morphing (run . run . premorph -> Just tree) = T_U $ \(TU (key :*: Identity value)) ->
-		let continue xs = run $ run # morph @(Vary Element) (Prefixed xs) # TU (key :*: Identity value)
+		let continue = ((vary @Element @k @_ @(Prefixed Binary _) key value =||) =||)
 		in let root = extract tree in Prefixed . lift $ key <=> attached root & order
-			# over (sub @Root) ($$> value) tree # over (sub @Left) continue tree # over (sub @Right) continue tree
+			# over (sub @Root) ($$$> value) tree
+			# over (sub @Left) continue tree
+			# over (sub @Right) continue tree
 
 ---------------------------------- Prefixed non-empty binary tree ----------------------------------
 
@@ -147,8 +157,8 @@
 	type Morphing (Lookup Key) (Prefixed (Construction Wye) key) = (->) key <:.> Maybe
 	morphing (run . premorph -> Construct x xs) = TU $ \key ->
 		key <=> attached x & order (Just # extract x)
-			(view # sub @Left # xs >>= lookup @Key key . Prefixed)
-			(view # sub @Right # xs >>= lookup @Key key . Prefixed)
+			(view # sub @Left # xs >>= lookup @Key key . Prefixed . extract)
+			(view # sub @Right # xs >>= lookup @Key key . Prefixed . extract)
 
 -------------------------------------- Zipper of binary tree ---------------------------------------
 
@@ -163,7 +173,8 @@
 
 type Bicursor = Identity <:.:> Binary := (:*:)
 
-type instance Zipper (Construction Wye) = Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)
+type instance Zipper (Construction Wye) (Up ::: Down Left ::: Down Right) =
+	Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)
 
 instance Morphable (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:)) where
 	type Morphing (Rotate Up) (Construction Wye <:.:> Bifurcation <:.> Bicursor := (:*:))
diff --git a/Pandora/Paradigm/Structure/Some/List.hs b/Pandora/Paradigm/Structure/Some/List.hs
--- a/Pandora/Paradigm/Structure/Some/List.hs
+++ b/Pandora/Paradigm/Structure/Some/List.hs
@@ -2,7 +2,8 @@
 
 module Pandora.Paradigm.Structure.Some.List where
 
-import Pandora.Core.Functor (type (:.), type (:=))
+import Pandora.Core.Functor (type (:.), type (:=), type (:::))
+import Pandora.Core.Impliable (imply)
 import Pandora.Pattern.Category ((.), ($), (#), identity)
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (.#..)))
 import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
@@ -33,21 +34,20 @@
 import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
 import Pandora.Paradigm.Inventory.State (State, fold, modify)
 import Pandora.Paradigm.Inventory.Store (Store (Store))
-import Pandora.Paradigm.Inventory.Optics (view)
+import Pandora.Paradigm.Inventory.Optics (Convex, Lens, view)
 import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
 import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
 import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
-import Pandora.Paradigm.Schemes.PQ_ (PQ_ (PQ_))
+import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
 import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
 import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
 import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
--- import Pandora.Paradigm.Structure.Ability.Focusable ()
 import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
 import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)
 import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
 	, Morph (Rotate, Into, Push, Pop, Delete, Find, Lookup, Element, Key)
 	, Occurrence (All, First), premorph, rotate, item, filter, find, lookup, into)
-import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure, sub), Segment (Root, Tail))
+import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure, sub), Segment (Root, Tail))
 import Pandora.Paradigm.Structure.Interface.Stack (Stack)
 import Pandora.Paradigm.Structure.Modification.Combinative (Combinative)
 import Pandora.Paradigm.Structure.Modification.Comprehension (Comprehension (Comprehension))
@@ -104,16 +104,18 @@
 	null = Predicate $ \case { TU Nothing -> True ; _ -> False }
 
 instance Substructure Root List where
-	type Substructural Root List = Maybe
-	substructure = PQ_ $ \zipper -> case run # lower zipper of
-		Just (Construct x xs) -> Store $ Just x :*: lift . resolve (lift . (Construct % xs)) empty
-		Nothing -> Store $ Nothing :*: lift . resolve (lift . (Construct % empty)) empty
+	type Available Root List = Maybe
+	type Substance Root List = Identity
+	substructure = P_Q_T $ \zipper -> case run # lower zipper of
+		Just (Construct x xs) -> Store $ Just (Identity x) :*: lift . resolve (lift . (Construct % xs) . extract @Identity) empty
+		Nothing -> Store $ Nothing :*: lift . resolve (lift . (Construct % empty) . extract @Identity) empty
 
 instance Substructure Tail List where
-	type Substructural Tail List = List
-	substructure = PQ_ $ \x -> case run . extract . run $ x of
+	type Available Tail List = Identity
+	type Substance Tail List = List
+	substructure = P_Q_T $ \x -> case run . extract . run $ x of
 		Just ns -> lift . lift <$> run (sub @Tail) ns
-		Nothing -> Store $ empty :*: lift . identity
+		Nothing -> Store $ Identity empty :*: lift . identity . extract
 
 -- | Transform any traversable structure into a stack
 linearize :: forall t a . Traversable t => t a -> List a
@@ -146,14 +148,16 @@
 	measurement (deconstruct . extract -> Just xs) = One + measure @Length xs
 
 instance Substructure Root (Construction Maybe) where
-	type Substructural Root (Construction Maybe) = Identity
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Construct x xs -> Store $ Identity x :*: lift . (Construct % xs) . extract
+	type Available Root (Construction Maybe) = Identity
+	type Substance Root (Construction Maybe) = Identity
+	substructure = imply @(Convex Lens _ _) (Identity . extract . lower)
+		(\source target -> lift $ Construct # extract target # deconstruct (lower source))
 
 instance Substructure Tail (Construction Maybe) where
-	type Substructural Tail (Construction Maybe) = List
-	substructure = PQ_ $ \stack -> case extract $ run stack of
-		Construct x xs -> Store $ TU xs :*: lift . Construct x . run
+	type Available Tail (Construction Maybe) = Identity
+	type Substance Tail (Construction Maybe) = List
+	substructure = imply @(Convex Lens _ _) (TU . deconstruct . lower)
+		(\source target -> lift $ Construct # extract (lower source) # run target)
 
 ---------------------------------------- Combinative list ------------------------------------------
 
@@ -161,7 +165,7 @@
 
 ----------------------------------------- Zipper of list -------------------------------------------
 
-type instance Zipper List = Tap (List <:.:> List := (:*:))
+type instance Zipper List (Left ::: Right) = Tap (List <:.:> List := (:*:))
 
 instance {-# OVERLAPS #-} Applicative (Tap (List <:.:> List := (:*:))) where
 	Tap f (T_U (lfs :*: rfs)) <*> Tap x (T_U (ls :*: rs)) = Tap # f x # T_U (lfs <*> ls :*: rfs <*> rs)
@@ -175,18 +179,20 @@
 		Tap # f z $ twosome # f <$> move (rotate @Left) # f <$> move (rotate @Right)
 
 instance Morphable (Rotate Left) (Tap (List <:.:> List := (:*:))) where
-	type Morphing (Rotate Left) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
-	morphing (premorph -> Tap x (T_U (future :*: past))) = TU
-		$ Tap % twosome (view (sub @Tail) future) (item @Push x past) <$> view (sub @Root) future
+	type Morphing (Rotate Left) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Tap (List <:.:> List := (:*:))
+	morphing (premorph -> Tap x (T_U (future :*: past))) =
+		let subtree = twosome # extract (view (sub @Tail) future) # item @Push x past in
+		TU $ (Tap . extract) % subtree <$> view (sub @Root) future
 
 instance Morphable (Rotate Right) (Tap (List <:.:> List := (:*:))) where
-	type Morphing (Rotate Right) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
-	morphing (premorph -> Tap x (T_U (future :*: past))) = TU
-		$ Tap % twosome (item @Push x future) (view (sub @Tail) past) <$> view (sub @Root) past
+	type Morphing (Rotate Right) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Tap (List <:.:> List := (:*:))
+	morphing (premorph -> Tap x (T_U (future :*: past))) =
+		let subtree = twosome # item @Push x future # extract (view (sub @Tail) past) in
+		TU $ (Tap . extract) % subtree <$> view (sub @Root) past
 
 instance Morphable (Into (Tap (List <:.:> List := (:*:)))) List where
-	type Morphing (Into (Tap (List <:.:> List := (:*:)))) List = Maybe <:.> Zipper List
-	morphing (premorph -> list) = (into @(Zipper List) <$>) ||= list
+	type Morphing (Into (Tap (List <:.:> List := (:*:)))) List = Maybe <:.> Tap (List <:.:> List := (:*:))
+	morphing (premorph -> list) = (into @(Zipper List (Left ::: Right)) <$>) ||= list
 
 instance Morphable (Into List) (Tap (List <:.:> List := (:*:))) where
 	type Morphing (Into List) (Tap (List <:.:> List := (:*:))) = List
@@ -200,24 +206,9 @@
 		# past ->> modify . item @Push @(Comprehension Maybe)
 		# item @Push x (Comprehension future)
 
-instance Substructure Root (Tap (List<:.:> List:= (:*:))) where
-	type Substructural Root (Tap (List<:.:> List:= (:*:))) = Identity
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x xs -> Store $ Identity x :*: lift . (Tap % xs) . extract
-
-instance Substructure Left (Tap (List <:.:> List := (:*:))) where
-	type Substructural Left (Tap (List <:.:> List := (:*:))) = List
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x (T_U (future :*: past)) -> Store $ future :*: lift . Tap x . T_U . (:*: past)
-
-instance Substructure Right (Tap (List <:.:> List := (:*:))) where
-	type Substructural Right (Tap (List <:.:> List := (:*:))) = List
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x (T_U (future :*: past)) -> Store $ past :*: lift . Tap x . T_U . (future :*:)
-
 ------------------------------------- Zipper of non-empty list -------------------------------------
 
-type instance Zipper (Construction Maybe) = Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
+type instance Zipper (Construction Maybe) (Left ::: Right) = Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
 
 instance {-# OVERLAPS #-} Applicative (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
 	Tap f (T_U (lfs :*: rfs)) <*> Tap x (T_U (ls :*: rs)) = Tap # f x # T_U (lfs <*> ls :*: rfs <*> rs)
@@ -227,23 +218,26 @@
 		<$> Reverse past ->> f <*> f x <*> future ->> f
 
 instance Morphable (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Morphing (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
+	type Morphing (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) =
+		Maybe <:.> Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
 	morphing (premorph -> Tap x (T_U (future :*: past))) = TU $ Tap (extract future) . twosome % item @Push x past <$> deconstruct future
 
 instance Morphable (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Morphing (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
+	type Morphing (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) =
+		Maybe <:.> Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
 	morphing (premorph -> Tap x (T_U (future :*: past))) = TU $ Tap (extract past) . twosome (item @Push x future) <$> deconstruct past
 
 instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) where
-	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) = Zipper List
-	morphing (premorph -> ne) = Tap # extract ne $ twosome # view (sub @Tail) ne # empty
+	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) = Tap (List <:.:> List := (:*:))
+	morphing (premorph -> ne) = Tap # extract ne $ twosome # extract (view # sub @Tail # ne) # empty
 
 instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Zipper List
+	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Tap (List <:.:> List := (:*:))
 	morphing (premorph -> zipper) = Tap # extract zipper $ lift <-> lift ||= lower zipper
 
 instance Morphable (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) where
-	type Morphing (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
+	type Morphing (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) =
+		Maybe <:.> Tap (Construction Maybe <:.:> Construction Maybe := (:*:))
 	morphing (premorph -> zipper) = let spread x y = (:*:) <$> x <*> y in TU $
 		Tap (extract zipper) . T_U <$> ((|- spread) . (run <-> run) . run $ lower zipper)
 
@@ -259,24 +253,9 @@
 		# past ->> modify . item @Push @List
 		# item @Push x (lift future)
 
-instance Substructure Root (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Substructural Root (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Identity
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x xs -> Store $ Identity x :*: lift . (Tap % xs) . extract
-
-instance Substructure Left (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Substructural Left (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x (T_U (future :*: past)) -> Store $ future :*: lift . Tap x . T_U . (:*: past)
-
-instance Substructure Right (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
-	type Substructural Right (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
-	substructure = PQ_ $ \zipper -> case lower zipper of
-		Tap x (T_U (future :*: past)) -> Store $ past :*: lift . Tap x . T_U . (future :*:)
-
 ------------------------------------ Zipper of combinative list ------------------------------------
 
-type instance Zipper (Comprehension Maybe) = Tap (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))
+type instance Zipper (Comprehension Maybe) (Left ::: Right) = Tap (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))
 
 instance {-# OVERLAPS #-} Applicative (Tap (Comprehension Maybe <:.:> Comprehension Maybe := (:*:))) where
 	Tap f (T_U (lfs :*: rfs)) <*> Tap x (T_U (ls :*: rs)) = Tap # f x # T_U (lfs <*> ls :*: rfs <*> rs)
diff --git a/Pandora/Paradigm/Structure/Some/Rose.hs b/Pandora/Paradigm/Structure/Some/Rose.hs
--- a/Pandora/Paradigm/Structure/Some/Rose.hs
+++ b/Pandora/Paradigm/Structure/Some/Rose.hs
@@ -18,15 +18,16 @@
 import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
 import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate), equate)
 import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
+import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
 import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
-import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), PQ_ (PQ_), type (<:.>), type (<:.:>))
+import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), P_Q_T (P_Q_T), type (<:.>), type (<:.:>))
 import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (=||$>))
 import Pandora.Paradigm.Inventory.Store (Store (Store))
 import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
 	, Morph (Lookup, Vary, Element, Key), premorph, find, vary)
 import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
 import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
-import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Root, Tail))
+import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure), Segment (Root, Tail))
 import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))
 import Pandora.Paradigm.Structure.Some.List (List)
 
@@ -35,29 +36,37 @@
 instance Nullable Rose where
 	null = Predicate $ \case { TU Nothing -> True ; _ -> False }
 
+-- FIXME: If we want to remove root node, we ruin the whole tree
 instance Substructure Root Rose where
-	type Substructural Root Rose = Maybe
-	substructure = PQ_ $ \rose -> case run # lower rose of
-		Nothing -> Store $ Nothing :*: lift . TU . (Construct % empty <$>)
+	type Available Root Rose = Maybe
+	type Substance Root Rose = Identity
+	substructure = P_Q_T $ \rose -> case run # lower rose of
+		Nothing -> Store $ Nothing :*: TU . Tag . TU . ((Construct % empty) . extract <$>)
+		Just nonempty_rose -> Store $ Just (Identity # extract nonempty_rose) :*: \case
+			Just (Identity new) -> lift . TU . Just . Construct new $ deconstruct nonempty_rose
+			Nothing -> lift empty
 
 instance Substructure Just Rose where
-	type Substructural Just Rose = List <:.> Construction List
-	substructure = PQ_ $ \rose -> case run . extract . run # rose of
-		Nothing -> Store $ empty :*: (lift empty !)
-		Just (Construct x xs) -> Store $ TU xs :*: lift . lift . Construct x . run
+	type Available Just Rose = Identity
+	type Substance Just Rose = List <:.> Construction List
+	substructure = P_Q_T $ \rose -> case run . extract . run # rose of
+		Nothing -> Store $ Identity empty :*: (lift empty !)
+		Just (Construct x xs) -> Store $ Identity (TU xs) :*: lift . lift . Construct x . run . extract
 
 --------------------------------------- Non-empty rose tree ----------------------------------------
 
 type instance Nonempty Rose = Construction List
 
 instance Substructure Root (Construction List) where
-	type Substructural Root (Construction List) = Identity
-	substructure = PQ_ $ \rose -> Store $ Identity # extract (lower rose) :*: lift . (Construct % deconstruct (lower rose)) . extract
+	type Available Root (Construction List) = Identity
+	type Substance Root (Construction List) = Identity
+	substructure = P_Q_T $ \rose -> Store $ Identity (Identity # extract (lower rose)) :*: lift . (Construct % deconstruct (lower rose)) . extract . extract
 
 instance Substructure Tail (Construction List) where
-	type Substructural Tail (Construction List) = List <:.> Construction List
-	substructure = PQ_ $ \rose -> case extract # run rose of
-		Construct x xs -> Store $ TU xs :*: lift . Construct x . run
+	type Available Tail (Construction List) = Identity
+	type Substance Tail (Construction List) = List <:.> Construction List
+	substructure = P_Q_T $ \rose -> case extract # run rose of
+		Construct x xs -> Store $ Identity (TU xs) :*: lift . Construct x . run . extract
 
 --------------------------------------- Prefixed rose tree -----------------------------------------
 
diff --git a/Pandora/Paradigm/Structure/Some/Splay.hs b/Pandora/Paradigm/Structure/Some/Splay.hs
--- a/Pandora/Paradigm/Structure/Some/Splay.hs
+++ b/Pandora/Paradigm/Structure/Some/Splay.hs
@@ -15,7 +15,7 @@
 import Pandora.Paradigm.Primary.Functor.Tagged (type (:#))
 import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
 import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
-import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
+import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite)
 import Pandora.Paradigm.Inventory.Optics (over)
 import Pandora.Paradigm.Schemes (TU (TU), type (<:.>))
 import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate, Into), premorph, rotate, into)
@@ -25,6 +25,32 @@
 
 data Splay a = Zig a | Zag a
 
+instance Morphable (Rotate (Left Zig)) Binary where
+	type Morphing (Rotate (Left Zig)) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Left Zig)
+
+instance Morphable (Rotate (Right Zig)) Binary where
+	type Morphing (Rotate (Right Zig)) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Right Zig)
+
+instance Morphable (Rotate (Left (Zig Zig))) Binary where
+	type Morphing (Rotate (Left (Zig Zig))) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Left (Zig Zig))
+
+instance Morphable (Rotate (Right (Zig Zig))) Binary where
+	type Morphing (Rotate (Right (Zig Zig))) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Right (Zig Zig))
+
+instance Morphable (Rotate (Left (Zig Zag))) Binary where
+	type Morphing (Rotate (Left (Zig Zag))) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Left (Zig Zag))
+
+instance Morphable (Rotate (Right (Zig Zag))) Binary where
+	type Morphing (Rotate (Right (Zig Zag))) Binary = Binary
+	morphing (premorph -> binary) = unite $ run binary >>= run . rotate @(Right (Zig Zag))
+
+-------------------------------------- Non-empty Splay tree ----------------------------------------
+
 instance Morphable (Rotate (Left Zig)) (Construction Wye) where
 	type Morphing (Rotate (Left Zig)) (Construction Wye) = Binary
 	morphing :: forall a . (:#) (Rotate (Left Zig)) <:.> Construction Wye := a -> Binary a
@@ -50,21 +76,25 @@
 		parent :: Maybe a
 		parent = extract <$> branch @Left xs
 
+-- TODO: Morphing ... = Conclussion Error <:.> Nonempty Binary
 instance Morphable (Rotate (Left (Zig Zig))) (Construction Wye) where
 	type Morphing (Rotate (Left (Zig Zig))) (Construction Wye) = Binary
 	morphing (premorph -> tree) = TU $ run # rotate @(Left Zig) tree >>= run . rotate @(Left Zig)
 
+-- TODO: Morphing ... = Conclussion Error <:.> Nonempty Binary
 instance Morphable (Rotate (Right (Zig Zig))) (Construction Wye) where
 	type Morphing (Rotate (Right (Zig Zig))) (Construction Wye) = Binary
 	morphing (premorph -> tree) = TU $ run # rotate @(Right Zig) tree >>= run . rotate @(Right Zig)
 
+-- TODO: Morphing ... = Conclussion Error <:.> Nonempty Binary
 instance Morphable (Rotate (Left (Zig Zag))) (Construction Wye) where
 	type Morphing (Rotate (Left (Zig Zag))) (Construction Wye) = Binary
-	morphing = rotate @(Left Zig) . over (sub @Left) ((>>= run . rotate @(Right Zig)) ||=) . premorph
+	morphing = rotate @(Left Zig) . over (sub @Left) (>>= run . rotate @(Right Zig)) . premorph
 
+-- TODO: Morphing ... = Conclussion Error <:.> Nonempty Binary
 instance Morphable (Rotate (Right (Zig Zag))) (Construction Wye) where
 	type Morphing (Rotate (Right (Zig Zag))) (Construction Wye) = Binary
-	morphing = rotate @(Right Zig) . over (sub @Right) ((>>= run . rotate @(Left Zig)) ||=) . premorph
+	morphing = rotate @(Right Zig) . over (sub @Right) (>>= run . rotate @(Left Zig)) . premorph
 
 branch :: forall b . Morphable (Into (b Maybe)) Wye => Wye ~> Morphing (Into (b Maybe)) Wye
 branch = into @(b Maybe)
diff --git a/Pandora/Paradigm/Structure/Some/Stream.hs b/Pandora/Paradigm/Structure/Some/Stream.hs
--- a/Pandora/Paradigm/Structure/Some/Stream.hs
+++ b/Pandora/Paradigm/Structure/Some/Stream.hs
@@ -2,7 +2,7 @@
 
 module Pandora.Paradigm.Structure.Some.Stream where
 
-import Pandora.Core.Functor (type (:=), type (:=>))
+import Pandora.Core.Functor (type (:=), type (:=>), type (:::))
 import Pandora.Pattern.Category ((.), ($), (#))
 import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
 import Pandora.Pattern.Functor.Pointable (point)
@@ -19,7 +19,7 @@
 
 type Stream = Construction Identity
 
-type instance Zipper Stream = Tap (Stream <:.:> Stream := (:*:))
+type instance Zipper (Construction Identity) (Left ::: Right) = Tap (Stream <:.:> Stream := (:*:))
 
 instance Morphable (Rotate Left) (Tap (Stream <:.:> Stream := (:*:))) where
 	type Morphing (Rotate Left) (Tap (Stream <:.:> Stream := (:*:))) = Tap (Stream <:.:> Stream := (:*:))
diff --git a/Pandora/Pattern/Category.hs b/Pandora/Pattern/Category.hs
--- a/Pandora/Pattern/Category.hs
+++ b/Pandora/Pattern/Category.hs
@@ -4,6 +4,13 @@
 infixr 0 $
 infixr 9 .
 
+{- |
+> When providing a new instance, you should ensure it satisfies:
+> * Left identity: identity . f ≡ f
+> * Right identity: f . identity ≡ f
+> * Associativity: f . (g . h) ≡ (f . g) . h
+-}
+
 class Category (m :: * -> * -> *) where
 	identity :: m a a
 	(.) :: m b c -> m a b -> m a c
diff --git a/Pandora/Pattern/Functor/Invariant.hs b/Pandora/Pattern/Functor/Invariant.hs
--- a/Pandora/Pattern/Functor/Invariant.hs
+++ b/Pandora/Pattern/Functor/Invariant.hs
@@ -6,11 +6,11 @@
 > Interpreted of morphisms: invmap g j . invmap f h = invmap (g . f) (h . j)
 -}
 
-infixl 4 >-<
+infixl 4 <$<
 
 class Invariant (t :: * -> *) where
-	{-# MINIMAL (>-<) #-}
-	(>-<) :: (a -> b) -> (b -> a) -> t a -> t b
-	-- | Prefix version of '>-<'
+	{-# MINIMAL (<$<) #-}
+	(<$<) :: (a -> b) -> (b -> a) -> t a -> t b
+	-- | Prefix version of '<$<'
 	invmap :: (a -> b) -> (b -> a) -> t a -> t b
-	invmap f g x = (f >-< g) x
+	invmap f g x = (f <$< g) x
diff --git a/pandora.cabal b/pandora.cabal
--- a/pandora.cabal
+++ b/pandora.cabal
@@ -1,5 +1,5 @@
 name:                pandora
-version:             0.4.1
+version:             0.4.2
 synopsis:            A box of patterns and paradigms
 description:         Humble attempt to define a library for problem solving based on math abstractions.
 homepage:            https://github.com/iokasimov/pandora
@@ -22,6 +22,7 @@
     -- Axioms set
     Pandora.Core
     Pandora.Core.Functor
+    Pandora.Core.Impliable
 
     Pandora.Paradigm
     -- Basic constructions
@@ -72,6 +73,9 @@
     Pandora.Paradigm.Schemes.UTU
     Pandora.Paradigm.Schemes.T_U
     Pandora.Paradigm.Schemes.U_T
+    Pandora.Paradigm.Schemes.PTU
+    Pandora.Paradigm.Schemes.P_T
+    Pandora.Paradigm.Schemes.P_Q_T
     Pandora.Paradigm.Schemes.PQ_
     -- Control flow primitives
     Pandora.Paradigm.Controlflow
@@ -169,7 +173,7 @@
     Pandora.Pattern.Transformer.Lowerable
   default-extensions:
     DataKinds, ConstraintKinds, ExistentialQuantification, GADTs, QuantifiedConstraints, InstanceSigs
-    FlexibleContexts, FlexibleInstances, KindSignatures, LiberalTypeSynonyms, LambdaCase, FunctionalDependencies
+    FlexibleContexts, FlexibleInstances, KindSignatures, StandaloneKindSignatures, LiberalTypeSynonyms, LambdaCase, FunctionalDependencies
     MultiParamTypeClasses, NoImplicitPrelude, PackageImports, PolyKinds, RankNTypes, ViewPatterns
     ScopedTypeVariables, TypeApplications, TypeFamilies, TypeFamilyDependencies, TypeOperators
   default-language: Haskell2010