{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
module Algebra.Category where

import Algebra.Classes (Additive(..))
import Algebra.Types
import Algebra.Category.Objects
import qualified Prelude
import Data.Kind
import qualified Algebra.CategoryRecords as R

type O2 k a b = (Obj k a, Obj k b)
type O3 k a b c =
  (Obj k a, Obj k b, Obj k c)
type O4 k a b c d =
  (Obj k a, Obj k b, Obj k c, Obj k d)

infixr 9 .

  
-- | A class for categories. Instances should satisfy the laws
--
-- @
-- f '.' 'id'  =  f  -- (right identity)
-- 'id' '.' f  =  f  -- (left identity)
-- f '.' (g '.' h)  =  (f '.' g) '.' h  -- (associativity)
-- @

class Category (cat :: k -> k -> Type) where
  type Obj (cat) :: k -> Constraint
  (.)      :: (Obj cat a, Obj cat b, Obj cat c) => b `cat` c -> a `cat` b -> a `cat` c
  id :: Obj cat a => a `cat` a


-- , (∘) = (∘), id = id


class Category cat => Dagger cat where
  dagger :: O2 cat a b => a `cat` b -> b `cat` a

(∘) :: forall {k} (cat :: k -> k -> Type) a b c con. (Category cat, con ~ Obj cat, con a, con b, con c) => cat b c -> cat a b -> cat a c
∘ :: forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
(∘) = cat b c -> cat a b -> cat a c
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
(.) 

type Monoidal :: forall {k}. (k -> k -> k) -> k -> (k -> k -> Type) -> Constraint

class Category cat => Monoidal x i (cat :: k -> k -> Type) | x -> i, i -> x where
  (⊗)      :: (Obj cat a, Obj cat b, Obj cat c, Obj cat d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d)
  assoc    :: (Obj cat a, Obj cat b, Obj cat c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c))
  assoc_   :: (Obj cat a, Obj cat b, Obj cat c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c)
  unitorR   :: (Obj cat a, Obj cat i) => a `cat` (a `x` i)
  unitorR_  :: (Obj cat a, Obj cat i) => (a `x` i) `cat` a
  unitorL   :: (Obj cat a, Obj cat i) => a `cat` (i `x` a)
  unitorL_  :: (Obj cat a, Obj cat i) => (i `x` a) `cat` a

  default unitorL :: forall a con. (con ~ Obj cat, con i, con (x a i), con (x i a), Symmetric x i cat, Obj cat a) => a `cat` (i `x` a)
  unitorL = cat (x a i) (x i a)
forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap cat (x a i) (x i a) -> cat a (x a i) -> cat a (x i a)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ cat a (x a i)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x a i)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  default unitorL_ :: forall a con. (con ~ Obj cat, Symmetric x i cat, con i, con (x a i), con (x i a), Obj cat a) => (i `x` a) `cat` a 
  unitorL_ = cat (x a i) a
forall (a :: k). (Obj cat a, Obj cat i) => cat (x a i) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_ cat (x a i) a -> cat (x i a) (x a i) -> cat (x i a) a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ cat (x i a) (x a i)
forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap

monoidalRec :: forall x cat i. Monoidal x i cat => R.MonoidalRec x i (Obj cat) cat
monoidalRec :: forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Monoidal x i cat =>
MonoidalRec x i (Obj cat) cat
monoidalRec = R.MonoidalRec { ⊗ :: forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
(⊗) = cat a b -> cat c d -> cat (x a c) (x b d)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
(⊗), assoc :: forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc = cat (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x (x a b) c) (x a (x b c))
assoc, assoc_ :: forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat (x a (x b c)) (x (x a b) c)
assoc_ = cat (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat (x a (x b c)) (x (x a b) c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat (x a (x b c)) (x (x a b) c)
assoc_,   unitorR :: forall (a :: k). (Obj cat a, Obj cat i) => cat a (x a i)
unitorR = cat a (x a i)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x a i)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR, unitorL :: forall (a :: k). (Obj cat a, Obj cat i) => cat a (x i a)
unitorL = cat a (x i a)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x i a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x i a)
unitorL, unitorL_ :: forall (a :: k). (Obj cat a, Obj cat i) => cat (x i a) a
unitorL_ = cat (x i a) a
forall (a :: k). (Obj cat a, Obj cat i) => cat (x i a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x i a) a
unitorL_, unitorR_ :: forall (a :: k). (Obj cat a, Obj cat i) => cat (x a i) a
unitorR_ = cat (x a i) a
forall (a :: k). (Obj cat a, Obj cat i) => cat (x a i) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_}



class Monoidal x i cat => Braided x i cat where
  swap     :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)
  swap_     :: (Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)
  default swap_ :: (Symmetric x i cat, Obj cat a, Obj cat b) => (a `x` b) `cat` (b `x` a)
  swap_ = cat (x a b) (x b a)
forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap

braidedRec :: forall x cat i. Braided x i cat => R.BraidedRec x i (Obj cat) cat
braidedRec :: forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
braidedRec = R.BraidedRec { swap :: forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap = cat (x a b) (x b a)
forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap, swap_ :: forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap_ = cat (x a b) (x b a)
forall (a :: k) (b :: k).
(Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap_}


class Braided x i cat => Symmetric x i cat



class Symmetric x i cat => Cartesian x i cat where
  {-# MINIMAL exl,exr,dup | exl,exr,(▵) | dis,dup | dis,(▵) #-}
  exl   ::   forall a b. O2 cat a b                     =>    (a `x` b) `cat` a
  exr   ::   forall a b. O2 cat a b                     =>    (a `x` b) `cat` b
  dis   ::   forall a.  Obj cat a                       =>    a `cat` i
  dup   ::   forall a. Obj cat a                        =>    a `cat` (a `x` a)
  (▵)   ::   forall a b c. (Obj cat a,Obj cat b, Obj cat c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)
  default dis :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => a `cat` i
  dis = cat (x a i) i
forall (a :: k) (b :: k). O2 cat a b => cat (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr cat (x a i) i -> cat a (x a i) -> cat a i
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. cat a (x a i)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x a i)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  default dup :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => a `cat` (a `x` a)
  dup = cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id cat a a -> cat a a -> cat a (x a a)
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id
  default exl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) =>  (a `x` b) `cat` a
  exl = cat (x a i) a
forall (a :: k). (Obj cat a, Obj cat i) => cat (x a i) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_ cat (x a i) a -> cat (x a b) (x a i) -> cat (x a b) a
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. (cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id cat a a -> cat b i -> cat (x a b) (x a i)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat b i
forall (a :: k). Obj cat a => cat a i
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis)
  default exr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) =>  (a `x` b) `cat` b
  exr = cat (x i b) b
forall (a :: k). (Obj cat a, Obj cat i) => cat (x i a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x i a) a
unitorL_ cat (x i b) b -> cat (x a b) (x i b) -> cat (x a b) b
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ (cat a i
forall (a :: k). Obj cat a => cat a i
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis cat a i -> cat b b -> cat (x a b) (x i b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat b b
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id)
  default (▵)   ::   forall a b c con. (con ~ Obj cat, con i, Con' x con, Obj cat a,Obj cat b, Obj cat c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)
  cat a b
f ▵ cat a c
g = (cat a b
f cat a b -> cat a c -> cat (x a a) (x b c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat a c
g) cat (x a a) (x b c) -> cat a (x a a) -> cat a (x b c)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ cat a (x a a)
forall (a :: k). Obj cat a => cat a (x a a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a (x a a)
dup 

cartesianRec :: forall x cat i. Cartesian x i cat => R.CartesianRec x i (Obj cat) cat
cartesianRec :: forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Cartesian x i cat =>
CartesianRec x i (Obj cat) cat
cartesianRec = R.CartesianRec {exl :: forall (a :: k) (b :: k). (Obj cat a, Obj cat b) => cat (x a b) a
exl = cat (x a b) a
forall (a :: k) (b :: k). O2 cat a b => cat (x a b) a
forall (a :: k) (b :: k). (Obj cat a, Obj cat b) => cat (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl , exr :: forall (a :: k) (b :: k). (Obj cat a, Obj cat b) => cat (x a b) b
exr = cat (x a b) b
forall (a :: k) (b :: k). O2 cat a b => cat (x a b) b
forall (a :: k) (b :: k). (Obj cat a, Obj cat b) => cat (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr , dis :: forall (a :: k). Obj cat a => cat a i
dis = cat a i
forall (a :: k). Obj cat a => cat a i
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis , dup :: forall (a :: k). Obj cat a => cat a (x a a)
dup = cat a (x a a)
forall (a :: k). Obj cat a => cat a (x a a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a (x a a)
dup , ▵ :: forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
(▵) = cat a b -> cat a c -> cat a (x b c)
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
(▵)}

cartesianCross :: (Obj k (b1 `x` b2), Obj k b3, Obj k c, Obj k b1, Obj k b2, Cartesian x i k) => k b1 b3 -> k b2 c -> k (b1 `x` b2) (b3 `x` c)
cartesianCross :: forall {k} (k :: k -> k -> *) (x :: k -> k -> k) (b1 :: k)
       (b2 :: k) (b3 :: k) (c :: k) (i :: k).
(Obj k (x b1 b2), Obj k b3, Obj k c, Obj k b1, Obj k b2,
 Cartesian x i k) =>
k b1 b3 -> k b2 c -> k (x b1 b2) (x b3 c)
cartesianCross k b1 b3
a k b2 c
b = (k b1 b3
a k b1 b3 -> k (x b1 b2) b1 -> k (x b1 b2) b3
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x b1 b2) b1
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl) k (x b1 b2) b3 -> k (x b1 b2) c -> k (x b1 b2) (x b3 c)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ (k b2 c
b k b2 c -> k (x b1 b2) b2 -> k (x b1 b2) c
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x b1 b2) b2
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr)

cartesianUnitor :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => a `k` (a `x` i)
cartesianUnitor :: forall {k} (a :: k) (k :: k -> k -> *) (x :: k -> k -> k) (i :: k).
(Obj k a, Obj k i, Cartesian x i k) =>
k a (x a i)
cartesianUnitor = k a a
forall (a :: k). Obj k a => k a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id k a a -> k a i -> k a (x a i)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ k a i
forall (a :: k). Obj k a => k a i
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis
cartesianUnitor_ :: forall a k x i. (Obj k a, Obj k i, Cartesian x i k) => (a `x` i) `k` a
cartesianUnitor_ :: forall {k} (a :: k) (k :: k -> k -> *) (x :: k -> k -> k) (i :: k).
(Obj k a, Obj k i, Cartesian x i k) =>
k (x a i) a
cartesianUnitor_ = k (x a i) a
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl
cartesianSwap :: forall a b k x i con. (Obj k a, Obj k b, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` b) `k` (b `x` a)
cartesianSwap :: forall {k} (a :: k) (b :: k) (k :: k -> k -> *) (x :: k -> k -> k)
       (i :: k) (con :: k -> Constraint).
(Obj k a, Obj k b, Cartesian x i k, Con' x con, con ~ Obj k) =>
k (x a b) (x b a)
cartesianSwap = k (x a b) b
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr k (x a b) b -> k (x a b) a -> k (x a b) (x b a)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ k (x a b) a
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl
cartesianAssoc :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => ((a `x` b) `x` c) `k` (a `x` (b `x` c))
cartesianAssoc :: forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k) (c :: k)
       (k :: k -> k -> *) (con :: k -> Constraint).
(Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con,
 con ~ Obj k) =>
k (x (x a b) c) (x a (x b c))
cartesianAssoc = (k (x a b) a
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl k (x a b) a -> k (x (x a b) c) (x a b) -> k (x (x a b) c) a
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x (x a b) c) (x a b)
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl) k (x (x a b) c) a
-> k (x (x a b) c) (x b c) -> k (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ ((k (x a b) b
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr k (x a b) b -> k (x (x a b) c) (x a b) -> k (x (x a b) c) b
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x (x a b) c) (x a b)
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl) k (x (x a b) c) b -> k (x (x a b) c) c -> k (x (x a b) c) (x b c)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ k (x (x a b) c) c
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr)
cartesianAssoc_ :: forall a b x i c k con. (Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con, con ~ Obj k) => (a `x` (b `x` c)) `k` ((a `x` b) `x` c)
cartesianAssoc_ :: forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k) (c :: k)
       (k :: k -> k -> *) (con :: k -> Constraint).
(Obj k a, Obj k b, Obj k c, Cartesian x i k, Con' x con,
 con ~ Obj k) =>
k (x a (x b c)) (x (x a b) c)
cartesianAssoc_ = (k (x a (x b c)) a
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl k (x a (x b c)) a -> k (x a (x b c)) b -> k (x a (x b c)) (x a b)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ (k (x b c) b
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl k (x b c) b -> k (x a (x b c)) (x b c) -> k (x a (x b c)) b
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x a (x b c)) (x b c)
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr)) k (x a (x b c)) (x a b)
-> k (x a (x b c)) c -> k (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ (k (x b c) c
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr k (x b c) c -> k (x a (x b c)) (x b c) -> k (x a (x b c)) c
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x a (x b c)) (x b c)
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr)


coCartesianExl ::  (O2 cat a b, CoCartesian x i cat, Additive (cat b a)) => (a `x` b) `cat` a
coCartesianExl :: forall {k} (cat :: k -> k -> *) (a :: k) (b :: k)
       (x :: k -> k -> k) (i :: k).
(O2 cat a b, CoCartesian x i cat, Additive (cat b a)) =>
cat (x a b) a
coCartesianExl = cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id cat a a -> cat b a -> cat (x a b) a
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ cat b a
forall a. Additive a => a
zero
coCartesianExr ::  (O2 cat a b, CoCartesian x i cat, Additive (cat a b)) => (a `x` b) `cat` b
coCartesianExr :: forall {k} (cat :: k -> k -> *) (a :: k) (b :: k)
       (x :: k -> k -> k) (i :: k).
(O2 cat a b, CoCartesian x i cat, Additive (cat a b)) =>
cat (x a b) b
coCartesianExr = cat a b
forall a. Additive a => a
zero cat a b -> cat b b -> cat (x a b) b
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ cat b b
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id

class Symmetric x i cat => CoCartesian x i cat where
  {-# MINIMAL inl,inr,jam | inl,inr,(▿) | new,jam | new,(▿) #-}
  inl   ::  O2 cat a b                                 =>  a `cat` (a `x` b)
  inr   ::  O2 cat a b                                 =>  b `cat` (a `x` b)
  new   ::  forall a. (Obj cat a)                      =>  i `cat` a
  jam   ::  Obj cat a                                  =>  (a `x` a) `cat` a
  (▿)    ::  forall a b c. (Obj cat a,Obj cat b, Obj cat c) =>  (b `cat` a) -> (c `cat` a) -> (b `x` c) `cat` a
  default new :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => i `cat` a 
  new = cat (x a i) a
forall (a :: k). (Obj cat a, Obj cat i) => cat (x a i) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat (x a i) a
unitorR_ cat (x a i) a -> cat i (x a i) -> cat i a
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. cat i (x a i)
forall (a :: k) (b :: k). O2 cat a b => cat b (x a b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat b (x a b)
inr
  default jam :: forall a con. (con ~ Obj cat, con i, Con' x con, Obj cat a) => (a `x` a) `cat` a 
  jam = cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id cat a a -> cat a a -> cat (x a a) a
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id
  default inl :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => a `cat` (a `x` b) 
  inl = (cat a a
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id cat a a -> cat i b -> cat (x a i) (x a b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat i b
forall (a :: k). Obj cat a => cat i a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat i a
new) cat (x a i) (x a b) -> cat a (x a i) -> cat a (x a b)
forall (a :: k) (b :: k) (c :: k).
(Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. cat a (x a i)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x a i)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR 
  default inr :: forall a b con. (con ~ Obj cat, con i, Con' x con, con a, con b) => b `cat`  (a `x` b)
  inr = (cat i a
forall (a :: k). Obj cat a => cat i a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat i a
new cat i a -> cat b b -> cat (x i b) (x a b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat b b
forall (a :: k). Obj cat a => cat a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id) cat (x i b) (x a b) -> cat b (x i b) -> cat b (x a b)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ cat b (x i b)
forall (a :: k). (Obj cat a, Obj cat i) => cat a (x i a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x i a)
unitorL
  default (▿)   ::   forall a b c con. (con ~ Obj cat, con i, Con' x con, Obj cat a,Obj cat b, Obj cat c) =>    (b `cat` a) -> (c `cat` a) -> (b `x` c) `cat` a
  cat b a
f ▿ cat c a
g = cat (x a a) a
forall (a :: k). Obj cat a => cat (x a a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat (x a a) a
jam cat (x a a) a -> cat (x b c) (x a a) -> cat (x b c) a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k)
       (con :: k -> Constraint).
(Category cat, con ~ Obj cat, con a, con b, con c) =>
cat b c -> cat a b -> cat a c
∘ (cat b a
f cat b a -> cat c a -> cat (x b c) (x a a)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
(Monoidal x i cat, Obj cat a, Obj cat b, Obj cat c, Obj cat d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat c a
g) 

type BiCartesian x i cat = (Cartesian x i cat, CoCartesian x i cat)

class Monoidal x i cat => Autonomous x i l r cat | x -> l, x -> r where
  turn   :: Obj cat a => i `cat` (l a `x` a)
  turn'  :: Obj cat a => (a `x` r a) `cat` i
  
class (Symmetric x i cat, Autonomous x i d d cat) => Compact x i d cat where


---------------------------
-- Instances
----------------------------

instance Category (->) where
  type Obj (->) = Trivial
  . :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> c) -> (a -> b) -> a -> c
(.) = (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(Prelude..)
  id :: forall a. Obj (->) a => a -> a
id = a -> a
forall a. a -> a
Prelude.id

instance Monoidal (⊗) One (->) where
  (a -> b
f ⊗ :: forall a b c d.
(Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) =>
(a -> b) -> (c -> d) -> (a ⊗ c) -> (b ⊗ d)
⊗ c -> d
g) (a
x `Pair` c
y) = (a -> b
f a
x b -> d -> b ⊗ d
forall x y. x -> y -> x ⊗ y
`Pair` c -> d
g c
y)
  assoc :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
((a ⊗ b) ⊗ c) -> (a ⊗ (b ⊗ c))
assoc ((a
x `Pair` b
y) `Pair` c
z) = (a
x a -> (b ⊗ c) -> a ⊗ (b ⊗ c)
forall x y. x -> y -> x ⊗ y
`Pair` (b
y b -> c -> b ⊗ c
forall x y. x -> y -> x ⊗ y
`Pair` c
z)) 
  assoc_ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a ⊗ (b ⊗ c)) -> ((a ⊗ b) ⊗ c)
assoc_ (a
x `Pair` (b
y `Pair` c
z)) = ((a
x a -> b -> a ⊗ b
forall x y. x -> y -> x ⊗ y
`Pair` b
y) (a ⊗ b) -> c -> (a ⊗ b) ⊗ c
forall x y. x -> y -> x ⊗ y
`Pair` c
z)  
  unitorR :: forall a. (Obj (->) a, Obj (->) One) => a -> (a ⊗ One)
unitorR a
x = (a
x a -> One -> a ⊗ One
forall x y. x -> y -> x ⊗ y
`Pair` One
Unit)
  unitorR_ :: forall a. (Obj (->) a, Obj (->) One) => (a ⊗ One) -> a
unitorR_ (a
x `Pair` One
R:OneTYPE
Unit) = a
x
instance Braided (⊗) One (->) where
  swap :: forall a b. (Obj (->) a, Obj (->) b) => (a ⊗ b) -> (b ⊗ a)
swap (a
x `Pair` b
y) = (b
y b -> a -> b ⊗ a
forall x y. x -> y -> x ⊗ y
`Pair` a
x)
instance Symmetric (⊗) One (->)

instance Monoidal (,) () (->) where
  (a -> b
f ⊗ :: forall a b c d.
(Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) =>
(a -> b) -> (c -> d) -> (a, c) -> (b, d)
⊗ c -> d
g) (a
x , c
y) = (a -> b
f a
x , c -> d
g c
y)
  assoc :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
((a, b), c) -> (a, (b, c))
assoc ((a
x , b
y) , c
z) = (a
x , (b
y , c
z)) 
  assoc_ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a, (b, c)) -> ((a, b), c)
assoc_ (a
x , (b
y , c
z)) = ((a
x , b
y) , c
z)  
  unitorR :: forall a. (Obj (->) a, Obj (->) ()) => a -> (a, ())
unitorR a
x = (a
x , ())
  unitorR_ :: forall a. (Obj (->) a, Obj (->) ()) => (a, ()) -> a
unitorR_ (a
x , ()) = a
x
instance Braided (,) () (->) where
  swap :: forall a b. (Obj (->) a, Obj (->) b) => (a, b) -> (b, a)
swap (a
x, b
y) = (b
y, a
x)
instance Symmetric (,) () (->)


instance Monoidal (⊕) Zero (->) where
  a -> b
f ⊗ :: forall a b c d.
(Obj (->) a, Obj (->) b, Obj (->) c, Obj (->) d) =>
(a -> b) -> (c -> d) -> (a ⊕ c) -> (b ⊕ d)
⊗ c -> d
g = \case
    Inj1 a
x -> b -> b ⊕ d
forall x y. x -> x ⊕ y
Inj1 (a -> b
f a
x)
    Inj2 c
x -> d -> b ⊕ d
forall x y. y -> x ⊕ y
Inj2 (c -> d
g c
x)
  assoc :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
((a ⊕ b) ⊕ c) -> (a ⊕ (b ⊕ c))
assoc = \case
    Inj1 (Inj1 a
x) -> a -> a ⊕ (b ⊕ c)
forall x y. x -> x ⊕ y
Inj1 a
x
    Inj1 (Inj2 b
x) -> (b ⊕ c) -> a ⊕ (b ⊕ c)
forall x y. y -> x ⊕ y
Inj2 (b -> b ⊕ c
forall x y. x -> x ⊕ y
Inj1 b
x)
    Inj2 c
x -> (b ⊕ c) -> a ⊕ (b ⊕ c)
forall x y. y -> x ⊕ y
Inj2 (c -> b ⊕ c
forall x y. y -> x ⊕ y
Inj2 c
x)
  assoc_ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a ⊕ (b ⊕ c)) -> ((a ⊕ b) ⊕ c)
assoc_ = \case
    (Inj1 a
x) -> ((a ⊕ b) -> (a ⊕ b) ⊕ c
forall x y. x -> x ⊕ y
Inj1 (a -> a ⊕ b
forall x y. x -> x ⊕ y
Inj1 a
x)) 
    (Inj2 (Inj1 b
x)) -> ((a ⊕ b) -> (a ⊕ b) ⊕ c
forall x y. x -> x ⊕ y
Inj1 (b -> a ⊕ b
forall x y. y -> x ⊕ y
Inj2 b
x)) 
    (Inj2 (Inj2 c
x)) -> (c -> (a ⊕ b) ⊕ c
forall x y. y -> x ⊕ y
Inj2 c
x) 
  unitorR :: forall a. (Obj (->) a, Obj (->) Zero) => a -> (a ⊕ Zero)
unitorR = a -> a ⊕ Zero
forall x y. x -> x ⊕ y
Inj1
  unitorL :: forall a. (Obj (->) a, Obj (->) Zero) => a -> (Zero ⊕ a)
unitorL = a -> Zero ⊕ a
forall x y. y -> x ⊕ y
Inj2
  unitorR_ :: forall a. (Obj (->) a, Obj (->) Zero) => (a ⊕ Zero) -> a
unitorR_ = \case
    Inj1 a
x -> a
x
    Inj2 Zero
x -> case Zero
x of

instance Symmetric (⊕) Zero (->) where
instance Braided (⊕) Zero (->) where
  swap :: forall a b. (Obj (->) a, Obj (->) b) => (a ⊕ b) -> (b ⊕ a)
swap = \case
    Inj1 a
x -> a -> b ⊕ a
forall x y. y -> x ⊕ y
Inj2 a
x
    Inj2 b
x -> b -> b ⊕ a
forall x y. x -> x ⊕ y
Inj1 b
x

instance Cartesian (⊗) One (->) where
  dup :: forall a. Obj (->) a => a -> (a ⊗ a)
dup a
x = a -> a -> a ⊗ a
forall x y. x -> y -> x ⊗ y
Pair a
x a
x
  exr :: forall a b. O2 (->) a b => (a ⊗ b) -> b
exr (Pair a
_ b
x) = b
x
  exl :: forall a b. O2 (->) a b => (a ⊗ b) -> a
exl (Pair a
x b
_) = a
x
  (a -> b
f ▵ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a -> b) -> (a -> c) -> a -> (b ⊗ c)
▵ a -> c
g) a
x = a -> b
f a
x b -> c -> b ⊗ c
forall x y. x -> y -> x ⊗ y
`Pair` a -> c
g a
x
  dis :: forall a. Obj (->) a => a -> One
dis a
_ = One
Unit

instance Cartesian (,) () (->) where
  dup :: forall a. Obj (->) a => a -> (a, a)
dup a
x = (a
x,a
x)
  exr :: forall a b. O2 (->) a b => (a, b) -> b
exr (a
_,b
x) = b
x
  exl :: forall a b. O2 (->) a b => (a, b) -> a
exl (a
x,b
_) = a
x
  (a -> b
f ▵ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a -> b) -> (a -> c) -> a -> (b, c)
▵ a -> c
g) a
x = (a -> b
f a
x, a -> c
g a
x)
  dis :: forall a. Obj (->) a => a -> ()
dis a
_ = ()

instance CoCartesian (⊕) Zero (->) where
  inl :: forall a b. O2 (->) a b => a -> (a ⊕ b)
inl = a -> a ⊕ b
forall x y. x -> x ⊕ y
Inj1
  inr :: forall a b. O2 (->) a b => b -> (a ⊕ b)
inr = b -> a ⊕ b
forall x y. y -> x ⊕ y
Inj2
  new :: forall a. Obj (->) a => Zero -> a
new = Zero -> a
\case
  b -> a
f ▿ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(b -> a) -> (c -> a) -> (b ⊕ c) -> a
▿ c -> a
g = \case
     Inj1 b
x -> b -> a
f b
x
     Inj2 c
y -> c -> a
g c
y
  jam :: forall a. Obj (->) a => (a ⊕ a) -> a
jam = \case
     Inj1 a
x -> a
x
     Inj2 a
x -> a
x