@MartinEscardo this is a definition of categories as monads in the bicategory of spans using some specific choice of construction of pullback in Set, but it is naturally a weak 2-category - so we should state it for pullbacks, but then we can’t even state the associativity law as it is a naturally a dependent equality (unless we use some kind of unbiased pullbacks)
@MartinEscardo "There is no reason to have "evilness" (in the categorical sense, rather than the emotional sense) built-in in the definition of category!"
If you mean that mathematicians could instead adopt a definition of category in dependent type theory where the morphisms are a dependent family a, b : C₀ |- C(a,b), then I would say there is a reason we usually don't do that: ignorance of type theory. Most mathematician know little about foundations, and what little we know is usually phrased in first order logic with equality, not type theory.
@oantolin@MartinEscardo - indeed, most of us needed to learn any definition of category whatsoever - the nuances don't matter so much - before we could be attuned to the nuances of sameness (equality vs. isomorphism, etc.) and understand the problems of "evil", and appreciate why we'd want to avoid a definition of category that mentions equations between objects!
@MartinEscardo@oantolin - I agree that it would be good to give people a nice definition of "category" the first time. But I don't see category theorists unwilling to give different styles of definition a fair chance. Maybe you're referring to non-category-theorists. I'd forgotten about them. 😳 I can easily imagine them sticking to the first definition of category they see, regarding it as sacrosanct.
@johncarlosbaez@MartinEscardo@oantolin so one would start with a class of composable maps, and their compositions, that would make a usable definition, and I guess one could eventually recover the definition of source and target from it.
@antoinechambertloir@MartinEscardo@oantolin - There is a rather elaborate and carefully worked out esthetic of formulating definitions in categorical logic, aimed to ensure that everything works out as smoothly as possible, e.g. that everything you say about a functor is invariant under natural isomorphisms, and everything you say about a category is invariant under equivalence. Equations between objects can easily break these principles so we call them 'evil'; this then pressures us to take an approach where we don't need to check that the source of one morphism equals the target of the next.
A common approach is to make morphisms 'dependently typed', so that for each pair of objects (a,b) you have a set of morphisms hom(a,b). You never talk about the set of all morphisms, so you never mention source and target maps. Composition is not a single partially defined function, but instead a bunch of functions hom(a,b) × hom(b,c) → hom(a,c). So, you never need to check that the source of one morphism equals the target of another: it's impossible to even dream of composing morphisms unless you already know you can do it!
Add comment