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

import qualified Algebra.CategoryRecords as R
-- import Algebra.CategoryRecords (MonoidalRec(MonoidalRec))
import Algebra.Category
import Algebra.Category.Op

import Algebra.Classes (nameLaw, TestEqual(..), product)
import Algebra.Category.Objects
import Data.Kind
import Data.Constraint
import Test.QuickCheck
import Prelude (Show(..),($))


law_id_comp :: forall {k} (f :: k -> k -> Type) a b. (Category f, TestEqual (f a b), O2 f a b) => f a b -> Property
law_id_comp :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(Category f, TestEqual (f a b), O2 f a b) =>
f a b -> Property
law_id_comp f a b
n = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"id/comp" (f b b
forall (a :: k). Obj f a => f a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id f b b -> f a b -> f a b
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a b
n f a b -> f a b -> Property
forall a. TestEqual a => a -> a -> Property
=.= f a b
n)

forallMorphism' :: forall f x i. TestableCat x i (Obj f) f -> (forall a b. (O2 f a b, TT f a b) => f a b -> Property) -> Property
forallMorphism' :: forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
TestableCat x i (Obj f) f
-> (forall (a :: k) (b :: k).
    (O2 f a b, TT f a b) =>
    f a b -> Property)
-> Property
forallMorphism' (TestableCat {o i
GenObj (Obj f) o f
forall (a :: k). o a -> Dict (TT f a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genObj :: GenObj (Obj f) o f
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable' :: forall (a :: k). o a -> Dict (TT f a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
..}) forall (a :: k) (b :: k). (O2 f a b, TT f a b) => f a b -> Property
p
  = GenObj (Obj f) o f
genObj (\o a
t1 -> 
    GenObj (Obj f) o f
genObj (\o a
t2 ->
    o a -> o a -> (TT f a a => f a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genMorph' o a
t1 o a
t2 (\f a a
f -> f a a -> Property
forall (a :: k) (b :: k). (O2 f a b, TT f a b) => f a b -> Property
p f a a
f)))


law_comp_id :: forall {k} (f :: k -> k -> Type) a b. (Category f, TestEqual (f a b), O2 f a b) => f a b -> Property
law_comp_id :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(Category f, TestEqual (f a b), O2 f a b) =>
f a b -> Property
law_comp_id f a b
n = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"comp/id" (f a b
n f a b -> f a a -> f a b
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a a
forall (a :: k). Obj f a => f a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id f a b -> f a b -> Property
forall a. TestEqual a => a -> a -> Property
=.= f a b
n)

law_comp_assoc :: forall {k} (f :: k -> k -> Type) a b c d. (Category f, TestEqual (f a d), O4 f a b c d) => f c d -> f b c -> f a b -> Property
law_comp_assoc :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k) (c :: k) (d :: k).
(Category f, TestEqual (f a d), O4 f a b c d) =>
f c d -> f b c -> f a b -> Property
law_comp_assoc f c d
n f b c
m f a b
o = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"comp/assoc" (f c d
n f c d -> f a c -> f a d
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. (f b c
m f b c -> f a b -> f a c
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a b
o) f a d -> f a d -> Property
forall a. TestEqual a => a -> a -> Property
=.= (f c d
n f c d -> f b c -> f b d
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f b c
m) f b d -> f a b -> f a d
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a b
o)

laws_category :: forall f x i. (Category f) => TestableCat x i (Obj f) f -> Property
laws_category :: forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
Category f =>
TestableCat x i (Obj f) f -> Property
laws_category tc :: TestableCat x i (Obj f) f
tc@TestableCat {o i
GenObj (Obj f) o f
forall (a :: k). o a -> Dict (TT f a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj (Obj f) o f
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable' :: forall (a :: k). o a -> Dict (TT f a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..}
  = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product [forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
TestableCat x i (Obj f) f
-> (forall (a :: k) (b :: k).
    (O2 f a b, TT f a b) =>
    f a b -> Property)
-> Property
forall (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
TestableCat x i (Obj f) f
-> (forall (a :: k) (b :: k).
    (O2 f a b, TT f a b) =>
    f a b -> Property)
-> Property
forallMorphism' @f TestableCat x i (Obj f) f
tc (\f a b
f -> Property -> Property
forall prop. Testable prop => prop -> Property
property (f a b -> Property
forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(Category f, TestEqual (f a b), O2 f a b) =>
f a b -> Property
law_id_comp f a b
f))
            ,forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
TestableCat x i (Obj f) f
-> (forall (a :: k) (b :: k).
    (O2 f a b, TT f a b) =>
    f a b -> Property)
-> Property
forall (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
TestableCat x i (Obj f) f
-> (forall (a :: k) (b :: k).
    (O2 f a b, TT f a b) =>
    f a b -> Property)
-> Property
forallMorphism' @f TestableCat x i (Obj f) f
tc (\f a b
f -> Property -> Property
forall prop. Testable prop => prop -> Property
property (f a b -> Property
forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(Category f, TestEqual (f a b), O2 f a b) =>
f a b -> Property
law_comp_id f a b
f))
            ,GenObj (Obj f) o f
genObj GenObj (Obj f) o f -> GenObj (Obj f) o f
forall a b. (a -> b) -> a -> b
$ \o a
t1 -> GenObj (Obj f) o f
genObj GenObj (Obj f) o f -> GenObj (Obj f) o f
forall a b. (a -> b) -> a -> b
$ \o a
t2 -> GenObj (Obj f) o f
genObj GenObj (Obj f) o f -> GenObj (Obj f) o f
forall a b. (a -> b) -> a -> b
$ \o a
t3 -> GenObj (Obj f) o f
genObj GenObj (Obj f) o f -> GenObj (Obj f) o f
forall a b. (a -> b) -> a -> b
$ \o a
t4 ->
             o a -> o a -> (f a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
genMorph o a
t1 o a
t2 ((f a a -> Property) -> Property)
-> (f a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ f a a
h -> o a -> o a -> (f a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
genMorph o a
t2 o a
t3 ((f a a -> Property) -> Property)
-> (f a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ f a a
g -> o a -> o a -> (f a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
genMorph o a
t3 o a
t4 ((f a a -> Property) -> Property)
-> (f a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ f a a
f ->
             (f a a
f f a a -> f a a -> f a a
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. (f a a
g f a a -> f a a -> f a a
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a a
h) f a a -> f a a -> Property
forall a. TestEqual a => a -> a -> Property
=.= (f a a
f f a a -> f a a -> f a a
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a a
g) f a a -> f a a -> f a a
forall (a :: k) (b :: k) (c :: k).
(Obj f a, Obj f b, Obj f c) =>
f b c -> f a b -> f 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
. f a a
h) (TestEqual (f a a) => Property)
-> Dict (TestEqual (f a a)) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o a -> o a -> Dict (TestEqual (f a a))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable o a
t1 o a
t4]


type TT f x y = TestEqual (f x y)
type GenObj obj o f = ((forall a. obj a => o a -> Property) -> Property)

data TestableCat x i obj f = forall o. TestableCat
  {()
genObj :: GenObj obj o f
  ,()
genMorph' :: forall a b. o a -> o b -> (TT f a b => f a b -> Property) -> Property
  ,()
genMorph :: forall a b. o a -> o b -> (f a b -> Property) -> Property
  ,()
getTestable :: forall a b. o a -> o b -> Dict (TT f a b)
  ,()
getTestable' :: forall a. o a -> Dict (TT f a a)
  ,()
(×) :: forall a b. o a -> o b -> o (a `x` b)
  ,()
unitObj :: o i
  }

testableCat :: forall f x i o obj. GenObj obj o f -> (forall a b. o a -> o b -> (f a b -> Property) -> Property) -> ( forall a b. o a -> o b -> Dict (TT f a b)) -> (forall a b. o a -> o b -> o (x a b)) -> o i -> TestableCat x i obj f
testableCat :: forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (o :: k -> *) (obj :: k -> Constraint).
GenObj obj o f
-> (forall (a :: k) (b :: k).
    o a -> o b -> (f a b -> Property) -> Property)
-> (forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b))
-> (forall (a :: k) (b :: k). o a -> o b -> o (x a b))
-> o i
-> TestableCat x i obj f
testableCat GenObj obj o f
genObj forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
genMorph forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable forall (a :: k) (b :: k). o a -> o b -> o (x a b)
(×) o i
unitObj = TestableCat{o i
o a -> o b -> (TT f a b => f a b -> Property) -> Property
o a -> o b -> (f a b -> Property) -> Property
o a -> o b -> Dict (TT f a b)
o a -> Dict (TT f a a)
o a -> o b -> o (x a b)
GenObj obj o f
forall (a :: k). o a -> Dict (TT f a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genObj :: GenObj obj o f
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable' :: forall (a :: k). o a -> Dict (TT f a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
genObj :: GenObj obj o f
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
getTestable' :: forall (a :: k). o a -> Dict (TT f a a)
..}
  where genMorph' :: forall a b. o a -> o b -> (TT f a b => f a b -> Property) -> Property
        genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT f a b => f a b -> Property) -> Property
genMorph' o a
a o b
b TestEqual (f a b) => f a b -> Property
k = o a -> o b -> (f a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (f a b -> Property) -> Property
genMorph o a
a o b
b ((f a b -> Property) -> Property)
-> (f a b -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \f a b
f -> f a b -> Property
TestEqual (f a b) => f a b -> Property
k f a b
f (TestEqual (f a b) => Property)
-> Dict (TestEqual (f a b)) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o a -> o b -> Dict (TestEqual (f a b))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable o a
a o b
b
        getTestable' :: forall a. o a -> Dict (TT f a a)
        getTestable' :: forall (a :: k). o a -> Dict (TT f a a)
getTestable' o a
a = o a -> o a -> Dict (TT f a a)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b)
getTestable o a
a o a
a


law_parallel_composition :: forall {k} {cat :: k -> k -> Type}
                                     {x :: k -> k -> k} {a :: k} {c :: k} {b1 :: k} {b2 :: k}
                                     {b3 :: k} {d :: k} {i :: k} obj.
                              (obj (x a c), obj (x b1 b2), obj (x b3 d), obj a,
                               obj b1, obj b3, obj c, obj b2, obj d, Category cat, Obj cat ~ obj,
                               TestEqual (cat (x a c) (x b3 d))) =>
                              R.MonoidalRec x i obj cat -> cat b1 b3 -> cat b2 d -> cat a b1 -> cat c b2 -> Property
law_parallel_composition :: forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {a :: k}
       {c :: k} {b1 :: k} {b2 :: k} {b3 :: k} {d :: k} {i :: k}
       (obj :: k -> Constraint).
(obj (x a c), obj (x b1 b2), obj (x b3 d), obj a, obj b1, obj b3,
 obj c, obj b2, obj d, Category cat, Obj cat ~ obj,
 TestEqual (cat (x a c) (x b3 d))) =>
MonoidalRec x i obj cat
-> cat b1 b3 -> cat b2 d -> cat a b1 -> cat c b2 -> Property
law_parallel_composition R.MonoidalRec{forall (a :: k). (obj a, obj i) => cat a (x i a)
forall (a :: k). (obj a, obj i) => cat a (x a i)
forall (a :: k). (obj a, obj i) => cat (x i a) a
forall (a :: k). (obj a, obj i) => cat (x a i) a
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ :: forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
assoc :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x (x a b) c) (x a (x b c))
assoc_ :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x a (x b c)) (x (x a b) c)
unitorR :: forall (a :: k). (obj a, obj i) => cat a (x a i)
unitorR_ :: forall (a :: k). (obj a, obj i) => cat (x a i) a
unitorL :: forall (a :: k). (obj a, obj i) => cat a (x i a)
unitorL_ :: forall (a :: k). (obj a, obj i) => cat (x i a) a
⊗ :: 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)
assoc :: 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 {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)
unitorR :: 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 {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
unitorL :: 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 {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
..} cat b1 b3
e cat b2 d
f cat a b1
g cat c b2
h = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"cross-comp" ((cat b1 b3
e cat b1 b3 -> cat b2 d -> cat (x b1 b2) (x b3 d)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat b2 d
f) cat (x b1 b2) (x b3 d)
-> cat (x a c) (x b1 b2) -> cat (x a c) (x b3 d)
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 b1
g cat a b1 -> cat c b2 -> cat (x a c) (x b1 b2)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ cat c b2
h) cat (x a c) (x b3 d) -> cat (x a c) (x b3 d) -> Property
forall a. TestEqual a => a -> a -> Property
=.= (cat b1 b3
e cat b1 b3 -> cat a b1 -> cat a b3
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 b1
g) cat a b3 -> cat c d -> cat (x a c) (x b3 d)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
⊗ (cat b2 d
f cat b2 d -> cat c b2 -> cat c d
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 c b2
h))

law_assoc_inv :: forall {k} (a::k) (b::k) (c::k) x i obj (cat :: k -> k -> Type) o.
  (obj a, obj b, obj c, Con' x obj, TestEqual (cat (x (x a b) c) (x (x a b) c)), Category cat, Obj cat ~ obj)
  => R.MonoidalRec x i obj cat -> o a -> o b -> o c -> Property
law_assoc_inv :: forall {k} (a :: k) (b :: k) (c :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x (x a b) c)), Category cat,
 Obj cat ~ obj) =>
MonoidalRec x i obj cat -> o a -> o b -> o c -> Property
law_assoc_inv R.MonoidalRec{forall (a :: k). (obj a, obj i) => cat a (x i a)
forall (a :: k). (obj a, obj i) => cat a (x a i)
forall (a :: k). (obj a, obj i) => cat (x i a) a
forall (a :: k). (obj a, obj i) => cat (x a i) a
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b 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) (d :: k).
   (con a, con b, con c, con d) =>
   cat a b -> cat c d -> cat (x a c) (x b d)
assoc :: 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 {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)
unitorR :: 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 {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
unitorL :: 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 {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
⊗ :: forall (a :: k) (b :: k) (c :: k) (d :: k).
(obj a, obj b, obj c, obj d) =>
cat a b -> cat c d -> cat (x a c) (x b d)
assoc :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x (x a b) c) (x a (x b c))
assoc_ :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x a (x b c)) (x (x a b) c)
unitorR :: forall (a :: k). (obj a, obj i) => cat a (x a i)
unitorR_ :: forall (a :: k). (obj a, obj i) => cat (x a i) a
unitorL :: forall (a :: k). (obj a, obj i) => cat a (x i a)
unitorL_ :: forall (a :: k). (obj a, obj i) => cat (x i a) a
..} o a
_ o b
_ o c
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"assoc-inv" (forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x a (x b c)) (x (x a b) c)
assoc_ @a @b @c cat (x a (x b c)) (x (x a b) c)
-> cat (x (x a b) c) (x a (x b c))
-> cat (x (x a b) c) (x (x a 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 (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat (x (x a b) c) (x a (x b c))
assoc cat (x (x a b) c) (x (x a b) c)
-> cat (x (x a b) c) (x (x a b) c) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat (x (x a b) c) (x (x a b) c)
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)
  

law_unitorR_inv :: forall {k} (cat :: k -> k -> Type) x i {b :: k} {con :: k -> Constraint} {o}.
                     (Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat,  con b, con i,
                      TestEqual (cat (x b i) (x b i))) =>
                     o b -> Property
law_unitorR_inv :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       {b :: k} {con :: k -> Constraint} {o :: k -> *}.
(Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x b i) (x b i))) =>
o b -> Property
law_unitorR_inv o b
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"unitor-inv" ((cat b (x b 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 :: b `cat` (b `x` i)) cat b (x b i) -> cat (x b i) b -> cat (x b i) (x b i)
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 b i) b
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 b i) (x b i) -> cat (x b i) (x b i) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat (x b i) (x b i)
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)


law_unitorL_inv :: forall {k} {cat :: k -> k -> Type}
                            {x :: k -> k -> k} {b :: k} {i :: k} {con :: k -> Constraint} {o}.
                     (Category cat, Obj cat ~ con, Con' x con, con ~ Obj cat,  con b, con i,
                      TestEqual (cat (x i b) (x i b))) =>
                     R.MonoidalRec x i con cat -> o b -> Property
law_unitorL_inv :: forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {b :: k}
       {i :: k} {con :: k -> Constraint} {o :: k -> *}.
(Category cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x i b) (x i b))) =>
MonoidalRec x i con cat -> o b -> Property
law_unitorL_inv  R.MonoidalRec{forall (a :: k). (con a, con i) => cat a (x i a)
forall (a :: k). (con a, con i) => cat a (x a i)
forall (a :: k). (con a, con i) => cat (x i a) a
forall (a :: k). (con a, con i) => cat (x a i) a
forall (a :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat (x (x a b) c) (x a (x b c))
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 {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)
assoc :: 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 {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)
unitorR :: 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 {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
unitorL :: 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 {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
⊗ :: 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)
assoc :: 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 :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat (x a (x b c)) (x (x a b) c)
unitorR :: forall (a :: k). (con a, con i) => cat a (x a i)
unitorR_ :: forall (a :: k). (con a, con i) => cat (x a i) a
unitorL :: forall (a :: k). (con a, con i) => cat a (x i a)
unitorL_ :: forall (a :: k). (con a, con i) => cat (x i a) a
..} o b
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"unitor_-inv" (forall (a :: k). (con a, con i) => cat a (x i a)
unitorL @b cat b (x i b) -> cat (x i b) b -> cat (x i b) (x i 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 (x i b) b
forall (a :: k). (con a, con i) => cat (x i a) a
unitorL_ cat (x i b) (x i b) -> cat (x i b) (x i b) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat (x i b) (x i 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)
  
law_monoidal_triangle :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a c obj o. (obj ~ Obj cat, Monoidal x i cat, obj a, obj c, obj i, Con' x obj, TestEqual (cat (x a c) (x a (x i c))))
  => o a -> o c -> Property
law_monoidal_triangle :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj c, obj i, Con' x obj,
 TestEqual (cat (x a c) (x a (x i c)))) =>
o a -> o c -> Property
law_monoidal_triangle o a
_ o c
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"monoidal-triangle"
   ((cat (x (x a i) c) (x a (x i 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 cat (x (x a i) c) (x a (x i c))
-> cat (x a c) (x (x a i) c) -> cat (x a c) (x a (x i 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
. (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 cat a (x a i) -> cat c c -> cat (x a c) (x (x a i) 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 c c
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 a c) (x a (x i c)) -> cat (x a c) (x a (x i c)) -> Property
forall a. TestEqual a => a -> a -> Property
=.=  ((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 c (x i c) -> cat (x a c) (x a (x i 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 c (x i c)
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) :: (cat (x a c) (x a (x i c)))))

law_monoidal_pentagon :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a b c d obj o.
   (obj ~ Obj cat, Monoidal x i cat, obj a, obj b, obj c, obj d, Con' x obj, (TestEqual (cat (x (x (x a b) c) d) (x a (x b (x c d))))))
  => o a -> o b -> o c -> o d -> Property
law_monoidal_pentagon :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (d :: k) (obj :: k -> Constraint)
       (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj b, obj c, obj d,
 Con' x obj,
 TestEqual (cat (x (x (x a b) c) d) (x a (x b (x c d))))) =>
o a -> o b -> o c -> o d -> Property
law_monoidal_pentagon o a
_ o b
_ o c
_ o d
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"monoidal-pentagon"
   (cat (x (x a b) (x c d)) (x a (x b (x c d)))
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 cat (x (x a b) (x c d)) (x a (x b (x c d)))
-> cat (x (x (x a b) c) d) (x (x a b) (x c d))
-> cat (x (x (x a b) c) d) (x a (x b (x c d)))
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 (x (x (x a b) c) d) (x (x a b) (x c d))
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 cat (x (x (x a b) c) d) (x a (x b (x c d)))
-> cat (x (x (x a b) c) d) (x a (x b (x c d))) -> Property
forall a. TestEqual a => a -> a -> Property
=.=  ((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 (x (x b c) d) (x b (x c d))
-> cat (x a (x (x b c) d)) (x a (x b (x c 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)
⊗ cat (x (x b c) d) (x b (x c d))
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) cat (x a (x (x b c) d)) (x a (x b (x c d)))
-> cat (x (x (x a b) c) d) (x a (x (x b c) d))
-> cat (x (x (x a b) c) d) (x a (x b (x c d)))
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 (x (x a (x b c)) d) (x a (x (x b c) d))
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 cat (x (x a (x b c)) d) (x a (x (x b c) d))
-> cat (x (x (x a b) c) d) (x (x a (x b c)) d)
-> cat (x (x (x a b) c) d) (x a (x (x b c) d))
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 (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 cat (x (x a b) c) (x a (x b c))
-> cat d d -> cat (x (x (x a b) c) d) (x (x a (x b c)) 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)
⊗ cat d d
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 (x (x a b) c) d) (x a (x b (x c d))))))


laws_monoidal :: forall {k} (cat :: k -> k -> Type) x i (obj :: k -> Constraint).
                 (obj ~ Obj cat, Con' x obj, Monoidal x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_monoidal :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint).
(obj ~ Obj cat, Con' x obj, Monoidal x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_monoidal  t :: TestableCat x i obj cat
t@TestableCat{o i
GenObj obj o cat
forall (a :: k). o a -> Dict (TT cat a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k). o a -> Dict (TT cat a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..}   = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product
   [ TestableCat x i (Obj cat) cat -> Property
forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k).
Category f =>
TestableCat x i (Obj f) f -> Property
laws_category TestableCat x i obj cat
TestableCat x i (Obj cat) cat
t
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t1 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t2 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t3 ->
     GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t4 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t5 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t6 ->
     o a -> o a -> (cat a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o a
t1 o a
t2 ((cat a a -> Property) -> Property)
-> (cat a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat a a
e -> o a -> o a -> (cat a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o a
t2 o a
t3 ((cat a a -> Property) -> Property)
-> (cat a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat a a
f ->
     o a -> o a -> (cat a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o a
t4 o a
t5 ((cat a a -> Property) -> Property)
-> (cat a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat a a
g -> o a -> o a -> (cat a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o a
t5 o a
t6 ((cat a a -> Property) -> Property)
-> (cat a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat a a
h ->
     MonoidalRec x i obj cat
-> cat a a -> cat a a -> cat a a -> cat a a -> Property
forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {a :: k}
       {c :: k} {b1 :: k} {b2 :: k} {b3 :: k} {d :: k} {i :: k}
       (obj :: k -> Constraint).
(obj (x a c), obj (x b1 b2), obj (x b3 d), obj a, obj b1, obj b3,
 obj c, obj b2, obj d, Category cat, Obj cat ~ obj,
 TestEqual (cat (x a c) (x b3 d))) =>
MonoidalRec x i obj cat
-> cat b1 b3 -> cat b2 d -> cat a b1 -> cat c b2 -> Property
law_parallel_composition MonoidalRec x i obj cat
m cat a a
f cat a a
h cat a a
e cat a a
g
     (TestEqual (cat (x a a) (x a a)) => Property)
-> Dict (TestEqual (cat (x a a) (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a) -> o (x a a) -> Dict (TestEqual (cat (x a a) (x a a)))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable (o a
t1 o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
t4) (o a
t3 o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
t6)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
c -> MonoidalRec x i obj cat -> o a -> o a -> o a -> Property
forall {k} (a :: k) (b :: k) (c :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x (x a b) c)), Category cat,
 Obj cat ~ obj) =>
MonoidalRec x i obj cat -> o a -> o b -> o c -> Property
law_assoc_inv MonoidalRec x i obj cat
m  o a
a o a
b o a
c
     (TestEqual (cat (x (x a a) a) (x (x a a) a)) => Property)
-> Dict (TestEqual (cat (x (x a a) a) (x (x a a) a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x (x a a) a)
-> Dict (TestEqual (cat (x (x a a) a) (x (x a a) a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' ((o a
a o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b) o (x a a) -> o a -> o (x (x a a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
c)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
c -> MonoidalRec x i obj (Op cat) -> o a -> o a -> o a -> Property
forall {k} (a :: k) (b :: k) (c :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x (x a b) c)), Category cat,
 Obj cat ~ obj) =>
MonoidalRec x i obj cat -> o a -> o b -> o c -> Property
law_assoc_inv MonoidalRec x i obj (Op cat)
mOp o a
a o a
b o a
c
     (TestEqual (cat (x (x a a) a) (x (x a a) a)) => Property)
-> Dict (TestEqual (cat (x (x a a) a) (x (x a a) a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x (x a a) a)
-> Dict (TestEqual (cat (x (x a a) a) (x (x a a) a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' ((o a
a o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b) o (x a a) -> o a -> o (x (x a a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
c)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       {b :: k} {con :: k -> Constraint} {o :: k -> *}.
(Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x b i) (x b i))) =>
o b -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) {b :: k}
       {con :: k -> Constraint} {o :: k -> *}.
(Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x b i) (x b i))) =>
o b -> Property
law_unitorR_inv @cat @x o a
a (TestEqual (cat (x a i) (x a i)) => Property)
-> Dict (TestEqual (cat (x a i) (x a i))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a i) -> Dict (TestEqual (cat (x a i) (x a i)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
a o a -> o i -> o (x a i)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o i
unitObj) 
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       {b :: k} {con :: k -> Constraint} {o :: k -> *}.
(Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x b i) (x b i))) =>
o b -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) {b :: k}
       {con :: k -> Constraint} {o :: k -> *}.
(Monoidal x i cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x b i) (x b i))) =>
o b -> Property
law_unitorR_inv @(Op cat) @x o a
a  (TestEqual (cat (x a i) (x a i)) => Property)
-> Dict (TestEqual (cat (x a i) (x a i))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a i) -> Dict (TestEqual (cat (x a i) (x a i)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
a o a -> o i -> o (x a i)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o i
unitObj)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> MonoidalRec x i obj cat -> o a -> Property
forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {b :: k}
       {i :: k} {con :: k -> Constraint} {o :: k -> *}.
(Category cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x i b) (x i b))) =>
MonoidalRec x i con cat -> o b -> Property
law_unitorL_inv MonoidalRec x i obj cat
m   o a
a  (TestEqual (cat (x i a) (x i a)) => Property)
-> Dict (TestEqual (cat (x i a) (x i a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x i a) -> Dict (TestEqual (cat (x i a) (x i a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o i
unitObj o i -> o a -> o (x i a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> MonoidalRec x i obj (Op cat) -> o a -> Property
forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {b :: k}
       {i :: k} {con :: k -> Constraint} {o :: k -> *}.
(Category cat, Obj cat ~ con, Con' x con, con ~ Obj cat, con b,
 con i, TestEqual (cat (x i b) (x i b))) =>
MonoidalRec x i con cat -> o b -> Property
law_unitorL_inv MonoidalRec x i obj (Op cat)
mOp o a
a  (TestEqual (cat (x i a) (x i a)) => Property)
-> Dict (TestEqual (cat (x i a) (x i a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x i a) -> Dict (TestEqual (cat (x i a) (x i a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o i
unitObj o i -> o a -> o (x i a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj c, obj i, Con' x obj,
 TestEqual (cat (x a c) (x a (x i c)))) =>
o a -> o c -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) (a :: k)
       (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj c, obj i, Con' x obj,
 TestEqual (cat (x a c) (x a (x i c)))) =>
o a -> o c -> Property
law_monoidal_triangle @cat @x o a
a o a
b
     (TestEqual (cat (x a a) (x a (x i a))) => Property)
-> Dict (TestEqual (cat (x a a) (x a (x i a)))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a)
-> o (x a (x i a)) -> Dict (TestEqual (cat (x a a) (x a (x i a))))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable (o a
a o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b) (o a
a o a -> o (x i a) -> o (x a (x i a))
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× (o i
unitObj o i -> o a -> o (x i a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b))
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
c -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
d ->
       forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (d :: k) (obj :: k -> Constraint)
       (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj b, obj c, obj d,
 Con' x obj,
 TestEqual (cat (x (x (x a b) c) d) (x a (x b (x c d))))) =>
o a -> o b -> o c -> o d -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) (a :: k)
       (b :: k) (c :: k) (d :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Monoidal x i cat, obj a, obj b, obj c, obj d,
 Con' x obj,
 TestEqual (cat (x (x (x a b) c) d) (x a (x b (x c d))))) =>
o a -> o b -> o c -> o d -> Property
law_monoidal_pentagon @cat @x o a
a o a
b o a
c o a
d
       (TestEqual (cat (x (x (x a a) a) a) (x a (x a (x a a)))) =>
 Property)
-> Dict (TestEqual (cat (x (x (x a a) a) a) (x a (x a (x a a)))))
-> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x (x (x a a) a) a)
-> o (x a (x a (x a a)))
-> Dict (TestEqual (cat (x (x (x a a) a) a) (x a (x a (x a a)))))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable (((o a
a o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b) o (x a a) -> o a -> o (x (x a a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
c) o (x (x a a) a) -> o a -> o (x (x (x a a) a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
d) (o a
a o a -> o (x a (x a a)) -> o (x a (x a (x a a)))
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× (o a
b o a -> o (x a a) -> o (x a (x a a))
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× (o a
c o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
d))) 
   ]
   where m :: R.MonoidalRec x i obj cat 
         m :: MonoidalRec x i obj cat
m@R.MonoidalRec{} = forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Monoidal x i cat =>
MonoidalRec x i (Obj cat) cat
forall (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Monoidal x i cat =>
MonoidalRec x i (Obj cat) cat
monoidalRec @x
         mOp :: R.MonoidalRec x i obj (Op cat)
         mOp :: MonoidalRec x i obj (Op cat)
mOp = forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Monoidal x i cat =>
MonoidalRec x i (Obj cat) cat
forall (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Monoidal x i cat =>
MonoidalRec x i (Obj cat) cat
monoidalRec @x
         -- running the test on the op category mean that we test the reverse compositions.

law_swap_inv :: forall {k} (a::k) (b::k) x i obj (cat :: k -> k -> Type) o.
  (obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b, TestEqual (cat (x b a) (x b a)))
  => R.BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_inv :: forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b,
 TestEqual (cat (x b a) (x b a))) =>
BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_inv R.BraidedRec{forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap_ :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap :: forall {k1} {k2} {k3} (x :: k1 -> k1 -> k2) (i :: k3)
       (con :: k1 -> Constraint) (cat :: k2 -> k2 -> *).
BraidedRec x i con cat
-> forall (a :: k1) (b :: k1).
   (con a, con b) =>
   cat (x a b) (x b a)
swap_ :: forall {k1} {k2} {k3} (x :: k1 -> k1 -> k2) (i :: k3)
       (con :: k1 -> Constraint) (cat :: k2 -> k2 -> *).
BraidedRec x i con cat
-> forall (a :: k1) (b :: k1).
   (con a, con b) =>
   cat (x a b) (x b a)
..} o a
_ o b
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"swap-inv" (forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap_ @a @b cat (x a b) (x b a) -> cat (x b a) (x a b) -> cat (x b a) (x b 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 b a) (x a b)
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap cat (x b a) (x b a) -> cat (x b a) (x b a) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat (x b a) (x b 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)

law_braided_hexagon1 :: forall {k} (cat :: k -> k -> Type) x i a b c obj o.
   (obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj, (TestEqual (cat (x (x a b) c) (x b (x c a)))))
  => o a -> o b -> o c -> Property
law_braided_hexagon1 :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x b (x c a)))) =>
o a -> o b -> o c -> Property
law_braided_hexagon1 o a
_ o b
_ o c
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"braided-hexagon-1"
   (cat (x (x b c) a) (x b (x c a))
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 cat (x (x b c) a) (x b (x c a))
-> cat (x (x a b) c) (x (x b c) a)
-> cat (x (x a b) c) (x b (x c 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 (x a (x b c)) (x (x b c) 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 (x b c)) (x (x b c) a)
-> cat (x (x a b) c) (x a (x b c))
-> cat (x (x a b) c) (x (x b c) 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 (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 cat (x (x a b) c) (x b (x c a))
-> cat (x (x a b) c) (x b (x c a)) -> Property
forall a. TestEqual a => a -> a -> Property
=.= ((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 b b -> cat (x a c) (x c a) -> cat (x b (x a c)) (x b (x c 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 (x a c) (x c 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 b (x a c)) (x b (x c a))
-> cat (x (x a b) c) (x b (x a c))
-> cat (x (x a b) c) (x b (x c 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 (x (x b a) c) (x b (x a 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 cat (x (x b a) c) (x b (x a c))
-> cat (x (x a b) c) (x (x b a) c)
-> cat (x (x a b) c) (x b (x 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
. (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 cat (x a b) (x b a) -> cat c c -> cat (x (x a b) c) (x (x b a) 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 c c
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 `x` b) `x` c) (b `x` (c `x` a))))

law_braided_hexagon2 :: forall {k} (cat :: k -> k -> Type) x i a b c obj o.
   (obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj, (TestEqual (cat (x a (x b c)) (x (x c a) b))))
  => o a -> o b -> o c -> Property
law_braided_hexagon2 :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x a (x b c)) (x (x c a) b))) =>
o a -> o b -> o c -> Property
law_braided_hexagon2 o a
_ o b
_ o c
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"braided-hexagon-2"
   (cat (x c (x a b)) (x (x c a) b)
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_ cat (x c (x a b)) (x (x c a) b)
-> cat (x a (x b c)) (x c (x a b))
-> cat (x a (x b c)) (x (x c 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 (x (x a b) c) (x c (x a b))
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 (x a b) c) (x c (x a b))
-> cat (x a (x b c)) (x (x a b) c)
-> cat (x a (x b c)) (x c (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 (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_ cat (x a (x b c)) (x (x c a) b)
-> cat (x a (x b c)) (x (x c a) b) -> Property
forall a. TestEqual a => a -> a -> Property
=.= ((cat (x a c) (x c 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 c) (x c a) -> cat b b -> cat (x (x a c) b) (x (x c 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 (x a c) b) (x (x c a) b)
-> cat (x a (x b c)) (x (x a c) b)
-> cat (x a (x b c)) (x (x c 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 (x a (x c b)) (x (x a c) b)
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_ cat (x a (x c b)) (x (x a c) b)
-> cat (x a (x b c)) (x a (x c b))
-> cat (x a (x b c)) (x (x a c) 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 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 (x b c) (x c b) -> cat (x a (x b c)) (x a (x c 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 (x b c) (x c b)
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 (a `x` (b `x` c)) ((c `x` a) `x` b)))

law_braided_triangle :: forall {k} (cat :: k -> k -> Type) (x :: k -> k -> k) (i :: k) a obj o. (obj ~ Obj cat, Braided x i cat, obj a, obj i, Con' x obj, TestEqual (cat (x a i) a))
  => o a -> Property
law_braided_triangle :: forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj i, Con' x obj,
 TestEqual (cat (x a i) a)) =>
o a -> Property
law_braided_triangle o a
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"monoidal-triangle"
   (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_ cat (x i a) a -> cat (x a i) (x i a) -> cat (x a 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 (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) a -> cat (x a i) a -> Property
forall a. TestEqual a => a -> a -> Property
=.=  (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)))


laws_braided :: forall {k} {x :: k -> k -> k}
                          {obj :: k -> Constraint} 
                          {i :: k} 
                          (cat :: k -> k -> Type).
                 (obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_braided :: forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_braided  t :: TestableCat x i obj cat
t@TestableCat{o i
GenObj obj o cat
forall (a :: k). o a -> Dict (TT cat a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k). o a -> Dict (TT cat a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..}   = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product
   [ TestableCat x i obj cat -> Property
forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint).
(obj ~ Obj cat, Con' x obj, Monoidal x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_monoidal TestableCat x i obj cat
t
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> BraidedRec x i obj cat -> o a -> o a -> Property
forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b,
 TestEqual (cat (x b a) (x b a))) =>
BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_inv BraidedRec x i obj cat
m   o a
a o a
b  (TestEqual (cat (x a a) (x a a)) => Property)
-> Dict (TestEqual (cat (x a a) (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a) -> Dict (TestEqual (cat (x a a) (x a a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
b o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> BraidedRec x i obj (Op cat) -> o a -> o a -> Property
forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b,
 TestEqual (cat (x b a) (x b a))) =>
BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_inv BraidedRec x i obj (Op cat)
mOp o a
a o a
b  (TestEqual (cat (x a a) (x a a)) => Property)
-> Dict (TestEqual (cat (x a a) (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a) -> Dict (TestEqual (cat (x a a) (x a a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
b o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj i, Con' x obj,
 TestEqual (cat (x a i) a)) =>
o a -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) (a :: k)
       (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj i, Con' x obj,
 TestEqual (cat (x a i) a)) =>
o a -> Property
law_braided_triangle @cat @x o a
a (TestEqual (cat (x a i) a) => Property)
-> Dict (TestEqual (cat (x a i) a)) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a i) -> o a -> Dict (TestEqual (cat (x a i) a))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable (o a
a o a -> o i -> o (x a i)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o i
unitObj) o a
a
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
c ->
       forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x b (x c a)))) =>
o a -> o b -> o c -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) (a :: k)
       (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x (x a b) c) (x b (x c a)))) =>
o a -> o b -> o c -> Property
law_braided_hexagon1 @cat @x o a
a o a
b o a
c (TestEqual (cat (x (x a a) a) (x a (x a a))) => Property)
-> Dict (TestEqual (cat (x (x a a) a) (x a (x a a)))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x (x a a) a)
-> o (x a (x a a))
-> Dict (TestEqual (cat (x (x a a) a) (x a (x a a))))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable ((o a
a o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b) o (x a a) -> o a -> o (x (x a a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
c) (o a
b o a -> o (x a a) -> o (x a (x a a))
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× (o a
c o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a))
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
c ->
       forall {k} (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (a :: k) (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x a (x b c)) (x (x c a) b))) =>
o a -> o b -> o c -> Property
forall (cat :: k -> k -> *) (x :: k -> k -> k) (i :: k) (a :: k)
       (b :: k) (c :: k) (obj :: k -> Constraint) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, obj a, obj b, obj c, Con' x obj,
 TestEqual (cat (x a (x b c)) (x (x c a) b))) =>
o a -> o b -> o c -> Property
law_braided_hexagon2 @cat @x o a
a o a
b o a
c (TestEqual (cat (x a (x a a)) (x (x a a) a)) => Property)
-> Dict (TestEqual (cat (x a (x a a)) (x (x a a) a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a (x a a))
-> o (x (x a a) a)
-> Dict (TestEqual (cat (x a (x a a)) (x (x a a) a)))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable (o a
a o a -> o (x a a) -> o (x a (x a a))
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× (o a
b o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
c)) ((o a
c o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a) o (x a a) -> o a -> o (x (x a a) a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
b)
   ]
   where m :: R.BraidedRec x i obj cat 
         m :: BraidedRec x i obj cat
m@R.BraidedRec{} = forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
forall (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
braidedRec @x
         mOp :: R.BraidedRec x i obj (Op cat)
         mOp :: BraidedRec x i obj (Op cat)
mOp = forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
forall (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
braidedRec @x
         -- running the test on the op category mean that we test the reverse compositions.

law_swap_invol :: forall {k} (a::k) (b::k) x i obj (cat :: k -> k -> Type) o.
  (obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b, TestEqual (cat (x b a) (x b a)))
  => R.BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_invol :: forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b,
 TestEqual (cat (x b a) (x b a))) =>
BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_invol R.BraidedRec{forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap :: forall {k1} {k2} {k3} (x :: k1 -> k1 -> k2) (i :: k3)
       (con :: k1 -> Constraint) (cat :: k2 -> k2 -> *).
BraidedRec x i con cat
-> forall (a :: k1) (b :: k1).
   (con a, con b) =>
   cat (x a b) (x b a)
swap_ :: forall {k1} {k2} {k3} (x :: k1 -> k1 -> k2) (i :: k3)
       (con :: k1 -> Constraint) (cat :: k2 -> k2 -> *).
BraidedRec x i con cat
-> forall (a :: k1) (b :: k1).
   (con a, con b) =>
   cat (x a b) (x b a)
swap :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap_ :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
..} o a
_ o b
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"swap-invol" (forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap @a @b cat (x a b) (x b a) -> cat (x b a) (x a b) -> cat (x b a) (x b 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 b a) (x a b)
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) (x b a)
swap cat (x b a) (x b a) -> cat (x b a) (x b a) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat (x b a) (x b 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)


laws_symmetric :: forall {k} {x :: k -> k -> k}
                          {obj :: k -> Constraint} 
                          {i :: k} 
                          (cat :: k -> k -> Type).
                 (obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_symmetric :: forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_symmetric  t :: TestableCat x i obj cat
t@TestableCat{o i
GenObj obj o cat
forall (a :: k). o a -> Dict (TT cat a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k). o a -> Dict (TT cat a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..}   = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product
   [ TestableCat x i obj cat -> Property
forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_braided TestableCat x i obj cat
t
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
a -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
b -> BraidedRec x i obj cat -> o a -> o a -> Property
forall {k} (a :: k) (b :: k) (x :: k -> k -> k) (i :: k)
       (obj :: k -> Constraint) (cat :: k -> k -> *) (o :: k -> *).
(obj ~ Obj cat, Braided x i cat, Con' x obj, obj a, obj b,
 TestEqual (cat (x b a) (x b a))) =>
BraidedRec x i obj cat -> o a -> o b -> Property
law_swap_invol BraidedRec x i obj cat
m o a
a o a
b
      (TestEqual (cat (x a a) (x a a)) => Property)
-> Dict (TestEqual (cat (x a a) (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a) -> Dict (TestEqual (cat (x a a) (x a a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
b o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
a) 
   ]
   where m :: R.BraidedRec x i obj cat 
         m :: BraidedRec x i obj cat
m@R.BraidedRec{} = forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
forall (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Braided x i cat =>
BraidedRec x i (Obj cat) cat
braidedRec @x


law_dup_commut :: forall {k} {cat :: k -> k -> Type}
                                     {x :: k -> k -> k}  {a :: k}
                                     {b :: k} {i :: k} obj.
                              (obj a, obj b, Category cat, Obj cat ~ obj,
                               TestEqual (cat a (x b b)), Cartesian x i cat, Con' x obj) =>
                              R.CartesianRec x i obj cat -> cat a b -> Property
law_dup_commut :: forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {a :: k}
       {b :: k} {i :: k} (obj :: k -> Constraint).
(obj a, obj b, Category cat, Obj cat ~ obj,
 TestEqual (cat a (x b b)), Cartesian x i cat, Con' x obj) =>
CartesianRec x i obj cat -> cat a b -> Property
law_dup_commut R.CartesianRec{forall (a :: k). obj a => cat a i
forall (a :: k). obj a => cat a (x a a)
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) a
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) b
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat a b -> cat a c -> cat a (x b c)
exl :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) a
exr :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) b
dis :: forall (a :: k). obj a => cat a i
dup :: forall (a :: k). obj a => cat a (x a a)
▵ :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat a b -> cat a c -> cat a (x b c)
exl :: 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
exr :: 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
dis :: 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
dup :: 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)
▵ :: 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)
..} cat a b
f = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"dup/cross" ((cat a b
f cat a b -> cat a b -> cat (x a a) (x b 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 a b
f) cat (x a a) (x b b) -> cat a (x a a) -> cat a (x b 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 a)
forall (a :: k). obj a => cat a (x a a)
dup cat a (x b b) -> cat a (x b b) -> Property
forall a. TestEqual a => a -> a -> Property
=.= cat b (x b b)
forall (a :: k). obj a => cat a (x a a)
dup cat b (x b b) -> cat a b -> cat a (x b 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 b
f)

law_projections :: forall {k} {con :: k -> Constraint} {x :: k -> k -> k}
                      {b :: k} {c :: k} {cat :: k -> k -> Type} {i :: k} {p}.
               (con (x b c), con b, con c, Obj cat (x b c), Con' x con,
                TestEqual (cat (x b c) (x b c)), Category cat) =>
               R.CartesianRec x i con cat -> p b -> p c -> Property
law_projections :: forall {k} {con :: k -> Constraint} {x :: k -> k -> k} {b :: k}
       {c :: k} {cat :: k -> k -> *} {i :: k} {p :: k -> *}.
(con (x b c), con b, con c, Obj cat (x b c), Con' x con,
 TestEqual (cat (x b c) (x b c)), Category cat) =>
CartesianRec x i con cat -> p b -> p c -> Property
law_projections R.CartesianRec{forall (a :: k). con a => cat a i
forall (a :: k). con a => cat a (x a a)
forall (a :: k) (b :: k). (con a, con b) => cat (x a b) a
forall (a :: k) (b :: k). (con a, con b) => cat (x a b) b
forall (a :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat a b -> cat a c -> cat a (x b c)
exl :: 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
exr :: 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
dis :: 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
dup :: 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)
▵ :: 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)
exl :: forall (a :: k) (b :: k). (con a, con b) => cat (x a b) a
exr :: forall (a :: k) (b :: k). (con a, con b) => cat (x a b) b
dis :: forall (a :: k). con a => cat a i
dup :: forall (a :: k). con a => cat a (x a a)
▵ :: forall (a :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat a b -> cat a c -> cat a (x b c)
..} p b
_ p c
_ = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
nameLaw String
"projections" (cat (x b c) b
forall (a :: k) (b :: k). (con a, con b) => cat (x a b) a
exl cat (x b c) b -> cat (x b c) c -> cat (x b c) (x b c)
forall (a :: k) (b :: k) (c :: k).
(con a, con b, con c) =>
cat a b -> cat a c -> cat a (x b c)
▵ cat (x b c) c
forall (a :: k) (b :: k). (con a, con b) => cat (x a b) b
exr  cat (x b c) (x b c) -> cat (x b c) (x b c) -> Property
forall a. TestEqual a => a -> a -> Property
=.= forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id @k @cat @(b `x` c))



laws_cartesian_extra :: forall {k} (x :: k -> k -> k)
                          {obj :: k -> Constraint} 
                          (i :: k )
                          (cat :: k -> k -> Type).
                 (obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_cartesian_extra :: forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian_extra  t :: TestableCat x i obj cat
t@TestableCat{o i
GenObj obj o cat
forall (a :: k). o a -> Dict (TT cat a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k). o a -> Dict (TT cat a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..}   = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product
   [ GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t1 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t2 -> o a -> o a -> (cat a a -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o a
t1 o a
t2 ((cat a a -> Property) -> Property)
-> (cat a a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat a a
f -> CartesianRec x i obj cat -> cat a a -> Property
forall {k} {cat :: k -> k -> *} {x :: k -> k -> k} {a :: k}
       {b :: k} {i :: k} (obj :: k -> Constraint).
(obj a, obj b, Category cat, Obj cat ~ obj,
 TestEqual (cat a (x b b)), Cartesian x i cat, Con' x obj) =>
CartesianRec x i obj cat -> cat a b -> Property
law_dup_commut CartesianRec x i obj cat
m cat a a
f  (TestEqual (cat a (x a a)) => Property)
-> Dict (TestEqual (cat a (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o a -> o (x a a) -> Dict (TestEqual (cat a (x a a)))
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable o a
t1 (o a
t2 o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
t2)
   , GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t1 -> GenObj obj o cat
genObj GenObj obj o cat -> GenObj obj o cat
forall a b. (a -> b) -> a -> b
$ \o a
t2 -> CartesianRec x i obj cat -> o a -> o a -> Property
forall {k} {con :: k -> Constraint} {x :: k -> k -> k} {b :: k}
       {c :: k} {cat :: k -> k -> *} {i :: k} {p :: k -> *}.
(con (x b c), con b, con c, Obj cat (x b c), Con' x con,
 TestEqual (cat (x b c) (x b c)), Category cat) =>
CartesianRec x i con cat -> p b -> p c -> Property
law_projections CartesianRec x i obj cat
m o a
t1 o a
t2  (TestEqual (cat (x a a) (x a a)) => Property)
-> Dict (TestEqual (cat (x a a) (x a a))) -> Property
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o (x a a) -> Dict (TestEqual (cat (x a a) (x a a)))
forall (a :: k). o a -> Dict (TT cat a a)
getTestable' (o a
t1 o a -> o a -> o (x a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
× o a
t2)
   ]
   where m :: R.CartesianRec x i obj cat 
         m :: CartesianRec x i obj cat
m@R.CartesianRec{forall (a :: k). obj a => cat a i
forall (a :: k). obj a => cat a (x a a)
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) a
forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) b
forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat a b -> cat a c -> cat a (x b c)
exl :: 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
exr :: 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
dis :: 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
dup :: 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)
▵ :: 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)
exl :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) a
exr :: forall (a :: k) (b :: k). (obj a, obj b) => cat (x a b) b
dis :: forall (a :: k). obj a => cat a i
dup :: forall (a :: k). obj a => cat a (x a a)
▵ :: forall (a :: k) (b :: k) (c :: k).
(obj a, obj b, obj c) =>
cat a b -> cat a c -> cat a (x b c)
..} = CartesianRec x i obj cat
CartesianRec x i (Obj cat) cat
forall {k} (x :: k -> k -> k) (cat :: k -> k -> *) (i :: k).
Cartesian x i cat =>
CartesianRec x i (Obj cat) cat
cartesianRec

laws_cartesian :: forall {k} (x :: k -> k -> k)
                          {obj :: k -> Constraint} 
                          (i :: k )
                          (cat :: k -> k -> Type).
                 (obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_cartesian :: forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian  t :: TestableCat x i obj cat
t@TestableCat{o i
GenObj obj o cat
forall (a :: k). o a -> Dict (TT cat a a)
forall (a :: k) (b :: k). o a -> o b -> o (x a b)
forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k) (b :: k).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k) (b :: k).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k) (b :: k). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k). o a -> Dict (TT cat a a)
× :: forall (a :: k) (b :: k). o a -> o b -> o (x a b)
unitObj :: o i
..} = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product
   [ TestableCat x i obj cat -> Property
forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_symmetric TestableCat x i obj cat
t , TestableCat x i obj cat -> Property
forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian_extra TestableCat x i obj cat
t]

laws_cocartesian :: forall {k} {x :: k -> k -> k}
                          {obj :: k -> Constraint} 
                          {i :: k} 
                          {cat :: k -> k -> Type}.
                 (obj ~ Obj cat, Con' x obj, CoCartesian x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_cocartesian :: forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       {cat :: k -> k -> *}.
(obj ~ Obj cat, Con' x obj, CoCartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cocartesian  TestableCat x i obj cat
t = TestableCat x i obj (Op cat) -> Property
forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian (TestableCat x i obj cat -> TestableCat x i obj (Op cat)
forall {k1} (x :: k1 -> k1 -> k1) (i :: k1)
       (obj :: k1 -> Constraint) (cat :: k1 -> k1 -> *).
TestableCat x i obj cat -> TestableCat x i obj (Op cat)
opTestable TestableCat x i obj cat
t)


opTestable :: TestableCat x i obj cat -> TestableCat x i obj (Op cat)
opTestable :: forall {k1} (x :: k1 -> k1 -> k1) (i :: k1)
       (obj :: k1 -> Constraint) (cat :: k1 -> k1 -> *).
TestableCat x i obj cat -> TestableCat x i obj (Op cat)
opTestable TestableCat{o i
GenObj obj o cat
forall (a :: k1). o a -> Dict (TT cat a a)
forall (a :: k1) (b :: k1). o a -> o b -> o (x a b)
forall (a :: k1) (b :: k1). o a -> o b -> Dict (TT cat a b)
forall (a :: k1) (b :: k1).
o a -> o b -> (cat a b -> Property) -> Property
forall (a :: k1) (b :: k1).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genObj :: ()
genMorph' :: ()
genMorph :: ()
getTestable :: ()
getTestable' :: ()
× :: ()
unitObj :: ()
genObj :: GenObj obj o cat
genMorph' :: forall (a :: k1) (b :: k1).
o a -> o b -> (TT cat a b => cat a b -> Property) -> Property
genMorph :: forall (a :: k1) (b :: k1).
o a -> o b -> (cat a b -> Property) -> Property
getTestable :: forall (a :: k1) (b :: k1). o a -> o b -> Dict (TT cat a b)
getTestable' :: forall (a :: k1). o a -> Dict (TT cat a a)
× :: forall (a :: k1) (b :: k1). o a -> o b -> o (x a b)
unitObj :: o i
..} = GenObj obj o cat
-> (forall (a :: k1) (b :: k1).
    o a -> o b -> (Op cat a b -> Property) -> Property)
-> (forall (a :: k1) (b :: k1).
    o a -> o b -> Dict (TT (Op cat) a b))
-> (forall (a :: k1) (b :: k1). o a -> o b -> o (x a b))
-> o i
-> TestableCat x i obj (Op cat)
forall {k} (f :: k -> k -> *) (x :: k -> k -> k) (i :: k)
       (o :: k -> *) (obj :: k -> Constraint).
GenObj obj o f
-> (forall (a :: k) (b :: k).
    o a -> o b -> (f a b -> Property) -> Property)
-> (forall (a :: k) (b :: k). o a -> o b -> Dict (TT f a b))
-> (forall (a :: k) (b :: k). o a -> o b -> o (x a b))
-> o i
-> TestableCat x i obj f
testableCat
                               GenObj obj o cat
genObj (\o a
a o b
b Op cat a b -> Property
k -> o b -> o a -> (cat b a -> Property) -> Property
forall (a :: k1) (b :: k1).
o a -> o b -> (cat a b -> Property) -> Property
genMorph o b
b o a
a ((cat b a -> Property) -> Property)
-> (cat b a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \cat b a
f -> Op cat a b -> Property
k (cat b a -> Op cat a b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Op k2 a b
Op cat b a
f))
                               (\o a
a o b
b -> Dict (TT (Op cat) a b)
TestEqual (cat b a) => Dict (TT (Op cat) a b)
forall (a :: Constraint). a => Dict a
Dict (TestEqual (cat b a) => Dict (TT (Op cat) a b))
-> Dict (TestEqual (cat b a)) -> Dict (TT (Op cat) a b)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ o b -> o a -> Dict (TestEqual (cat b a))
forall (a :: k1) (b :: k1). o a -> o b -> Dict (TT cat a b)
getTestable o b
b o a
a)
                               o a -> o b -> o (x a b)
forall (a :: k1) (b :: k1). o a -> o b -> o (x a b)
(×) o i
unitObj

laws_bicartesian :: forall {k} {x :: k -> k -> k}
                          {obj :: k -> Constraint} 
                          {i :: k} 
                          (cat :: k -> k -> Type).
                 (obj ~ Obj cat, Con' x obj, BiCartesian x i cat, obj i) 
                 => TestableCat x i obj cat -> Property
laws_bicartesian :: forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, BiCartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_bicartesian  TestableCat x i obj cat
t = [Property] -> Property
forall a (f :: * -> *). (Multiplicative a, Foldable f) => f a -> a
product [ TestableCat x i obj cat -> Property
forall {k} {x :: k -> k -> k} {obj :: k -> Constraint} {i :: k}
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Braided x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_symmetric TestableCat x i obj cat
t
                              , TestableCat x i obj cat -> Property
forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian_extra TestableCat x i obj cat
t
                              , TestableCat x i obj (Op cat) -> Property
forall {k} (x :: k -> k -> k) {obj :: k -> Constraint} (i :: k)
       (cat :: k -> k -> *).
(obj ~ Obj cat, Con' x obj, Cartesian x i cat, obj i) =>
TestableCat x i obj cat -> Property
laws_cartesian_extra (TestableCat x i obj cat -> TestableCat x i obj (Op cat)
forall {k1} (x :: k1 -> k1 -> k1) (i :: k1)
       (obj :: k1 -> Constraint) (cat :: k1 -> k1 -> *).
TestableCat x i obj cat -> TestableCat x i obj (Op cat)
opTestable TestableCat x i obj cat
t)]