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

-- | Monoidal categories in which every object carries a cocommutative comonoid (the
-- @'Supplies' 'CocommutativeComonoid' k@ superclass), with @'copy' :: a ~> a ** a@ and
-- @'discard' :: a ~> 'Unit'@ defaulting to its comult\/counit. This gives projections
-- 'fst'\/'snd' without @tensor = product@, e.g. in the biproduct categories
-- "Proarrow.Category.Instance.Mat" and "Proarrow.Category.Instance.FinRel". Unlike in
-- 'Proarrow.Category.Monoidal.Cartesian.Cartesian' (which has this class as a superclass, by Fox's
-- theorem) the comonoids need not be /natural/, so morphisms may duplicate\/delete resources
-- non-uniformly.
module Proarrow.Category.Monoidal.CopyDiscard where

import Data.Kind (Constraint, Type)
import Prelude (Applicative, ($))

import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT, Sub (..), SubMonoidal)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , Tensor
  , leftUnitorWith
  , rightUnitorWith
  , swapInner
  )
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Category.Monoidal.Strictified (Strictified (..), listCase)
import Proarrow.Core (CategoryOf (..), Kind, OB, Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Supplies)
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Representable (Rep (..))
import Proarrow.Tools.Laws (Equation, Law (..), Laws (..), (===))

class (SymMonoidal k, Supplies CocommutativeComonoid k) => CopyDiscard k where
  copy :: (Ob (a :: k)) => a ~> a ** a
  copy = a ~> (a ** a)
forall {k :: Kind} (c :: k). Comonoid c => c ~> (c ** c)
comult
  discard :: (Ob (a :: k)) => a ~> Unit
  discard = a ~> Unit
forall {k :: Kind} (c :: k). Comonoid c => c ~> Unit
counit

-- | The constant functor ignores the acting object: discard it. Only copying\/discarding is
-- needed, so this works in biproduct categories as well as cartesian ones.
instance (CopyDiscard k, Ob r) => Strong Tensor (Rep (Constant r) :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
Rep (Constant r) x y
-> Rep (Constant r) (Act Tensor a x) (Act Tensor a y)
act @a (Rep @y x ~> (Constant r @ y)
p) = forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @y (((a ** x) ~> (Constant r @ (a ** y)))
-> Rep (Constant r) (a ** x) (a ** y)
forall {j :: Kind} {k :: Kind} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x ~> r
x ~> (Constant r @ y)
p (x ~> r) -> ((a ** x) ~> x) -> (a ** x) ~> r
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> Unit) -> (a ** x) ~> x
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a))) ((Ob x, Ob r) => Rep (Constant r) (a ** x) (a ** y))
-> (x ~> r) -> Rep (Constant r) (a ** x) (a ** y)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ x ~> r
x ~> (Constant r @ y)
p

-- | The structures the laws of a copy-discard category are stated for.
type CopyDiscardStructures :: [Kind -> Constraint]
type CopyDiscardStructures = '[Monoidal, SymMonoidal, CopyDiscard]

-- | 'copy' and 'discard' are the supplied comonoid, and they respect the tensor: copying or
-- discarding @a '**' b@ is copying or discarding both parts, and on the unit they do nothing.
-- The comonoid laws and cocommutativity are those of the supply, in "Proarrow.Monoid".
instance Laws CopyDiscardStructures where
  laws :: [Law CopyDiscardStructures]
laws =
    [ String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copy is comult" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @_ @a (a ~> (a ** a)) -> (a ~> (a ** a)) -> m (Equation k)
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k :: Kind} (c :: k). Comonoid c => c ~> (c ** c)
comult @a
    , String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"discard is counit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @_ @a (a ~> Unit) -> (a ~> Unit) -> m (Equation k)
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (c :: k). Comonoid c => c ~> Unit
forall {k :: Kind} (c :: k). Comonoid c => c ~> Unit
counit @a
    , String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copy of a tensor" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** b) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
          forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @a ((Ob (a ** a) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** a) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
            forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @b ((Ob (b ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** b) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
              forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(a ** b) @(a ** b) ((Ob ((a ** b) ** (a ** b)) => m (Equation k)) -> m (Equation k))
-> (Ob ((a ** b) ** (a ** b)) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
                forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @_ @(a ** b) ((a ** b) ~> ((a ** b) ** (a ** b)))
-> ((a ** b) ~> ((a ** b) ** (a ** b))) -> m (Equation k)
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k :: Kind} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @a @a @b @b (((a ** a) ** (b ** b)) ~> ((a ** b) ** (a ** b)))
-> ((a ** b) ~> ((a ** a) ** (b ** b)))
-> (a ** b) ~> ((a ** b) ** (a ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @_ @a (a ~> (a ** a))
-> (b ~> (b ** b)) -> (a ** b) ~> ((a ** a) ** (b ** b))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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 (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @_ @b)
    , String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"discard of a tensor" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @_ @(a ** b) ((a ** b) ~> Unit) -> ((a ** b) ~> Unit) -> m (Equation k)
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @Unit ((Unit ** Unit) ~> Unit)
-> ((a ** b) ~> (Unit ** Unit)) -> (a ** b) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @_ @a (a ~> Unit) -> (b ~> Unit) -> (a ** b) ~> (Unit ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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 (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @_ @b))
    , String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"copy of the unit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
forall {k :: Kind} (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
copyOfUnit @a
    , String
-> LawBody CopyDiscardStructures -> Law CopyDiscardStructures
forall (cs :: [Kind -> Constraint]). String -> LawBody cs -> Law cs
Law String
"discard of the unit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
forall {k :: Kind} (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
discardOfUnit @a
    ]

-- | 'copy' on the unit is a unitor; @a@ only says which category.
copyOfUnit :: forall {k} (a :: k) m. (CopyDiscard k, Applicative m) => m (Equation k)
copyOfUnit :: forall {k :: Kind} (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
copyOfUnit = forall (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @Unit @Unit (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy @k @Unit (Unit ~> (Unit ** Unit))
-> (Unit ~> (Unit ** Unit)) -> m (ProEquation (~>))
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @Unit)

-- | 'discard' on the unit is the identity; @a@ only says which category.
discardOfUnit :: forall {k} (a :: k) m. (CopyDiscard k, Applicative m) => m (Equation k)
discardOfUnit :: forall {k :: Kind} (a :: k) (m :: Kind -> Kind).
(CopyDiscard k, Applicative m) =>
m (Equation k)
discardOfUnit = forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @Unit (Unit ~> Unit) -> (Unit ~> Unit) -> m (ProEquation (~>))
forall {i :: Kind} (m :: Kind -> Kind) (r :: Kind) (a :: i)
       (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @Unit

copyS :: (CopyDiscard k, Ob (a :: k)) => '[a] ~> '[a, a]
copyS :: forall (k :: Kind) (a :: k).
(CopyDiscard k, Ob a) =>
'[a] ~> '[a, a]
copyS = (Fold '[a] ~> Fold '[a, a]) -> Strictified '[a] '[a, a]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> (a ** a)
Fold '[a] ~> Fold '[a, a]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy

discardS :: (CopyDiscard k, Ob (a :: k)) => '[a] ~> '[]
discardS :: forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => '[a] ~> '[]
discardS = (Fold '[a] ~> Fold '[]) -> Strictified '[a] '[]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold '[a] ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance CopyDiscard Type
instance CopyDiscard ()

instance CopyDiscard BOOL

-- | The comonoid supply of a product category, a subcategory and a strictified category are
-- inherited componentwise: each object's comonoid is the ambient 'copy'\/'discard'.
instance (CopyDiscard j, CopyDiscard k, Ob (a :: (j, k))) => Comonoid (a :: (j, k)) where
  counit :: a ~> Unit
counit = a ~> Unit
'(Fst @ a, Snd @ a) ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
forall (a :: (j, k)). Ob a => a ~> Unit
discard
  comult :: a ~> (a ** a)
comult = a ~> (a ** a)
'(Fst @ a, Snd @ a) ~> ('(Fst @ a, Snd @ a) ** '(Fst @ a, Snd @ a))
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
forall (a :: (j, k)). Ob a => a ~> (a ** a)
copy

instance (CopyDiscard j, CopyDiscard k, Ob (a :: (j, k))) => CocommutativeComonoid (a :: (j, k))

instance (CopyDiscard j, CopyDiscard k) => CopyDiscard (j, k) where
  copy :: forall (a :: (j, k)). Ob a => a ~> (a ** a)
copy = (Fst @ a) ~> ((Fst @ a) ** (Fst @ a))
forall (a :: j). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy ((Fst @ a) ~> ((Fst @ a) ** (Fst @ a)))
-> ((Snd @ a) ~> ((Snd @ a) ** (Snd @ a)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ a, Snd @ a)
     '((Fst @ a) ** (Fst @ a), (Snd @ a) ** (Snd @ a))
forall {j1 :: Kind} {k1 :: Kind} {j2 :: Kind} {k2 :: Kind}
       (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1) (d :: j2 +-> k2) (a2 :: k2)
       (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (Snd @ a) ~> ((Snd @ a) ** (Snd @ a))
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: (j, k)). Ob a => a ~> Unit
discard = (Fst @ a) ~> Unit
forall (a :: j). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard ((Fst @ a) ~> Unit)
-> ((Snd @ a) ~> Unit)
-> (:**:) (~>) (~>) '(Fst @ a, Snd @ a) '(Unit, Unit)
forall {j1 :: Kind} {k1 :: Kind} {j2 :: Kind} {k2 :: Kind}
       (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1) (d :: j2 +-> k2) (a2 :: k2)
       (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (Snd @ a) ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (SubMonoidal ob, CopyDiscard k, Ob (a :: SUBCAT ob)) => Comonoid (a :: SUBCAT (ob :: OB k)) where
  counit :: a ~> Unit
counit = a ~> Unit
SUB (UN SUB a) ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
forall (a :: SUBCAT ob). Ob a => a ~> Unit
discard
  comult :: a ~> (a ** a)
comult = a ~> (a ** a)
SUB (UN SUB a) ~> (SUB (UN SUB a) ** SUB (UN SUB a))
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
forall (a :: SUBCAT ob). Ob a => a ~> (a ** a)
copy
instance (SubMonoidal ob, CopyDiscard k, Ob (a :: SUBCAT ob)) => CocommutativeComonoid (a :: SUBCAT (ob :: OB k))
instance (SubMonoidal ob, CopyDiscard k) => CopyDiscard (SUBCAT (ob :: OB k)) where
  copy :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** a)
copy = (UN SUB a ~> (UN SUB a ** UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (UN SUB a ** UN SUB a))
forall {k :: Kind} (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 ~> (UN SUB a ** UN SUB a)
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: SUBCAT ob). Ob a => a ~> Unit
discard = (UN SUB a ~> Unit) -> Sub (~>) (SUB (UN SUB a)) (SUB Unit)
forall {k :: Kind} (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 ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (CopyDiscard k, Ob (as :: [k])) => Comonoid (as :: [k]) where
  counit :: as ~> Unit
counit = as ~> Unit
forall (a :: [k]). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard
  comult :: as ~> (as ** as)
comult = as ~> (as ** as)
forall (a :: [k]). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
instance (CopyDiscard k, Ob (as :: [k])) => CocommutativeComonoid (as :: [k])
instance (CopyDiscard k) => CopyDiscard [k] where
  copy :: forall (a :: [k]). Ob a => a ~> (a ** a)
copy @as0 =
    forall (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k :: Kind} (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as0
      Strictified a (a ++ a)
Strictified '[] '[]
(a ~ '[]) => Strictified a (a ++ a)
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
      (\ @a -> forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[a, a] a ~> (a ** a)
Fold '[a] ~> Fold '[a, a]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy)
      ( \ @a @as ->
          (forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a] Strictified '[b] '[b]
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : (cs ++ (b : c : cs)))
-> Strictified
     ('[b] ** ((b : c : cs) ++ (c : cs)))
     ('[b] ** (c : (cs ++ (b : c : cs))))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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 (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @as @'[a] @as Strictified
  (c : ((cs ++ '[b]) ++ (c : cs))) (c : (cs ++ (b : c : cs)))
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : ((cs ++ '[b]) ++ (c : cs)))
-> Strictified
     ((b : c : cs) ++ (c : cs)) (c : (cs ++ (b : c : cs)))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @[k] @'[a] @as Strictified (b : c : cs) (c : (cs ++ '[b]))
-> Strictified (c : cs) (c : cs)
-> Strictified
     ((b : c : cs) ** (c : cs)) ((c : (cs ++ '[b])) ** (c : cs))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (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 :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @as)))
            Strictified
  ('[b] ++ ((b : c : cs) ++ (c : cs))) (b : c : (cs ++ (b : c : cs)))
-> Strictified a ('[b] ++ ((b : c : cs) ++ (c : cs)))
-> Strictified a (b : c : (cs ++ (b : c : cs)))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[a, a] b ~> (b ** b)
Fold '[b] ~> Fold '[b, b]
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy Strictified '[b] '[b, b]
-> Strictified (c : cs) (c : (cs ++ (c : cs)))
-> Strictified
     ('[b] ** (c : cs)) ('[b, b] ** (c : (cs ++ (c : cs))))
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (c : cs) ~> ((c : cs) ** (c : cs))
Strictified (c : cs) (c : (cs ++ (c : cs)))
forall (a :: [k]). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy)
      )
  discard :: forall (a :: [k]). Ob a => a ~> Unit
discard @as =
    forall (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k :: Kind} (as :: [k]) (r :: Kind).
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as
      Strictified a '[]
Strictified '[] '[]
(a ~ '[]) => Strictified a '[]
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: CAT k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
      ((Fold a ~> Fold '[]) -> Strictified a '[]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold a ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard)
      (\ @a -> forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @'[] b ~> Unit
Fold '[b] ~> Fold '[]
forall (a :: k). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard Strictified '[b] '[]
-> Strictified (c : cs) '[]
-> Strictified ('[b] ** (c : cs)) ('[] ** '[])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (c : cs) ~> Unit
Strictified (c : cs) '[]
forall (a :: [k]). Ob a => a ~> Unit
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard)

fst :: forall {k} (a :: k) b. (CopyDiscard k, Ob a, Ob b) => (a ** b) ~> a
fst :: forall {k :: Kind} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> a
fst = (b ~> Unit) -> (a ** b) ~> a
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @b)

snd :: forall {k} a (b :: k). (CopyDiscard k, Ob a, Ob b) => (a ** b) ~> b
snd :: forall {k :: Kind} (a :: k) (b :: k).
(CopyDiscard k, Ob a, Ob b) =>
(a ** b) ~> b
snd = (a ~> Unit) -> (a ** b) ~> b
forall {k :: Kind} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a)

(&&&) :: forall {k} (a :: k) x y. (CopyDiscard k) => a ~> x -> a ~> y -> a ~> x ** y
a ~> x
f &&& :: forall {k :: Kind} (a :: k) (x :: k) (y :: k).
CopyDiscard k =>
(a ~> x) -> (a ~> y) -> a ~> (x ** y)
&&& a ~> y
g = (a ~> x
f (a ~> x) -> (a ~> y) -> (a ** a) ~> (x ** y)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** a ~> y
g) ((a ** a) ~> (x ** y)) -> (a ~> (a ** a)) -> a ~> (x ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a ** a)
forall (a :: k). Ob a => a ~> (a ** a)
forall (k :: Kind) (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy ((Ob a, Ob x) => a ~> (x ** y)) -> (a ~> x) -> a ~> (x ** y)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> x
f