module Proarrow.Category.Instance.Bool where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd'
  )
import Proarrow.Object.Dual (StarAutonomous (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..), initiate)
import Proarrow.Object.Terminal (HasTerminalObject (..), terminate)
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..))

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

class IsBoolArr (a :: BOOL) b where boolArr :: a ~> b
instance IsBoolArr FLS FLS where boolArr :: 'FLS ~> 'FLS
boolArr = 'FLS ~> 'FLS
Booleans 'FLS 'FLS
Fls
instance IsBoolArr FLS TRU where boolArr :: 'FLS ~> 'TRU
boolArr = 'FLS ~> 'TRU
Booleans 'FLS 'TRU
F2T
instance IsBoolArr TRU TRU where boolArr :: 'TRU ~> 'TRU
boolArr = 'TRU ~> 'TRU
Booleans 'TRU 'TRU
Tru

instance ThinProfunctor Booleans where
  type HasArrow Booleans a b = IsBoolArr a b
  arr :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b, HasArrow Booleans a b) =>
Booleans a b
arr = a ~> b
Booleans a b
forall (a :: BOOL) (b :: BOOL). IsBoolArr a b => a ~> b
boolArr
  withArr :: forall (a :: BOOL) (b :: BOOL) r.
Booleans a b -> (HasArrow Booleans a b => r) -> r
withArr Booleans a b
Fls HasArrow Booleans a b => r
r = r
HasArrow Booleans a b => r
r
  withArr Booleans a b
F2T HasArrow Booleans a b => r
r = r
HasArrow Booleans a b => r
r
  withArr Booleans a b
Tru HasArrow Booleans a b => r
r = r
HasArrow Booleans a b => r
r

instance HasTerminalObject BOOL where
  type TerminalObject = TRU
  terminate :: forall (a :: BOOL). Ob a => a ~> TerminalObject
terminate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> a ~> TerminalObject
Booleans 'FLS 'TRU
F2T
    Obj a
Booleans a a
Tru -> a ~> TerminalObject
Booleans 'TRU 'TRU
Tru

instance HasBinaryProducts BOOL where
  type TRU && b = b
  type FLS && b = FLS
  type a && TRU = a
  type a && FLS = FLS
  fst :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> a
fst @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> (a && b) ~> a
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @b
  snd :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> b
snd @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b of
    Obj b
Booleans b b
Fls -> (a && b) ~> b
Booleans 'FLS 'FLS
Fls
    Obj b
Booleans b b
Tru -> forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @a
  a ~> x
Booleans a x
Fls &&& :: forall (a :: BOOL) (x :: BOOL) (y :: BOOL).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
_ = a ~> (x && y)
Booleans 'FLS 'FLS
Fls
  a ~> x
Booleans a x
F2T &&& a ~> y
b = a ~> y
a ~> (x && y)
b
  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). Ob a => InitialObject ~> a
initiate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> InitialObject ~> a
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> InitialObject ~> a
Booleans 'FLS 'TRU
F2T

instance HasBinaryCoproducts BOOL where
  type FLS || b = b
  type TRU || b = TRU
  type a || FLS = a
  type a || TRU = TRU
  lft :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => a ~> (a || b)
lft @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b
    Obj a
Booleans a a
Tru -> a ~> (a || b)
Booleans 'TRU 'TRU
Tru
  rgt :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => b ~> (a || b)
rgt @a @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b of
    Obj b
Booleans b b
Fls -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a
    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
b = y ~> a
(x || y) ~> a
b
  x ~> a
Booleans x a
Tru ||| y ~> a
_ = (x || y) ~> a
Booleans 'TRU 'TRU
Tru

instance MonoidalProfunctor Booleans where
  par0 :: Booleans Unit Unit
par0 = Booleans Unit Unit
Booleans 'TRU 'TRU
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: BOOL). Ob a => Booleans a a
id
  Booleans x1 x2
f par :: forall (x1 :: BOOL) (x2 :: BOOL) (y1 :: BOOL) (y2 :: BOOL).
Booleans x1 x2 -> Booleans y1 y2 -> Booleans (x1 ** y1) (x2 ** y2)
`par` Booleans y1 y2
g = x1 ~> x2
Booleans x1 x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
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)
*** y1 ~> y2
Booleans y1 y2
g

instance Monoidal BOOL where
  type Unit = TerminalObject
  type a ** b = a && b
  leftUnitor :: forall (a :: BOOL). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && a) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: BOOL). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
a ~> (TerminalObject && a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: BOOL). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(a && TerminalObject) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: BOOL). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
a ~> (a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(HasProducts BOOL, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(HasProducts BOOL, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c

instance SymMonoidal BOOL where
  swap' :: forall (a :: BOOL) (a' :: BOOL) (b :: BOOL) (b' :: BOOL).
(a ~> a') -> (b ~> 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) (a' :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
(a ~> a') -> (b ~> b') -> (a && b) ~> (b' && a')
swapProd'

instance Distributive BOOL where
  distL :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (b || c) ~> (b || c)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts 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)
+++ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c
  distR :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c of
    Obj c
Booleans c c
Fls -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
Booleans 'FLS 'FLS
Fls
    Obj c
Booleans c c
Tru -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> (a || b) ~> (a || b)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts 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)
+++ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b
  distL0 :: forall (a :: BOOL). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
Booleans 'FLS 'FLS
Fls
  distR0 :: forall (a :: BOOL). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
Booleans 'FLS 'FLS
Fls

instance Closed BOOL where
  type FLS ~~> b = TRU
  type a ~~> TRU = TRU
  type TRU ~~> FLS = FLS
  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
_ = 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
_ = 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
c a ~> (b ~~> c)
_ = Obj c -> InitialObject ~> c
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: BOOL) (a :: BOOL). (a' ~> a) -> InitialObject ~> a
initiate' Obj c
c
  uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Fls a ~> (b ~~> c)
a = a ~> (b ~~> c)
(a ** b) ~> c
a
  uncurry' Obj b
Booleans b b
Tru Obj c
Booleans c c
Tru a ~> (b ~~> c)
a = a ~> (b ~~> c)
(a ** b) ~> c
a
  b ~> y
_ ^^^ :: 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
Tru ^^^ x ~> a
_ = (a ~~> b) ~> (x ~~> y)
Booleans 'TRU 'TRU
Tru
  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
Fls ^^^ 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
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

instance StarAutonomous BOOL where
  type Bottom = FLS
  bottomObj :: Obj Bottom
bottomObj = Obj Bottom
Booleans 'FLS 'FLS
Fls
  doubleNeg :: forall (a :: BOOL).
(StarAutonomous BOOL, Ob a) =>
Dual (Dual a) ~> a
doubleNeg @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> Dual (Dual a) ~> a
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> Dual (Dual a) ~> a
Booleans 'TRU 'TRU
Tru

instance Monoid TRU where
  mempty :: Unit ~> 'TRU
mempty = Unit ~> 'TRU
Booleans 'TRU 'TRU
Tru
  mappend :: ('TRU ** 'TRU) ~> 'TRU
mappend = ('TRU ** 'TRU) ~> 'TRU
Booleans 'TRU 'TRU
Tru

instance Comonoid TRU where
  counit :: 'TRU ~> Unit
counit = 'TRU ~> Unit
Booleans 'TRU 'TRU
Tru
  comult :: 'TRU ~> ('TRU ** 'TRU)
comult = 'TRU ~> ('TRU ** 'TRU)
Booleans 'TRU 'TRU
Tru

instance Comonoid FLS where
  counit :: 'FLS ~> Unit
counit = 'FLS ~> Unit
Booleans 'FLS 'TRU
F2T
  comult :: 'FLS ~> ('FLS ** 'FLS)
comult = 'FLS ~> ('FLS ** 'FLS)
Booleans 'FLS 'FLS
Fls