{-# 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.CategoryRecords where


data CategoryRec con cat = CategoryRec{
  forall {k} (con :: k -> Constraint) (cat :: k -> k -> *).
CategoryRec con cat
-> forall (a :: k) (b :: k) (c :: k).
   (con a, con b, con c) =>
   cat b c -> cat a b -> cat a c
(∘)      :: forall a b c. (con a, con b, con c) => b `cat` c -> a `cat` b -> a `cat` c
  ,forall {k} (con :: k -> Constraint) (cat :: k -> k -> *).
CategoryRec con cat -> forall (a :: k). con a => cat a a
id :: forall a. con a => a `cat` a
  }
   
data MonoidalRec x i con cat = MonoidalRec
  {forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k) (b :: k) (c :: k) (d :: k).
   (con a, con b, con c, con d) =>
   cat a b -> cat c d -> cat (x a c) (x b d)
(⊗) :: forall a b c d. (con a, con b, con c, con d) => (a `cat` b) -> (c `cat` d) -> (a `x` c) `cat` (b `x` d)
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k) (b :: k) (c :: k).
   (con a, con b, con c) =>
   cat (x (x a b) c) (x a (x b c))
assoc     :: forall a b c. (con a, con b, con c) => ((a `x` b) `x` c) `cat` (a `x` (b `x` c))
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k) (b :: k) (c :: k).
   (con a, con b, con c) =>
   cat (x a (x b c)) (x (x a b) c)
assoc_    :: forall a b c. (con a, con b, con c) => (a `x` (b `x` c)) `cat` ((a `x` b) `x` c)
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k). (con a, con i) => cat a (x a i)
unitorR   :: forall a. (con a,con i) => a `cat` (a `x` i)
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k). (con a, con i) => cat (x a i) a
unitorR_  :: forall a. (con a,con i) => (a `x` i) `cat` a
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k). (con a, con i) => cat a (x i a)
unitorL   :: forall a. (con a, con i) => a `cat` (i `x` a)
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
MonoidalRec x i con cat
-> forall (a :: k). (con a, con i) => cat (x i a) a
unitorL_  :: forall a. (con a, con i) => (i `x` a) `cat` a
  }

data BraidedRec x i con cat = BraidedRec
  {forall {k} {k} {k} (x :: k -> k -> k) (i :: k)
       (con :: k -> Constraint) (cat :: k -> k -> *).
BraidedRec x i con cat
-> forall (a :: k) (b :: k). (con a, con b) => cat (x a b) (x b a)
swap, forall {k} {k} {k} (x :: k -> k -> k) (i :: k)
       (con :: k -> Constraint) (cat :: k -> k -> *).
BraidedRec x i con cat
-> forall (a :: k) (b :: k). (con a, con b) => cat (x a b) (x b a)
swap_ :: forall a b. (con a, con b) => (a `x` b) `cat` (b `x` a)
  }

data CartesianRec x i con cat = CartesianRec
  {forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
CartesianRec x i con cat
-> forall (a :: k) (b :: k). (con a, con b) => cat (x a b) a
exl   ::   forall a b. (con a, con b)                     =>    (a `x` b) `cat` a
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
CartesianRec x i con cat
-> forall (a :: k) (b :: k). (con a, con b) => cat (x a b) b
exr   ::   forall a b. (con a, con b)                     =>    (a `x` b) `cat` b
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
CartesianRec x i con cat -> forall (a :: k). con a => cat a i
dis   ::   forall a.  con a                       =>    a `cat` i
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
CartesianRec x i con cat -> forall (a :: k). con a => cat a (x a a)
dup   ::   forall a. con a                        =>    a `cat` (a `x` a)
  ,forall {k} (x :: k -> k -> k) (i :: k) (con :: k -> Constraint)
       (cat :: k -> k -> *).
CartesianRec x i con cat
-> forall (a :: k) (b :: k) (c :: k).
   (con a, con b, con c) =>
   cat a b -> cat a c -> cat a (x b c)
(▵)   ::   forall a b c. (con a,con b, con c) =>    (a `cat` b) -> (a `cat` c) -> a `cat` (b `x` c)
  
  }