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

-- | Distributivity of a tensor over coproducts: a 'Distributive' category has 'distL'\/'distR' and
-- absorption by the initial object, and a 'DistributiveProfunctor' is monoidal for both tensor and
-- coproduct. Also home to 'Traversable' and 'Cotraversable' profunctors, which distribute any
-- 'StrongDistributiveProfunctor' and underlie 'Proarrow.Optic.Traversal.Traversal'.
module Proarrow.Category.Monoidal.Distributive where

import Data.Bifunctor (bimap)
import Data.Kind (Constraint, Type)
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Free (Elems, FREE, Free (..), HasStructure (..), Lower, withLowerOb)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), first, second, type (**!))
import Proarrow.Category.Monoidal.Action (CoprodAction)
import Proarrow.Category.Monoidal.Closed (Closed (..), uncurry)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Strength (MonStrong, Strong (..))
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , codiag
  , (++)
  , type (+)
  )
import Proarrow.Colimit.Initial (HasInitialObject (..), InitF)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), lmap, obj, (//), (:~>), type (+->))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), coindex, corepUniv)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Rep (..), RepCostar (..), Representable (..), repUniv)
import Proarrow.Tools.Laws (Inverses (..), Labelled (..), Laws (..), inverses)
import Prelude (($))

class (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p
instance (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p

-- | A distributive monoidal category: the tensor distributes over coproducts, and annihilates the
-- 'InitialObject'. The monoidal and coproduct worlds meet here.
--
-- __Laws:__
--
-- Each of the four arrows is invertible, with the named inverse:
--
-- * @'distL'@ is inverse to 'distLInv', and @'distR'@ to 'distRInv'
-- * @'absorbL'@ and @'absorbR'@ are inverse to 'Proarrow.Colimit.Initial.initiate'
--
-- Checked by 'Proarrow.Testing.Laws.testDistributive'.
class (Monoidal k, HasCoproducts k) => Distributive k where
  -- | Distributes a tensor on the left over a coproduct.
  distL :: (Ob (a :: k), Ob b, Ob c) => (a ** (b || c)) ~> (a ** b || a ** c)

  -- | Distributes a tensor on the right over a coproduct.
  distR :: (Ob (a :: k), Ob b, Ob c) => ((a || b) ** c) ~> (a ** c || b ** c)

  -- | The 'InitialObject' annihilates the tensor on the right.
  absorbL :: (Ob (a :: k)) => (a ** InitialObject) ~> InitialObject

  -- | The 'InitialObject' annihilates the tensor on the left.
  absorbR :: (Ob (a :: k)) => (InitialObject ** a) ~> InitialObject

-- | The structures the free category needs for 'Distributive', and those its laws are stated for.
type DistributiveStructures :: [Kind -> Constraint]
type DistributiveStructures = '[Monoidal, HasInitialObject, HasBinaryCoproducts, Distributive]

-- | The free-category structure for 'Distributive': formal distributors and absorbers,
-- interpreted by 'foldStructure' through the target's own. Together with the coproduct and
-- monoidal structures this makes a free category over a bare quiver distributive without asking
-- anything of the quiver's category.
instance
  (DistributiveStructures `Elems` cs)
  => HasStructure cs (p :: CAT k) Distributive
  where
  data Struct Distributive i o where
    DistL :: (Ob a, Ob b, Ob c) => Struct Distributive (a **! (b + c)) ((a **! b) + (a **! c))
    DistR :: (Ob a, Ob b, Ob c) => Struct Distributive ((a + b) **! c) ((a **! c) + (b **! c))
    AbsorbL :: (Ob a) => Struct Distributive (a **! InitF) InitF
    AbsorbR :: (Ob a) => Struct Distributive (InitF **! a) InitF
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Distributive k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct Distributive a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (DistL @a @b @c) =
    forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @c (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @_ @(Lower f a) @(Lower f b) @(Lower f c))))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (DistR @a @b @c) =
    forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @c (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @_ @(Lower f a) @(Lower f b) @(Lower f c))))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (AbsorbL @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @_ @(Lower f a))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (AbsorbR @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @_ @(Lower f a))

instance P.Show (Struct Distributive a b) where
  showsPrec :: Int -> Struct Distributive a b -> ShowS
showsPrec Int
_ Struct Distributive a b
R:StructkcspDistributiveio k cs p a b
DistL = String -> ShowS
P.showString String
"distL"
  showsPrec Int
_ Struct Distributive a b
R:StructkcspDistributiveio k cs p a b
DistR = String -> ShowS
P.showString String
"distR"
  showsPrec Int
_ Struct Distributive a b
R:StructkcspDistributiveio k cs p a b
AbsorbL = String -> ShowS
P.showString String
"absorbL"
  showsPrec Int
_ Struct Distributive a b
R:StructkcspDistributiveio k cs p a b
AbsorbR = String -> ShowS
P.showString String
"absorbR"

instance (DistributiveStructures `Elems` cs) => Distributive (FREE cs (p :: CAT k)) where
  distL :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL = Struct Distributive (a **! (b + c)) ((a **! b) + (a **! c))
-> Free (a **! (b + c)) (a **! (b + c))
-> Free (a **! (b + c)) ((a **! b) + (a **! c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct Distributive (a **! (b + c)) ((a **! b) + (a **! c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Distributive (a **! (b + c)) ((a **! b) + (a **! c))
DistL Free (a **! (b + c)) (a **! (b + c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  distR :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR = Struct Distributive ((a + b) **! c) ((a **! c) + (b **! c))
-> Free ((a + b) **! c) ((a + b) **! c)
-> Free ((a + b) **! c) ((a **! c) + (b **! c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct Distributive ((a + b) **! c) ((a **! c) + (b **! c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Distributive ((a + b) **! c) ((a **! c) + (b **! c))
DistR Free ((a + b) **! c) ((a + b) **! c)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  absorbL :: forall (a :: FREE cs p).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL = Struct Distributive (a **! InitF) InitF
-> Free (a **! InitF) (a **! InitF) -> Free (a **! InitF) InitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct Distributive (a **! InitF) InitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Distributive (a **! InitF) InitF
AbsorbL Free (a **! InitF) (a **! InitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  absorbR :: forall (a :: FREE cs p).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR = Struct Distributive (InitF **! a) InitF
-> Free (InitF **! a) (InitF **! a) -> Free (InitF **! a) InitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct Distributive (InitF **! a) InitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Distributive (InitF **! a) InitF
AbsorbR Free (InitF **! a) (InitF **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

distLInv
  :: forall {k} a b c. (Distributive k, Ob (a :: k), Ob b, Ob c) => (a ** b || a ** c) ~> (a ** (b || c))
distLInv :: forall {k} (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** b) || (a ** c)) ~> (a ** (b || c))
distLInv = forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @a (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @b @c) ((a ** b) ~> (a ** (b || c)))
-> ((a ** c) ~> (a ** (b || c)))
-> ((a ** b) || (a ** c)) ~> (a ** (b || c))
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @a (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @c)

distRInv
  :: forall {k} a b c. (Distributive k, Ob (a :: k), Ob b, Ob c) => (a ** c || b ** c) ~> ((a || b) ** c)
distRInv :: forall {k} (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** c) || (b ** c)) ~> ((a || b) ** c)
distRInv = forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) ((a ** c) ~> ((a || b) ** c))
-> ((b ** c) ~> ((a || b) ** c))
-> ((a ** c) || (b ** c)) ~> ((a || b) ** c)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b)

-- | Distributive promonads seem similar to selective applicative functors.
-- https://blog.veritates.love/selective_applicatives_theoretical_basis.html
branch
  :: forall {k} a b c i (p :: k +-> k)
   . (DistributiveProfunctor p, Promonad p, Distributive k, Ob a, Ob b, Ob c)
  => p i (a || b) -> p a c -> p b c -> p i c
branch :: forall {k} (a :: k) (b :: k) (c :: k) (i :: k) (p :: k +-> k).
(DistributiveProfunctor p, Promonad p, Distributive k, Ob a, Ob b,
 Ob c) =>
p i (a || b) -> p a c -> p b c -> p i c
branch p i (a || b)
pab p a c
pac p b c
pbc = ((c || c) ~> c) -> p i (c || c) -> p i c
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 (c || c) ~> c
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag ((p a c
pac p a c -> p b c -> p (a || b) (c || c)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p b c
pbc) p (a || b) (c || c) -> p i (a || b) -> p i (c || c)
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> 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
. p i (a || b)
pab)

instance Distributive Type where
  distL :: forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL (a
a, Either b c
e) = (b -> (a, b))
-> (c -> (a, c)) -> Either b c -> Either (a, b) (a, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (a
a,) (a
a,) Either b c
e
  distR :: forall a b c.
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR (Either a b
e, c
c) = (a -> (a, c))
-> (b -> (b, c)) -> Either a b -> Either (a, c) (b, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (,c
c) (,c
c) Either a b
e
  absorbL :: forall a. Ob a => (a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
(a, Void) -> Void
forall a b. (a, b) -> b
P.snd
  absorbR :: forall a. Ob a => (InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
(Void, a) -> Void
forall a b. (a, b) -> a
P.fst

instance Distributive () where
  distL :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL = (a ** (b || c)) ~> ((a ** b) || (a ** c))
Unit '() '()
U.Unit
  distR :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR = ((a || b) ** c) ~> ((a ** c) || (b ** c))
Unit '() '()
U.Unit
  absorbL :: forall (a :: ()). Ob a => (a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
Unit '() '()
U.Unit
  absorbR :: forall (a :: ()). Ob a => (InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
Unit '() '()
U.Unit

instance Distributive BOOL where
  distL :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (b || c) ~> (b || c)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c
  distR :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c of
    Obj c
Booleans c c
Fls -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
Booleans 'FLS 'FLS
Fls
    Obj c
Booleans c c
Tru -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> (a || b) ~> (a || b)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b
  absorbL :: forall (a :: BOOL). Ob a => (a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
Booleans 'FLS 'FLS
Fls
  absorbR :: forall (a :: BOOL). Ob a => (InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
Booleans 'FLS 'FLS
Fls

-- | A product of distributive categories distributes componentwise.
instance (Distributive j, Distributive k) => Distributive (j, k) where
  distL :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @'(a1, a2) @'(b1, b2) @'(c1, c2) = forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @j @a1 @b1 @c1 (((Fst @ a) ** ((Fst @ b) || (Fst @ c)))
 ~> (((Fst @ a) ** (Fst @ b)) || ((Fst @ a) ** (Fst @ c))))
-> (((Snd @ a) ** ((Snd @ b) || (Snd @ c)))
    ~> (((Snd @ a) ** (Snd @ b)) || ((Snd @ a) ** (Snd @ c))))
-> (:**:)
     (~>)
     (~>)
     '((Fst @ a) ** ((Fst @ b) || (Fst @ c)),
       (Snd @ a) ** ((Snd @ b) || (Snd @ c)))
     '(((Fst @ a) ** (Fst @ b)) || ((Fst @ a) ** (Fst @ c)),
       ((Snd @ a) ** (Snd @ b)) || ((Snd @ a) ** (Snd @ c)))
forall {j1} {k1} {j2} {k2} (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)
:**: forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @k @a2 @b2 @c2
  distR :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @'(a1, a2) @'(b1, b2) @'(c1, c2) = forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @j @a1 @b1 @c1 ((((Fst @ a) || (Fst @ b)) ** (Fst @ c))
 ~> (((Fst @ a) ** (Fst @ c)) || ((Fst @ b) ** (Fst @ c))))
-> ((((Snd @ a) || (Snd @ b)) ** (Snd @ c))
    ~> (((Snd @ a) ** (Snd @ c)) || ((Snd @ b) ** (Snd @ c))))
-> (:**:)
     (~>)
     (~>)
     '(((Fst @ a) || (Fst @ b)) ** (Fst @ c),
       ((Snd @ a) || (Snd @ b)) ** (Snd @ c))
     '(((Fst @ a) ** (Fst @ c)) || ((Fst @ b) ** (Fst @ c)),
       ((Snd @ a) ** (Snd @ c)) || ((Snd @ b) ** (Snd @ c)))
forall {j1} {k1} {j2} {k2} (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)
:**: forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @k @a2 @b2 @c2
  absorbL :: forall (a :: (j, k)). Ob a => (a ** InitialObject) ~> InitialObject
absorbL @'(a1, a2) = forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @j @a1 (((Fst @ a) ** InitialObject) ~> InitialObject)
-> (((Snd @ a) ** InitialObject) ~> InitialObject)
-> (:**:)
     (~>)
     (~>)
     '((Fst @ a) ** InitialObject, (Snd @ a) ** InitialObject)
     '(InitialObject, InitialObject)
forall {j1} {k1} {j2} {k2} (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)
:**: forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @k @a2
  absorbR :: forall (a :: (j, k)). Ob a => (InitialObject ** a) ~> InitialObject
absorbR @'(a1, a2) = forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @j @a1 ((InitialObject ** (Fst @ a)) ~> InitialObject)
-> ((InitialObject ** (Snd @ a)) ~> InitialObject)
-> (:**:)
     (~>)
     (~>)
     '(InitialObject ** (Fst @ a), InitialObject ** (Snd @ a))
     '(InitialObject, InitialObject)
forall {j1} {k1} {j2} {k2} (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)
:**: forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @k @a2

distLClosed
  :: forall {k} (a :: k) (b :: k) (c :: k)
   . (Closed k, SymMonoidal k, HasBinaryCoproducts k, Ob a, Ob b, Ob c) => (a ** (b || c)) ~> (a ** b || a ** c)
distLClosed :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, SymMonoidal k, HasBinaryCoproducts k, Ob a, Ob b,
 Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distLClosed = (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @a ((b ** a) ~> (a ** b))
-> ((c ** a) ~> (a ** c))
-> ((b ** a) || (c ** a)) ~> ((a ** b) || (a ** c))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @a) (((b ** a) || (c ** a)) ~> ((a ** b) || (a ** c)))
-> ((a ** (b || c)) ~> ((b ** a) || (c ** a)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** 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
. forall (a :: k) (b :: k) (c :: k).
(Closed k, HasBinaryCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, HasBinaryCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distRClosed @b @c @a (((b || c) ** a) ~> ((b ** a) || (c ** a)))
-> ((a ** (b || c)) ~> ((b || c) ** a))
-> (a ** (b || c)) ~> ((b ** a) || (c ** a))
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
. forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @b @c (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @(b || c))

distRClosed
  :: forall {k} (a :: k) (b :: k) (c :: k)
   . (Closed k, HasBinaryCoproducts k, Ob a, Ob b, Ob c) => ((a || b) ** c) ~> (a ** c || b ** c)
distRClosed :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, HasBinaryCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distRClosed =
  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @c ((Ob (a ** c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (a ** c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @c ((Ob (b ** c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (b ** c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(a ** c) @(b ** c) ((Ob ((a ** c) || (b ** c)) =>
  ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob ((a ** c) || (b ** c)) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
        forall (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @c (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @(a ** c) @(b ** c)) (a ~> (c ~~> ((a ** c) || (b ** c))))
-> (b ~> (c ~~> ((a ** c) || (b ** c))))
-> (a || b) ~> (c ~~> ((a ** c) || (b ** c)))
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @b @c (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @(a ** c) @(b ** c)))

class
  (DistributiveProfunctor (p :: k +-> k), MonStrong p, Strong CoprodAction p) =>
  StrongDistributiveProfunctor (p :: k +-> k)
instance
  (DistributiveProfunctor (p :: k +-> k), MonStrong p, Strong CoprodAction p)
  => StrongDistributiveProfunctor (p :: k +-> k)

-- | The constant functor absorbs a coproduct action: the injected summand is discarded onto
-- the monoid's unit, so this needs only copying\/discarding on the tensor side and coproducts.
instance (CopyDiscard k, HasCoproducts k, Monoid r) => Strong CoprodAction (Rep (Constant r) :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
Rep (Constant r) x y
-> Rep (Constant r) (Act CoprodAction a x) (Act CoprodAction a y)
act @(COPR a) (Rep @y x ~> (Constant r @ y)
p) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @y (((UN COPR a || x) ~> (Constant r @ (UN COPR a || y)))
-> Rep (Constant r) (UN COPR a || x) (UN COPR a || y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @r (Unit ~> r) -> (UN COPR a ~> Unit) -> UN COPR a ~> r
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
. forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a (UN COPR a ~> r) -> (x ~> r) -> (UN COPR a || x) ~> r
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| x ~> r
x ~> (Constant r @ y)
p))

type Traversable :: forall {k}. (k +-> k) -> Constraint
class (Profunctor t) => Traversable (t :: k +-> k) where
  traverse :: (StrongDistributiveProfunctor p) => t :.: p :~> p :.: t

-- | With a representable traversable profunctor, you get a traversal a la one-liner.
repTraverse
  :: forall {k} (t :: k +-> k) p a b
   . (Traversable t, Representable t, StrongDistributiveProfunctor p)
  => p a b -> p (t % a) (t % b)
repTraverse :: forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
repTraverse p a b
p = p a b
p p a b -> ((Ob a, Ob b) => p (t % a) (t % b)) -> p (t % a) (t % b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case (:.:) t p (t % a) b -> (:.:) p t (t % a) b
(t :.: p) :~> (p :.: t)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(t :.: p) :~> (p :.: t)
traverse (t (t % a) a
forall (a :: k). Ob a => t (t % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv t (t % a) a -> p a b -> (:.:) t p (t % a) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p) of p (t % a) b
x :.: t b b
y -> (b ~> (t % b)) -> p (t % a) b -> p (t % a) (t % b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @t t b b
y) p (t % a) b
x

-- | If both profunctors are representable, you get traversals as in base.
baseTraverse
  :: forall {k} (t :: k +-> k) f a b
   . (Traversable t, Representable t, Representable f, StrongDistributiveProfunctor f, Ob b)
  => a ~> f % b -> t % a ~> f % (t % b)
baseTraverse :: forall {k} (t :: k +-> k) (f :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, Representable f,
 StrongDistributiveProfunctor f, Ob b) =>
(a ~> (f % b)) -> (t % a) ~> (f % (t % b))
baseTraverse = f (t % a) (t % b) -> (t % a) ~> (f % (t % b))
forall (a :: k) (b :: k). f a b -> a ~> (f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (f (t % a) (t % b) -> (t % a) ~> (f % (t % b)))
-> ((a ~> (f % b)) -> f (t % a) (t % b))
-> (a ~> (f % b))
-> (t % a) ~> (f % (t % b))
forall b c a. (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
. forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
repTraverse @t @f @a @b (f a b -> f (t % a) (t % b))
-> ((a ~> (f % b)) -> f a b) -> (a ~> (f % b)) -> f (t % a) (t % b)
forall b c a. (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 ~> (f % b)) -> f a b
forall (b :: k) (a :: k). Ob b => (a ~> (f % b)) -> f a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate

instance (CategoryOf k) => Traversable (Id :: k +-> k) where
  traverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(Id :.: p) :~> (p :.: Id)
traverse (Id a ~> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall (c :: k) (a :: k) (b :: k). (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 a ~> b
f p b b
p p a b -> Id b b -> (:.:) p Id a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob b, Ob b) => (:.:) p Id a b) -> p b b -> (:.:) p Id a b
forall (a :: k) (b :: k) 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 b b
p

instance Traversable (->) where
  traverse :: forall (p :: Type -> Type -> Type).
StrongDistributiveProfunctor p =>
((->) :.: p) :~> (p :.: (->))
traverse (a -> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall c a b. (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 a ~> b
a -> b
f p b b
p p a b -> (b -> b) -> (:.:) p (->) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: b -> b
forall a. Ob a => a -> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Traversable p, Traversable q) => Traversable (p :.: q) where
  traverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
((p :.: q) :.: p) :~> (p :.: (p :.: q))
traverse ((p a b
p :.: q b b
q) :.: p b b
r) = case (:.:) q p b b -> (:.:) p q b b
(q :.: p) :~> (p :.: q)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(q :.: p) :~> (p :.: q)
traverse (q b b
q q b b -> p b b -> (:.:) q p b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of
    p b b
r' :.: q b b
q' -> case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r') of
      p a b
r'' :.: p b b
p' -> p a b
r'' p a b -> (:.:) p q b b -> (:.:) p (p :.: q) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q')

instance (Traversable p, Traversable q) => Traversable (p :+: q) where
  traverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
((p :+: q) :.: p) :~> (p :.: (p :+: q))
traverse (InjL p a b
p :.: p b b
r) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of p a b
r' :.: p b b
p' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b -> (:+:) p q b b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL p b b
p'
  traverse (InjR q a b
q :.: p b b
r) = case (:.:) q p a b -> (:.:) p q a b
(q :.: p) :~> (p :.: q)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(q :.: p) :~> (p :.: q)
traverse (q a b
q q a b -> p b b -> (:.:) q p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of p a b
r' :.: q b b
q' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b -> (:+:) p q b b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR q b b
q'

type Cotraversable :: forall {k}. (k +-> k) -> Constraint
class (Profunctor t) => Cotraversable (t :: k +-> k) where
  cotraverse :: (StrongDistributiveProfunctor (p :: k +-> k)) => p :.: t :~> t :.: p

-- | With a corepresentable cotraversable profunctor, you get a co-traversal a la one-liner.
corepTraverse
  :: forall {k} (t :: k +-> k) p a b
   . (Cotraversable t, Corepresentable t, StrongDistributiveProfunctor p)
  => p a b -> p (t %% a) (t %% b)
corepTraverse :: forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t,
 StrongDistributiveProfunctor p) =>
p a b -> p (t %% a) (t %% b)
corepTraverse p a b
p = p a b
p p a b
-> ((Ob a, Ob b) => p (t %% a) (t %% b)) -> p (t %% a) (t %% b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case (:.:) p t a (t %% b) -> (:.:) t p a (t %% b)
(p :.: t) :~> (t :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: t) :~> (t :.: p)
cotraverse (p a b
p p a b -> t b (t %% b) -> (:.:) p t a (t %% b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: t b (t %% b)
forall (a :: k). Ob a => t a (t %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv) of t a b
x :.: p b (t %% b)
y -> ((t %% a) ~> b) -> p b (t %% b) -> p (t %% a) (t %% b)
forall (c :: k) (a :: k) (b :: k). (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 (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @t t a b
x) p b (t %% b)
y

instance (CategoryOf k) => Cotraversable (Id :: k +-> k) where
  cotraverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: Id) :~> (Id :.: p)
cotraverse (p a b
p :.: Id b ~> b
f) = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> p a b -> (:.:) Id p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> p a b -> p a b
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 ~> b
f p a b
p ((Ob a, Ob b) => (:.:) Id p a b) -> p a b -> (:.:) Id p a b
forall (a :: k) (b :: k) 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

instance Cotraversable (->) where
  cotraverse :: forall (p :: Type -> Type -> Type).
StrongDistributiveProfunctor p =>
(p :.: (->)) :~> ((->) :.: p)
cotraverse (p a b
p :.: b -> b
f) = a -> a
forall a. Ob a => a -> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (a -> a) -> p a b -> (:.:) (->) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> p a b -> p a b
forall b d a. (b ~> d) -> p a b -> 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 ~> b
b -> b
f p a b
p

instance (Cotraversable p, Cotraversable q) => Cotraversable (p :.: q) where
  cotraverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: (p :.: q)) :~> ((p :.: q) :.: p)
cotraverse (p a b
r :.: (p b b
p :.: q b b
q)) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p) of
    p a b
p' :.: p b b
r' -> case (:.:) p q b b -> (:.:) q p b b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: q) :~> (q :.: p)
cotraverse (p b b
r' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q) of
      q b b
q' :.: p b b
r'' -> (p a b
p' p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q') (:.:) p q a b -> p b b -> (:.:) (p :.: q) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r''

instance (HasBinaryCoproducts k, Cotraversable p, Cotraversable q) => Cotraversable ((p :: k +-> k) :*: q) where
  cotraverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: (p :*: q)) :~> ((p :*: q) :.: p)
cotraverse (p a b
r :.: (p b b
p :*: q b b
q)) = case ((:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p), (:.:) p q a b -> (:.:) q p a b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: q) :~> (q :.: p)
cotraverse (p a b
r p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q)) of
    ((:.:) @a p a b
p' p b b
r', (:.:) @b q a b
q' p b b
r'') -> ((b ~> (b || b)) -> p a b -> p a (b || b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) p a b
p' p a (b || b) -> q a (b || b) -> (:*:) p q a (b || b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: (b ~> (b || b)) -> q a b -> q a (b || b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> q a b -> q 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 (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b) q a b
q') (:*:) p q a (b || b) -> p (b || b) b -> (:.:) (p :*: q) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((b || b) ~> b) -> p (b || b) (b || b) -> p (b || b) b
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 || b) ~> b
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag (p b b
r' p b b -> p b b -> p (b || b) (b || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p b b
r'') ((Ob b, Ob b) => (:.:) (p :*: q) p a b)
-> p b b -> (:.:) (p :*: q) p a b
forall (a :: k) (b :: k) 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 b b
p ((Ob a, Ob b) => (:.:) (p :*: q) p a b)
-> p a b -> (:.:) (p :*: q) p a b
forall (a :: k) (b :: k) 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 a, Ob b) => (:.:) (p :*: q) p a b)
-> q a b -> (:.:) (p :*: q) p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> q 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
\\ q a b
q'

instance (Cotraversable p, Cotraversable q) => Cotraversable (p :+: q) where
  cotraverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: (p :+: q)) :~> ((p :+: q) :.: p)
cotraverse (p a b
r :.: InjL p b b
p) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
cotraverse (p a b
r p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p) of p a b
p' :.: p b b
r' -> p a b -> (:+:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL p a b
p' (:+:) p q a b -> p b b -> (:.:) (p :+: q) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r'
  cotraverse (p a b
r :.: InjR q b b
q) = case (:.:) p q a b -> (:.:) q p a b
(p :.: q) :~> (q :.: p)
forall {k} (t :: k +-> k) (p :: k +-> k).
(Cotraversable t, StrongDistributiveProfunctor p) =>
(p :.: t) :~> (t :.: p)
forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: q) :~> (q :.: p)
cotraverse (p a b
r p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q) of q a b
q' :.: p b b
r' -> q a b -> (:+:) p q a b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR q a b
q' (:+:) p q a b -> p b b -> (:.:) (p :+: q) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r'

-- | This breaks for possibly infinite traversals like Star [].
instance (Traversable t, Representable t) => Cotraversable (RepCostar t) where
  cotraverse :: forall (p :: k +-> k).
StrongDistributiveProfunctor p =>
(p :.: RepCostar t) :~> (RepCostar t :.: p)
cotraverse (p a b
p :.: RepCostar (t % b) ~> b
t) = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (RepCostar t) p a b)
-> (:.:) (RepCostar t) p a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case forall {k} (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (t :: k +-> k) (p :: k +-> k).
(Traversable t, StrongDistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
traverse @t (t (t % a) a
forall (a :: k). Ob a => t (t % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv t (t % a) a -> p a b -> (:.:) t p (t % a) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p) of p (t % a) b
p' :.: t b b
t' -> RepCostar t a (RepCostar t %% a)
RepCostar t a (t % a)
forall (a :: k). Ob a => RepCostar t a (RepCostar t %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv RepCostar t a (t % a) -> p (t % a) b -> (:.:) (RepCostar t) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> p (t % a) b -> p (t % a) b
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> 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 ((t % b) ~> b
t ((t % b) ~> b) -> (b ~> (t % b)) -> 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
. t b b -> b ~> (t % b)
forall (a :: k) (b :: k). t a b -> a ~> (t % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index t b b
t') p (t % a) b
p'

-- | The tensor distributes over coproducts and is absorbed by the initial object:
-- 'distL', 'distR', 'absorbL' and 'absorbR' are isomorphisms, with the inverses 'distLInv',
-- 'distRInv' and 'initiate'.
instance Laws DistributiveStructures where
  laws :: [Law DistributiveStructures]
laws =
    String
-> PureLawBody DistributiveStructures Inverses
-> [Law DistributiveStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"distL" (\ @a @b @c -> ((a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (((a ** b) || (a ** c)) ~> (a ** (b || c))) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @_ @a @b @c) (String
-> (((a ** b) || (a ** c)) ~> (a ** (b || c)))
-> ((a ** b) || (a ** c)) ~> (a ** (b || c))
forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b
forall k (a :: k) (b :: k).
Labelled k =>
String -> (a ~> b) -> a ~> b
label String
"distLInv" (forall (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** b) || (a ** c)) ~> (a ** (b || c))
forall {k} (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** b) || (a ** c)) ~> (a ** (b || c))
distLInv @a @b @c)))
      [Law DistributiveStructures]
-> [Law DistributiveStructures] -> [Law DistributiveStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> PureLawBody DistributiveStructures Inverses
-> [Law DistributiveStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"distR" (\ @a @b @c -> (((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (((a ** c) || (b ** c)) ~> ((a || b) ** c)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @_ @a @b @c) (String
-> (((a ** c) || (b ** c)) ~> ((a || b) ** c))
-> ((a ** c) || (b ** c)) ~> ((a || b) ** c)
forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b
forall k (a :: k) (b :: k).
Labelled k =>
String -> (a ~> b) -> a ~> b
label String
"distRInv" (forall (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** c) || (b ** c)) ~> ((a || b) ** c)
forall {k} (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a ** c) || (b ** c)) ~> ((a || b) ** c)
distRInv @a @b @c)))
      [Law DistributiveStructures]
-> [Law DistributiveStructures] -> [Law DistributiveStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> PureLawBody DistributiveStructures Inverses
-> [Law DistributiveStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses
        String
"absorbL"
        (\ @a -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @InitialObject (((a ** InitialObject) ~> InitialObject)
-> (InitialObject ~> (a ** InitialObject)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @_ @a) InitialObject ~> (a ** InitialObject)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))
      [Law DistributiveStructures]
-> [Law DistributiveStructures] -> [Law DistributiveStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> PureLawBody DistributiveStructures Inverses
-> [Law DistributiveStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses
        String
"absorbR"
        (\ @a -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @InitialObject @a (((InitialObject ** a) ~> InitialObject)
-> (InitialObject ~> (InitialObject ** a)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @_ @a) InitialObject ~> (InitialObject ** a)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))