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

import Pandora.Core.Functor (type (:.), type (>>>), type (~>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~), (<~~~), (<~~~~), (=#-)))
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.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(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 :: * -> * -> *) a b. Category m => m (m a b) (m a 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 @(-->) @(:*:) @(:+:)
			((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 (:*:)
_ = (Straight (->) One a -> (<.:>) t u a)
-> Straight (->) (Straight (->) One a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> (<.:>) t u a)
 -> Straight (->) (Straight (->) One a) ((<.:>) t u a))
-> (Straight (->) One a -> (<.:>) t u a)
-> Straight (->) (Straight (->) One a) ((<.:>) t u a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((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)
-> (Straight (->) One a -> (u :. t) >>> a)
-> Straight (->) 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)
-> (Straight (->) One a -> t a)
-> Straight (->) 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)
-> (Straight (->) One a -> a) -> Straight (->) One a -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- ((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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(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) >>> 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)
<-|--- 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
<~~~~ (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 -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<.:>) t u a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) ((<.:>) t u a))
-> ((<.:>) t u a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) ((<.:>) t u a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(UT (u :. t) >>> a
x) -> (One -> a) -> Straight (->) 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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((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 :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- 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