{-# LANGUAGE MonoLocalBinds #-}
module Control.Category.Tensor
  ( -- * Iso
    Iso (..),

    -- * GBifunctor
    GBifunctor (..),
    (#),
    grmap,
    glmap,
    -- * Associative
    Associative (..),

    -- * Tensor
    Tensor (..),

    -- * Symmetric
    Symmetric (..),
  )
where

--------------------------------------------------------------------------------

import Control.Applicative (Applicative (..))
import Control.Category (Category (..))
import Data.Biapplicative (Biapplicative (..), Bifunctor (..))
import Data.Functor.Contravariant (Op (..))
import Data.Profunctor (Profunctor (..), Star (..))
import Data.These (These (..), these)
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

--------------------------------------------------------------------------------

-- | An invertible mapping between 'a' and 'b' in category 'cat'.
--
-- === Laws
--
-- @
-- 'fwd' '.' 'bwd' ≡ 'id'
-- 'bwd' '.' 'fwd' ≡ 'id'
-- @
data Iso cat a b = Iso { forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd :: cat a b, forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd :: cat b a }

instance Category cat => Category (Iso cat) where
  id :: Iso cat a a
  id :: forall a. Iso cat a a
id = forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

  (.) :: Iso cat b c -> Iso cat a b -> Iso cat a c
  Iso cat b c
bc . :: forall b c a. Iso cat b c -> Iso cat a b -> Iso cat a c
. Iso cat a b
ab = forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso cat b c
bc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso cat a b
ab) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso cat a b
ab forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso cat b c
bc)

--------------------------------------------------------------------------------

-- | A Bifunctor @t@ is a 'Functor' whose domain is the product of two
-- categories. 'GBifunctor' is equivalent to the ordinary
-- 'Data.Bifunctor.Bifunctor' class but we replace the implicit '(->)' 'Category' with
-- three distinct higher kinded variables @cat1@, @cat2@, and @cat3@ allowing the user
-- to pickout a functor from \(cat_1 \times cat_2\) to \(cat_3\).
--
-- === Laws
--
-- @
-- 'gbimap' 'id' 'id' ≡ 'id'
-- 'grmap' 'id' ≡ 'id'
-- 'glmap' 'id' ≡ 'id'
--
-- 'gbimap' (f '.' g) (h '.' i) ≡ 'gbimap' f h '.' 'gbimap' g i
-- 'grmap' (f '.' g) ≡ 'grmap' f '.' 'grmap' g
-- 'glmap' (f '.' g) ≡ 'glmap' f '.' 'glmap' g
-- @
class (Category cat1, Category cat2, Category cat3) => GBifunctor cat1 cat2 cat3 t | t cat3 -> cat1 cat2 where
  -- | Covariantly map over both variables.
  --
  -- @'gbimap' f g ≡ 'glmap' f '.' 'grmap' g@
  --
  -- ==== __Examples__
  -- >>> gbimap @(->) @(->) @(->) @(,) show not (123, False)
  -- ("123",True)
  --
  -- >>> gbimap @(->) @(->) @(->) @Either show not (Right False)
  -- Right True
  --
  -- >>> getOp (gbimap @Op @Op @Op @Either (Op (+ 1)) (Op show)) (Right True)
  -- Right "True"
  gbimap :: cat1 a b -> cat2 c d -> cat3 (a `t` c)  (b `t` d)

-- | Infix operator for 'gbimap'.
infixr 9 #
(#) :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat2 c d -> cat3 (a `t` c)  (b `t` d)
# :: forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
(#) = forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
gbimap

-- | Covariantally map over the right variable.
grmap :: GBifunctor cat1 cat2 cat3 t => cat2 c d -> cat3 (a `t` c) (a `t` d)
grmap :: forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) c d a.
GBifunctor cat1 cat2 cat3 t =>
cat2 c d -> cat3 (t a c) (t a d)
grmap = forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
(#) forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Covariantally map over the left variable.
glmap :: GBifunctor cat1 cat2 cat3 t => cat1 a b -> cat3 (a `t` c) (b `t` c)
glmap :: forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat3 (t a c) (t b c)
glmap = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
(#) forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

instance GBifunctor (->) (->) (->) t => GBifunctor Op Op Op t where
  gbimap :: Op a b -> Op c d -> Op (t a c) (t b d)
  gbimap :: forall a b c d. Op a b -> Op c d -> Op (t a c) (t b d)
gbimap (Op b -> a
f) (Op d -> c
g) = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
gbimap b -> a
f d -> c
g

instance Bifunctor t => GBifunctor (->) (->) (->) t where
  gbimap :: forall a b c d. (a -> b) -> (c -> d) -> t a c -> t b d
gbimap = forall (t :: * -> * -> *) a b c d.
Bifunctor t =>
(a -> b) -> (c -> d) -> t a c -> t b d
bimap

instance GBifunctor (Star Maybe) (Star Maybe) (Star Maybe) These where
  gbimap :: Star Maybe a b -> Star Maybe c d -> Star Maybe (These a c) (These b d)
  gbimap :: forall a b c d.
Star Maybe a b
-> Star Maybe c d -> Star Maybe (These a c) (These b d)
gbimap (Star a -> Maybe b
f) (Star c -> Maybe d
g) =
    forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \case
      This a
a    -> forall a b. a -> These a b
This forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a
      That c
c    -> forall a b. b -> These a b
That forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Maybe d
g c
c
      These a
a c
c -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a b. a -> b -> These a b
These (a -> Maybe b
f a
a) (c -> Maybe d
g c
c)

instance GBifunctor cat cat cat t => GBifunctor (Iso cat) (Iso cat) (Iso cat) t where
  gbimap :: Iso cat a b -> Iso cat c d -> Iso cat (t a c) (t b d)
  gbimap :: forall a b c d.
Iso cat a b -> Iso cat c d -> Iso cat (t a c) (t b d)
gbimap Iso cat a b
iso1 Iso cat c d
iso2 = forall (cat :: * -> * -> *) a b. cat a b -> cat b a -> Iso cat a b
Iso (forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
gbimap (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso cat a b
iso1) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd Iso cat c d
iso2)) (forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c d.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat2 c d -> cat3 (t a c) (t b d)
gbimap (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso cat a b
iso1) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd Iso cat c d
iso2))

--------------------------------------------------------------------------------

-- | A bifunctor \(\_\otimes\_: \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is
-- 'Associative' if it is equipped with a
-- <https://ncatlab.org/nlab/show/natural+isomorphism natural isomorphism> of the form
-- \(\alpha_{x,y,z} : (x \otimes (y \otimes z)) \to ((x \otimes y) \otimes z)\), which
-- we call 'assoc'.
--
-- === Laws
--
-- @
-- 'fwd' 'assoc' '.' 'bwd' 'assoc' ≡ 'id'
-- 'bwd' 'assoc' '.' 'fwd' 'assoc' ≡ 'id'
-- @
class (Category cat, GBifunctor cat cat cat t) => Associative cat t where
  -- | The <https://ncatlab.org/nlab/show/natural+isomorphism natural isomorphism> between left and
  -- right associated nestings of @t@.
  --
  -- ==== __Examples__
  --
  -- >>> :t assoc @(->) @(,) 
  -- assoc @(->) @(,) :: Iso (->) (a, (b, c)) ((a, b), c)
  --
  -- >>> fwd (assoc @(->) @(,)) (1, ("hello", True))
  -- ((1,"hello"),True)
  assoc :: Iso cat (a `t` (b `t` c)) ((a `t` b) `t` c)

instance Associative (->) t => Associative Op t where
  assoc :: Iso Op (a `t` (b `t` c)) ((a `t` b) `t` c)
  assoc :: forall a b c. Iso Op (t a (t b c)) (t (t a b) c)
assoc = Iso
    { fwd :: Op (t a (t b c)) (t (t a b) c)
fwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) a b c.
Associative cat t =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc
    , bwd :: Op (t (t a b) c) (t a (t b c))
bwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) a b c.
Associative cat t =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc
    }

instance Associative (->) (,) where
  assoc :: Iso (->) (a, (b, c)) ((a, b), c)
  assoc :: forall a b c. Iso (->) (a, (b, c)) ((a, b), c)
assoc = Iso
    { fwd :: (a, (b, c)) -> ((a, b), c)
fwd = \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)
    , bwd :: ((a, b), c) -> (a, (b, c))
bwd = \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))
    }

instance Associative (->) Either where
  assoc :: Iso (->) (Either a (Either b c)) (Either (Either a b) c)
  assoc :: forall a b c.
Iso (->) (Either a (Either b c)) (Either (Either a b) c)
assoc = Iso
    { fwd :: Either a (Either b c) -> Either (Either a b) c
fwd = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right) forall a b. b -> Either a b
Right)
    , bwd :: Either (Either a b) c -> Either a (Either b c)
bwd = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left) (forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right)
    }

instance Associative (->) These where
  assoc :: Iso (->) (These a (These b c)) (These (These a b) c)
  assoc :: forall a b c. Iso (->) (These a (These b c)) (These (These a b) c)
assoc = Iso
    { fwd :: These a (These b c) -> These (These a b) c
fwd = forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these (forall a b. a -> These a b
This forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> These a b
This) (forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat3 (t a c) (t b c)
glmap forall a b. b -> These a b
That) (forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) a b c.
GBifunctor cat1 cat2 cat3 t =>
cat1 a b -> cat3 (t a c) (t b c)
glmap forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> b -> These a b
These)
    , bwd :: These (These a b) c -> These a (These b c)
bwd = forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these (forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) c d a.
GBifunctor cat1 cat2 cat3 t =>
cat2 c d -> cat3 (t a c) (t a d)
grmap forall a b. a -> These a b
This) (forall a b. b -> These a b
That forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> These a b
That) (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (t :: * -> * -> *) c d a.
GBifunctor cat1 cat2 cat3 t =>
cat2 c d -> cat3 (t a c) (t a d)
grmap forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. a -> b -> These a b
These)
    }

instance (Monad m, Associative (->) t, GBifunctor (Star m) (Star m) (Star m) t) => Associative (Star m) t where
  assoc :: Iso (Star m) (a `t` (b `t` c)) ((a `t` b) `t` c)
  assoc :: forall a b c. Iso (Star m) (t a (t b c)) (t (t a b) c)
assoc = Iso
    { fwd :: Star m (t a (t b c)) (t (t a b) c)
fwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) a b c.
Associative cat t =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc)
    , bwd :: Star m (t (t a b) c) (t a (t b c))
bwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) a b c.
Associative cat t =>
Iso cat (t a (t b c)) (t (t a b) c)
assoc)
    }

--------------------------------------------------------------------------------

-- | A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\)
-- that maps out of the <https://ncatlab.org/nlab/show/product+category product category> \(\mathcal{C} \times \mathcal{C}\)
-- is a 'Tensor' if it has:
--
-- 1. a corresponding identity type \(I\)
-- 2. Left and right <https://ncatlab.org/nlab/show/unitor#in_monoidal_categories unitor>
-- operations \(\lambda_{x} : 1 \otimes x \to x\) and \(\rho_{x} : x \otimes 1 \to x\), which we call 'unitr' and 'unitl'.
--
-- === Laws
--
-- @
-- 'fwd' 'unitr' (a ⊗ i) ≡ a
-- 'bwd' 'unitr' a ≡ (a ⊗ i)
--
-- 'fwd' 'unitl' (i ⊗ a) ≡ a 
-- 'bwd' 'unitl' a ≡ (i ⊗ a)
-- @
class Associative cat t => Tensor cat t i | t -> i where
  -- | The <https://ncatlab.org/nlab/show/natural+isomorphism natural isomorphism> between @(i \`t\` a)@ and @a@.
  --
  -- ==== __Examples__
  --
  -- >>> fwd (unitl @_ @(,)) ((), True)
  -- True
  -- 
  -- >>> bwd (unitl @_ @(,)) True
  -- ((),True)
  --
  -- >>> bwd (unitl @_ @Either) True
  -- Right True
  --
  -- >>> :t bwd (unitl @_ @Either) True
  -- bwd (unitl @_ @Either) True :: Either Void Bool
  unitl :: Iso cat (i `t` a) a
  -- | The <https://ncatlab.org/nlab/show/natural+isomorphism natural isomorphism> between @(a \`t\` i)@ and @a@.
  --
  -- ==== __Examples__
  --
  -- >>> fwd (unitr @_ @(,)) (True, ())
  -- True
  -- 
  -- >>> bwd (unitr @_ @(,)) True
  -- (True,())
  --
  -- >>> bwd (unitr @_ @Either) True
  -- Left True
  --
  -- >>> :t bwd (unitr @_ @Either) True
  -- bwd (unitr @_ @Either) True :: Either Bool Void
  unitr :: Iso cat (a `t` i) a

instance (Tensor (->) t i) => Tensor Op t i where
  unitl :: Iso Op (i `t` a) a
  unitl :: forall a. Iso Op (t i a) a
unitl = Iso
    { fwd :: Op (t i a) a
fwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t i a) a
unitl
    , bwd :: Op a (t i a)
bwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t i a) a
unitl
    }

  unitr :: Iso Op (a `t` i) a
  unitr :: forall a. Iso Op (t a i) a
unitr = Iso
    { fwd :: Op (t a i) a
fwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t a i) a
unitr
    , bwd :: Op a (t a i)
bwd = forall a b. (b -> a) -> Op a b
Op forall a b. (a -> b) -> a -> b
$ forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t a i) a
unitr
    }

instance Tensor (->) (,) () where
  unitl :: Iso (->) ((), a) a
  unitl :: forall a. Iso (->) ((), a) a
unitl = Iso
    { fwd :: ((), a) -> a
fwd = forall a b. (a, b) -> b
snd
    , bwd :: a -> ((), a)
bwd = forall (p :: * -> * -> *) a b. Biapplicative p => a -> b -> p a b
bipure ()
    }

  unitr :: Iso (->) (a, ()) a
  unitr :: forall a. Iso (->) (a, ()) a
unitr = Iso
    { fwd :: (a, ()) -> a
fwd = forall a b. (a, b) -> a
fst
    , bwd :: a -> (a, ())
bwd = (forall (p :: * -> * -> *) a b. Biapplicative p => a -> b -> p a b
`bipure` ())
    }

instance Tensor (->) Either Void where
  unitl :: Iso (->) (Either Void a) a
  unitl :: forall a. Iso (->) (Either Void a) a
unitl = Iso
     { fwd :: Either Void a -> a
fwd = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Void -> a
absurd forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
     , bwd :: a -> Either Void a
bwd = forall (f :: * -> *) a. Applicative f => a -> f a
pure
     }

  unitr :: Iso (->) (Either a Void) a
  unitr :: forall a. Iso (->) (Either a Void) a
unitr = Iso
    { fwd :: Either a Void -> a
fwd = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall a. Void -> a
absurd
    , bwd :: a -> Either a Void
bwd = forall a b. a -> Either a b
Left
    }

instance Tensor (->) These Void where
  unitl :: Iso (->) (These Void a) a
  unitl :: forall a. Iso (->) (These Void a) a
unitl = Iso
    { fwd :: These Void a -> a
fwd = forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these forall a. Void -> a
absurd forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (\ Void
_ a
x -> a
x)
    , bwd :: a -> These Void a
bwd = forall a b. b -> These a b
That
    }

  unitr :: Iso (->) (These a Void) a
  unitr :: forall a. Iso (->) (These a Void) a
unitr = Iso
    { fwd :: These a Void -> a
fwd = forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall a. Void -> a
absurd forall a b. a -> b -> a
const
    , bwd :: a -> These a Void
bwd = forall a b. a -> These a b
This
    }

instance (Monad m, Tensor (->) t i, Associative (Star m) t) => Tensor (Star m) t i where
  unitl :: Iso (Star m) (i `t` a) a
  unitl :: forall a. Iso (Star m) (t i a) a
unitl = Iso
    { fwd :: Star m (t i a) a
fwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t i a) a
unitl)
    , bwd :: Star m a (t i a)
bwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t i a) a
unitl)
    }

  unitr :: Iso (Star m) (a `t` i) a
  unitr :: forall a. Iso (Star m) (t a i) a
unitr = Iso
    { fwd :: Star m (t a i) a
fwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat a b
fwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t a i) a
unitr)
    , bwd :: Star m a (t a i)
bwd = (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
`rmap` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t a i) a
unitr)
    }

--------------------------------------------------------------------------------

-- | A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\)
-- is 'Symmetric' if it has a product operation \(B_{x,y} : x \otimes y \to y \otimes x\)
-- such that \(B_{x,y} \circ B_{x,y} \equiv 1_{x \otimes y}\), which we call 'swap'.
--
-- === Laws
--
-- @
-- 'swap' '.' 'swap' ≡ 'id'
-- @
class Associative cat t => Symmetric cat t where
  -- | @swap@ is a symmetry isomorphism for @t@
  --
  -- ==== __Examples__
  --
  -- >>> :t swap @(->) @(,)
  -- swap @(->) @(,) :: (a, b) -> (b, a)
  --
  -- >>> swap @(->) @(,) (True, "hello")
  -- ("hello",True)
  --
  -- >>> :t swap @(->) @Either (Left True)
  -- swap @(->) @Either (Left True) :: Either b Bool
  --
  -- >>> swap @(->) @Either (Left True)
  -- Right True
  swap :: cat (a `t` b) (b `t` a)

instance Symmetric (->) t => Symmetric Op t where
  swap :: Op (a `t` b) (b `t` a)
  swap :: forall a b. Op (t a b) (t b a)
swap = forall a b. (b -> a) -> Op a b
Op forall (cat :: * -> * -> *) (t :: * -> * -> *) a b.
Symmetric cat t =>
cat (t a b) (t b a)
swap

instance Symmetric (->) (,) where
  swap :: (a, b) -> (b, a)
  swap :: forall a b. (a, b) -> (b, a)
swap (a
a, b
b) = (b
b, a
a)

instance Symmetric (->) Either where
  swap :: Either a b -> Either b a
  swap :: forall a b. Either a b -> Either b a
swap = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left

instance Symmetric (->) These where
  swap :: These a b -> These b a
  swap :: forall a b. These a b -> These b a
swap = forall a c b.
(a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c
these forall a b. b -> These a b
That forall a b. a -> These a b
This (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. a -> b -> These a b
These)

instance (Monad m, Symmetric (->) t, Associative (Star m) t) => Symmetric (Star m) t where
  swap :: Star m (a `t` b) (b `t` a)
  swap :: forall a b. Star m (t a b) (t b a)
swap = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (cat :: * -> * -> *) (t :: * -> * -> *) a b.
Symmetric cat t =>
cat (t a b) (t b a)
swap