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.
True is the terminal object in the Boolean category.
False is the initial object in the Boolean category.
Conjunction is the binary product in the Boolean category.
Disjunction is the binary coproduct in the Boolean category.
Implication makes the Boolean category cartesian closed.
|NatAsFunctor :: (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Nat (Dom f) (Cod f) f g -> NatAsFunctor f g|