{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, LambdaCase, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}
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
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
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
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
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
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
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)
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
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
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