{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Category.Op where

import Algebra.Category
import Algebra.Classes
import Algebra.Category.Objects
import Prelude (Show)
import Test.QuickCheck

newtype Op k a b = Op {forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
Op k a b -> k b a
fromOp :: k b a}

deriving instance Additive (f b a) => Additive (Op f a b)
deriving instance Group (f b a) => Group (Op f a b)
deriving instance Arbitrary (f b a) => Arbitrary (Op f a b)
deriving instance Show (f b a) => Show (Op f a b)
deriving instance TestEqual (f b a) => TestEqual (Op f a b)

instance Category k => Category (Op k) where
  type Obj (Op k) = Obj k
  id :: forall (a :: k). Obj (Op k) a => Op k a a
id = k a a -> Op k a a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a a
forall (a :: k). Obj k a => k a a
forall k (cat :: k -> k -> *) (a :: k).
(Category cat, Obj cat a) =>
cat a a
id
  Op k c b
f . :: forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k b c -> Op k a b -> Op k a c
. Op k b a
g = k c a -> Op k a c
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b a
g k b a -> k c b -> k c a
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k c b
f)

instance Monoidal x i k => Monoidal x i (Op k) where
  Op k b a
f ⊗ :: forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c, Obj (Op k) d) =>
Op k a b -> Op k c d -> Op k (x a c) (x b d)
⊗ Op k d c
g = k (x b d) (x a c) -> Op k (x a c) (x b d)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b a
f k b a -> k d c -> k (x b d) (x a c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (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)
⊗ k d c
g)
  assoc :: forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k (x (x a b) c) (x a (x b c))
assoc = k (x a (x b c)) (x (x a b) c) -> Op k (x (x a b) c) (x a (x b c))
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a (x b c)) (x (x a b) c)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k (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_
  assoc_ :: forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k (x a (x b c)) (x (x a b) c)
assoc_ = k (x (x a b) c) (x a (x b c)) -> Op k (x a (x b c)) (x (x a b) c)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x (x a b) c) (x a (x b c))
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k (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
  unitorR :: forall (a :: k). (Obj (Op k) a, Obj (Op k) i) => Op k a (x a i)
unitorR = k (x a i) a -> Op k a (x a i)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a i) a
forall (a :: k). (Obj k a, Obj k i) => k (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_
  unitorR_ :: forall (a :: k). (Obj (Op k) a, Obj (Op k) i) => Op k (x a i) a
unitorR_ = k a (x a i) -> Op k (x a i) a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a (x a i)
forall (a :: k). (Obj k a, Obj k i) => k a (x a i)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Monoidal x i cat, Obj cat a, Obj cat i) =>
cat a (x a i)
unitorR
  unitorL :: forall (a :: k). (Obj (Op k) a, Obj (Op k) i) => Op k a (x i a)
unitorL = k (x i a) a -> Op k a (x i a)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x i a) a
forall (a :: k). (Obj k a, Obj k i) => k (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_
  unitorL_ :: forall (a :: k). (Obj (Op k) a, Obj (Op k) i) => Op k (x i a) a
unitorL_ = k a (x i a) -> Op k (x i a) a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a (x i a)
forall (a :: k). (Obj k a, Obj k i) => k 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

instance Cartesian x i k => CoCartesian x i (Op k) where
  inl :: forall (a :: k) (b :: k). O2 (Op k) a b => Op k a (x a b)
inl = k (x a b) a -> Op k a (x a b)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a b) a
forall (a :: k) (b :: k). O2 k a b => k (x a b) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) a
exl
  inr :: forall (a :: k) (b :: k). O2 (Op k) a b => Op k b (x a b)
inr = k (x a b) b -> Op k b (x a b)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a b) b
forall (a :: k) (b :: k). O2 k a b => k (x a b) b
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Cartesian x i cat, O2 cat a b) =>
cat (x a b) b
exr
  new :: forall (a :: k). Obj (Op k) a => Op k i a
new = k a i -> Op k i a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a i
forall (a :: k). Obj k a => k a i
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a i
dis
  jam :: forall (a :: k). Obj (Op k) a => Op k (x a a) a
jam = k a (x a a) -> Op k (x a a) a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a (x a a)
forall (a :: k). Obj k a => k a (x a a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(Cartesian x i cat, Obj cat a) =>
cat a (x a a)
dup
  Op k a b
f ▿ :: forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k b a -> Op k c a -> Op k (x b c) a
▿ Op k a c
g = k a (x b c) -> Op k (x b c) a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k a b
f k a b -> k a c -> k a (x b c)
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (x b c)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(Cartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat a b -> cat a c -> cat a (x b c)
▵ k a c
g)

instance CoCartesian x i k => Cartesian x i (Op k) where
  exl :: forall (a :: k) (b :: k). O2 (Op k) a b => Op k (x a b) a
exl = k a (x a b) -> Op k (x a b) a
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a (x a b)
forall (a :: k) (b :: k). O2 k a b => k a (x a b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat a (x a b)
inl
  exr :: forall (a :: k) (b :: k). O2 (Op k) a b => Op k (x a b) b
exr = k b (x a b) -> Op k (x a b) b
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k b (x a b)
forall (a :: k) (b :: k). O2 k a b => k b (x a b)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(CoCartesian x i cat, O2 cat a b) =>
cat b (x a b)
inr
  dis :: forall (a :: k). Obj (Op k) a => Op k a i
dis = k i a -> Op k a i
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k i a
forall (a :: k). Obj k a => k i a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat i a
new
  dup :: forall (a :: k). Obj (Op k) a => Op k a (x a a)
dup = k (x a a) a -> Op k a (x a a)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a a) a
forall (a :: k). Obj k a => k (x a a) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k).
(CoCartesian x i cat, Obj cat a) =>
cat (x a a) a
jam
  Op k b a
f ▵ :: forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k a b -> Op k a c -> Op k a (x b c)
▵ Op k c a
g = k (x b c) a -> Op k a (x b c)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b a
f k b a -> k c a -> k (x b c) a
forall (a :: k) (b :: k) (c :: k).
(Obj k a, Obj k b, Obj k c) =>
k b a -> k c a -> k (x b c) a
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k) (c :: k).
(CoCartesian x i cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b a -> cat c a -> cat (x b c) a
▿ k c a
g)

instance Braided x i k => Braided x i (Op k) where
  swap :: forall (a :: k) (b :: k).
(Obj (Op k) a, Obj (Op k) b) =>
Op k (x a b) (x b a)
swap = k (x b a) (x a b) -> Op k (x a b) (x b a)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x b a) (x a b)
forall (a :: k) (b :: k). (Obj k a, Obj k b) => k (x a b) (x b a)
forall {k} (x :: k -> k -> k) (i :: k) (cat :: k -> k -> *)
       (a :: k) (b :: k).
(Braided x i cat, Obj cat a, Obj cat b) =>
cat (x a b) (x b a)
swap
  swap_ :: forall (a :: k) (b :: k).
(Obj (Op k) a, Obj (Op k) b) =>
Op k (x a b) (x b a)
swap_ = k (x b a) (x a b) -> Op k (x a b) (x b a)
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x b a) (x a b)
forall (a :: k) (b :: k). (Obj k a, Obj k b) => k (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_

instance Symmetric x i k => Symmetric x i (Op k) where

instance (con ~ Obj k, Con' x con, UnCon r con, UnCon l con, con i, Autonomous x i r l k, Braided x i k) => Autonomous x i l r (Op k) where
  turn :: forall (a :: k). Obj (Op k) a => Op k i (x (l a) a)
turn = Op k (x a (l a)) (x (l a) a)
forall (a :: k) (b :: k).
(Obj (Op k) a, Obj (Op k) b) =>
Op k (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 Op k (x a (l a)) (x (l a) a)
-> Op k i (x a (l a)) -> Op k i (x (l a) a)
forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k b c -> Op k a b -> Op k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. k (x a (l a)) i -> Op k i (x a (l a))
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k (x a (l a)) i
forall (a :: k). Obj k a => k (x a (l a)) i
forall {k} (x :: k -> k -> k) (i :: k) (l :: k -> k) (r :: k -> k)
       (cat :: k -> k -> *) (a :: k).
(Autonomous x i l r cat, Obj cat a) =>
cat (x a (r a)) i
turn'
  turn' :: forall (a :: k). Obj (Op k) a => Op k (x a (r a)) i
turn' = k i (x (r a) a) -> Op k (x (r a) a) i
forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k i (x (r a) a)
forall (a :: k). Obj k a => k i (x (r a) a)
forall {k} (x :: k -> k -> k) (i :: k) (l :: k -> k) (r :: k -> k)
       (cat :: k -> k -> *) (a :: k).
(Autonomous x i l r cat, Obj cat a) =>
cat i (x (l a) a)
turn Op k (x (r a) a) i
-> Op k (x a (r a)) (x (r a) a) -> Op k (x a (r a)) i
forall (a :: k) (b :: k) (c :: k).
(Obj (Op k) a, Obj (Op k) b, Obj (Op k) c) =>
Op k b c -> Op k a b -> Op k a c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
(Category cat, Obj cat a, Obj cat b, Obj cat c) =>
cat b c -> cat a b -> cat a c
. Op k (x a (r a)) (x (r a) a)
forall (a :: k) (b :: k).
(Obj (Op k) a, Obj (Op k) b) =>
Op k (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

instance (con ~ Obj k, Con' x con, UnCon d con, con i, Compact x i d k, Braided x i k) => Compact x i d (Op k) where