module Proarrow.Category.Instance.Bool where

import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..), dimapDefault)
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..), leftUnitorProd, leftUnitorProdInv, rightUnitorProd, rightUnitorProdInv, associatorProd, associatorProdInv, swapProd)
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..))
import Proarrow.Object.Exponential (Closed(..))
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal (..))


data BOOL = FLS | TRU

type Booleans :: CAT BOOL
data Booleans a b where
  Fls :: Booleans FLS FLS
  F2T :: Booleans FLS TRU
  Tru :: Booleans TRU TRU


class IsBool (b :: BOOL) where boolId :: b ~> b
instance IsBool FLS where boolId :: 'FLS ~> 'FLS
boolId = 'FLS ~> 'FLS
Booleans 'FLS 'FLS
Fls
instance IsBool TRU where boolId :: 'TRU ~> 'TRU
boolId = 'TRU ~> 'TRU
Booleans 'TRU 'TRU
Tru

-- | The category of 2 objects and one arrow between them, a.k.a. the walking arrow.
instance CategoryOf BOOL where
  type (~>) = Booleans
  type Ob b = IsBool b

instance Promonad Booleans where
  id :: forall (a :: BOOL). Ob a => Booleans a a
id = a ~> a
Booleans a a
forall (b :: BOOL). IsBool b => b ~> b
boolId
  Booleans b c
Fls . :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL).
Booleans b c -> Booleans a b -> Booleans a c
. Booleans a b
Fls = Booleans a c
Booleans 'FLS 'FLS
Fls
  Booleans b c
F2T . Booleans a b
Fls = Booleans a c
Booleans 'FLS 'TRU
F2T
  Booleans b c
Tru . Booleans a b
F2T = Booleans a c
Booleans 'FLS 'TRU
F2T
  Booleans b c
Tru . Booleans a b
Tru = Booleans a c
Booleans 'TRU 'TRU
Tru

instance Profunctor Booleans where
  dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL).
(c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d
dimap = (c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d
Booleans c a -> Booleans b d -> Booleans a b -> Booleans c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: BOOL) (b :: BOOL) r.
((Ob a, Ob b) => r) -> Booleans a b -> r
\\ Booleans a b
Fls = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Booleans a b
F2T = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Booleans a b
Tru = r
(Ob a, Ob b) => r
r


instance HasTerminalObject BOOL where
  type TerminalObject = TRU
  terminate' :: forall (a :: BOOL). Obj a -> a ~> TerminalObject
terminate' Obj a
Booleans a a
Fls = a ~> TerminalObject
Booleans 'FLS 'TRU
F2T
  terminate' Obj a
Booleans a a
Tru = a ~> TerminalObject
Booleans 'TRU 'TRU
Tru

instance HasBinaryProducts BOOL where
  type TRU && TRU = TRU
  type FLS && TRU = FLS
  type TRU && FLS = FLS
  type FLS && FLS = FLS
  fst' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> (a && b) ~> a
fst' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = (a && b) ~> a
Booleans 'FLS 'FLS
Fls
  fst' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = (a && b) ~> a
Booleans 'FLS 'FLS
Fls
  fst' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = (a && b) ~> a
Booleans 'FLS 'TRU
F2T
  fst' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = (a && b) ~> a
Booleans 'TRU 'TRU
Tru
  snd' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> (a && b) ~> b
snd' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = (a && b) ~> b
Booleans 'FLS 'FLS
Fls
  snd' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = (a && b) ~> b
Booleans 'FLS 'TRU
F2T
  snd' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = (a && b) ~> b
Booleans 'FLS 'FLS
Fls
  snd' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = (a && b) ~> b
Booleans 'TRU 'TRU
Tru
  a ~> x
Booleans a x
Fls &&& :: forall (a :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
Booleans 'FLS y
Fls = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
  a ~> x
Booleans a x
Fls &&& a ~> y
Booleans 'FLS y
F2T = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
  a ~> x
Booleans a x
F2T &&& a ~> y
Booleans 'FLS y
Fls = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
  a ~> x
Booleans a x
F2T &&& a ~> y
Booleans 'FLS y
F2T = a ~> (x && y)
Booleans 'FLS 'TRU
F2T
  a ~> x
Booleans a x
Tru &&& a ~> y
Booleans 'TRU y
Tru = a ~> (x && y)
Booleans 'TRU 'TRU
Tru

instance HasInitialObject BOOL where
  type InitialObject = FLS
  initiate' :: forall (a :: BOOL). Obj a -> InitialObject ~> a
initiate' Obj a
Booleans a a
Fls = InitialObject ~> a
Booleans 'FLS 'FLS
Fls
  initiate' Obj a
Booleans a a
Tru = InitialObject ~> a
Booleans 'FLS 'TRU
F2T

instance HasBinaryCoproducts BOOL where
  type FLS || FLS = FLS
  type FLS || TRU = TRU
  type TRU || FLS = TRU
  type TRU || TRU = TRU
  lft' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> a ~> (a || b)
lft' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = a ~> (a || b)
Booleans 'FLS 'FLS
Fls
  lft' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = a ~> (a || b)
Booleans 'FLS 'TRU
F2T
  lft' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = a ~> (a || b)
Booleans 'TRU 'TRU
Tru
  lft' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = a ~> (a || b)
Booleans 'TRU 'TRU
Tru
  rgt' :: forall (a :: BOOL) (b :: BOOL). Obj a -> Obj b -> b ~> (a || b)
rgt' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls = b ~> (a || b)
Booleans 'FLS 'FLS
Fls
  rgt' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru = b ~> (a || b)
Booleans 'TRU 'TRU
Tru
  rgt' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls = b ~> (a || b)
Booleans 'FLS 'TRU
F2T
  rgt' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru = b ~> (a || b)
Booleans 'TRU 'TRU
Tru
  x ~> a
Booleans x a
Fls ||| :: forall (x :: BOOL) (a :: BOOL) (y :: BOOL).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Booleans y 'FLS
Fls = (x || y) ~> a
Booleans 'FLS 'FLS
Fls
  x ~> a
Booleans x a
F2T ||| y ~> a
Booleans y 'TRU
F2T = (x || y) ~> a
Booleans 'FLS 'TRU
F2T
  x ~> a
Booleans x a
F2T ||| y ~> a
Booleans y 'TRU
Tru = (x || y) ~> a
Booleans 'TRU 'TRU
Tru
  x ~> a
Booleans x a
Tru ||| y ~> a
Booleans y 'TRU
F2T = (x || y) ~> a
Booleans 'TRU 'TRU
Tru
  x ~> a
Booleans x a
Tru ||| y ~> a
Booleans y 'TRU
Tru = (x || y) ~> a
Booleans 'TRU 'TRU
Tru

instance Monoidal BOOL where
  type Unit = TerminalObject
  type a ** b = a && b
  a ~> b
f par :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL) (d :: BOOL).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` c ~> d
g = a ~> b
f (a ~> b) -> (c ~> d) -> (a && c) ~> (b && d)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** c ~> d
g
  leftUnitor :: forall (a :: BOOL). Obj a -> (Unit ** a) ~> a
leftUnitor = (a ~> a) -> (Unit ** a) ~> a
(a ~> a) -> (TerminalObject && a) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: BOOL). Obj a -> a ~> (Unit ** a)
leftUnitorInv = (a ~> a) -> a ~> (Unit ** a)
(a ~> a) -> a ~> (TerminalObject && a)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: BOOL). Obj a -> (a ** Unit) ~> a
rightUnitor = (a ~> a) -> (a ** Unit) ~> a
(a ~> a) -> (a && TerminalObject) ~> a
forall k (a :: k).
HasProducts k =>
Obj a -> (a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: BOOL). Obj a -> a ~> (a ** Unit)
rightUnitorInv = (a ~> a) -> a ~> (a ** Unit)
(a ~> a) -> a ~> (a && TerminalObject)
forall k (a :: k).
HasProducts k =>
Obj a -> a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator = (a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a ** b) ** c) ~> (a ** (b ** c))
(a ~> a)
-> (b ~> b) -> (c ~> c) -> ((a && b) && c) ~> (a && (b && c))
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> ((a && b) && c) ~> (a && (b && c))
associatorProd
  associatorInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ~> a)
-> (b ~> b) -> (c ~> c) -> (a ** (b ** c)) ~> ((a ** b) ** c)
(a ~> a)
-> (b ~> b) -> (c ~> c) -> (a && (b && c)) ~> ((a && b) && c)
forall k (a :: k) (b :: k) (c :: k).
HasProducts k =>
Obj a -> Obj b -> Obj c -> (a && (b && c)) ~> ((a && b) && c)
associatorProdInv

instance SymMonoidal BOOL where
  swap' :: forall (a :: BOOL) (b :: BOOL).
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' = (a ~> a) -> (b ~> b) -> (a ** b) ~> (b ** a)
(a ~> a) -> (b ~> b) -> (a && b) ~> (b && a)
forall {k} (a :: k) (b :: k).
HasBinaryProducts k =>
Obj a -> Obj b -> (a && b) ~> (b && a)
swapProd

instance Closed BOOL where
  type FLS ~~> FLS = TRU
  type FLS ~~> TRU = TRU
  type TRU ~~> FLS = FLS
  type TRU ~~> TRU = TRU
  curry' :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
  curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
  curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'FLS 'FLS
Fls
  curry' Obj a
Booleans a a
Fls Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'FLS 'TRU
F2T
  curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
Fls = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
  curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Fls (a ** b) ~> c
Booleans 'FLS c
F2T = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
  curry' Obj a
Booleans a a
Tru Obj b
Booleans b b
Tru (a ** b) ~> c
Booleans 'TRU c
Tru = a ~> (b ~~> c)
Booleans 'TRU 'TRU
Tru
  uncurry' :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
  uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
  uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
  uncurry' Obj b
Booleans b b
Fls Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
  uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Fls a ~> (b ~~> c)
Booleans a 'FLS
Fls = (a ** b) ~> c
Booleans 'FLS 'FLS
Fls
  uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
F2T = (a ** b) ~> c
Booleans 'FLS 'TRU
F2T
  uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Tru a ~> (b ~~> c)
Booleans a 'TRU
Tru = (a ** b) ~> c
Booleans 'TRU 'TRU
Tru
  b ~> y
Booleans b y
Fls ^^^ :: forall (b :: BOOL) (y :: BOOL) (x :: BOOL) (a :: BOOL).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
  b ~> y
Booleans b y
Fls ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
  b ~> y
Booleans b y
Fls ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'FLS
Fls
  b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
  b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
  b ~> y
Booleans b y
F2T ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'FLS 'TRU
F2T
  b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
Fls = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
  b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
F2T = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
  b ~> y
Booleans b y
Tru ^^^ x ~> a
Booleans x a
Tru = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru