You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Mar 10 2021 at 20:26):Just like asking for two objects to be equal (instead of equivalent) is against the spirit of a modern understanding of category theory, it strikes me that specifying what a Functor should do to objects 'on the nose' is equally un-categorical. Specifically, equality-on-objects functors seem rather odd. It's right up there with asking for a category to be skeletal, or at least so it feels.
To turn this into a constructive query instead of merely an opinion: what would be a more categorical property to ask for?
Nathanael Arkor (Mar 10 2021 at 20:31):One of the most important features of identity-on-objects functors is that they form the left class of a strict orthogonal factorisation system on Cat (with the right class being fully faithful functors). We may weaken the left class to bijective-on-objects functors, and further to essentially surjective functors, to form an orthogonal factorisation system and a 2-categorical factorisation system respectively.
James Wood (Mar 10 2021 at 20:32):It's been a while since I've dealt with identity-on-objects functors, but my guess would be that it is rather a type-preserving mapping of morphisms that preserves identity and composition. That is, the definition of identity-on-object functor does not depend on the definition of functor, but is rather a new concept.
Nathanael Arkor (Mar 10 2021 at 20:35):I think it worth pointing out, though, that there is a point to strictness in category theory: by always demanding everything hold only up to equivalence, one can sometimes miss the point. This often occurs when one wants to relate syntax to categorical structure: in the former everything must necessarily be strict; only after proving a coherence theorem is it valid to relax the strictness of the constructions.
Sam Staton (Mar 10 2021 at 20:36):I think that’s a good point, Nathanael, and matches the way that ioo functors are used in Freyd categories and in Lawvere theories.
Jacques Carette (Mar 10 2021 at 20:50):@Nathanael Arkor That seems to, in part, just move the problem around. For one, factorization systems themselves are problematic because they assume that is a set (class) that can be neatly divided into pieces. But, categorically, subsets are not so nice. So that's not helping... (and was meant to be fodder of a question in the future).
However, the point about relating syntax to categorical structure is indeed relevant. Indeed, as @Sam Staton alludes to, this is how Lawvere theories are usually presented - but not on the nLab where a weaker version is used. I formalized that in Agda instead, but then tried to do the simplest theory, the theory of equality (suitably interpreted) that shows up later down that page and... failed. My current feeling is that I should just bite the bullet and formalize the classical thing with as objects. It still feels like cheating.
Furthermore, I must admit that I rather like Fiore's relatively recent work on bicategorical approaches to the lambda calculus, which goes in the opposite direction of making things strict because of 'syntax'!
I do accept that when dealing with syntax, decidable equality (for example, over the 'set' of variables) is needed. But that's fine, because this is user-facing. Nevertheless, that doesn't mean that everything needs to be a singleton: it is extremely useful to have keyword redundancy ( and ), which CT handles just fine, unless you impose too much strictness.
Nathanael Arkor (Mar 10 2021 at 20:53):Factorisation systems are entirely categorical: for instance, categories with factorisation systems are algebras for a 2-monad on Cat (see Korostenski–Tholen's Factorization systems as Eilenberg–Moore algebras).
Jacques Carette (Mar 10 2021 at 20:55):I was imprecise: I did not mean to imply that factorization systems are not categorical. I meant to say that their usual presentation is not done in a very categorical manner. I've definitely seen enough results around factorization systems to be convinced that they are indeed categorical.
Nathanael Arkor (Mar 10 2021 at 20:56):But then you agree that it doesn't move the problem around?
Nathanael Arkor (Mar 10 2021 at 20:57):My current feeling is that I should just bite the bullet and formalize the classical thing with as objects. It still feels like cheating.
I do not intend for this to come across badly, but you seem to have taken the nLab's tongue-in-cheek use of the word "evil" much more closely to heart than was intended. A Lawvere theory, as traditionally presented, was formulated to be a precise and exact match for the concept of abstract clone in universal algebra. A weaker notion no longer matches the intended definition. So saying that a Lawvere theory is "too strict" entirely overlooks the reason for which Lawvere theories were devised.
Jacques Carette (Mar 10 2021 at 20:58):I will agree in a future where I see a simple yet categorical presentation of them. They are high on list to formalize, but are not yet done, because I am still missing that.
Nathanael Arkor (Mar 10 2021 at 20:58):See the paper I referenced: this is very categorical.
Nathanael Arkor (Mar 10 2021 at 21:01):Furthermore, I must admit that I rather like Fiore's relatively recent work on bicategorical approaches to the lambda calculus, which goes in the opposite direction of making things strict because of 'syntax'!
Note, though, that coherence is treated as an important part of the story for Fiore and coauthors. For instance, see @Philip Saville's thesis Cartesian closed bicategories: type theory and coherence, which is essentially a justification that using weakened structure for bicategorical type theories is valid at all.
James Wood (Mar 10 2021 at 21:03):Have you checked what is done in HoTT? There, they have the strong constraint that a category doesn't necessarily have a set of objects in any canonical way. Also, it's quite common to strictify types – that is, to produce a type equivalent to the original one for which the notion of identity on closed terms is judgemental equality (IIRC with similar motivation to strictification in category theory). This is left as a metatheoretic notion.
Jacques Carette (Mar 10 2021 at 21:03):And it seems that the definition given in section 2.1 of the Korostenski-Tholen paper may indeed satisfy my needs! Wonderful.
Nathanael Arkor (Mar 10 2021 at 21:06):I suppose one question I might ask is: why are you even bothering to formalise a Lawvere theory where you are not concerned with syntax? It's much easier to formalise a cartesian category, which plays essentially the same role.
Jacques Carette (Mar 10 2021 at 21:06):On "evil": I prefer the principle of equivalence as the reasonable, non-tongue-in-cheek version. This appeals to me greatly.
Jacques Carette (Mar 10 2021 at 21:08):Oh, the answer to "why are you bothering to formalize XXX" is always the same simple answer: to learn. I don't know this stuff, and formalizing it forces me to learn it well.
Nathanael Arkor (Mar 10 2021 at 21:11):You may also be interested that identity-on-objects functors are more categorical than might appear at first glance: for instance, monads in the bicategory of profunctors are precisely identity-on-objects functors.
Jacques Carette (Mar 10 2021 at 21:11):My formal math background was very (very) analysis heavy. I loved the stuff. I also spent years doing symbolic computation. But now I'm retooling myself on other topics (type theory, category theory, others), and learning it all on my own. So I have the weirdest holes while at the same time knowing some really advanced material. I'm happy people here are (mostly) patient.
Nathanael Arkor (Mar 10 2021 at 21:12):Jacques Carette said:
Oh, the answer to "why are you bothering to formalize XXX" is always the same simple answer: to learn. I don't know this stuff, and formalizing it forces me to learn it well.
I suppose then the argument to formalising the nLab's definition over the classical definition is that it is more complex, and thus a better learning opportunity?
Jacques Carette (Mar 10 2021 at 21:14):Nathanael Arkor said:
I suppose then the argument to formalising the nLab's definition over the classical definition is that it is more complex, and thus a better learning opportunity?
Actually, no. It's because I "didn't know better", have no guide, and that definition struck me as somehow more sensible. I would be so happy to have a guide on my journey through learning category theory!
Nathanael Arkor (Mar 10 2021 at 21:14):(Let me apologise if I am coming across in any way confrontational: it is just that I have an affection for strict structures in category theory and think syntax is often undervalued.)
Jacques Carette (Mar 10 2021 at 21:15):Nathanael Arkor said:
You may also be interested that identity-on-objects functors are more categorical than might appear at first glance: for instance, monads in the bicategory of profunctors are precisely identity-on-objects functors.
Oh, I need to bookmark that and prove it for myself. That sounds very instructive.
Jacques Carette (Mar 10 2021 at 21:19):I too think that syntax is very under-valued. I have a PhD student defending her thesis on Monday which is 100% about leveraging the power of syntax to do generation lots of math at no human cost. Classical Universal Algebra was really helpful there. It's not that I claim that this is the right way to do things (some people seem to misunderstand that), but rather to show that no one should be wasting their time doing it by hand because it is all automatable. The question of how to achieve it 'well' is left to the future.
On the other hand, I have a strong fondness for weak category theory! :grinning_face_with_smiling_eyes:
Jacques Carette (Mar 10 2021 at 21:22):And, on Lawvere theories: do you have any recommended reading? Preferably something that is fairly explicit about the intent. That seems to be where I went astray.
Nathanael Arkor (Mar 10 2021 at 21:23):Jacques Carette said:
Nathanael Arkor said:
I suppose then the argument to formalising the nLab's definition over the classical definition is that it is more complex, and thus a better learning opportunity?
Actually, no. It's because I "didn't know better", have no guide, and that definition struck me as somehow more sensible. I would be so happy to have a guide on my journey through learning category theory!
I think the nLab page is much in need of some clarification in that respect (that is, how the different definitions relate). I will try to add some comments at some point.
Regarding the difference in this instance: the original definition of Lawvere theory was single-sorted (to match classical universal algebra). However, this was quickly generalised to multisorted theories; upon doing so, it becomes clear that multisorted algebraic theories are essentially the same as cartesian categories, which are "more categorical" and certainly simpler (at the cost of losing the information pertaining to the generating sorts). The definition on the nLab is what one might get if they took multisorted Lawvere theory to mean "cartesian category" and tried to produce a one-sorted definition. It is arguable how much value there is in doing so, because restricting to a single sort is quite a syntactic operation to want to perform (and rarely necessary even then). If one wants to consider models of algebraic structure in a general category, it is much more likely that a cartesian category will be the right abstraction.
Fawzi Hreiki (Mar 10 2021 at 21:24):I think the ‘right way’ to think about Lawvere theories is as just finite product categories, with the sorted versions arising from presentations via sorts, function symbols, and equations
Fawzi Hreiki (Mar 10 2021 at 21:25):So the theories are a priori weak, but the strictness comes in with the syntax
Jacques Carette (Mar 10 2021 at 21:27):In my work, it is extremely important to separate presentation and semantics. [Yes, I am indeed a computer scientist, no longer a mathematician, even though that was my Ph.D.] And I'm definitely working my way up to Cartmell's generalized algebraic theories. I just want to get the basics done right, first.
Just to double check again: "finite product categories" and "cartesian categories" are the same thing, right? Just a different name to emphasize a different structure?
Nathanael Arkor (Mar 10 2021 at 21:29):Jacques Carette said:
And, on Lawvere theories: do you have any recommended reading? Preferably something that is fairly explicit about the intent. That seems to be where I went astray.
To get an appreciation of the structure of Lawvere theories as pertains to syntax (as was their original motivation), I think Chapter 2 of Mahmoud's thesis Second-order algebraic theories is very nicely written, and gives an explicit proof of the equivalence between syntax in the form of presentations and equational logic, and Lawvere theories.
Fawzi Hreiki (Mar 10 2021 at 21:29):Well ‘Cartesian’ sometimes means finite limits so that can be vague
Fawzi Hreiki (Mar 10 2021 at 21:30):I mean categories with finite Cartesian products
Nathanael Arkor (Mar 10 2021 at 21:31):I don't know of a good reference for the precise relationship between Lawvere theories and cartesian categories; as far as I know it is folklore, though some of the story may be found in Pitts's Categorical logic.
Fawzi Hreiki (Mar 10 2021 at 21:33):Well there’s ‘Algebraic Theories’ by Adamek, Rosicky, and Vitale
Fawzi Hreiki (Mar 10 2021 at 21:33):Which is basically the book on Lawvere theories.
Jacques Carette (Mar 10 2021 at 21:34):I've actually read both of those (Mahmoud's thesis and Pitt's article). But merely reading is insufficient to really learn. I own 'Algebraic Theories', which is even less sufficient for learning...
Nathanael Arkor (Mar 10 2021 at 21:34):Fawzi Hreiki said:
Which is basically the book on Lawvere theories.
This is good for one interested in the categorical perspective (i.e. cartesian categories), but not if one is interested in the syntax; which I do not believe they discuss at all..?
Fawzi Hreiki (Mar 10 2021 at 21:35):They discuss syntax in the second half of the book where they define presentations of algebraic theories I believe
Fawzi Hreiki (Mar 10 2021 at 21:35):If by syntax you mean the type calculus of finite products though, then no they don’t deal with that aspect
Fawzi Hreiki (Mar 10 2021 at 21:36):For deduction related stuff, you’re better off with Mike Shulman’s notes on categorical logic
Jacques Carette (Mar 10 2021 at 21:38):Oh, I've read Shulman's catlog notes very attentively! They match my understanding of things very well.
Nathanael Arkor (Mar 10 2021 at 21:43):One last point about the strictness of Lawvere theories: it is by virtue of the fact that you specify the generating sorts that you can get the correspondence between Lawvere theories and monads on powers of Set.
Nathanael Arkor (Mar 10 2021 at 21:43):(This is related to the point earlier that monads in Prof are identity-on-objects functors. Martin Hyland has some good notes on this topic.)
Jacques Carette (Mar 10 2021 at 21:46):Much material for me to (re)read, thank you. I had too many things saved up in my 'theories' bucket, having a short list helps.
I'll have to see how much of this generalizes when Set is replaced with Setoid. [The vast majority of category theory does.]
Nathanael Arkor (Mar 10 2021 at 21:48):I'll have to see how much of this generalizes when Set is replaced with Setoid.
If this means moving to the Setoid-enriched setting, everything does indeed generalise without too much fuss (and I imagine won't lead to any surprises after the Set-enriched setting is understood). But that says nothing about ease of formalisation :)
Jacques Carette (Mar 10 2021 at 21:50):Yes, that's what this means. Once the definitions are down correctly, slogging through the proofs is generally not bad. The types guide you a lot. Tedious, sure.
Mike Shulman (Mar 10 2021 at 23:59):FWIW, I think usually a definition involving an identity-on-objects functor (or other structure violating the principle of equivalence) should usually be regarded not as structure on a previously given collection of categories but as a definition of a different, sui generis categorical structure. For instance, a dagger-category can be defined as a category with an identity-on-objects contravariant involution, but it's better to think of it as a new kind of categorical structure that happens to have an underlying category rather than as a "dagger-structure" on a previously given category. Same with Freyd-categories, etc.
Mike Shulman (Mar 11 2021 at 00:00):Similarly, the definition of a Grothendieck fibration involves an equality of objects when defining cartesian lifts, so from an equivalence-principle point of view it's better to think of "a fibration over B" as a sui generis thing (or an instance of something a bit more general, like a "displayed category") rather than as a property of a functor with codomain B.
Mike Shulman (Mar 11 2021 at 00:02):When working in a set-theoretic formal system, of course, one can in fact define these structures in the traditional way using functors that have the property of being identity-on-objects and so on. But "morally" it's better to think of them as sui generis structures, and when formalizing things in HoTT you're forced to that point of view. In https://arxiv.org/abs/2102.06275 we tried to lay out a general approach to such dependently typed categorical structures inspired by Makkai's FOLDS; see particularly the examples in chapters 12 and 13.
Jacques Carette (Mar 11 2021 at 00:04):That's exactly the kind of answer I was hoping for, thank you. For dagger category, that makes sense.
So identity-on-object functors, from that perspective, are 'other' things, which can be proven post-facto to be functors?
Jacques Carette (Mar 11 2021 at 01:11):I've tried to read the paper you linked... It would require serious study on my part to be able to understand those examples.
Mike Shulman (Mar 11 2021 at 01:15):Yeah.
Jacques Carette (Mar 11 2021 at 01:20):I don't know if you can read Adga, but if you could verify that our definition of (Grothendieck) Fibration is correct, I'd certainly appreciate it!
Jade Master (Mar 11 2021 at 04:02):I think that identity morphisms in general should be excluded from "evilness". Identity morphisms are a an essential part of every category which are necessary for defining equivalences in the first place. Identity on object functors aren't identity morphisms but their object components are.
Sam Staton (Mar 11 2021 at 09:38):I've included the id-on-objs definition of Lawvere theory on the nlab page. Happy to be overridden. I almost made the id-on-objs definition the "A" definition, which is what it is in my head, but I didn't have the guts (so to speak). I also noticed that Mike wrote a similar explanation about id-on-objs back in 2017.
Fawzi Hreiki (Mar 11 2021 at 09:59):Obviously the two definitions are equivalent in the traditional case, but the B definition generalises better to the enriched case
Sam Staton (Mar 11 2021 at 10:11):I think it depends what you mean by "equivalent"; personally I don't think they're equivalent definitions. I expect both definitions can be enriched, but I agree that B is the more usual one to start from.
Mike Shulman (Mar 11 2021 at 14:15):@Jade Master The point is that if you have two given categories, saying that there is an io functor between them is not an equivalence-invariant statement.
Jade Master (Mar 11 2021 at 14:22):@Mike Shulman Okay that's true. I see what you mean. Why would you want it to be equivalence invariant in this case? Having an object component which is the identity seems very nice to me already.
Jade Master (Mar 11 2021 at 14:27):I suppose that having things be equivalence invariant is in general a good thing I get that.
Jade Master (Mar 11 2021 at 14:30):But yeah there are some things which just aren't equivalent invariant but are nevertheless the best definition for something? And your idea is that were just using the wrong type of equivalence for these things?
Fawzi Hreiki (Mar 11 2021 at 14:30):I guess that's the interesting thing about the interaction between type theory (which strives to be as strict as possible) and category theory (which strives to be as weak as possible)
Fawzi Hreiki (Mar 11 2021 at 14:31):I think one of the reasons why things should be formulated as weak as possible is to not mistakenly use a fact or property which is not invariant under equivalence.
Jacques Carette (Mar 11 2021 at 14:33):That's why I like @Mike Shulman 's idea of an ioo functor as a sui generis structure which induces a functor rather then being a functor. That fixes all the issues in one go.
Jade Master (Mar 11 2021 at 14:37):Does this fix it by introducing a new type of equivalence?
Morgan Rogers (he/him) (Mar 11 2021 at 15:04):Jade Master said:
Does this fix it by introducing a new type of equivalence?
I presume it does as follows: given an equivalent base category, you have sufficient data to define an identity on objects functor over it.
Nick Hu (Mar 11 2021 at 15:26):Nathanael Arkor said:
(This is related to the point earlier that monads in Prof are identity-on-objects functors. Martin Hyland has some good notes on this topic.)
Won't this only be true up to a Cauchy completeness assumption?
Mike Shulman (Mar 11 2021 at 15:34):Jacques Carette said:
I don't know if you can read Adga, but if you could verify that our definition of (Grothendieck) Fibration is correct, I'd certainly appreciate it!
It looks like you are defining the weakened notion of Street fibration, which is equivalence-invariant.
Mike Shulman (Mar 11 2021 at 15:35):Nick Hu said:
Nathanael Arkor said:
(This is related to the point earlier that monads in Prof are identity-on-objects functors. Martin Hyland has some good notes on this topic.)
Won't this only be true up to a Cauchy completeness assumption?
Nope. Cauchy completeness is necessary to identify left adjoint profunctors with functors, but that's not how this result goes.
Jacques Carette (Mar 11 2021 at 15:36):Mike Shulman said:
It looks like you are defining the weakened notion of Street fibration, which is equivalence-invariant.
In which case, we should fix our documentation to say that clearly.
Jacques Carette (Mar 11 2021 at 15:37):Thanks.
Mike Shulman (Mar 11 2021 at 15:40):Jade Master said:
Mike Shulman Okay that's true. I see what you mean. Why would you want it to be equivalence invariant in this case? Having an object component which is the identity seems very nice to me already.
There's an argument that anything we say about "a category" should be invariant under equivalence of that category, just like anything we say about "a group" should be invariant under isomorphism. You would look at someone strangely if they said something like "Definition: a group G is splanzy if it contains the number 24", since that's not an isomorphism-invariant property. (Of course, it makes sense to talk about whether a subgroup of contains 24.) Similarly, you should look at someone strangely if they say "A category is plitzy if it contains exactly 53 objects," since that's not invariant under equivalence.
Mike Shulman (Mar 11 2021 at 15:40):When doing mathematics in HoTT this is actually necessary, because equivalent categories are actually equal to each other, and anything we say about one of them can always be transported to another one.
Nathanael Arkor (Mar 11 2021 at 15:42):(Hence Voevodsky's renaming of "contextual categories" to "C-systems".)
Mike Shulman (Mar 11 2021 at 15:42):But it is true that having an identity-on-objects component is nice, and we can use such definitions even in HoTT. It's just that we can't express it as two given categories together with a functor between them that has the "property" of being identity-on-objects. Rather, we say "there's a single type of objects equipped with two different families of hom-sets forming categories and a map between them that preserves composition and identities". Then we observe afterwards that from these data we can extract two categories and a functor between them.
Mike Shulman (Mar 11 2021 at 15:44):Nathanael Arkor said:
(Hence Voevodsky's renaming of "contextual categories" to "C-systems".)
I'm actually not sold on that reasoning for that. I think of a contextual category as a dependently typed analogue of a multicategory, and multicategories are really category-like things, defined up to equivalence and forming a 2-category and not just a 1-category. But I haven't tried to see whether that can be made precise.
Nathanael Arkor (Mar 11 2021 at 15:52):I would be interested to see if that could be made precise.
Jacques Carette (Mar 11 2021 at 16:08):Meta comment: I was apprehensive about asking this question, originally. Now I'm quite glad that I did.
Mike Shulman (Mar 12 2021 at 13:17):After a bit of thought, it seems to me that you can just take a 2-cell of contextual categories to be an ordinary natural transformation between their underlying categories. Since it's natural on the projection maps and the functors preserve the specified pullbacks, this means a transformation between the values of each "type in context", lying over the transformation between the contexts themselves induced by the components of its constituent types, which is stable under weakening.
Mike Shulman (Mar 12 2021 at 13:18):For instance, any multi-sorted Lawvere theory (i.e. cartesian strict monoidal category whose monoid of objects is free) is a contextual category, and this yields the correct notion of 2-cells between them, which is equivalently the notion of 2-cell for cartesian multicategories.
Jacques Carette (Mar 12 2021 at 14:09):Can you make more explicit which aspect of this thread your current comments apply to? I must admit I'm very confused about the 'fit'.
Nathanael Arkor (Mar 12 2021 at 14:13):Mike Shulman said:
Nathanael Arkor said:
(Hence Voevodsky's renaming of "contextual categories" to "C-systems".)
I'm actually not sold on that reasoning for that. I think of a contextual category as a dependently typed analogue of a multicategory, and multicategories are really category-like things, defined up to equivalence and forming a 2-category and not just a 1-category. But I haven't tried to see whether that can be made precise.
Mike's following up on his earlier comment.
Steve Awodey (Mar 12 2021 at 17:43):that's what Colin Z. does for 2-cells between maps of natural models, which generalize contextual categories. They are just 2-cells of the underlying functors.
Mike Shulman (Mar 12 2021 at 22:49):Ah thanks, Steve, I had forgotten that, but now you mention it I remember.