content: {-# 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 Fls   = Fls
    src F2T   = Fls
    src Tru   = Tru
  
    tgt Fls   = Fls
    tgt F2T   = Tru
    tgt Tru   = Tru
  
    Fls . Fls = Fls
    F2T . Fls = F2T
    Tru . F2T = F2T
    Tru . Tru = Tru
  
  
  -- | False is the initial object in the Boolean category.
  instance HasInitialObject Boolean where
    type InitialObject Boolean = Fls
    initialObject = Fls
    initialize Fls = Fls
    initialize Tru = F2T
  
  -- | True is the terminal object in the Boolean category.
  instance HasTerminalObject Boolean where
    type TerminalObject Boolean = Tru
    terminalObject = Tru
    terminate Fls = F2T
    terminate 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 Fls Fls = Fls
    proj1 Fls Tru = Fls
    proj1 Tru Fls = F2T
    proj1 Tru Tru = Tru
    proj2 Fls Fls = Fls
    proj2 Fls Tru = F2T
    proj2 Tru Fls = Fls
    proj2 Tru Tru = Tru
  
    Fls &&& Fls = Fls
    Fls &&& F2T = Fls
    F2T &&& Fls = Fls
    F2T &&& F2T = F2T
    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 Fls Fls = Fls
    inj1 Fls Tru = F2T
    inj1 Tru Fls = Tru
    inj1 Tru Tru = Tru
    inj2 Fls Fls = Fls
    inj2 Fls Tru = Tru
    inj2 Tru Fls = F2T
    inj2 Tru Tru = Tru
  
    Fls ||| Fls = Fls
    F2T ||| F2T = F2T
    F2T ||| Tru = Tru
    Tru ||| F2T = Tru
    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 Fls Fls = Fls
    apply Fls Tru = F2T
    apply Tru Fls = Fls
    apply Tru Tru = Tru
  
    tuple Fls Fls = F2T
    tuple Fls Tru = Tru
    tuple Tru Fls = Fls
    tuple Tru Tru = Tru
  
    Fls ^^^ Fls = Tru
    Fls ^^^ F2T = F2T
    Fls ^^^ Tru = Fls
    F2T ^^^ Fls = Tru
    F2T ^^^ F2T = F2T
    F2T ^^^ Tru = F2T
    Tru ^^^ Fls = Tru
    Tru ^^^ F2T = Tru
    Tru ^^^ Tru = Tru
  
  
  trueProductMonoid :: MonoidObject (ProductFunctor Boolean) Tru
  trueProductMonoid = MonoidObject Tru Tru
  
  falseCoproductComonoid :: ComonoidObject (CoproductFunctor Boolean) Fls
  falseCoproductComonoid = ComonoidObject Fls Fls
  
  trueProductComonoid :: ComonoidObject (ProductFunctor Boolean) Tru
  trueProductComonoid = ComonoidObject Tru Tru
  
  falseCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Fls
  falseCoproductMonoid = MonoidObject Fls Fls
  
  trueCoproductMonoid :: MonoidObject (CoproductFunctor Boolean) Tru
  trueCoproductMonoid = MonoidObject F2T Tru
  
  falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls
  falseProductComonoid = ComonoidObject F2T 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 f % Fls = src f
    Arrow f % F2T = f
    Arrow f % Tru = tgt 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 (Nat f _ _) = Nat (Const (f % Fls)) f (\case Fls -> f % Fls; Tru -> f % F2T)
    limitFactorizer n = n ! 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 (Nat f _ _) = Nat f (Const (f % Tru)) (\case Fls -> f % F2T; Tru -> f % Tru)
    colimitFactorizer n = n ! 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 % f = Nat (Arrow (terminate (src f))) (Arrow (terminate (tgt f))) (\case Fls -> f; Tru -> terminalObject)
  
  -- | @Terminator@ is right adjoint to the source functor.
  terminatorLimitAdj :: HasTerminalObject k => Adjunction k (Nat Boolean k) (SrcFunctor k) (Terminator k)
  terminatorLimitAdj = mkAdjunctionInit LimitFunctor Terminator
    (\(Nat b _ _) -> Nat b (Arrow (terminate (b % Fls))) (\case Fls -> b % Fls; Tru -> terminate (b % Tru)))
    (\_ n -> n ! 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 % f = Nat (Arrow (initialize (src f))) (Arrow (initialize (tgt f))) (\case Fls -> initialObject; Tru -> f)
  
  -- | @Initializer@ is left adjoint to the target functor.
  initializerColimitAdj :: HasInitialObject k => Adjunction (Nat Boolean k) k (Initializer k) (TgtFunctor k)
  initializerColimitAdj = mkAdjunctionTerm Initializer ColimitFunctor
    (\_ n -> n ! Tru)
    (\(Nat b _ _) -> Nat (Arrow (initialize (b % Tru))) b (\case Fls -> initialize (b % Fls); Tru -> b % Tru))
  