Documentation

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 Source #

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 Source #

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 Source #

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 Source #

laws_category :: forall f x i. Category f => TestableCat x i (Obj f) f -> Property Source #

type TT f x y = TestEqual (f x y) Source #

type GenObj obj o f = (forall a. obj a => o a -> Property) -> Property Source #

data TestableCat x i obj f Source #

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 Source #

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))) => MonoidalRec x i obj cat -> cat b1 b3 -> cat b2 d -> cat a b1 -> cat c b2 -> Property Source #

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) => MonoidalRec x i obj cat -> o a -> o b -> o c -> Property Source #

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 Source #

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))) => MonoidalRec x i con cat -> o b -> Property Source #

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 Source #

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 Source #

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 Source #

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))) => BraidedRec x i obj cat -> o a -> o b -> Property Source #

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 Source #

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 Source #

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 Source #

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 Source #

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))) => BraidedRec x i obj cat -> o a -> o b -> Property Source #

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 Source #

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) => CartesianRec x i obj cat -> cat a b -> Property Source #

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) => CartesianRec x i con cat -> p b -> p c -> Property Source #

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 Source #

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 Source #

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 Source #

opTestable :: TestableCat x i obj cat -> TestableCat x i obj (Op cat) Source #

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 Source #