{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Schemes.UT where

import Pandora.Core.Functor (type (:.), type (:=), type (~>))
import Pandora.Pattern.Betwixt (Betwixt)
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (identity)
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)), (<-|-|-))
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<--)))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (!), (=#-)))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (point, extract, (<-||-))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))

newtype UT ct cu t u a = UT (u :. t := a)

infixr 3 <.:>, >.:>, <.:<, >.:<

type (<.:>) = UT Covariant Covariant
type (>.:>) = UT Contravariant Covariant
type (<.:<) = UT Covariant Contravariant
type (>.:<) = UT Contravariant Contravariant

instance Interpreted (->) (UT ct cu t u) where
	type Primary (UT ct cu t u) a = u :. t := a
	run :: UT ct cu t u a -> Primary (UT ct cu t u) a
run ~(UT (u :. t) := a
x) = (u :. t) := a
Primary (UT ct cu t u) a
x
	unite :: Primary (UT ct cu t u) a -> UT ct cu t u a
unite = Primary (UT ct cu t u) a -> UT ct cu t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT

instance (Semigroupoid m, Covariant m m u, Covariant m m t, Covariant m (Betwixt m m) t, Covariant (Betwixt m m) m u, Interpreted m (t <.:> u)) => Covariant m m (t <.:> u) where
	<-|- :: m a b -> m ((<.:>) t u a) ((<.:>) t u b)
(<-|-) m a b
f = m (Primary (t <.:> u) a) (Primary (t <.:> u) b)
-> m ((<.:>) t u a) ((<.:>) t u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(=#-) (m a b -> m (u (t a)) (u (t b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-) m a b
f)

instance (Covariant (->) (->) u, 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)
! ((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b)
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> (u :. t) := (a :*: b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> (<.:>) t u (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t a :*: t b) -> t (a :*: b))
-> u (t a :*: t b) -> (u :. t) := (a :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) (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)
!) (u (t a :*: t b) -> (u :. t) := (a :*: b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> u (t a :*: t b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> (u :. t) := (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (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 (t a) :*: u (t b)) --> u (t a :*: t b))
-> (u (t a) :*: u (t b)) -> u (t a :*: t b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) ((u (t a) :*: u (t b)) -> u (t a :*: t b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> u (t a) :*: u (t b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> u (t a :*: t b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((<.:>) t u a -> u (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<.:>) t u a -> u (t a))
-> ((<.:>) t u a :*: u (t b)) -> u (t a) :*: u (t b)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) (((<.:>) t u a :*: u (t b)) -> u (t a) :*: u (t b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u a :*: u (t b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> u (t a) :*: u (t b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall (t :: * -> *) a. Interpreted (->) t => t a -> Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) ((<.:>) t u b -> u (t b))
-> ((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u a :*: u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)

instance (Covariant (->) (->) u, Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) u, Semimonoidal (-->) (:*:) (:+:) t) => 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)
! \(UT (u :. t) := a
x :*: UT (u :. t) := b
y) -> ((u :. t) := (a :+: b)) -> (<.:>) t u (a :+: b)
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := (a :+: b)) -> (<.:>) t u (a :+: b))
-> ((u :. t) := (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 (t :: * -> *) a b.
Semimonoidal (-->) (:*:) (:+:) t =>
(t a :*: t b) --> t (a :+: b)
mult @(-->) @(:*:) @(:+:)) ((t a :*: t b) --> t (a :+: b))
-> u (t a :*: t b) -> (u :. t) := (a :+: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (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 (t :: * -> *) a b.
Semimonoidal (-->) (:*:) (:*:) t =>
(t a :*: t b) --> t (a :*: b)
mult @(-->) @(:*:) @(:*:) ((((u :. t) := a) :*: ((u :. t) := b)) --> u (t a :*: t b))
-> (((u :. t) := a) :*: ((u :. t) := b)) -> u (t a :*: t b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((u :. t) := a
x ((u :. t) := a)
-> ((u :. t) := b) -> ((u :. t) := a) :*: ((u :. t) := b)
forall s a. s -> a -> s :*: a
:*: (u :. t) := b
y))

instance (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) u, Monoidal (-->) (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:*:) u) => Monoidal (-->) (-->) (:*:) (:*:) (t <.:> u) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> (<.:>) t u a
unit Proxy (:*:)
_ = ((One --> a) -> (<.:>) t u a)
-> Straight (->) (One --> a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One --> a) -> (<.:>) t u a)
 -> Straight (->) (One --> a) ((<.:>) t u a))
-> ((One --> a) -> (<.:>) t u a)
-> Straight (->) (One --> a) ((<.:>) t u a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((u :. t) := a) -> (<.:>) t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> (<.:>) t u a)
-> ((One --> a) -> (u :. t) := a) -> (One --> a) -> (<.:>) t u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. t a -> (u :. t) := a
forall (t :: * -> *) a. Pointable t => a -> t a
point (t a -> (u :. t) := a)
-> ((One --> a) -> t a) -> (One --> a) -> (u :. t) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> t a) -> ((One --> a) -> a) -> (One --> a) -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! One
One) ((One -> a) -> a) -> ((One --> a) -> One -> a) -> (One --> a) -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (One --> a) -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run

instance (Traversable (->) (->) t, Bindable (->) t, Semimonoidal (-->) (:*:) (:*:) u, Monoidal (-->) (-->) (:*:) (:*:) u, Bindable (->) u) => Bindable (->) (t <.:> u) where
	a -> (<.:>) t u b
f =<< :: (a -> (<.:>) t u b) -> (<.:>) t u a -> (<.:>) t u b
=<< UT (u :. t) := a
x = ((u :. t) := b) -> (<.:>) t u b
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := b) -> (<.:>) t u b)
-> ((u :. t) := b) -> (<.:>) t u b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((t b -> t b
forall (m :: * -> * -> *) a. Category m => m a a
identity (t b -> t b) -> t (t b) -> t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<<) (t (t b) -> t b) -> u (t (t b)) -> (u :. t) := b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (u (t (t b)) -> (u :. t) := b)
-> (t a -> u (t (t b))) -> t a -> (u :. t) := b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((<.:>) t u b -> (u :. t) := b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((<.:>) t u b -> (u :. t) := b)
-> (a -> (<.:>) t u b) -> a -> (u :. t) := b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> (<.:>) t u b
f (a -> (u :. t) := b) -> t a -> u (t (t b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<--) (t a -> (u :. t) := b) -> ((u :. t) := a) -> (u :. t) := b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< (u :. t) := a
x

instance (Covariant (->) (->) u, Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <.:> u) where
	mult :: ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b)
mult = ((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b)
-> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b)
 -> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b))
-> ((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b)
-> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(UT (u :. t) := (a :*: b)
xys) -> (((u :. t) := a) -> (<.:>) t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> (<.:>) t u a)
-> (((u :. t) := a) :*: (<.:>) t u b)
-> (<.:>) t u a :*: (<.:>) t u b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) ((((u :. t) := a) :*: (<.:>) t u b)
 -> (<.:>) t u a :*: (<.:>) t u b)
-> (u (t a :*: t b) -> ((u :. t) := a) :*: (<.:>) t u b)
-> u (t a :*: t b)
-> (<.:>) t u a :*: (<.:>) t u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((u :. t) := b) -> (<.:>) t u b
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := b) -> (<.:>) t u b)
-> (((u :. t) := a) :*: ((u :. t) := b))
-> ((u :. t) := a) :*: (<.:>) t u b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) ((((u :. t) := a) :*: ((u :. t) := b))
 -> ((u :. t) := a) :*: (<.:>) t u b)
-> (u (t a :*: t b) -> ((u :. t) := a) :*: ((u :. t) := b))
-> u (t a :*: t b)
-> ((u :. t) := a) :*: (<.:>) t u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (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 :. t) := a) :*: ((u :. t) := b)) <-- u (t a :*: t b))
-> u (t a :*: t b) -> ((u :. t) := a) :*: ((u :. t) := b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) (u (t a :*: t b) -> (<.:>) t u a :*: (<.:>) t u b)
-> u (t a :*: t b) -> (<.:>) t u a :*: (<.:>) t u 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 :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
!) (t (a :*: b) -> t a :*: t b)
-> ((u :. t) := (a :*: b)) -> u (t a :*: t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (u :. t) := (a :*: b)
xys

instance (Covariant (->) (->) u, Monoidal (<--) (-->) (:*:) (:*:) t, Monoidal (<--) (-->) (:*:) (:*:) u) => Monoidal (<--) (-->) (:*:) (:*:) (t <.:> u) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- (<.:>) t u a
unit Proxy (:*:)
_ = ((<.:>) t u a -> One --> a) -> Flip (->) (One --> a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<.:>) t u a -> One --> a)
 -> Flip (->) (One --> a) ((<.:>) t u a))
-> ((<.:>) t u a -> One --> a)
-> Flip (->) (One --> a) ((<.:>) t u a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(UT (u :. t) := a
x) -> (One -> a) -> One --> a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (t a -> a) -> t a -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((u :. t) := a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (u :. t) := a
x)

instance Monoidal (-->) (-->) (:*:) (:*:) t => Liftable (->) (UT Covariant Covariant t) where
	lift :: Covariant (->) (->) u => u ~> t <.:> u
	lift :: u ~> (t <.:> u)
lift u a
x = ((u :. t) := a) -> UT Covariant Covariant t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> UT Covariant Covariant t u a)
-> ((u :. t) := a) -> UT Covariant Covariant t u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> t a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> t a) -> u a -> (u :. t) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- u a
x

instance Monoidal (<--) (-->) (:*:) (:*:) t => Lowerable (->) (UT Covariant Covariant t) where
	lower :: Covariant (->) (->) u => t <.:> u ~> u
	lower :: (t <.:> u) ~> u
lower (UT (u :. t) := a
x) = t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (t a -> a) -> ((u :. t) := a) -> u a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (u :. t) := a
x