{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Algebraic.Functor where

import Pandora.Core.Interpreted (Interpreted ((<~), (<~~~), (-#=), run))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Trip (Trip)
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), Unit)
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
import Pandora.Paradigm.Algebraic.Exponential (type (-->), type (<--), (&))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:) (Option, Adoption))
import Pandora.Paradigm.Algebraic.Zero (Zero, absurd)
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Functor.Proxy (Proxy (Proxy))

infixl 1 <-*------, <-||-----, >-||-----
infixl 2 <-*-----, <-||----, >-||----
infixl 3 <-*----, <-||---, >-||---
infixl 4 <-*---, <-*-*-, <-||--, >-||--
infixl 5 <-*--, <-||-, >-||-
infixl 6 <-*-, <-+-

infixr 1 --------*
infixr 2 -------*
infixr 3 ------*
infixr 4 -----*
infixr 5 ----*, -*-*-
infixr 6 ---*
infixr 7 --*
infixr 8 -*, -+

infixl 6 <-|-<-|-, <-|->-|-, >-|-<-|-, >-|->-|-

type instance Unit (:*:) = One
type instance Unit (:+:) = Zero

type Applicative t = (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Monoidal (-->) (-->) (:*:) (:*:) t)
type Alternative t = (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t, Monoidal (-->) (-->) (:*:) (:+:) t)
type Divisible t = (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t, Monoidal (-->) (<--) (:*:) (:*:) t)
type Decidable t = (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:+:) t, Monoidal (-->) (<--) (:*:) (:+:) t)

instance Adjoint (->) (->) ((:*:) s) ((->) s) where
	(-|) :: ((s :*: a) -> b) -> a -> (s -> b)
	(s :*: a) -> b
f -| :: ((s :*: a) -> b) -> a -> s -> b
-| a
x = \s
s -> (s :*: a) -> b
f (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x)
	(|-) :: (a -> s -> b) -> (s :*: a) -> b
	a -> s -> b
f |- :: (a -> s -> b) -> (s :*: a) -> b
|- ~(s
s :*: a
x) = a -> s -> b
f a
x s
s

(<-*--------), (<-*-------), (<-*------), (<-*-----), (<-*----), (<-*---), (<-*--), (<-*-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t (a -> b) -> t a -> t b
t (a -> b)
f <-*-------- :: t (a -> b) -> t a -> t b
<-*-------- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*------- :: t (a -> b) -> t a -> t b
<-*------- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*------ :: t (a -> b) -> t a -> t b
<-*------ t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*----- :: t (a -> b) -> t a -> t b
<-*----- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*---- :: t (a -> b) -> t a -> t b
<-*---- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*--- :: t (a -> b) -> t a -> t b
<-*--- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*-- :: t (a -> b) -> t a -> t b
<-*-- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x
t (a -> b)
f <-*- :: t (a -> b) -> t a -> t b
<-*- t a
x = (a -> (a -> b) -> b) -> ((a -> b) :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
(|-) @(->) @(->) a -> (a -> b) -> b
forall a b. a -> (a -> b) -> b
(&) (((a -> b) :*: a) -> b) -> t ((a -> b) :*: a) -> t 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 @(-->) @_ @(:*:) ((t (a -> b) :*: t a) --> t ((a -> b) :*: a))
-> (t (a -> b) :*: t a) -> t ((a -> b) :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t (a -> b)
f t (a -> b) -> t a -> t (a -> b) :*: t a
forall s a. s -> a -> s :*: a
:*: t a
x

(--------*), (-------*), (------*), (-----*), (----*), (---*), (--*), (-*)
	:: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t a -> t b -> t b
t a
x --------* :: t a -> t b -> t b
--------* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x -------* :: t a -> t b -> t b
-------* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x ------* :: t a -> t b -> t b
------* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x -----* :: t a -> t b -> t b
-----* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x ----* :: t a -> t b -> t b
----* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x ---* :: t a -> t b -> t b
---* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x --* :: t a -> t b -> t b
--* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y
t a
x -* :: t a -> t b -> t b
-* t b
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t a -> t (b -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x t (b -> b) -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t b
y

(<-*-*-) :: (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => t (u (a -> b)) -> t (u a) -> t (u b)
t (u (a -> b))
f <-*-*- :: t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- t (u a)
x = u (a -> b) -> u a -> u b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
(<-*-) (u (a -> b) -> u a -> u b) -> t (u (a -> b)) -> t (u a -> u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t (u (a -> b))
f t (u a -> u b) -> t (u a) -> t (u b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t (u a)
x

(-*-*-) :: (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => t (u a) -> t (u b) -> t (u b)
t (u a)
x -*-*- :: t (u a) -> t (u b) -> t (u b)
-*-*- t (u b)
y = (\a
_ b
y' -> b
y') (a -> b -> b) -> t (u a) -> t (u (b -> 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))
<-|-|- t (u a)
x t (u (b -> b)) -> t (u b) -> t (u b)
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant (->) (->) t, Covariant (->) (->) u,
 Semimonoidal (-->) (:*:) (:*:) t,
 Semimonoidal (-->) (:*:) (:*:) u) =>
t (u (a -> b)) -> t (u a) -> t (u b)
<-*-*- t (u b)
y

(<-+-) :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) => t b -> t a -> (a :+: b -> r) -> t r
t b
y <-+- :: t b -> t a -> ((a :+: b) -> r) -> t r
<-+- t a
x = \(a :+: b) -> r
f -> (a :+: b) -> r
f ((a :+: b) -> r) -> t (a :+: b) -> t r
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
<~~~ t a
x t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
y

(--------+), (-------+), (------+), (-----+), (----+), (---+), (--+), (-+)
	:: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:+:) t) => t a -> t a -> t a
t a
x --------+ :: t a -> t a -> t a
--------+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x -------+ :: t a -> t a -> t a
-------+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x ------+ :: t a -> t a -> t a
------+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x -----+ :: t a -> t a -> t a
-----+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x ----+ :: t a -> t a -> t a
----+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x ---+ :: t a -> t a -> t a
---+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x --+ :: t a -> t a -> t a
--+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y
t a
x -+ :: t a -> t a -> t a
-+ t a
y = (\a :+: a
r -> case a :+: a
r of Option a
rx -> a
rx; Adoption a
ry -> a
ry) ((a :+: a) -> a) -> t (a :+: a) -> t a
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 a) --> t (a :+: a)) -> (t a :*: t a) -> t (a :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
x t a -> t a -> t a :*: t a
forall s a. s -> a -> s :*: a
:*: t a
y

loop :: (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t a -> t b
loop :: t a -> t b
loop t a
x = let r :: t b
r = t a
x t a -> t b -> t b
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t a -> t b -> t b
-* t b
r in t b
r

type Extractable t = Monoidal (<--) (-->) (:*:) (:*:) t
type Pointable t = Monoidal (-->) (-->) (:*:) (:*:) t
type Emptiable t = Monoidal (-->) (-->) (:*:) (:+:) t

extract :: Extractable t => t a -> a
extract :: t a -> a
extract t a
j = Proxy (:*:) -> (Unit (:*:) --> a) <-- t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(<--) @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Flip (->) (Straight (->) One a) (t a) -> t a -> Straight (->) One a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ t a
j Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One

point :: Pointable t => a -> t a
point :: a -> t a
point a
x = Proxy (:*:) -> Straight (->) (Unit (:*:)) a --> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Straight (->) (Straight (->) One a) (t a)
-> Straight (->) One a -> t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((One -> a) -> Straight (->) One a)
-> (One -> a) -> Straight (->) One a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \One
One -> a
x

pass :: Pointable t => t ()
pass :: t ()
pass = () -> t ()
forall (t :: * -> *) a. Pointable t => a -> t a
point ()

empty :: Emptiable t => t a
empty :: t a
empty = Proxy (:*:) -> Straight (->) (Unit (:+:)) a --> t a
forall (p :: * -> * -> *) (q :: * -> * -> *)
       (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a.
Monoidal p q source target t =>
Proxy source -> p (q (Unit target) a) (t a)
unit @(-->) Proxy (:*:)
forall k (a :: k). Proxy a
Proxy Straight (->) (Straight (->) Zero a) (t a)
-> Straight (->) Zero a -> t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (Zero -> a) -> Straight (->) Zero a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight Zero -> a
forall a. Zero -> a
absurd

-- TODO: Rename <-||- to <<-|-
(<-||-), (<-||--), (<-||---), (<-||----), (<-||-----), (<-||------), (<-||-------), (<-||--------)
	:: 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)
<-||-------- :: m a b -> m (p a c) (p b c)
(<-||--------) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||------- :: m a b -> m (p a c) (p b c)
(<-||-------) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||------ :: m a b -> m (p a c) (p b c)
(<-||------) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||----- :: m a b -> m (p a c) (p b c)
(<-||-----) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||---- :: m a b -> m (p a c) (p b c)
(<-||----) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||--- :: m a b -> m (p a c) (p b c)
(<-||---) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||-- :: m a b -> m (p a c) (p b c)
(<-||--) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-||- :: m a b -> m (p a c) (p b c)
(<-||-) m a b
f = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)

-- TODO: Rename <-|||- to <<<-|-
(<-|||-), (<-|||--), (<-|||---), (<-|||----), (<-|||-----), (<-|||------), (<-|||-------), (<-|||--------)
	:: forall (m :: * -> * -> *) (v :: * -> * -> * -> *) a b c d .
	(Covariant m m (Trip v d c), Interpreted m (Trip v d c)) => m a b -> m (v a c d) (v b c d)
<-|||-------- :: m a b -> m (v a c d) (v b c d)
(<-|||--------) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||------- :: m a b -> m (v a c d) (v b c d)
(<-|||-------) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||------ :: m a b -> m (v a c d) (v b c d)
(<-|||------) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||----- :: m a b -> m (v a c d) (v b c d)
(<-|||-----) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||---- :: m a b -> m (v a c d) (v b c d)
(<-|||----) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||--- :: m a b -> m (v a c d) (v b c d)
(<-|||---) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||-- :: m a b -> m (v a c d) (v b c d)
(<-|||--) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)
<-|||- :: m a b -> m (v a c d) (v b c d)
(<-|||-) m a b
f = ((m < Trip v d c a) < Trip v d c b)
-> (m < Primary (Trip v d c) a) < Primary (Trip v d c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Trip v d c) (m a b -> (m < Trip v d c a) < Trip v d c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f)

(>-||-), (>-||--), (>-||---), (>-||----), (>-||-----), (>-||------), (>-||-------), (>-||--------)
	:: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c .
	(Contravariant m m (Flip p c), Interpreted m (Flip p c)) => m a b -> m (p b c) (p a c)
>-||-------- :: m a b -> m (p b c) (p a c)
(>-||--------) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||------- :: m a b -> m (p b c) (p a c)
(>-||-------) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||------ :: m a b -> m (p b c) (p a c)
(>-||------) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||----- :: m a b -> m (p b c) (p a c)
(>-||-----) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||---- :: m a b -> m (p b c) (p a c)
(>-||----) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||--- :: m a b -> m (p b c) (p a c)
(>-||---) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||-- :: m a b -> m (p b c) (p a c)
(>-||--) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)
>-||- :: m a b -> m (p b c) (p a c)
(>-||-) m a b
f = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f)

(<-|-<-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Covariant m m (p a), Covariant m m (Flip p d), Interpreted m (Flip p d))
	=> m a b :*: m c d -> m (p a c) (p b d)
<-|-<-|- :: (m a b :*: m c d) -> m (p a c) (p b d)
(<-|-<-|-) (m a b
f :*: m c d
g) = ((m < Flip p d a) < Flip p d b)
-> (m < Primary (Flip p d) a) < Primary (Flip p d) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p d) (m a b -> (m < Flip p d a) < Flip p d b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f) m (p a d) (p b d) -> m (p a c) (p a d) -> m (p a c) (p b d)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p a c) (p a d)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m c d
g)

(<-|->-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Covariant m m (Flip p c), Contravariant m m (p a), Interpreted m (Flip p c))
	=> m a b :*: m c d -> m (p a d) (p b c)
<-|->-|- :: (m a b :*: m c d) -> m (p a d) (p b c)
(<-|->-|-) (m a b
f :*: m c d
g) = ((m < Flip p c a) < Flip p c b)
-> (m < Primary (Flip p c) a) < Primary (Flip p c) b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c a) < Flip p c b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m a b
f) m (p a c) (p b c) -> m (p a d) (p a c) -> m (p a d) (p b c)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p a d) (p a c)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m c d
g)

(>-|-<-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Contravariant m m (Flip p d), Covariant m m (p b), Interpreted m (Flip p d))
	=> m a b :*: m c d -> m (p b c) (p a d)
>-|-<-|- :: (m a b :*: m c d) -> m (p b c) (p a d)
(>-|-<-|-) (m a b
f :*: m c d
g) = ((m < Flip p d b) < Flip p d a)
-> (m < Primary (Flip p d) b) < Primary (Flip p d) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p d) (m a b -> (m < Flip p d b) < Flip p d a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f) m (p b d) (p a d) -> m (p b c) (p b d) -> m (p b c) (p a d)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p b c) (p b d)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) m c d
g)

(>-|->-|-) :: forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d .
	(Contravariant m m (p b), Contravariant m m (Flip p c), Interpreted m (Flip p c))
	=> m a b :*: m c d -> m (p b d) (p a c)
>-|->-|- :: (m a b :*: m c d) -> m (p b d) (p a c)
(>-|->-|-) (m a b
f :*: m c d
g) = ((m < Flip p c b) < Flip p c a)
-> (m < Primary (Flip p c) b) < Primary (Flip p c) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @m @(Flip p c) (m a b -> (m < Flip p c b) < Flip p c a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m a b
f) m (p b c) (p a c) -> m (p b d) (p b c) -> m (p b d) (p a c)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (m c d -> m (p b d) (p b c)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
(>-|-) m c d
g)

void :: Covariant (->) (->) t => t a -> t ()
void :: t a -> t ()
void t a
x = () -> a -> ()
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant () (a -> ()) -> t a -> t ()
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x

-- TODO: generalize (->), it's hard to do since we don't have such a method: run <-|-- f <-/- unite x
(<<-/-) :: forall v u a b c .
	( Covariant (->) (->) u, Monoidal (Straight (->)) (Straight (->)) (:*:) (:*:) u
	, Interpreted (->) (Flip v c), Traversable (->) (->) (Flip v c))
	=> (a -> u b) -> v a c -> u (v b c)
<<-/- :: (a -> u b) -> v a c -> u (v b c)
(<<-/-) a -> u b
f = (Flip v c b -> v b c) -> u (Flip v c b) -> u (v b c)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|--) (forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->)) (u (Flip v c b) -> u (v b c))
-> (v a c -> u (Flip v c b)) -> v a c -> u (v b c)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> u b) -> Flip v c a -> u (Flip v c 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))
(<-/-) @(->) @(->) @(Flip v c) a -> u b
f (Flip v c a -> u (Flip v c b))
-> (v a c -> Flip v c a) -> v a c -> u (Flip v c b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. v a c -> Flip v c a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip