{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Free constructions: 'HasFree' captures the object constraints @ob@ whose forgetful functor has a left
-- adjoint, with @Free ob@ the free object, 'lift' the unit and 'foldMap' the universal property of the
-- adjunction (packaged as a 'Corepresentable' heteromorphism profunctor).
module Proarrow.Profunctor.Free where

import Data.Foldable1 (Foldable1 (foldMap1))
import Data.Kind (Constraint, Type)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (Maybe (..))
import Prelude (($))
import Prelude qualified as P

import Proarrow.Category.Instance.Free (FREE (..), IsFreeOb (..), liftFree, retractFree)
import Proarrow.Category.Instance.IntConstruction (INT (..), IntConstruction (..), toInt)
import Proarrow.Category.Instance.Nat (Nat (..), first)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (Forget, On, SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), swap)
import Proarrow.Category.Monoidal.Applicative (Applicative (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..), dualityCounit, dualityUnit)
import Proarrow.Category.Monoidal.StarAutonomous (Dual, dualObj)
import Proarrow.Category.Monoidal.Strength (TracedMonoidal)
import Proarrow.Category.Monoidal.Strictified (Fold, Strictified (..), (==))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Hom
  , Kind
  , OB
  , Profunctor (..)
  , Promonad (..)
  , UN
  , arr
  , lmap
  , obj
  , rmap
  , tgt
  , (//)
  , (:~>)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts)
import Proarrow.Limit.Terminal (HasTerminalObject)
import Proarrow.Monoid (Monoid (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id)
import Proarrow.Profunctor.Instance.List (LIST (..), List (..))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Representable (Rep (..))

type HasFree :: forall {k}. OB k -> Constraint
class (CategoryOf k, forall a. (Ob a) => ob (Free ob a)) => HasFree (ob :: OB k) where
  type Free ob (a :: k) :: k
  lift :: (Ob a) => a ~> Free ob a
  foldMap :: (ob b) => (a ~> b) -> Free ob a ~> b

retract :: forall ob a. (HasFree ob, ob a, Ob a) => Free ob a ~> a
retract :: forall {k} (ob :: OB k) (a :: k).
(HasFree ob, ob a, Ob a) =>
Free ob a ~> a
retract = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

freeMap :: (HasFree ob) => (a ~> b) -> Free ob a ~> Free ob b
freeMap :: forall {k} (ob :: OB k) (a :: k) (b :: k).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
freeMap @ob a ~> b
f = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB k) (a :: k). (HasFree ob, Ob a) => a ~> Free ob a
lift @ob (b ~> Free ob b) -> (a ~> b) -> a ~> Free ob b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f) ((Ob a, Ob b) => Free ob a ~> Free ob b)
-> (a ~> b) -> Free ob a ~> Free ob b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

freeComp :: (HasFree ob, Ob c) => b ~> Free ob c -> a ~> Free ob b -> a ~> Free ob c
freeComp :: forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @ob b ~> Free ob c
l a ~> Free ob b
r = forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob b ~> Free ob c
l (Free ob b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Free ob b
r

-- | By creating the left adjoint to the forgetful functor,
-- we obtain the free-forgetful adjunction.
instance (HasFree ob) => Corepresentable (Rep (Forget (ob :: OB k))) where
  type Rep (Forget ob) %% a = SUB (Free ob a)
  coindex :: forall (a :: k) (b :: SUBCAT ob).
Rep (Forget ob) a b -> (Rep (Forget ob) %% a) ~> b
coindex (Rep a ~> (Forget ob @ b)
f) = (Free ob a ~> UN SUB b)
-> Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {k} (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
forall (ob :: OB k) (b :: k) (a :: k).
(HasFree ob, ob b) =>
(a ~> b) -> Free ob a ~> b
foldMap @ob a ~> UN SUB b
a ~> (Forget ob @ b)
f) ((Ob a, Ob (UN SUB b)) =>
 Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b)))
-> (a ~> UN SUB b) -> Sub (~>) (SUB (Free ob a)) (SUB (UN SUB b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> UN SUB b
a ~> (Forget ob @ b)
f
  corepUniv :: forall (a :: k). Ob a => Rep (Forget ob) a (Rep (Forget ob) %% a)
corepUniv @a = let f :: a ~> Free ob a
f = forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB k) (a :: k). (HasFree ob, Ob a) => a ~> Free ob a
lift @ob @a in (a ~> (Forget ob @ SUB (Free ob a)))
-> Rep (Forget ob) a (SUB (Free ob a))
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep a ~> (Forget ob @ SUB (Free ob a))
a ~> Free ob a
f ((Ob a, Ob (Free ob a)) => Rep (Forget ob) a (SUB (Free ob a)))
-> (a ~> Free ob a) -> Rep (Forget ob) a (SUB (Free ob a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Free ob a
f

instance HasFree P.Monoid where
  type Free P.Monoid a = [a]
  lift :: forall a. Ob a => a ~> Free Monoid a
lift = a ~> Free Monoid a
a -> [a]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure
  foldMap :: forall b a. Monoid b => (a ~> b) -> Free Monoid a ~> b
foldMap = (a ~> b) -> Free Monoid a ~> b
(a -> b) -> [a] -> b
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
P.foldMap

instance HasFree P.Semigroup where
  type Free P.Semigroup a = NonEmpty a
  lift :: forall a. Ob a => a ~> Free Semigroup a
lift = a ~> Free Semigroup a
a -> NonEmpty a
forall a. a -> NonEmpty a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure
  foldMap :: forall b a. Semigroup b => (a ~> b) -> Free Semigroup a ~> b
foldMap = (a ~> b) -> Free Semigroup a ~> b
(a -> b) -> NonEmpty a -> b
forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
forall (t :: Type -> Type) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1

instance HasFree (P.Monoid `On` P.Semigroup) where
  type Free (P.Monoid `On` P.Semigroup) (SUB a) = SUB (Maybe a)
  lift :: forall (a :: SUBCAT Semigroup).
Ob a =>
a ~> Free (On Monoid Semigroup) a
lift = (UN SUB a -> Maybe (UN SUB a))
-> Sub (->) (SUB (UN SUB a)) (SUB (Maybe (UN SUB a)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub UN SUB a -> Maybe (UN SUB a)
forall a. a -> Maybe a
Just
  foldMap :: forall (b :: SUBCAT Semigroup) (a :: SUBCAT Semigroup).
On Monoid Semigroup b =>
(a ~> b) -> Free (On Monoid Semigroup) a ~> b
foldMap (Sub a1 -> b1
f) = (Maybe a1 -> b1) -> Sub (->) (SUB (Maybe a1)) (SUB b1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((a1 -> b1) -> Maybe a1 -> b1
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
P.foldMap a1 -> b1
f)

-- | The free 'Applicative' on a functor @f@ (the 'HasFree' instance for 'Applicative'): formal 'pure',
-- effect and 'liftA2' nodes, retracted into any applicative by 'retractAp'.
type Ap :: (k -> Type) -> k -> Type
data Ap f a where
  Pure :: Unit ~> a -> Ap f a
  Eff :: f a -> Ap f a
  LiftA2 :: (Ob a, Ob b) => (a ** b ~> c) -> Ap f a -> Ap f b -> Ap f c

instance (CategoryOf k, Functor f) => Functor (Ap (f :: k -> Type)) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> Ap f a ~> Ap f b
map a ~> b
f (Pure Unit ~> a
a) = (Unit ~> b) -> Ap f b
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure (a ~> b
f (a ~> b) -> (Unit ~> a) -> Unit ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> a
a)
  map a ~> b
f (Eff f a
x) = f b -> Ap f b
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff ((a ~> b) -> f a ~> f b
forall (a :: k) (b :: k). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f f a
x)
  map a ~> b
f (LiftA2 (a ** b) ~> a
k Ap f a
x Ap f b
y) = ((a ** b) ~> b) -> Ap f a -> Ap f b -> Ap f b
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ~> b
f (a ~> b) -> ((a ** b) ~> a) -> (a ** b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** b) ~> a
k) Ap f a
x Ap f b
y

instance Functor Ap where
  map :: forall (a :: k -> Type) (b :: k -> Type). (a ~> b) -> Ap a ~> Ap b
map (Nat a .~> b
n) = (Ap a .~> Ap b) -> Nat (Ap a) (Ap b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Ap a .~> Ap b) -> Nat (Ap a) (Ap b))
-> (Ap a .~> Ap b) -> Nat (Ap a) (Ap b)
forall a b. (a -> b) -> a -> b
$ \case
    Pure Unit ~> a
a -> (Unit ~> a) -> Ap b a
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> a
a
    Eff a a
fa -> b a -> Ap b a
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff (a a ~> b a
a a -> b a
a .~> b
n a a
fa)
    LiftA2 (a ** b) ~> a
k Ap a a
x Ap a b
y -> ((a ** b) ~> a) -> Ap b a -> Ap b b -> Ap b a
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ** b) ~> a
k ((a ~> b) -> Ap a a ~> Ap b a
forall i j k (f :: i -> j -> k) (c :: j) (a :: i) (b :: i).
(Functor f, (~>) ~ Nat, Ob c) =>
(a ~> b) -> f a c ~> f b c
first ((a .~> b) -> Nat a b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> b a
a .~> b
n) Ap a a
x) ((a ~> b) -> Ap a b ~> Ap b b
forall i j k (f :: i -> j -> k) (c :: j) (a :: i) (b :: i).
(Functor f, (~>) ~ Nat, Ob c) =>
(a ~> b) -> f a c ~> f b c
first ((a .~> b) -> Nat a b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> b a
a .~> b
n) Ap a b
y)

instance (Monoidal k) => Promonad (Star Ap :: CAT (k -> Type)) where
  id :: forall (a :: k -> Type). Ob a => Star Ap a a
id = (a ~> Ap a) -> Star Ap a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB (k -> Type)) (a :: k -> Type).
(HasFree ob, Ob a) =>
a ~> Free ob a
lift @Applicative)
  Star b ~> Ap c
l . :: forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
Star Ap b c -> Star Ap a b -> Star Ap a c
. Star a ~> Ap b
r = (a ~> Ap c) -> Star Ap a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (ob :: OB (k -> Type)) (c :: k -> Type) (b :: k -> Type)
       (a :: k -> Type).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @Applicative b ~> Ap c
b ~> Free Applicative c
l a ~> Ap b
a ~> Free Applicative b
r)

instance (Monoidal k, Functor f) => Applicative (Ap (f :: k -> Type)) where
  pure :: forall (a :: k). (Unit ~> a) -> Unit ~> Ap f a
pure Unit ~> a
a () = (Unit ~> a) -> Ap f a
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> a
a
  liftA2 :: forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> (Ap f a ** Ap f b) ~> Ap f c
liftA2 (a ** b) ~> c
f (Ap f a
fa, Ap f b
fb) = ((a ** b) ~> c) -> Ap f a -> Ap f b -> Ap f c
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (a ** b) ~> c
f Ap f a
fa Ap f b
fb

instance (Monoidal k, Monoid m) => Monoid (Ap (f :: k -> Type) m) where
  mempty :: Unit ~> Ap f m
mempty () = (Unit ~> m) -> Ap f m
forall {k} (a :: k) (f :: k -> Type). (Unit ~> a) -> Ap f a
Pure Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  mappend :: (Ap f m ** Ap f m) ~> Ap f m
mappend (Ap f m
l, Ap f m
r) = ((m ** m) ~> m) -> Ap f m -> Ap f m -> Ap f m
forall {k} (b :: k) (b :: k) (c :: k) (f :: k -> Type).
(Ob b, Ob b) =>
((b ** b) ~> c) -> Ap f b -> Ap f b -> Ap f c
LiftA2 (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend Ap f m
l Ap f m
r

retractAp :: (Applicative f) => Ap f a -> f a
retractAp :: forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp (Pure Unit ~> a
a) = (Unit ~> a) -> Unit ~> f a
forall (a :: k). (Unit ~> a) -> Unit ~> f a
forall {j} {k} (f :: j -> k) (a :: j).
Applicative f =>
(Unit ~> a) -> Unit ~> f a
pure Unit ~> a
a ()
retractAp (Eff f a
fa) = f a
fa
retractAp (LiftA2 (a ** b) ~> a
k Ap f a
x Ap f b
y) = ((a ** b) ~> a) -> (f a ** f b) ~> f a
forall (a :: k) (b :: k) (c :: k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 (a ** b) ~> a
k (Ap f a -> f a
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Ap f a
x, Ap f b -> f b
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Ap f b
y)

instance (Monoidal k) => HasFree (Applicative :: OB (k -> Type)) where
  type Free Applicative f = Ap f
  lift :: forall (a :: k -> Type). Ob a => a ~> Free Applicative a
lift = (a .~> Ap a) -> Nat a (Ap a)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> Ap a a
a a -> Ap a a
a .~> Ap a
forall {k} (f :: k -> Type) (a :: k). f a -> Ap f a
Eff
  foldMap :: forall (b :: k -> Type) (a :: k -> Type).
Applicative b =>
(a ~> b) -> Free Applicative a ~> b
foldMap f :: a ~> b
f@Nat{} = (Ap b .~> b) -> Nat (Ap b) b
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat Ap b a ~> b a
Ap b a -> b a
Ap b .~> b
forall {k} (f :: k -> Type) (a :: k).
Applicative f =>
Ap f a -> f a
retractAp Nat (Ap b) b -> Nat (Ap a) (Ap b) -> Nat (Ap a) b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k -> Type) (c :: k -> Type) (a :: k -> Type).
Nat b c -> Nat a b -> Nat a c
. (a ~> b) -> Ap a ~> Ap b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k -> Type) (b :: k -> Type). (a ~> b) -> Ap a ~> Ap b
map a ~> b
f

-- | The free 'Promonad' on a profunctor @p@: a chain of @p@s ending in a hom arrow, folded into any
-- promonad by 'foldFreePromonad'.
data FreePromonad p a b where
  Unit :: (a ~> b) -> FreePromonad p a b
  Comp :: p a b -> FreePromonad p b c -> FreePromonad p a c

freePromonadAlg :: p :.: FreePromonad p :~> FreePromonad p
freePromonadAlg :: forall {k} (p :: k +-> k) (a :: k) (b :: k).
(:.:) p (FreePromonad p) a b -> FreePromonad p a b
freePromonadAlg (p a b
p :.: FreePromonad p b b
pp) = p a b -> FreePromonad p b b -> FreePromonad p a b
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp p a b
p FreePromonad p b b
pp

foldFreePromonad :: (Promonad q) => p :~> q -> FreePromonad p :~> q
foldFreePromonad :: forall {k1} (q :: CAT k1) (p :: CAT k1).
Promonad q =>
(p :~> q) -> FreePromonad p :~> q
foldFreePromonad p :~> q
_ (Unit a ~> b
f) = (a ~> b) -> q a b
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr a ~> b
f
foldFreePromonad p :~> q
n (Comp p a b
p FreePromonad p b b
pp) = (p :~> q) -> FreePromonad p :~> q
forall {k1} (q :: CAT k1) (p :: CAT k1).
Promonad q =>
(p :~> q) -> FreePromonad p :~> q
foldFreePromonad p a b -> q a b
p :~> q
n FreePromonad p b b
pp q b b -> q a b -> q a b
forall (b :: k1) (c :: k1) (a :: k1). q b c -> q a b -> q a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> q a b
p :~> q
n p a b
p

instance (Profunctor p) => Profunctor (FreePromonad p) where
  dimap :: forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> FreePromonad p a b -> FreePromonad p c d
dimap c ~> a
l b ~> d
r (Unit a ~> b
f) = (c ~> d) -> FreePromonad p c d
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit (b ~> d
r (b ~> d) -> (c ~> b) -> c ~> d
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f (a ~> b) -> (c ~> a) -> c ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l)
  dimap c ~> a
l b ~> d
r (Comp p a b
p FreePromonad p b b
q) = p c b -> FreePromonad p b d -> FreePromonad p c d
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp ((c ~> a) -> p a b -> p c b
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p) ((b ~> d) -> FreePromonad p b b -> FreePromonad p b d
forall (b :: j) (d :: j) (a :: j).
(b ~> d) -> FreePromonad p a b -> FreePromonad p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r FreePromonad p b b
q)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> FreePromonad p a b -> r
\\ (Unit a ~> b
f) = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  (Ob a, Ob b) => r
r \\ Comp p a b
p FreePromonad p b b
q = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p ((Ob b, Ob b) => r) -> FreePromonad p b b -> r
forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> FreePromonad p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ FreePromonad p b b
q

instance (Profunctor p) => Promonad (FreePromonad p) where
  id :: forall (a :: k). Ob a => FreePromonad p a a
id = (a ~> a) -> FreePromonad p a a
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  FreePromonad p b c
p . :: forall (b :: k) (c :: k) (a :: k).
FreePromonad p b c -> FreePromonad p a b -> FreePromonad p a c
. Unit a ~> b
f = (a ~> b) -> FreePromonad p b c -> FreePromonad p a c
forall (c :: k) (a :: k) (b :: k).
(c ~> a) -> FreePromonad p a b -> FreePromonad p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f FreePromonad p b c
p
  FreePromonad p b c
p . Comp p a b
r FreePromonad p b b
q = p a b -> FreePromonad p b c -> FreePromonad p a c
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
Comp p a b
r (FreePromonad p b c
p FreePromonad p b c -> FreePromonad p b b -> FreePromonad p b c
forall (b :: k) (c :: k) (a :: k).
FreePromonad p b c -> FreePromonad p a b -> FreePromonad p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. FreePromonad p b b
q)
instance Functor FreePromonad where
  map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type).
(a ~> b) -> FreePromonad a ~> FreePromonad b
map = forall {k} (ob :: OB k) (a :: k) (b :: k).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
forall (ob :: OB (k -> k -> Type)) (a :: k -> k -> Type)
       (b :: k -> k -> Type).
HasFree ob =>
(a ~> b) -> Free ob a ~> Free ob b
freeMap @Promonad
instance Promonad (Star FreePromonad) where
  id :: forall (a :: k -> k -> Type). Ob a => Star FreePromonad a a
id = (a ~> FreePromonad a) -> Star FreePromonad a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (a :: k).
(HasFree ob, Ob a) =>
a ~> Free ob a
forall (ob :: OB (k -> k -> Type)) (a :: k -> k -> Type).
(HasFree ob, Ob a) =>
a ~> Free ob a
lift @Promonad)
  Star b ~> FreePromonad c
l . :: forall (b :: k -> k -> Type) (c :: k -> k -> Type)
       (a :: k -> k -> Type).
Star FreePromonad b c
-> Star FreePromonad a b -> Star FreePromonad a c
. Star a ~> FreePromonad b
r = (a ~> FreePromonad c) -> Star FreePromonad a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (forall {k} (ob :: OB k) (c :: k) (b :: k) (a :: k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
forall (ob :: OB (k -> k -> Type)) (c :: k -> k -> Type)
       (b :: k -> k -> Type) (a :: k -> k -> Type).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @Promonad b ~> FreePromonad c
b ~> Free Promonad c
l a ~> FreePromonad b
a ~> Free Promonad b
r)
instance HasFree Promonad where
  type Free Promonad p = FreePromonad p
  lift :: forall (a :: CAT k). Ob a => a ~> Free Promonad a
lift = (a :~> FreePromonad a) -> Prof a (FreePromonad a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> a a b
p a a b -> FreePromonad a b b -> FreePromonad a a b
forall {k} (p :: k -> k -> Type) (a :: k) (b :: k) (c :: k).
p a b -> FreePromonad p b c -> FreePromonad p a c
`Comp` (b ~> b) -> FreePromonad a b b
forall {k} (a :: k) (b :: k) (p :: k -> k -> Type).
(a ~> b) -> FreePromonad p a b
Unit (a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a a b
p)
  foldMap :: forall (b :: CAT k) (a :: CAT k).
Promonad b =>
(a ~> b) -> Free Promonad a ~> b
foldMap (Prof a :~> b
n) = (FreePromonad a :~> b) -> Prof (FreePromonad a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((a :~> b) -> FreePromonad a :~> b
forall {k1} (q :: CAT k1) (p :: CAT k1).
Promonad q =>
(p :~> q) -> FreePromonad p :~> q
foldFreePromonad a a b -> b a b
a :~> b
n)

-- | The free @c@-structured kind over a @b@-structured kind @k@. A standalone family (rather than
-- an associated type of 'HasFreeK') because the kinds of 'Lift' and 'Retract' mention it.
type family FreeK (b :: Kind -> Constraint) (c :: Kind -> Constraint) (k :: Kind) :: Kind

-- | 'Proarrow.Object.Ob''-style helper: the quantified superclass of 'HasFreeK' needs to state
-- @c ('FreeK' b c k)@, and a type family application cannot head a quantified constraint directly.
class (c (FreeK b c k)) => FreeK' (b :: Kind -> Constraint) (c :: Kind -> Constraint) (k :: Kind)

instance (c (FreeK b c k)) => FreeK' b c k

-- | @'FreeK' b c@ builds the free @c@-structured kind over any @b@-structured kind: 'liftK'
-- embeds the arrows of @k@, and when @k@ itself is already @c@-structured 'retractK' interprets
-- back into @k@.
-- | The embedding of an object of @k@ into the free @c@-structured kind.
type family Lift (b :: Kind -> Constraint) (c :: Kind -> Constraint) (a :: k) :: FreeK b c k

-- | Interpret an object of the free @c@-structured kind back into @k@.
type family Retract (b :: Kind -> Constraint) (c :: Kind -> Constraint) (k :: Kind) (a :: FreeK b c k) :: k

class
  (forall k. (b k) => FreeK' b c k) =>
  HasFreeK (b :: Kind -> Constraint) (c :: Kind -> Constraint)
  where
  liftK :: (b k) => (x :: k) ~> y -> Lift b c x ~> Lift b c y
  retractK
    :: forall k (x :: FreeK b c k) (y :: FreeK b c k)
     . (c k)
    => x ~> y -> Retract b c k x ~> Retract b c k y

type instance FreeK CategoryOf Monoidal k = LIST k

type instance Lift CategoryOf Monoidal a = L '[a]
type instance Retract CategoryOf Monoidal k (a :: LIST k) = Fold (UN L a)

instance HasFreeK CategoryOf Monoidal where
  liftK :: forall k (x :: k) (y :: k).
CategoryOf k =>
(x ~> y)
-> Lift CategoryOf Monoidal x ~> Lift CategoryOf Monoidal y
liftK x ~> y
f = (x ~> y)
-> List (~>) (L '[]) (L '[]) -> List (~>) (L '[x]) (L '[y])
forall {k} {j} (as1 :: [k]) (bs1 :: [j]) (p :: j +-> k) (a :: k)
       (b :: j).
(IsList as1, IsList bs1) =>
p a b
-> List p (L as1) (L bs1) -> List p (L (a : as1)) (L (b : bs1))
Cons x ~> y
f List (~>) (L '[]) (L '[])
forall {j} {k} (p :: j +-> k). List p (L '[]) (L '[])
Nil
  retractK :: forall k (x :: FreeK CategoryOf Monoidal k)
       (y :: FreeK CategoryOf Monoidal k).
Monoidal k =>
(x ~> y)
-> Retract CategoryOf Monoidal k x
   ~> Retract CategoryOf Monoidal k y
retractK x ~> y
List (~>) x y
Nil = Unit ~> Unit
Retract CategoryOf Monoidal k x ~> Retract CategoryOf Monoidal k y
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  retractK (Cons a ~> b
f List (~>) (L as1) (L bs1)
Nil) = a ~> b
Retract CategoryOf Monoidal k x ~> Retract CategoryOf Monoidal k y
f
  retractK (Cons a ~> b
f fs :: List (~>) (L as1) (L bs1)
fs@Cons{}) = a ~> b
f (a ~> b)
-> (Fold (UN L (L (a : as1))) ~> Fold (UN L (L (b : bs1))))
-> (a ** Fold (UN L (L (a : as1))))
   ~> (b ** Fold (UN L (L (b : bs1))))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (b :: Type -> Constraint) (c :: Type -> Constraint) k
       (x :: FreeK b c k) (y :: FreeK b c k).
(HasFreeK b c, c k) =>
(x ~> y) -> Retract b c k x ~> Retract b c k y
retractK @CategoryOf @Monoidal L (a : as1) ~> L (b : bs1)
List (~>) (L as1) (L bs1)
fs

-- | The free category with a terminal object over @k@, built with
-- "Proarrow.Category.Instance.Free".
type instance FreeK CategoryOf HasTerminalObject k = FREE '[HasTerminalObject] (Hom k)

type instance Lift CategoryOf HasTerminalObject (a :: k) = EMB a
type instance Retract CategoryOf HasTerminalObject k (a :: FREE '[HasTerminalObject] (Hom k)) = Lower (Id :: CAT k) a

instance HasFreeK CategoryOf HasTerminalObject where
  liftK :: forall k (x :: k) (y :: k).
CategoryOf k =>
(x ~> y)
-> Lift CategoryOf HasTerminalObject x
   ~> Lift CategoryOf HasTerminalObject y
liftK = (x ~> y) -> 'EMB x ~> 'EMB y
(x ~> y)
-> Lift CategoryOf HasTerminalObject x
   ~> Lift CategoryOf HasTerminalObject y
forall {k} (cs :: [Type -> Constraint]) (x :: k) (y :: k).
CategoryOf k =>
(x ~> y) -> 'EMB x ~> 'EMB y
liftFree
  retractK :: forall k (x :: FreeK CategoryOf HasTerminalObject k)
       (y :: FreeK CategoryOf HasTerminalObject k).
HasTerminalObject k =>
(x ~> y)
-> Retract CategoryOf HasTerminalObject k x
   ~> Retract CategoryOf HasTerminalObject k y
retractK = forall (cs :: [Type -> Constraint]) {k} (a :: FREE cs (Hom k))
       (b :: FREE cs (Hom k)).
(CategoryOf k, All cs k) =>
(a ~> b) -> Lower Id a ~> Lower Id b
retractFree @'[HasTerminalObject]

-- | The free category with binary products over @k@, built with
-- "Proarrow.Category.Instance.Free".
type instance FreeK CategoryOf HasBinaryProducts k = FREE '[HasBinaryProducts] (Hom k)

type instance Lift CategoryOf HasBinaryProducts (a :: k) = EMB a
type instance Retract CategoryOf HasBinaryProducts k (a :: FREE '[HasBinaryProducts] (Hom k)) = Lower (Id :: CAT k) a

instance HasFreeK CategoryOf HasBinaryProducts where
  liftK :: forall k (x :: k) (y :: k).
CategoryOf k =>
(x ~> y)
-> Lift CategoryOf HasBinaryProducts x
   ~> Lift CategoryOf HasBinaryProducts y
liftK = (x ~> y) -> 'EMB x ~> 'EMB y
(x ~> y)
-> Lift CategoryOf HasBinaryProducts x
   ~> Lift CategoryOf HasBinaryProducts y
forall {k} (cs :: [Type -> Constraint]) (x :: k) (y :: k).
CategoryOf k =>
(x ~> y) -> 'EMB x ~> 'EMB y
liftFree
  retractK :: forall k (x :: FreeK CategoryOf HasBinaryProducts k)
       (y :: FreeK CategoryOf HasBinaryProducts k).
HasBinaryProducts k =>
(x ~> y)
-> Retract CategoryOf HasBinaryProducts k x
   ~> Retract CategoryOf HasBinaryProducts k y
retractK = forall (cs :: [Type -> Constraint]) {k} (a :: FREE cs (Hom k))
       (b :: FREE cs (Hom k)).
(CategoryOf k, All cs k) =>
(a ~> b) -> Lower Id a ~> Lower Id b
retractFree @'[HasBinaryProducts]

type instance FreeK TracedMonoidal CompactClosed k = INT k

type instance Lift TracedMonoidal CompactClosed (a :: k) = I a Unit
type instance Retract TracedMonoidal CompactClosed k (I a b :: INT k) = a ** Dual b

instance HasFreeK TracedMonoidal CompactClosed where
  liftK :: forall k (x :: k) (y :: k).
TracedMonoidal k =>
(x ~> y)
-> Lift TracedMonoidal CompactClosed x
   ~> Lift TracedMonoidal CompactClosed y
liftK = (x ~> y) -> 'I x Unit ~> 'I y Unit
(x ~> y)
-> Lift TracedMonoidal CompactClosed x
   ~> Lift TracedMonoidal CompactClosed y
forall {k} (a :: k) (b :: k) (m :: k).
(TracedMonoidal k, Ob m) =>
(a ~> b) -> 'I a m ~> 'I b m
toInt
  retractK :: forall k (x :: FreeK TracedMonoidal CompactClosed k)
       (y :: FreeK TracedMonoidal CompactClosed k).
CompactClosed k =>
(x ~> y)
-> Retract TracedMonoidal CompactClosed k x
   ~> Retract TracedMonoidal CompactClosed k y
retractK (Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f) =
    forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @am Obj (Dual am)
-> ((Ob (Dual am), Ob (Dual am)) =>
    (ap ** Dual am) ~> (bp ** Dual bm))
-> (ap ** Dual am) ~> (bp ** Dual bm)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @bm Obj (Dual bm)
-> ((Ob (Dual bm), Ob (Dual bm)) =>
    (ap ** Dual am) ~> (bp ** Dual bm))
-> (ap ** Dual am) ~> (bp ** Dual bm)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        Strictified '[ap, Dual am] '[bp, Dual bm]
-> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (Strictified '[ap, Dual am] '[bp, Dual bm]
 -> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm])
-> Strictified '[ap, Dual am] '[bp, Dual bm]
-> Fold '[ap, Dual am] ~> Fold '[bp, Dual bm]
forall a b. (a -> b) -> a -> b
$
          forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[ap, Dual am] @[Dual am, ap] (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @ap @(Dual am)) Strictified '[ap, Dual am] '[Dual am, ap]
-> Strictified '[] '[bm, Dual bm]
-> Strictified
     ('[ap, Dual am] ** '[]) ('[Dual am, ap] ** '[bm, Dual bm])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[] @[bm, Dual bm] (forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @bm)
            (('[ap, Dual am] ++ '[]) ~> ('[Dual am, ap] ++ '[bm, Dual bm]))
-> (('[Dual am, ap] ++ '[bm, Dual bm])
    ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm]))
-> ('[ap, Dual am] ++ '[])
   ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual am] Strictified '[Dual am] '[Dual am]
-> Strictified '[ap, bm] '[am, bp]
-> Strictified ('[Dual am] ** '[ap, bm]) ('[Dual am] ** '[am, bp])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[ap, bm] @[am, bp] (ap ** bm) ~> (am ** bp)
Fold '[ap, bm] ~> Fold '[am, bp]
f Strictified ('[Dual am] ++ '[ap, bm]) ('[Dual am] ++ '[am, bp])
-> Strictified '[Dual bm] '[Dual bm]
-> Strictified
     (('[Dual am] ++ '[ap, bm]) ** '[Dual bm])
     (('[Dual am] ++ '[am, bp]) ** '[Dual bm])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual bm]
            (('[ap, Dual am] ++ '[])
 ~> (('[Dual am] ++ '[am, bp]) ++ '[Dual bm]))
-> ((('[Dual am] ++ '[am, bp]) ++ '[Dual bm])
    ~> ('[bp] ++ '[Dual bm]))
-> ('[ap, Dual am] ++ '[]) ~> ('[bp] ++ '[Dual bm])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[Dual am, am] @'[] (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @am) Strictified '[Dual am, am] '[]
-> Strictified '[bp] '[bp]
-> Strictified ('[Dual am, am] ** '[bp]) ('[] ** '[bp])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[bp] Strictified ('[Dual am, am] ++ '[bp]) '[bp]
-> Strictified '[Dual bm] '[Dual bm]
-> Strictified
     (('[Dual am, am] ++ '[bp]) ** '[Dual bm]) ('[bp] ** '[Dual bm])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[Dual bm]