{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, LambdaCase, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Boolean
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- /2/, or the Boolean category.
-- It contains 2 objects, one for true and one for false.
-- It contains 3 arrows, 2 identity arrows and one from false to true.
-----------------------------------------------------------------------------
module Data.Category.Boolean where

import Data.Category
import Data.Category.Limit
import Data.Category.Monoidal
import Data.Category.CartesianClosed

import Data.Category.Functor
import Data.Category.NaturalTransformation


data Fls
data Tru

data Boolean a b where
  Fls :: Boolean Fls Fls
  F2T :: Boolean Fls Tru
  Tru :: Boolean Tru Tru

-- | @Boolean@ is the category with true and false as objects, and an arrow from false to true.
instance Category Boolean where

  src :: Boolean a b -> Obj Boolean a
src Boolean a b
Fls   = Obj Boolean a
Boolean Fls Fls
Fls
  src Boolean a b
F2T   = Obj Boolean a
Boolean Fls Fls
Fls
  src Boolean a b
Tru   = Obj Boolean a
Boolean Tru Tru
Tru

  tgt :: Boolean a b -> Obj Boolean b
tgt Boolean a b
Fls   = Obj Boolean b
Boolean Fls Fls
Fls
  tgt Boolean a b
F2T   = Obj Boolean b
Boolean Tru Tru
Tru
  tgt Boolean a b
Tru   = Obj Boolean b
Boolean Tru Tru
Tru

  Boolean b c
Fls . :: Boolean b c -> Boolean a b -> Boolean a c
. Boolean a b
Fls = Boolean a c
Boolean Fls Fls
Fls
  Boolean b c
F2T . Boolean a b
Fls = Boolean a c
Boolean Fls Tru
F2T
  Boolean b c
Tru . Boolean a b
F2T = Boolean a c
Boolean Fls Tru
F2T
  Boolean b c
Tru . Boolean a b
Tru = Boolean a c
Boolean Tru Tru
Tru


-- | False is the initial object in the Boolean category.
instance HasInitialObject Boolean where
  type InitialObject Boolean = Fls
  initialObject :: Obj Boolean (InitialObject Boolean)
initialObject = Obj Boolean (InitialObject Boolean)
Boolean Fls Fls
Fls
  initialize :: Obj Boolean a -> Boolean (InitialObject Boolean) a
initialize Obj Boolean a
Fls = Boolean (InitialObject Boolean) a
Boolean Fls Fls
Fls
  initialize Obj Boolean a
Tru = Boolean (InitialObject Boolean) a
Boolean Fls Tru
F2T

-- | True is the terminal object in the Boolean category.
instance HasTerminalObject Boolean where
  type TerminalObject Boolean = Tru
  terminalObject :: Obj Boolean (TerminalObject Boolean)
terminalObject = Obj Boolean (TerminalObject Boolean)
Boolean Tru Tru
Tru
  terminate :: Obj Boolean a -> Boolean a (TerminalObject Boolean)
terminate Obj Boolean a
Fls = Boolean a (TerminalObject Boolean)
Boolean Fls Tru
F2T
  terminate Obj Boolean a
Tru = Boolean a (TerminalObject Boolean)
Boolean Tru Tru
Tru


-- | Conjunction is the binary product in the Boolean category.
instance HasBinaryProducts Boolean where

  type BinaryProduct Boolean Fls Fls = Fls
  type BinaryProduct Boolean Fls Tru = Fls
  type BinaryProduct Boolean Tru Fls = Fls
  type BinaryProduct Boolean Tru Tru = Tru

  proj1 :: Obj Boolean x
-> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) x
proj1 Obj Boolean x
Fls Obj Boolean y
Fls = Boolean (BinaryProduct Boolean x y) x
Boolean Fls Fls
Fls
  proj1 Obj Boolean x
Fls Obj Boolean y
Tru = Boolean (BinaryProduct Boolean x y) x
Boolean Fls Fls
Fls
  proj1 Obj Boolean x
Tru Obj Boolean y
Fls = Boolean (BinaryProduct Boolean x y) x
Boolean Fls Tru
F2T
  proj1 Obj Boolean x
Tru Obj Boolean y
Tru = Boolean (BinaryProduct Boolean x y) x
Boolean Tru Tru
Tru
  proj2 :: Obj Boolean x
-> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) y
proj2 Obj Boolean x
Fls Obj Boolean y
Fls = Boolean (BinaryProduct Boolean x y) y
Boolean Fls Fls
Fls
  proj2 Obj Boolean x
Fls Obj Boolean y
Tru = Boolean (BinaryProduct Boolean x y) y
Boolean Fls Tru
F2T
  proj2 Obj Boolean x
Tru Obj Boolean y
Fls = Boolean (BinaryProduct Boolean x y) y
Boolean Fls Fls
Fls
  proj2 Obj Boolean x
Tru Obj Boolean y
Tru = Boolean (BinaryProduct Boolean x y) y
Boolean Tru Tru
Tru

  Boolean a x
Fls &&& :: Boolean a x -> Boolean a y -> Boolean a (BinaryProduct Boolean x y)
&&& Boolean a y
Fls = Boolean a (BinaryProduct Boolean x y)
Boolean Fls Fls
Fls
  Boolean a x
Fls &&& Boolean a y
F2T = Boolean a (BinaryProduct Boolean x y)
Boolean Fls Fls
Fls
  Boolean a x
F2T &&& Boolean a y
Fls = Boolean a (BinaryProduct Boolean x y)
Boolean Fls Fls
Fls
  Boolean a x
F2T &&& Boolean a y
F2T = Boolean a (BinaryProduct Boolean x y)
Boolean Fls Tru
F2T
  Boolean a x
Tru &&& Boolean a y
Tru = Boolean a (BinaryProduct Boolean x y)
Boolean Tru Tru
Tru


-- | Disjunction is the binary coproduct in the Boolean category.
instance HasBinaryCoproducts Boolean where

  type BinaryCoproduct Boolean Fls Fls = Fls
  type BinaryCoproduct Boolean Fls Tru = Tru
  type BinaryCoproduct Boolean Tru Fls = Tru
  type BinaryCoproduct Boolean Tru Tru = Tru

  inj1 :: Obj Boolean x
-> Obj Boolean y -> Boolean x (BinaryCoproduct Boolean x y)
inj1 Obj Boolean x
Fls Obj Boolean y
Fls = Boolean x (BinaryCoproduct Boolean x y)
Boolean Fls Fls
Fls
  inj1 Obj Boolean x
Fls Obj Boolean y
Tru = Boolean x (BinaryCoproduct Boolean x y)
Boolean Fls Tru
F2T
  inj1 Obj Boolean x
Tru Obj Boolean y
Fls = Boolean x (BinaryCoproduct Boolean x y)
Boolean Tru Tru
Tru
  inj1 Obj Boolean x
Tru Obj Boolean y
Tru = Boolean x (BinaryCoproduct Boolean x y)
Boolean Tru Tru
Tru
  inj2 :: Obj Boolean x
-> Obj Boolean y -> Boolean y (BinaryCoproduct Boolean x y)
inj2 Obj Boolean x
Fls Obj Boolean y
Fls = Boolean y (BinaryCoproduct Boolean x y)
Boolean Fls Fls
Fls
  inj2 Obj Boolean x
Fls Obj Boolean y
Tru = Boolean y (BinaryCoproduct Boolean x y)
Boolean Tru Tru
Tru
  inj2 Obj Boolean x
Tru Obj Boolean y
Fls = Boolean y (BinaryCoproduct Boolean x y)
Boolean Fls Tru
F2T
  inj2 Obj Boolean x
Tru Obj Boolean y
Tru = Boolean y (BinaryCoproduct Boolean x y)
Boolean Tru Tru
Tru

  Boolean x a
Fls ||| :: Boolean x a
-> Boolean y a -> Boolean (BinaryCoproduct Boolean x y) a
||| Boolean y a
Fls = Boolean (BinaryCoproduct Boolean x y) a
Boolean Fls Fls
Fls
  Boolean x a
F2T ||| Boolean y a
F2T = Boolean (BinaryCoproduct Boolean x y) a
Boolean Fls Tru
F2T
  Boolean x a
F2T ||| Boolean y a
Tru = Boolean (BinaryCoproduct Boolean x y) a
Boolean Tru Tru
Tru
  Boolean x a
Tru ||| Boolean y a
F2T = Boolean (BinaryCoproduct Boolean x y) a
Boolean Tru Tru
Tru
  Boolean x a
Tru ||| Boolean y a
Tru = Boolean (BinaryCoproduct Boolean x y) a
Boolean Tru Tru
Tru


-- | Implication makes the Boolean category cartesian closed.
instance CartesianClosed Boolean where

  type Exponential Boolean Fls Fls = Tru
  type Exponential Boolean Fls Tru = Tru
  type Exponential Boolean Tru Fls = Fls
  type Exponential Boolean Tru Tru = Tru

  apply :: Obj Boolean y
-> Obj Boolean z
-> Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
apply Obj Boolean y
Fls Obj Boolean z
Fls = Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
Boolean Fls Fls
Fls
  apply Obj Boolean y
Fls Obj Boolean z
Tru = Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
Boolean Fls Tru
F2T
  apply Obj Boolean y
Tru Obj Boolean z
Fls = Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
Boolean Fls Fls
Fls
  apply Obj Boolean y
Tru Obj Boolean z
Tru = Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
Boolean Tru Tru
Tru

  tuple :: Obj Boolean y
-> Obj Boolean z
-> Boolean z (Exponential Boolean y (BinaryProduct Boolean z y))
tuple Obj Boolean y
Fls Obj Boolean z
Fls = Boolean z (Exponential Boolean y (BinaryProduct Boolean z y))
Boolean Fls Tru
F2T
  tuple Obj Boolean y
Fls Obj Boolean z
Tru = Boolean z (Exponential Boolean y (BinaryProduct Boolean z y))
Boolean Tru Tru
Tru
  tuple Obj Boolean y
Tru Obj Boolean z
Fls = Boolean z (Exponential Boolean y (BinaryProduct Boolean z y))
Boolean Fls Fls
Fls
  tuple Obj Boolean y
Tru Obj Boolean z
Tru = Boolean z (Exponential Boolean y (BinaryProduct Boolean z y))
Boolean Tru Tru
Tru

  Boolean z1 z2
Fls ^^^ :: Boolean z1 z2
-> Boolean y2 y1
-> Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
^^^ Boolean y2 y1
Fls = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Tru Tru
Tru
  Boolean z1 z2
Fls ^^^ Boolean y2 y1
F2T = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Fls Tru
F2T
  Boolean z1 z2
Fls ^^^ Boolean y2 y1
Tru = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Fls Fls
Fls
  Boolean z1 z2
F2T ^^^ Boolean y2 y1
Fls = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Tru Tru
Tru
  Boolean z1 z2
F2T ^^^ Boolean y2 y1
F2T = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Fls Tru
F2T
  Boolean z1 z2
F2T ^^^ Boolean y2 y1
Tru = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Fls Tru
F2T
  Boolean z1 z2
Tru ^^^ Boolean y2 y1
Fls = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Tru Tru
Tru
  Boolean z1 z2
Tru ^^^ Boolean y2 y1
F2T = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Tru Tru
Tru
  Boolean z1 z2
Tru ^^^ Boolean y2 y1
Tru = Boolean (Exponential Boolean y1 z1) (Exponential Boolean y2 z2)
Boolean Tru Tru
Tru


trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru
trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru
trueProductMonoid = Cod (ProductFunctor Boolean) (Unit (ProductFunctor Boolean)) Tru
-> Cod
     (ProductFunctor Boolean) (ProductFunctor Boolean :% (Tru, Tru)) Tru
-> MonoidObject (ProductFunctor Boolean) Tru
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject Cod (ProductFunctor Boolean) (Unit (ProductFunctor Boolean)) Tru
Boolean Tru Tru
Tru Cod
  (ProductFunctor Boolean) (ProductFunctor Boolean :% (Tru, Tru)) Tru
Boolean Tru Tru
Tru

falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls
falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls
falseCoproductComonoid = Cod
  (CoproductFunctor Boolean) Fls (Unit (CoproductFunctor Boolean))
-> Cod
     (CoproductFunctor Boolean)
     Fls
     (CoproductFunctor Boolean :% (Fls, Fls))
-> ComonoidObject (CoproductFunctor Boolean) Fls
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject Cod
  (CoproductFunctor Boolean) Fls (Unit (CoproductFunctor Boolean))
Boolean Fls Fls
Fls Cod
  (CoproductFunctor Boolean)
  Fls
  (CoproductFunctor Boolean :% (Fls, Fls))
Boolean Fls Fls
Fls

trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru
trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru
trueProductComonoid = Cod (ProductFunctor Boolean) Tru (Unit (ProductFunctor Boolean))
-> Cod
     (ProductFunctor Boolean) Tru (ProductFunctor Boolean :% (Tru, Tru))
-> ComonoidObject (ProductFunctor Boolean) Tru
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject Cod (ProductFunctor Boolean) Tru (Unit (ProductFunctor Boolean))
Boolean Tru Tru
Tru Cod
  (ProductFunctor Boolean) Tru (ProductFunctor Boolean :% (Tru, Tru))
Boolean Tru Tru
Tru

falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls
falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls
falseCoproductMonoid = Cod
  (CoproductFunctor Boolean) (Unit (CoproductFunctor Boolean)) Fls
-> Cod
     (CoproductFunctor Boolean)
     (CoproductFunctor Boolean :% (Fls, Fls))
     Fls
-> MonoidObject (CoproductFunctor Boolean) Fls
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject Cod
  (CoproductFunctor Boolean) (Unit (CoproductFunctor Boolean)) Fls
Boolean Fls Fls
Fls Cod
  (CoproductFunctor Boolean)
  (CoproductFunctor Boolean :% (Fls, Fls))
  Fls
Boolean Fls Fls
Fls

trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru
trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru
trueCoproductMonoid = Cod
  (CoproductFunctor Boolean) (Unit (CoproductFunctor Boolean)) Tru
-> Cod
     (CoproductFunctor Boolean)
     (CoproductFunctor Boolean :% (Tru, Tru))
     Tru
-> MonoidObject (CoproductFunctor Boolean) Tru
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject Cod
  (CoproductFunctor Boolean) (Unit (CoproductFunctor Boolean)) Tru
Boolean Fls Tru
F2T Cod
  (CoproductFunctor Boolean)
  (CoproductFunctor Boolean :% (Tru, Tru))
  Tru
Boolean Tru Tru
Tru

falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
falseProductComonoid = Cod (ProductFunctor Boolean) Fls (Unit (ProductFunctor Boolean))
-> Cod
     (ProductFunctor Boolean) Fls (ProductFunctor Boolean :% (Fls, Fls))
-> ComonoidObject (ProductFunctor Boolean) Fls
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject Cod (ProductFunctor Boolean) Fls (Unit (ProductFunctor Boolean))
Boolean Fls Tru
F2T Cod
  (ProductFunctor Boolean) Fls (ProductFunctor Boolean :% (Fls, Fls))
Boolean Fls Fls
Fls


data Arrow k a b = Arrow (k a b)
-- | Any functor from the Boolean category points to an arrow in its target category.
instance Category k => Functor (Arrow k a b) where
  type Dom (Arrow k a b) = Boolean
  type Cod (Arrow k a b) = k
  type Arrow k a b :% Fls = a
  type Arrow k a b :% Tru = b
  Arrow k a b
f % :: Arrow k a b
-> Dom (Arrow k a b) a b
-> Cod (Arrow k a b) (Arrow k a b :% a) (Arrow k a b :% b)
% Dom (Arrow k a b) a b
Fls = k a b -> Obj k a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k a b
f
  Arrow k a b
f % Dom (Arrow k a b) a b
F2T = k a b
Cod (Arrow k a b) (Arrow k a b :% a) (Arrow k a b :% b)
f
  Arrow k a b
f % Dom (Arrow k a b) a b
Tru = k a b -> Obj k b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
f


type instance LimitFam Boolean k f = f :% Fls
-- | The limit of a functor from the Boolean category is the source of the arrow it points to.
instance Category k => HasLimits Boolean k where
  limit :: Obj (Nat Boolean k) f -> Cone Boolean k f (LimitFam Boolean k f)
limit (Nat f
f f
_ forall z. Obj Boolean z -> Component f f z
_) = Const Boolean k (f :% Fls)
-> f
-> (forall z.
    Obj Boolean z -> Component (Const Boolean k (f :% Fls)) f z)
-> Nat Boolean k (Const Boolean k (f :% Fls)) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k (f :% Fls) -> Const Boolean k (f :% Fls)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f Fls Fls -> Cod f (f :% Fls) (f :% Fls)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Fls Fls
Boolean Fls Fls
Fls)) f
f (\case Obj Boolean z
Fls -> f
f f -> Dom f Fls Fls -> Cod f (f :% Fls) (f :% Fls)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Fls Fls
Boolean Fls Fls
Fls; Obj Boolean z
Tru -> f
f f -> Dom f Fls Tru -> Cod f (f :% Fls) (f :% Tru)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Fls Tru
Boolean Fls Tru
F2T)
  limitFactorizer :: Cone Boolean k f n -> k n (LimitFam Boolean k f)
limitFactorizer Cone Boolean k f n
n = Cone Boolean k f n
n Cone Boolean k f n
-> Boolean Fls Fls -> k (Const Boolean k n :% Fls) (f :% Fls)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Boolean Fls Fls
Fls

type instance ColimitFam Boolean k f = f :% Tru
-- | The colimit of a functor from the Boolean category is the target of the arrow it points to.
instance Category k => HasColimits Boolean k where
  colimit :: Obj (Nat Boolean k) f
-> Cocone Boolean k f (ColimitFam Boolean k f)
colimit (Nat f
f f
_ forall z. Obj Boolean z -> Component f f z
_) = f
-> Const Boolean k (f :% Tru)
-> (forall z.
    Obj Boolean z -> Component f (Const Boolean k (f :% Tru)) z)
-> Nat Boolean k f (Const Boolean k (f :% Tru))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj k (f :% Tru) -> Const Boolean k (f :% Tru)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f Tru Tru -> Cod f (f :% Tru) (f :% Tru)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Tru Tru
Boolean Tru Tru
Tru)) (\case Obj Boolean z
Fls -> f
f f -> Dom f Fls Tru -> Cod f (f :% Fls) (f :% Tru)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Fls Tru
Boolean Fls Tru
F2T; Obj Boolean z
Tru -> f
f f -> Dom f Tru Tru -> Cod f (f :% Tru) (f :% Tru)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f Tru Tru
Boolean Tru Tru
Tru)
  colimitFactorizer :: Cocone Boolean k f n -> k (ColimitFam Boolean k f) n
colimitFactorizer Cocone Boolean k f n
n = Cocone Boolean k f n
n Cocone Boolean k f n
-> Boolean Tru Tru -> k (f :% Tru) (Const Boolean k n :% Tru)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Boolean Tru Tru
Tru