úÎ`$[IV      !"#$%&'()*+,-./0123456789:;<=> ? @ A B C D E F G H I J K L M N O P Q R S T U portable experimentalEdward Kmett <ekmett@gmail.com>CCategory of discrete objects. The only arrows are identity arrows. WDiscrete a b acts as a proof that a = b, lift that proof into something of kind * -> * 5Lower the proof that a ~ b to an arbitrary category. Bnon-portable (either class-associated types or MPTCs with fundeps) experimentalEdward Kmett <ekmett@gmail.com>The  Category (~>)$ has an initial (coterminal) object  Initial (~>) such that for all objects  a in (~>)&, there exists a unique morphism from  Initial (~>)  to a. The  Category (~>) has a terminal object  Terminal (~>) such that for all objects a in (~>), % there exists a unique morphism from a to  Terminal (~>).    portable experimentalEdward Kmett <ekmett@gmail.com> VWX    &non-portable (functional-dependencies) experimentalEdward Kmett <ekmett@gmail.com>    portable experimentalEdward Kmett <ekmett@gmail.com>JA category with a disassociative bifunctor satisyfing the dual of Mac Lane'%s pentagonal coherence identity law: \ bimap disassociate id . disassociate . bimap id disassociate = disassociate . disassociate <A category with an associative bifunctor satisfying Mac Lane'%s pentagonal coherence identity law: M bimap id associate . associate . bimap associate id = associate . associate %non-portable (class-associated types) experimentalEdward Kmett <ekmett@gmail.com>IA comonoidal category satisfies the dual form of the triangle identities  ' first idr = disassociate . second idl ' second idl = disassociate . first idr gThis type class is also (ab)used for the inverse operations needed for a strict (co)monoidal category. 3A strict (co)monoidal category is one that is both  and # and satisfies the following laws:  idr . coidr = id  idl . coidl = id  coidl . idl = id  coidr . idr = id A monoidal category.   and !* are traditionally denoted lambda and rho  the triangle identity holds: % first idr = second idl . associate $ second idl = first idr . associate !"/Denotes that we have some reasonable notion of Identity for a particular  in this Category. This " notion is currently used by both  and  # !"#"# ! ! !"##portable experimentalEdward Kmett <ekmett@gmail.com>$If we have a symmetric (co)Monoidal' category, you get the additional law:  swap . swap = id %rA braided (co)(monoidal or associative) category can commute the arguments of its bi-endofunctor. Obeys the laws:  I associate . braid . associate = second braid . associate . first braid R disassociate . braid . disassociate = first braid . disassociate . second braid CIf the category is Monoidal the following laws should be satisfied   idr . braid = idl  idl . braid = idr FIf the category is Comonoidal the following laws should be satisfied  braid . coidr = coidl  braid . coidl = coidr &'$%&'%&$'$%&&'%non-portable (class-associated types) experimentalEdward Kmett <ekmett@gmail.com>()*+,-./0VNB: This is weaker than traditional category with products! That is Cartesian, below. The problem is (->)D lacks an initial object, since every type is inhabited in Haskell. ]Consequently its coproduct is merely a semigroup, not a monoid (as it has no identity), and Xsince we want to be able to describe its dual category, which has this non-traditional bform being built over a category with an associative bifunctor rather than as a monoidal category for the product monoid. Minimum definition:  fst, snd, diag  fst, snd, (&&&) 123456free construction of  for the product   Product k if (&&&) is known 7free construction of % for the product   Product k / braidProduct :: (PreCartesian k, Product k ~ ( * )) => a  * b ~> b  * a 8free construction of  for the product   Product k ' associateProduct :: (PreCartesian k, ( *) ~ Product k) => (a  * b)  * c ~> (a  * (b  * c)) 9free construction of  for the product   Product k * disassociateProduct:: (PreCartesian k, ( *) ~ Product k) => a  * (b  * c) ~> (a  * b)  * c :free construction of  for the coproduct  Sum k if (|||) is known ;free construction of % for the coproduct  Sum k <free construction of  for the coproduct  Sum k S associateSum :: (PreCoCartesian k, (+) ~ Sum k) => ((a + b) + c) ~> (a + (b + c)) =free construction of  for the coproduct  Sum k V disassociateSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + (b + c)) ~> ((a + b) + c) ()*+,-./0123456789:;<=0123456789)*+,-.:;<=/(()*+,-.*+,-./012345123456789:;<= %non-portable (class-associated types) experimentalEdward Kmett <ekmett@gmail.com>>JA Co-CCC has full-fledged comonoidal finite coproducts and coexponentials ?@ABCA C< has full-fledged monoidal finite products and exponentials DEFGHIJK>?@ABCDEFGHIJKCDEFGHI>?@ABJK>?@AB?@ABCDEFGDEFGHIJK %non-portable (class-associated types) experimentalEdward Kmett <ekmett@gmail.com>LA category in which N is an isomorphism  class ( PreCartesian k  , (*) ~ Product k  , PreCoCartesian k  , (+) ~ Sum k ! ) => Distributive k where MN"The canonical factoring morphism.  factor :: ( PreCartesian k  , (*) ~ Product k  , PreCoCartesian k  , (+) ~ Sum k 4 ) => ((a * b) + (a * c)) `k` (a * (b + c)) LMNNLMLMMN &non-portable (functional-dependencies) experimentalEdward Kmett <ekmett@gmail.com> OPQRSTUYZ[\]^OPQRSTUPQOTURSOPQQRSSTUU_   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGH I J K L M N O P Q R S T U V W X Y Z [ \ ] ] ^ ^_`a b c d e f ghcategories-0.57.0Control.Category.DiscreteControl.Categorical.ObjectControl.Category.DualControl.Categorical.BifunctorControl.Category.AssociativeControl.Category.MonoidalControl.Category.BraidedControl.Category.Cartesian!Control.Category.Cartesian.ClosedControl.Category.DistributiveControl.Categorical.FunctorDiscreteRefl liftDiscretecastinverseHasInitialObjectInitialinitiateHasTerminalObjectTerminal terminateDualrunDual BifunctorbimapQFunctorsecondPFunctorfirst firstDefaultdifirst secondDefaultdimapDisassociative disassociate Associative associate ComonoidalcoidlcoidrMonoidalidlidr HasIdentityId SymmetricBraidedbraidswap CoCartesianPreCoCartesianSuminlinrcodiag||| Cartesian PreCartesianProductfstsnddiag&&& bimapProduct braidProductassociateProductdisassociateProductbimapSumbraidSum associateSumdisassociateSumCoCCCCoexpcoapplycocurry uncocurryCCCExpapplycurryuncurryunitCCC counitCCC unitCoCCC counitCoCCC Distributive distributefactor EndoFunctorFunctorfmapLoweredFunctor LiftedFunctor dataTyCon dualConstr dataDataType liftedTyCon liftedConstrliftedDataType loweredTyCon loweredConstrloweredDataType