module Control.Category.Cartesian
  ( -- * Semicartesian
    Semicartesian (..),
    (/\),

    -- * Semicocartesian
    Semicocartesian (..),
    (\/),

    -- * Cartesian
    Cartesian (..),

    -- * Cocartesian
    Cocartesian (..),
  )
where

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

import Control.Category (id, (>>>))
import Control.Category.Tensor (Iso (..), Symmetric, Tensor (..), (#))
import Data.Functor.Contravariant (Op (..))
import Data.Void (Void, absurd)
import Prelude hiding (fst, id, snd)

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

-- | A 'Category' is 'Semicartesian' if it is equipped with a
-- 'Symmetric' bifunctor @t@ and each object comes equipped with a
-- <https://ncatlab.org/nlab/show/diagonal+morphism diagonal morphism>
-- \(\Delta_x: x \to x \otimes x \), which we call 'split'.
--
-- === Laws
--
-- @
-- 'Control.Category.Tensor.grmap' 'split' '.' 'split' ≡ 'bwd' 'Control.Category.Tensor.assoc' '.' 'Control.Category.Tensor.glmap' 'split' '.' 'split'
-- 'Control.Category.Tensor.glmap' 'split' '.' 'split' ≡ 'fwd' 'Control.Category.Tensor.assoc' '.' 'Control.Category.Tensor.grmap' 'split' '.' 'split'
-- @
class Symmetric cat t => Semicartesian cat t where
  -- | The <https://ncatlab.org/nlab/show/diagonal+morphism diagonal morphism> of @a@ in @cat@. We can think of 'split'
  -- as duplicating data.
  --
  -- ==== __Examples__
  --
  -- >>> split @(->) @(,) True
  -- (True,True)
  split :: cat a (a `t` a)

  -- | Given morphisms @cat a x@ and @cat a y@, construct the
  -- universal map @cat a (x \`t\` y)@.
  --
  -- ==== __Examples__
  --
  -- >>> :t fork @(->) @(,) show not
  -- fork @(->) @(,) show not :: Bool -> (String, Bool)
  --
  -- >>> fork @(->) @(,) show not True
  -- ("True",False)
  fork :: cat a x -> cat a y -> cat a (x `t` y)
  fork cat a x
f cat a y
g = forall (cat :: * -> * -> *) (t :: * -> * -> *) a.
Semicartesian cat t =>
cat a (t a a)
split forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> cat a x
f 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)
# cat a y
g

  {-# MINIMAL split #-}

-- | Infix version of 'fork'.
infixr 9 /\

(/\) :: Semicartesian cat t => cat a x -> cat a y -> cat a (x `t` y)
/\ :: forall (cat :: * -> * -> *) (t :: * -> * -> *) a x y.
Semicartesian cat t =>
cat a x -> cat a y -> cat a (t x y)
(/\) = forall (cat :: * -> * -> *) (t :: * -> * -> *) a x y.
Semicartesian cat t =>
cat a x -> cat a y -> cat a (t x y)
fork

instance Semicartesian (->) (,) where
  split :: a -> (a, a)
  split :: forall a. a -> (a, a)
split a
a = (a
a, a
a)

instance Semicocartesian (->) t => Semicartesian Op t where
  split :: Semicocartesian (->) t => Op a (t a a)
  split :: forall a. Semicocartesian (->) t => Op a (t a a)
split = forall a b. (b -> a) -> Op a b
Op forall (cat :: * -> * -> *) (t :: * -> * -> *) a.
Semicocartesian cat t =>
cat (t a a) a
merge

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

-- | A 'Category' is 'Semicocartesian' if it is equipped with a
-- 'Symmetric' type operator @t@ and each object comes equipped with a
-- morphism \(\Delta^{-1}_x: x \otimes x \to x\), which we call 'merge'.
--
-- === Laws
--
-- @
-- 'merge' '.' 'Control.Category.Tensor.grmap' 'merge' ≡ 'merge' . 'Control.Category.Tensor.glmap' 'merge' '.' 'fwd' 'Control.Category.Tensor.assoc'
-- 'merge' '.' 'Control.Category.Tensor.glmap' 'merge' ≡ 'merge' . 'Control.Category.Tensor.grmap' 'merge' '.' 'bwd' 'Control.Category.Tensor.assoc'
-- @
class Symmetric cat t => Semicocartesian cat t where
  -- | The <https://ncatlab.org/nlab/show/codiagonal co-diagonal morphism> of @a@ in @cat@.
  --
  -- ==== __Examples__
  --
  -- >>> :t merge @(->) @(Either) (Left True)
  -- merge @(->) @(Either) (Left True) :: Bool
  --
  -- >>> merge @(->) @(Either) (Left True)
  -- True
  merge :: cat (a `t` a) a

  -- | Given morphisms @cat x a@ and @cat y a@, construct the
  -- universal map @cat (x \`t\` y) a@.
  --
  -- ==== __Examples__
  fuse :: cat x a -> cat y a -> cat (x `t` y) a
  fuse cat x a
f cat y a
g = cat x a
f 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)
# cat y a
g forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (cat :: * -> * -> *) (t :: * -> * -> *) a.
Semicocartesian cat t =>
cat (t a a) a
merge

  {-# MINIMAL merge #-}

-- | Infix version of 'fuse'.
infixr 9 \/

(\/) :: Semicocartesian cat t => cat x a -> cat y a -> cat (x `t` y) a
\/ :: forall (cat :: * -> * -> *) (t :: * -> * -> *) x a y.
Semicocartesian cat t =>
cat x a -> cat y a -> cat (t x y) a
(\/) = forall (cat :: * -> * -> *) (t :: * -> * -> *) x a y.
Semicocartesian cat t =>
cat x a -> cat y a -> cat (t x y) a
fuse

instance Semicocartesian (->) Either where
  merge :: Either a a -> a
  merge :: forall a. Either a a -> a
merge = forall x a y. (x -> a) -> (y -> a) -> Either x y -> a
either 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

instance Semicartesian (->) t => Semicocartesian Op t where
  merge :: Semicartesian (->) t => Op (t a a) a
  merge :: forall a. Semicartesian (->) t => Op (t a a) a
merge = forall a b. (b -> a) -> Op a b
Op forall (cat :: * -> * -> *) (t :: * -> * -> *) a.
Semicartesian cat t =>
cat a (t a a)
split

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

-- | A 'Category' equipped with a 'Tensor' @t@ where the 'Tensor' unit @i@ is the <https://ncatlab.org/nlab/show/terminal+object terminal object>
-- in @cat@ and thus every object @a@ is equipped with a morphism \(e_x: x \to I\), which we call 'kill'.
--
-- === Laws
--
-- @
-- 'fwd' 'unitl' '.' 'Control.Category.Tensor.glmap' 'kill' '.' 'split' ≡ 'id'
-- 'fwd' 'unitr' '.' 'Control.Category.Tensor.grmap' 'kill' '.' 'split' ≡ 'id'
-- @
class (Semicartesian cat t, Tensor cat t i) => Cartesian cat t i | i -> t, t -> i where
  -- | A morphism from the @a@ to the terminal object @i@ in @cat. We
  -- can think of 'kill' as deleting data where 'split' duplicates it.
  --
  -- ==== __Examples__
  --
  -- >>> kill @(->) @(,) @() True
  -- ()
  kill :: cat a i

  -- | The left projection for @t@.
  --
  -- ==== __Examples__
  --
  -- >>> projl @(->) @(,) (True, "hello")
  -- True
  projl :: cat (x `t` y) x
  projl = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id 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 (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cartesian cat t i =>
cat a i
kill forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> 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

  -- | The right projection for @t@.
  --
  -- ==== __Examples__
  --
  -- >>> projr @(->) @(,) (True, "hello")
  -- "hello"
  projr :: cat (x `t` y) y
  projr = forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cartesian cat t i =>
cat a i
kill 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 forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> 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

  -- | Given the universal map @cat a (x `t` y)@, construct morphisms @cat a x@ and @cat a y@.
  --
  -- ==== __Examples__
  unfork :: cat a (x `t` y) -> (cat a x, cat a y)
  unfork cat a (t x y)
h = (cat a (t x y)
h forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (cat :: * -> * -> *) (t :: * -> * -> *) i x y.
Cartesian cat t i =>
cat (t x y) x
projl, cat a (t x y)
h forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (cat :: * -> * -> *) (t :: * -> * -> *) i x y.
Cartesian cat t i =>
cat (t x y) y
projr)

  {-# MINIMAL kill #-}

instance Cartesian (->) (,) () where
  kill :: a -> ()
  kill :: forall a. a -> ()
kill = forall a b. a -> b -> a
const ()

instance Cocartesian (->) t i => Cartesian Op t i where
  kill :: Cocartesian (->) t i => Op a i
  kill :: forall a. Cocartesian (->) t i => Op a i
kill = forall a b. (b -> a) -> Op a b
Op forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cocartesian cat t i =>
cat i a
spawn

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

-- | A 'Category' equipped with a 'Tensor' @t@ where the 'Tensor' unit @i@ is the <https://ncatlab.org/nlab/show/initial+object initial object>
-- in @cat@ and thus every object @a@ is equipped with a morphism \(e^{-1}_x: I \to x\), which we call 'spawn'.
--
-- === Laws
--
-- @
-- 'merge' '.' 'Control.Category.Tensor.glmap' 'spawn' '.' 'bwd' 'unitl' ≡ 'id'
-- 'merge' '.' 'Control.Category.Tensor.grmap' 'spawn' '.' 'bwd' 'unitr' ≡ 'id'
-- @
class (Semicocartesian cat t, Tensor cat t i) => Cocartesian cat t i | i -> t, t -> i where
  -- | A morphism from the initial object @i@ in @cat@ to @a@.
  --
  -- ==== __Examples__
  spawn :: cat i a

  -- | The left inclusion for @t@.
  --
  -- ==== __Examples__
  incll :: cat x (x `t` y)
  incll = 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 forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id 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 (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cocartesian cat t i =>
cat i a
spawn

  -- | The right inclusion for @t@.
  --
  -- ==== __Examples__
  inclr :: cat y (x `t` y)
  inclr = 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 forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cocartesian cat t i =>
cat i a
spawn 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

  -- | Given the universal map @cat (x `t` y) a@, construct morphisms @cat x a@ and @cat y a@.
  --
  -- ==== __Examples__
  unfuse :: cat (x `t` y) a -> (cat x a, cat y a)
  unfuse cat (t x y) a
h = (forall (cat :: * -> * -> *) (t :: * -> * -> *) i x y.
Cocartesian cat t i =>
cat x (t x y)
incll forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> cat (t x y) a
h, forall (cat :: * -> * -> *) (t :: * -> * -> *) i y x.
Cocartesian cat t i =>
cat y (t x y)
inclr forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> cat (t x y) a
h)

  {-# MINIMAL spawn #-}

instance Cartesian (->) t i => Cocartesian Op t i where
  spawn :: Cartesian (->) t i => Op i a
  spawn :: forall a. Cartesian (->) t i => Op i a
spawn = forall a b. (b -> a) -> Op a b
Op forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cartesian cat t i =>
cat a i
kill

instance Cocartesian (->) Either Void where
  spawn :: Void -> a
  spawn :: forall a. Void -> a
spawn = forall a. Void -> a
absurd