module Proarrow.Category.Instance.Bool where

import Prelude (type (~))

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Category.Instance.Sub (FUN, SUBCAT (..), (!))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj, type (+->))
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 (ExpSA, StarAutonomous (..), applySA, currySA)
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.NaturalNumbers (HasParamNNO (..))
import Proarrow.Object.Pullback (HasPullbacks (..), thinPullback)
import Proarrow.Object.Pushout (HasPushouts (..), thinPushout)
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Prelude qualified as P

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

deriving instance P.Eq (Booleans a b)
deriving instance P.Show (Booleans a b)

class (IsBool (Dual b)) => 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 :: 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 Representable Booleans where
  type Booleans % x = x
  index :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> a ~> (Booleans % b)
index = Booleans a b -> a ~> (Booleans % b)
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  tabulate :: forall (b :: BOOL) (a :: BOOL).
Ob b =>
(a ~> (Booleans % b)) -> Booleans a b
tabulate = (a ~> (Booleans % b)) -> Booleans a b
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  repMap :: forall (a :: BOOL) (b :: BOOL).
(a ~> b) -> (Booleans % a) ~> (Booleans % b)
repMap = (a ~> b) -> (Booleans % a) ~> (Booleans % b)
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

instance Corepresentable Booleans where
  type Booleans %% x = x
  coindex :: forall (a :: BOOL) (b :: BOOL).
Booleans a b -> (Booleans %% a) ~> b
coindex = Booleans a b -> (Booleans %% a) ~> b
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  cotabulate :: forall (a :: BOOL) (b :: BOOL).
Ob a =>
((Booleans %% a) ~> b) -> Booleans a b
cotabulate = ((Booleans %% a) ~> b) -> Booleans a b
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  corepMap :: forall (a :: BOOL) (b :: BOOL).
(a ~> b) -> (Booleans %% a) ~> (Booleans %% b)
corepMap = (a ~> b) -> (Booleans %% a) ~> (Booleans %% b)
Booleans a b -> Booleans a b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

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
  withObProd :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a Ob (a && b) => r
r = 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
Tru -> r
Ob (a && b) => r
r
    Obj a
Booleans a a
Fls -> r
Ob (a && b) => r
r
  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 HasPullbacks BOOL where
  pullback :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback = (a ~> o) -> (b ~> o) -> Cosink '[a, b]
forall {k} (o :: k) (a :: k) (b :: k).
HasProducts k =>
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
thinPullback

instance HasPushouts BOOL where
  pushout :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL).
(o ~> a) -> (o ~> b) -> Sink '[a, b]
pushout = (o ~> a) -> (o ~> b) -> Sink '[a, b]
forall {k} (o :: k) (a :: k) (b :: k).
HasCoproducts k =>
(o ~> a) -> (o ~> b) -> Sink '[a, b]
thinPushout

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
  withObCoprod :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a Ob (a || b) => r
r = 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
Tru -> r
Ob (a || b) => r
r
    Obj a
Booleans a a
Fls -> r
Ob (a || b) => r
r
  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 :: 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

-- | Products as monoidal structure.
instance Monoidal BOOL where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @BOOL @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) (b :: BOOL).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall (a :: BOOL) (b :: BOOL).
(HasBinaryProducts BOOL, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

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 a ~~> b = ExpSA a b
  withObExp :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a Ob (a ~~> b) => r
r = 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 -> r
Ob (a ~~> b) => r
r
    Obj a
Booleans a a
Tru -> r
Ob (a ~~> b) => r
r
  curry :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(StarAutonomous BOOL, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @a @b
  apply :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @b @c = forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
forall (b :: BOOL) (c :: BOOL).
(StarAutonomous BOOL, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA @b @c

instance StarAutonomous BOOL where
  type Dual FLS = TRU
  type Dual TRU = FLS
  dual :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> Dual b ~> Dual a
dual a ~> b
Booleans a b
Fls = Dual b ~> Dual a
Booleans 'TRU 'TRU
Tru
  dual a ~> b
Booleans a b
F2T = Dual b ~> Dual a
Booleans 'FLS 'TRU
F2T
  dual a ~> b
Booleans a b
Tru = Dual b ~> Dual a
Booleans 'FLS 'FLS
Fls
  dualInv :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @a @b Dual a ~> Dual b
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b, Dual a ~> Dual b
Booleans (Dual a) (Dual b)
f) of
    (Booleans a a
Fls, Booleans b b
Fls, Booleans (Dual a) (Dual b)
Booleans 'TRU 'TRU
Tru) -> b ~> a
Booleans 'FLS 'FLS
Fls
    (Booleans a a
Tru, Booleans b b
Fls, Booleans (Dual a) (Dual b)
Booleans 'FLS 'TRU
F2T) -> b ~> a
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Tru, Booleans (Dual a) (Dual b)
Booleans 'FLS 'FLS
Fls) -> b ~> a
Booleans 'TRU 'TRU
Tru
    (Booleans a a
Fls, Booleans b b
Tru, Booleans (Dual a) (Dual b)
f') -> case Booleans (Dual a) (Dual b)
f' of {}
  linDist :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b (a ** b) ~> Dual c
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> a ~> Dual (b ** c)
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Fls) -> a ~> Dual (b ** c)
Booleans 'TRU 'TRU
Tru
    (Booleans a a
_, Booleans b b
Tru) -> a ~> Dual (b ** c)
(a ** b) ~> Dual c
f
  linDistInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @b @c a ~> Dual (b ** c)
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c) of
    (Booleans b b
Fls, Booleans c c
Fls) -> (a ** b) ~> Dual c
Booleans 'FLS 'TRU
F2T
    (Booleans b b
Fls, Booleans c c
Tru) -> (a ** b) ~> Dual c
Booleans 'FLS 'FLS
Fls
    (Booleans b b
Tru, Booleans c c
_) -> a ~> Dual (b ** c)
(a ** b) ~> Dual c
f

-- BOOL is not CompactClosed

instance HasParamNNO BOOL where
  type NNO = TRU
  zero :: Unit ~> NNO
zero = Unit ~> NNO
Booleans 'TRU 'TRU
Tru
  succ :: NNO ~> NNO
succ = NNO ~> NNO
Booleans 'TRU 'TRU
Tru
  nnoUniv :: forall (a :: BOOL) (x :: BOOL).
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv a ~> x
z x ~> x
_ = a ~> x
(a ** NNO) ~> x
z

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 (Ob a) => Comonoid (a :: BOOL) where
  counit :: a ~> Unit
counit = 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 ~> Unit
Booleans 'FLS 'TRU
F2T
    Obj a
Booleans a a
Tru -> a ~> Unit
Booleans 'TRU 'TRU
Tru
  comult :: a ~> (a ** a)
comult = 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 ~> (a ** a)
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> a ~> (a ** a)
Booleans 'TRU 'TRU
Tru

instance CopyDiscard BOOL

type NonTrivialProfunctor :: (BOOL, BOOL) -> BOOL +-> BOOL
data NonTrivialProfunctor ft a b where
  FF :: NonTrivialProfunctor '(TRU, tt) FLS FLS
  FT :: NonTrivialProfunctor ft FLS TRU
  TT :: NonTrivialProfunctor '(ff, TRU) TRU TRU

deriving instance P.Eq (NonTrivialProfunctor ft a b)
deriving instance P.Show (NonTrivialProfunctor ft a b)

-- | There are 4 non-trivial profunctors BOOL +-> BOOL, all with FLS->TRU, and optionally FLS->FLS and TRU->TRU.
instance Profunctor (NonTrivialProfunctor ft) where
  dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL).
(c ~> a)
-> (b ~> d)
-> NonTrivialProfunctor ft a b
-> NonTrivialProfunctor ft c d
dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
FF = NonTrivialProfunctor ft c d
NonTrivialProfunctor '( 'TRU, tt) 'FLS 'FLS
forall (ff :: BOOL). NonTrivialProfunctor '( 'TRU, ff) 'FLS 'FLS
FF
  dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
FF = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
Fls b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
FT = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
TT = NonTrivialProfunctor ft c d
NonTrivialProfunctor ft 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
Tru NonTrivialProfunctor ft a b
TT = NonTrivialProfunctor ft c d
NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
forall (ff :: BOOL). NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
TT
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
Fls NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
Tru b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  dimap c ~> a
Booleans c a
F2T b ~> d
Booleans b d
F2T NonTrivialProfunctor ft a b
x = case NonTrivialProfunctor ft a b
x of {}
  (Ob a, Ob b) => r
r \\ :: forall (a :: BOOL) (b :: BOOL) r.
((Ob a, Ob b) => r) -> NonTrivialProfunctor ft a b -> r
\\ NonTrivialProfunctor ft a b
FF = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ NonTrivialProfunctor ft a b
FT = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ NonTrivialProfunctor ft a b
TT = r
(Ob a, Ob b) => r
r

-- | The arrow category of @k@ as functor category from @2@ to @k@.
type ARROW k = FUN BOOL k

commSquare
  :: forall {k} f g a b c d
   . (a ~ f % FLS, b ~ f % TRU, c ~ g % FLS, d ~ g % TRU) => SUB f ~> (SUB g :: ARROW k) -> (a ~> b, b ~> d, a ~> c, c ~> d)
commSquare :: forall {k} (f :: BOOL +-> k) (g :: BOOL +-> k) (a :: k) (b :: k)
       (c :: k) (d :: k).
(a ~ (f % 'FLS), b ~ (f % 'TRU), c ~ (g % 'FLS), d ~ (g % 'TRU)) =>
(SUB f ~> SUB g) -> (a ~> b, b ~> d, a ~> c, c ~> d)
commSquare SUB f ~> SUB g
n = (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: BOOL +-> k) (a :: BOOL) (b :: BOOL).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f 'FLS ~> 'TRU
Booleans 'FLS 'TRU
F2T, SUB f ~> SUB g
n (SUB f ~> SUB g)
-> ('TRU ~> 'TRU)
-> (UN SUB (SUB f) % 'TRU) ~> (UN SUB (SUB g) % 'TRU)
forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
! 'TRU ~> 'TRU
Booleans 'TRU 'TRU
Tru, SUB f ~> SUB g
n (SUB f ~> SUB g)
-> ('FLS ~> 'FLS)
-> (UN SUB (SUB f) % 'FLS) ~> (UN SUB (SUB g) % 'FLS)
forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
! 'FLS ~> 'FLS
Booleans 'FLS 'FLS
Fls, forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: BOOL +-> k) (a :: BOOL) (b :: BOOL).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g 'FLS ~> 'TRU
Booleans 'FLS 'TRU
F2T) ((Ob (SUB f), Ob (SUB g)) => (a ~> b, b ~> d, a ~> c, c ~> d))
-> Sub Prof (SUB f) (SUB g) -> (a ~> b, b ~> d, a ~> c, c ~> d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: SUBCAT Representable) (b :: SUBCAT Representable) r.
((Ob a, Ob b) => r) -> Sub Prof a b -> r
\\ SUB f ~> SUB g
Sub Prof (SUB f) (SUB g)
n