{-# 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/ a.k.a. the Boolean category a.k.a. the walking arrow.
-- It contains 2 objects, one for false and one for true.
-- It contains 3 arrows, 2 identity arrows and one from false to true.
-----------------------------------------------------------------------------
module Data.Category.Boolean where

import Data.Kind (Type)

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

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


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 :: forall a b. Boolean a b -> Obj Boolean a
src Boolean a b
Fls   = Boolean Fls Fls
Fls
  src Boolean a b
F2T   = Boolean Fls Fls
Fls
  src Boolean a b
Tru   = Boolean Tru Tru
Tru

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

  Boolean b c
Fls . :: forall b c a. Boolean b c -> Boolean a b -> Boolean a c
. Boolean a b
Fls = Boolean Fls Fls
Fls
  Boolean b c
F2T . Boolean a b
Fls = Boolean Fls Tru
F2T
  Boolean b c
Tru . Boolean a b
F2T = Boolean Fls Tru
F2T
  Boolean b c
Tru . Boolean a b
Tru = 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 = Boolean Fls Fls
Fls
  initialize :: forall a. Obj Boolean a -> Boolean (InitialObject Boolean) a
initialize Boolean a a
Fls = Boolean Fls Fls
Fls
  initialize Boolean a a
Tru = 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 = Boolean Tru Tru
Tru
  terminate :: forall a. Obj Boolean a -> Boolean a (TerminalObject Boolean)
terminate Boolean a a
Fls = Boolean Fls Tru
F2T
  terminate Boolean a a
Tru = 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 :: forall x y.
Obj Boolean x
-> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) x
proj1 Boolean x x
Fls Boolean y y
Fls = Boolean Fls Fls
Fls
  proj1 Boolean x x
Fls Boolean y y
Tru = Boolean Fls Fls
Fls
  proj1 Boolean x x
Tru Boolean y y
Fls = Boolean Fls Tru
F2T
  proj1 Boolean x x
Tru Boolean y y
Tru = Boolean Tru Tru
Tru
  proj2 :: forall x y.
Obj Boolean x
-> Obj Boolean y -> Boolean (BinaryProduct Boolean x y) y
proj2 Boolean x x
Fls Boolean y y
Fls = Boolean Fls Fls
Fls
  proj2 Boolean x x
Fls Boolean y y
Tru = Boolean Fls Tru
F2T
  proj2 Boolean x x
Tru Boolean y y
Fls = Boolean Fls Fls
Fls
  proj2 Boolean x x
Tru Boolean y y
Tru = Boolean Tru Tru
Tru

  Boolean a x
Fls &&& :: forall a x y.
Boolean a x -> Boolean a y -> Boolean a (BinaryProduct Boolean x y)
&&& Boolean a y
Fls = Boolean Fls Fls
Fls
  Boolean a x
Fls &&& Boolean a y
F2T = Boolean Fls Fls
Fls
  Boolean a x
F2T &&& Boolean a y
Fls = Boolean Fls Fls
Fls
  Boolean a x
F2T &&& Boolean a y
F2T = Boolean Fls Tru
F2T
  Boolean a x
Tru &&& Boolean a y
Tru = 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 :: forall x y.
Obj Boolean x
-> Obj Boolean y -> Boolean x (BinaryCoproduct Boolean x y)
inj1 Boolean x x
Fls Boolean y y
Fls = Boolean Fls Fls
Fls
  inj1 Boolean x x
Fls Boolean y y
Tru = Boolean Fls Tru
F2T
  inj1 Boolean x x
Tru Boolean y y
Fls = Boolean Tru Tru
Tru
  inj1 Boolean x x
Tru Boolean y y
Tru = Boolean Tru Tru
Tru
  inj2 :: forall x y.
Obj Boolean x
-> Obj Boolean y -> Boolean y (BinaryCoproduct Boolean x y)
inj2 Boolean x x
Fls Boolean y y
Fls = Boolean Fls Fls
Fls
  inj2 Boolean x x
Fls Boolean y y
Tru = Boolean Tru Tru
Tru
  inj2 Boolean x x
Tru Boolean y y
Fls = Boolean Fls Tru
F2T
  inj2 Boolean x x
Tru Boolean y y
Tru = Boolean Tru Tru
Tru

  Boolean x a
Fls ||| :: forall x a y.
Boolean x a
-> Boolean y a -> Boolean (BinaryCoproduct Boolean x y) a
||| Boolean y a
Fls = Boolean Fls Fls
Fls
  Boolean x a
F2T ||| Boolean y a
F2T = Boolean Fls Tru
F2T
  Boolean x a
F2T ||| Boolean y a
Tru = Boolean Tru Tru
Tru
  Boolean x a
Tru ||| Boolean y a
F2T = Boolean Tru Tru
Tru
  Boolean x a
Tru ||| Boolean y a
Tru = 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 :: forall y z.
Obj Boolean y
-> Obj Boolean z
-> Boolean (BinaryProduct Boolean (Exponential Boolean y z) y) z
apply Boolean y y
Fls Boolean z z
Fls = Boolean Fls Fls
Fls
  apply Boolean y y
Fls Boolean z z
Tru = Boolean Fls Tru
F2T
  apply Boolean y y
Tru Boolean z z
Fls = Boolean Fls Fls
Fls
  apply Boolean y y
Tru Boolean z z
Tru = Boolean Tru Tru
Tru

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

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


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

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

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

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

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

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


newtype 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 % :: forall a b.
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
Boolean a b
Fls = 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
Boolean a b
F2T = k a b
f
  Arrow k a b
f % Dom (Arrow k a b) a b
Boolean a b
Tru = forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k a b
f


-- | 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
  type LimitFam Boolean k f = f :% Fls
  limit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Fls
Fls)) f
f (\case Obj Boolean z
Fls -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Fls
Fls; Obj Boolean z
Tru -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Tru
F2T)
  limitFactorizer :: forall f n. Cone Boolean k f n -> k n (LimitFam Boolean k f)
limitFactorizer Cone Boolean k f n
n = Cone Boolean k f n
n 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

-- | The source functor sends arrows (as functors from the Boolean category) to their source.
type SrcFunctor = LimitFunctor Boolean

-- | 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
  type ColimitFam Boolean k f = f :% Tru
  colimit :: forall f.
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
_) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Tru Tru
Tru)) (\case Obj Boolean z
Fls -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Tru
F2T; Obj Boolean z
Tru -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Tru Tru
Tru)
  colimitFactorizer :: forall f n. Cocone Boolean k f n -> k (ColimitFam Boolean k f) n
colimitFactorizer Cocone Boolean k f n
n = Cocone Boolean k f n
n 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

-- | The target functor sends arrows (as functors from the Boolean category) to their target.
type TgtFunctor = ColimitFunctor Boolean


data Terminator (k :: Type -> Type -> Type) = Terminator
-- | @Terminator k@ is the functor that sends an object to its terminating arrow.
instance HasTerminalObject k => Functor (Terminator k) where
  type Dom (Terminator k) = k
  type Cod (Terminator k) = Nat Boolean k
  type Terminator k :% a = Arrow k a (TerminalObject k)
  Terminator k
Terminator % :: forall a b.
Terminator k
-> Dom (Terminator k) a b
-> Cod (Terminator k) (Terminator k :% a) (Terminator k :% b)
% Dom (Terminator k) a b
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 (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (Terminator k) a b
f))) (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (Terminator k) a b
f))) (\case Obj Boolean z
Fls -> Dom (Terminator k) a b
f; Obj Boolean z
Tru -> forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject)

-- | @Terminator@ is right adjoint to the source functor.
terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)
terminatorLimitAdj :: forall (k :: * -> * -> *).
HasTerminalObject k =>
Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)
terminatorLimitAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit forall (j :: * -> * -> *) (k :: * -> * -> *). LimitFunctor j k
LimitFunctor forall (k :: * -> * -> *). Terminator k
Terminator
  (\(Nat a
b a
_ forall z. Obj Boolean z -> Component a a z
_) -> 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 a
b (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (a
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Fls
Fls))) (\case Obj Boolean z
Fls -> a
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Fls
Fls; Obj Boolean z
Tru -> forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (a
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Tru Tru
Tru)))
  (\Obj k b
_ Nat Boolean k a (Terminator k :% b)
n -> Nat Boolean k a (Terminator k :% b)
n 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)


data Initializer (k :: Type -> Type -> Type) = Initializer
-- | @Initializer k@ is the functor that sends an object to its initializing arrow.
instance HasInitialObject k => Functor (Initializer k) where
  type Dom (Initializer k) = k
  type Cod (Initializer k) = Nat Boolean k
  type Initializer k :% a = Arrow k (InitialObject k) a
  Initializer k
Initializer % :: forall a b.
Initializer k
-> Dom (Initializer k) a b
-> Cod (Initializer k) (Initializer k :% a) (Initializer k :% b)
% Dom (Initializer k) a b
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 (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (Initializer k) a b
f))) (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (Initializer k) a b
f))) (\case Obj Boolean z
Fls -> forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject; Obj Boolean z
Tru -> Dom (Initializer k) a b
f)

-- | @Initializer@ is left adjoint to the target functor.
initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)
initializerColimitAdj :: forall (k :: * -> * -> *).
HasInitialObject k =>
Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)
initializerColimitAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm forall (k :: * -> * -> *). Initializer k
Initializer forall (j :: * -> * -> *) (k :: * -> * -> *). ColimitFunctor j k
ColimitFunctor
  (\Obj k a
_ Nat Boolean k (Initializer k :% a) b
n -> Nat Boolean k (Initializer k :% a) b
n 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)
  (\(Nat b
b b
_ forall z. Obj Boolean z -> Component b b z
_) -> 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 (forall (k :: * -> * -> *) a b. k a b -> Arrow k a b
Arrow (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (b
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Tru Tru
Tru))) b
b (\case Obj Boolean z
Fls -> forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (b
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Fls Fls
Fls); Obj Boolean z
Tru -> b
b forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Boolean Tru Tru
Tru))