{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Primary (module Exports, twosome) where

import Pandora.Paradigm.Primary.Linear as Exports
import Pandora.Paradigm.Primary.Transformer as Exports
import Pandora.Paradigm.Primary.Functor as Exports
import Pandora.Paradigm.Primary.Object as Exports
import Pandora.Paradigm.Primary.Algebraic as Exports

import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Kernel (Kernel (constant))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((|-), (-|)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!))
import Pandora.Paradigm.Controlflow.Effect.Conditional (Conditional ((?)))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), 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 (Available, Substance, substructure))

instance Adjoint (->) (->) (Flip (:*:) s) ((->) s) where
	Flip (:*:) s a -> b
f -| :: (Flip (:*:) s a -> b) -> a -> s -> b
-| a
x = \s
s -> Flip (:*:) s a -> b
f (Flip (:*:) s a -> b)
-> ((a :*: s) -> Flip (:*:) s a) -> (a :*: s) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :*: s) -> Flip (:*:) s a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((a :*: s) -> b) -> (a :*: s) -> b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a
x a -> s -> a :*: s
forall s a. s -> a -> s :*: a
:*: s
s
	a -> s -> b
f |- :: (a -> s -> b) -> Flip (:*:) s a -> b
|- Flip (a
x :*: s
s) = a -> s -> b
f a
x s
s

instance Morphable (Into Maybe) (Conclusion e) where
	type Morphing (Into Maybe) (Conclusion e) = Maybe
	morphing :: (<::>) (Tagged ('Into Maybe)) (Conclusion e) a
-> Morphing ('Into Maybe) (Conclusion e) a
morphing = (e -> Maybe a) -> (a -> Maybe a) -> Conclusion e a -> Maybe a
forall e r a. (e -> r) -> (a -> r) -> Conclusion e a -> r
conclusion (Maybe a -> e -> Maybe a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant Maybe a
forall a. Maybe a
Nothing) a -> Maybe a
forall a. a -> Maybe a
Just (Conclusion e a -> Maybe a)
-> ((<::>) (Tagged ('Into Maybe)) (Conclusion e) a
    -> Conclusion e a)
-> (<::>) (Tagged ('Into Maybe)) (Conclusion e) a
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Maybe)) (Conclusion e) a -> Conclusion e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph

instance Morphable (Into (Conclusion e)) Maybe where
	type Morphing (Into (Conclusion e)) Maybe = (->) e <:.> Conclusion e
	morphing :: (<::>) (Tagged ('Into (Conclusion e))) Maybe a
-> Morphing ('Into (Conclusion e)) Maybe a
morphing ((<::>) (Tagged ('Into (Conclusion e))) Maybe a -> Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Just a
x) = (((->) e :. Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Conclusion e) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) e :. Conclusion e) := a)
 -> TU Covariant Covariant ((->) e) (Conclusion e) a)
-> (((->) e :. Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Conclusion e) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \e
_ -> a -> Conclusion e a
forall e a. a -> Conclusion e a
Success a
x
	morphing ((<::>) (Tagged ('Into (Conclusion e))) Maybe a -> Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Maybe a
Nothing) = (((->) e :. Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Conclusion e) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) e :. Conclusion e) := a)
 -> TU Covariant Covariant ((->) e) (Conclusion e) a)
-> (((->) e :. Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Conclusion e) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \e
e -> ((->) e :. Conclusion e) := a
forall e a. e -> Conclusion e a
Failure e
e

instance Morphable (Into (Flip Conclusion e)) Maybe where
	type Morphing (Into (Flip Conclusion e)) Maybe = (->) e <:.> Flip Conclusion e
	morphing :: (<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a
-> Morphing ('Into (Flip Conclusion e)) Maybe a
morphing (Maybe a -> Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Maybe a -> Maybe a)
-> ((<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a -> Maybe a)
-> (<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a -> Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Just a
x) = (((->) e :. Flip Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Flip Conclusion e) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) e :. Flip Conclusion e) := a)
 -> TU Covariant Covariant ((->) e) (Flip Conclusion e) a)
-> (((->) e :. Flip Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Flip Conclusion e) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \e
_ -> Conclusion a e -> Flip Conclusion e a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Conclusion a e -> Flip Conclusion e a)
-> Conclusion a e -> Flip Conclusion e a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Conclusion a e
forall e a. e -> Conclusion e a
Failure a
x
	morphing (Maybe a -> Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Maybe a -> Maybe a)
-> ((<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a -> Maybe a)
-> (<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a
-> Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into (Flip Conclusion e))) Maybe a -> Maybe a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Maybe a
Nothing) = (((->) e :. Flip Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Flip Conclusion e) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU ((((->) e :. Flip Conclusion e) := a)
 -> TU Covariant Covariant ((->) e) (Flip Conclusion e) a)
-> (((->) e :. Flip Conclusion e) := a)
-> TU Covariant Covariant ((->) e) (Flip Conclusion e) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Conclusion a e -> Flip Conclusion e a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Conclusion a e -> Flip Conclusion e a)
-> (e -> Conclusion a e) -> ((->) e :. Flip Conclusion e) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> Conclusion a e
forall e a. a -> Conclusion e a
Success

instance Morphable (Into (Left Maybe)) Wye where
	type Morphing (Into (Left Maybe)) Wye = Maybe
	morphing :: (<::>) (Tagged ('Into ('Left Maybe))) Wye a
-> Morphing ('Into ('Left Maybe)) Wye a
morphing ((<::>) (Tagged ('Into ('Left Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Both a
ls a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
ls
	morphing ((<::>) (Tagged ('Into ('Left Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Left a
ls) = a -> Maybe a
forall a. a -> Maybe a
Just a
ls
	morphing ((<::>) (Tagged ('Into ('Left Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Right a
_) = Morphing ('Into ('Left Maybe)) Wye a
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into ('Left Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Wye a
End) = Morphing ('Into ('Left Maybe)) Wye a
forall a. Maybe a
Nothing

instance Morphable (Into (Right Maybe)) Wye where
	type Morphing (Into (Right Maybe)) Wye = Maybe
	morphing :: (<::>) (Tagged ('Into ('Right Maybe))) Wye a
-> Morphing ('Into ('Right Maybe)) Wye a
morphing ((<::>) (Tagged ('Into ('Right Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Both a
_ a
rs) = a -> Maybe a
forall a. a -> Maybe a
Just a
rs
	morphing ((<::>) (Tagged ('Into ('Right Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Left a
_) = Morphing ('Into ('Right Maybe)) Wye a
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into ('Right Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Right a
rs) = a -> Maybe a
forall a. a -> Maybe a
Just a
rs
	morphing ((<::>) (Tagged ('Into ('Right Maybe))) Wye a -> Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Wye a
End) = Morphing ('Into ('Right Maybe)) Wye a
forall a. Maybe a
Nothing

instance Morphable (Into (This Maybe)) (These e) where
	type Morphing (Into (This Maybe)) (These e) = Maybe
	morphing :: (<::>) (Tagged ('Into ('This Maybe))) (These e) a
-> Morphing ('Into ('This Maybe)) (These e) a
morphing ((<::>) (Tagged ('Into ('This Maybe))) (These e) a -> These e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> This a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
	morphing ((<::>) (Tagged ('Into ('This Maybe))) (These e) a -> These e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> That e
_) = Morphing ('Into ('This Maybe)) (These e) a
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into ('This Maybe))) (These e) a -> These e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> These e
_ a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x

instance Morphable (Into (That Maybe)) (Flip These a) where
	type Morphing (Into (That Maybe)) (Flip These a) = Maybe
	morphing :: (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> Morphing ('Into ('That Maybe)) (Flip These a) a
morphing (Flip These a a -> These a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip These a a -> These a a)
-> ((<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
    -> Flip These a a)
-> (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> These a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> Flip These a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> This a
_) = Morphing ('Into ('That Maybe)) (Flip These a) a
forall a. Maybe a
Nothing
	morphing (Flip These a a -> These a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip These a a -> These a a)
-> ((<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
    -> Flip These a a)
-> (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> These a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> Flip These a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> That a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
	morphing (Flip These a a -> These a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip These a a -> These a a)
-> ((<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
    -> Flip These a a)
-> (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> These a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('That Maybe))) (Flip These a) a
-> Flip These a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> These a
y a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
y

instance Morphable (Into (Here Maybe)) (Flip Wedge a) where
	type Morphing (Into (Here Maybe)) (Flip Wedge a) = Maybe
	morphing :: (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Morphing ('Into ('Here Maybe)) (Flip Wedge a) a
morphing (Flip Wedge a a -> Wedge a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip Wedge a a -> Wedge a a)
-> ((<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
    -> Flip Wedge a a)
-> (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Wedge a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Flip Wedge a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Wedge a a
Nowhere) = Morphing ('Into ('Here Maybe)) (Flip Wedge a) a
forall a. Maybe a
Nothing
	morphing (Flip Wedge a a -> Wedge a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip Wedge a a -> Wedge a a)
-> ((<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
    -> Flip Wedge a a)
-> (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Wedge a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Flip Wedge a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Here a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
	morphing (Flip Wedge a a -> Wedge a a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip Wedge a a -> Wedge a a)
-> ((<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
    -> Flip Wedge a a)
-> (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Wedge a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into ('Here Maybe))) (Flip Wedge a) a
-> Flip Wedge a a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> There a
_) = Morphing ('Into ('Here Maybe)) (Flip Wedge a) a
forall a. Maybe a
Nothing

instance Morphable (Into (There Maybe)) (Wedge e) where
	type Morphing (Into (There Maybe)) (Wedge e) = Maybe
	morphing :: (<::>) (Tagged ('Into ('There Maybe))) (Wedge e) a
-> Morphing ('Into ('There Maybe)) (Wedge e) a
morphing ((<::>) (Tagged ('Into ('There Maybe))) (Wedge e) a -> Wedge e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Wedge e a
Nowhere) = Morphing ('Into ('There Maybe)) (Wedge e) a
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into ('There Maybe))) (Wedge e) a -> Wedge e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Here e
_) = Morphing ('Into ('There Maybe)) (Wedge e) a
forall a. Maybe a
Nothing
	morphing ((<::>) (Tagged ('Into ('There Maybe))) (Wedge e) a -> Wedge e a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> There a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x

instance Morphable (Into Wye) (Maybe <:.:> Maybe := (:*:)) where
	type Morphing (Into Wye) (Maybe <:.:> Maybe := (:*:)) = Wye
	morphing :: (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> Morphing ('Into Wye) ((Maybe <:.:> Maybe) := (:*:)) a
morphing ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a)
-> ((<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
    -> (:=) (Maybe <:.:> Maybe) (:*:) a)
-> (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> Maybe a :*: Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> (:=) (Maybe <:.:> Maybe) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Just a
x :*: Just a
y) = a -> a -> Wye a
forall a. a -> a -> Wye a
Both a
x a
y
	morphing ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a)
-> ((<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
    -> (:=) (Maybe <:.:> Maybe) (:*:) a)
-> (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> Maybe a :*: Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> (:=) (Maybe <:.:> Maybe) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Maybe a
Nothing :*: Just a
y) = a -> Wye a
forall a. a -> Wye a
Right a
y
	morphing ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a)
-> ((<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
    -> (:=) (Maybe <:.:> Maybe) (:*:) a)
-> (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> Maybe a :*: Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> (:=) (Maybe <:.:> Maybe) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Just a
x :*: Maybe a
Nothing) = a -> Wye a
forall a. a -> Wye a
Left a
x
	morphing ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (Maybe <:.:> Maybe) (:*:) a -> Maybe a :*: Maybe a)
-> ((<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
    -> (:=) (Maybe <:.:> Maybe) (:*:) a)
-> (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> Maybe a :*: Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>) (Tagged ('Into Wye)) ((Maybe <:.:> Maybe) := (:*:)) a
-> (:=) (Maybe <:.:> Maybe) (:*:) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Maybe a
Nothing :*: Maybe a
Nothing) = Morphing ('Into Wye) ((Maybe <:.:> Maybe) := (:*:)) a
forall a. Wye a
End

instance Substructure Left Wye where
	type Available Left Wye = Maybe
	type Substance Left Wye = Exactly
	substructure :: Lens
  (Available 'Left Wye)
  ((<:.>) (Tagged 'Left) Wye a)
  (Substance 'Left Wye a)
substructure = ((<:.>) (Tagged 'Left) Wye a
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> P_Q_T (->) Store Maybe ((<:.>) (Tagged 'Left) Wye a) (Exactly 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) Wye a
  -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
 -> P_Q_T
      (->) Store Maybe ((<:.>) (Tagged 'Left) Wye a) (Exactly a))
-> ((<:.>) (Tagged 'Left) Wye a
    -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> P_Q_T (->) Store Maybe ((<:.>) (Tagged 'Left) Wye a) (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) Wye a
new -> case (<:.>) (Tagged 'Left) Wye a -> Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) Wye a
new of
		Wye a
End -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Left) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Exactly a)
forall a. Maybe a
Nothing Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Left) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Left) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Left) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Left) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Left) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve a -> Wye a
forall a. a -> Wye a
Left Wye a
forall a. Wye a
End (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Left a
x -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Left) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Maybe (Exactly a)
forall a. a -> Maybe a
Just (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x) Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Left) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Left) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Left) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Left) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Left) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve a -> Wye a
forall a. a -> Wye a
Left Wye a
forall a. Wye a
End (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Right a
y -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Left) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Exactly a)
forall a. Maybe a
Nothing Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Left) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Left) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Left) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Left) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Left) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Wye a -> Maybe a -> Wye a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (a -> Wye a
forall a. a -> Wye a
Right a
y) (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Both a
x a
y -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Left) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Left) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Left) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Maybe (Exactly a)
forall a. a -> Maybe a
Just (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x) Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Left) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Left) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Left) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Left) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Left) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a -> a -> Wye a
forall a. a -> a -> Wye a
Both (a -> a -> Wye a) -> a -> a -> Wye a
forall a b c. (a -> b -> c) -> b -> a -> c
% a
y) (a -> Wye a
forall a. a -> Wye a
Right a
y) (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)

instance Substructure Right Wye where
	type Available Right Wye = Maybe
	type Substance Right Wye = Exactly
	substructure :: Lens
  (Available 'Right Wye)
  ((<:.>) (Tagged 'Right) Wye a)
  (Substance 'Right Wye a)
substructure = ((<:.>) (Tagged 'Right) Wye a
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> P_Q_T
     (->) Store Maybe ((<:.>) (Tagged 'Right) Wye a) (Exactly 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) Wye a
  -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
 -> P_Q_T
      (->) Store Maybe ((<:.>) (Tagged 'Right) Wye a) (Exactly a))
-> ((<:.>) (Tagged 'Right) Wye a
    -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> P_Q_T
     (->) Store Maybe ((<:.>) (Tagged 'Right) Wye a) (Exactly a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) Wye a
new -> case (<:.>) (Tagged 'Right) Wye a -> Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) Wye a
new of
		Wye a
End -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Right) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Exactly a)
forall a. Maybe a
Nothing Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Right) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Right) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Right) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Right) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Right) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve a -> Wye a
forall a. a -> Wye a
Right Wye a
forall a. Wye a
End (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Left a
x -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Right) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe (Exactly a)
forall a. Maybe a
Nothing Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Right) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Right) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Right) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Right) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Right) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Wye a -> Maybe a -> Wye a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (a -> Wye a
forall a. a -> Wye a
Left a
x) (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Right a
y -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Right) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Maybe (Exactly a)
forall a. a -> Maybe a
Just (a -> Exactly a
forall a. a -> Exactly a
Exactly a
y) Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Right) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Right) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Right) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Right) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Right) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve a -> Wye a
forall a. a -> Wye a
Right Wye a
forall a. Wye a
End (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
		Both a
x a
y -> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
 := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
  := (<:.>) (Tagged 'Right) Wye a)
 -> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a))
-> (((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
    := (<:.>) (Tagged 'Right) Wye a)
-> Store (Maybe (Exactly a)) ((<:.>) (Tagged 'Right) Wye a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Exactly a -> Maybe (Exactly a)
forall a. a -> Maybe a
Just (a -> Exactly a
forall a. a -> Exactly a
Exactly a
y) Maybe (Exactly a)
-> (Maybe (Exactly a) -> (<:.>) (Tagged 'Right) Wye a)
-> ((:*:) (Maybe (Exactly a)) :. (->) (Maybe (Exactly a)))
   := (<:.>) (Tagged 'Right) Wye a
forall s a. s -> a -> s :*: a
:*: Wye a -> (<:.>) (Tagged 'Right) Wye a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Wye a -> (<:.>) (Tagged 'Right) Wye a)
-> (Maybe (Exactly a) -> Wye a)
-> Maybe (Exactly a)
-> (<:.>) (Tagged 'Right) Wye a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Wye a) -> Wye a -> Maybe a -> Wye a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (a -> a -> Wye a
forall a. a -> a -> Wye a
Both a
x) (a -> Wye a
forall a. a -> Wye a
Left a
x) (Maybe a -> Wye a)
-> (Maybe (Exactly a) -> Maybe a) -> Maybe (Exactly a) -> Wye 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 (Exactly a -> a) -> Maybe (Exactly a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)

instance (Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => Semimonoidal (-->) (:*:) (:*:) (t <:.:> u := (:*:)) where
	mult :: ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
--> (:=) (t <:.:> u) (:*:) (a :*: b)
mult = (((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
 -> (:=) (t <:.:> u) (:*:) (a :*: b))
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   --> (:=) (t <:.:> u) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
  -> (:=) (t <:.:> u) (:*:) (a :*: b))
 -> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
    --> (:=) (t <:.:> u) (:*:) (a :*: b))
-> (((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
    -> (:=) (t <:.:> u) (:*:) (a :*: b))
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   --> (:=) (t <:.:> u) (:*:) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(T_U (t a
xls :*: u a
xrs) :*: T_U (t b
yls :*: u b
yrs)) -> (t (a :*: b) :*: u (a :*: b)) -> (:=) (t <:.:> u) (:*:) (a :*: b)
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t (a :*: b) :*: u (a :*: b)) -> (:=) (t <:.:> u) (:*:) (a :*: b))
-> (t (a :*: b) :*: u (a :*: b))
-> (:=) (t <:.:> u) (:*:) (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) (t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls) t (a :*: b) -> u (a :*: b) -> t (a :*: b) :*: u (a :*: b)
forall s a. s -> a -> s :*: a
:*: (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((u a :*: u b) --> u (a :*: b)) -> (u a :*: u b) -> u (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) (u a
xrs u a -> u b -> u a :*: u b
forall s a. s -> a -> s :*: a
:*: u b
yrs)

twosome :: t a -> u a -> (<:.:>) t u (:*:) a
twosome :: t a -> u a -> (<:.:>) t u (:*:) a
twosome t a
x u a
y = (t a :*: u a) -> (<:.:>) t u (:*:) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: u a) -> (<:.:>) t u (:*:) a)
-> (t a :*: u a) -> (<:.:>) t u (:*:) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a
x t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
y