Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I removed some spam on category theory.
I copied the “list of theorems” from category theory - contents to a section Theorems at category theory, after seeing this MO event.
That list deserves to be further organized and commented. Maybe somebody feels inspired to do so.
Added the recent
to the references at category theory.
Added what seems to be the original quote by Freyd on “categories were introduced to define natural transformations” to category theory – References – History
(prompted by this MO discussion)
added a pointer to
which Todd had kindly pointed out as a nice enthusiastic lecture. Apparently the speaker mentions the nLab at some point.
It’s perhaps aimed at those who don’t know the first thing about categories. The nLab and its authors are mentioned several times in terms of very high praise.
We should add brief comments to the list of lectures linked to in the entry, indicating roughly what the intended audience is. (Myself, am quasi-offline right now.)
I decided to put LaGatta’s talk under a new heading, Videos. The Catsters have now been entered under that heading as well.
Thanks, Todd!
I have added pointer to Emily Riehl’s “Category theory on context” in the section category theory – References – Basic category theory
Incidentally, might anyone feel inspired to complete the bibliographical information in that section and give that list of references its proper chronological ordering?
added pointer to Fong-Spivak 18:
Did anyone ever prominently try to make the point that, in turn, the main point of natural transformations in category theory is as a way to define… adjunctions?
I think the point of Freyd’s remark for which there is an even more authoritative variant from Mac Lane in CWM (p.18) that Mac Lane and Eilenberg literally formalized the concepts of functor&category to discern natural from unnatural isomorphism. The concept of an adjunction has rather been a late-comer to the show.
The concept of an adjunction has rather been a late-comer to the show.
It seems to have been popularized by Freyd 64. Therefore my question: Has anyone publically tried to make the point that the historical progression of concepts for category theory should really be considered with one further layer added:
| hierarchy of fundamental concepts in category theory |
|---|
| adjunctions |
| natural transformations |
| functors |
| categories |
Mac Lane in Categories for the Working Mathematician (p. 103) has this:
Freyd in his 1960 Princeton thesis (unpublished but widely circulated) and in his book [1964] and Lawvere [1963], [1964] emphasized the dominant position of adjunctions. One must pause to ask if there are other basic general notions still to be discovered.
Hm, Lawvere [1963], [1964]? Not 1969?
I guess [1963] is “Functorial semantics”? Is that so much about adjunctions? What’s Lawvere [1964]?
I don’t know, because I can’t find my copy of Mac Lane. I copied it off Google Books which doesn’t permit a full view.
Actually, I quoted it as Mac Lane publicly making a point which I took to be similar to the one you’re after in #15.
The Triples Seminar at ETH was in 1966/67. By then, I think, Eilenberg-Moore and Kleisli categories and the links with ‘triples’ i.e. monads were clear. I suggest that looking back at the introductions to those seminars may provide some insight. Remember Kan defined adjoint functors in the 1950s. Already when I started learning category theory in about 1968 adjoints were standard fare for elementary courses and the Isle of Thorns conferences were thick with them! I do not remember that Peter Freyd’s book was the source for them as his presentation tended towards the Abelian case. I learnt them mostly from Gavin Wraith and Chris Mulvey.
Don’t forget that Grothendieck introduced adjoint equivalences in Tohoku, and if these are taken to be the fundamental notion rather than generic equivalences (fully faithful+eso, or else non-coherent quasi-inverses) then to properly talk about the principle of equivalence in one needs adjunctions.
Re #17, Lawvere 1964 is ’An elementary theory of the category of sets’. I’ve added that to William Lawvere, and corrected the date at ETCS.
Ah, thanks. Hm, what specifically in Lawvere [1963], [1964] might MacLane have had in mind, in that quote from #16, with respect to “empahsis of the dominant position of adjunctions”?
To take a random guess…
At the very least, the structure of an elementary topos with NNO can be presented by the existence of certain adjunctions: finite limits, colimits, power objects, cartesian closure. Presented in this way, one immediately sees the algebraic nature of the topos axioms, which is even more striking than noticing that they are elementary.
Maybe MacLane really meant that the expert can recognize the secret dominant role of adjunctions, rather than that their role is really emphasized (in the sense of: highlighted explicitly)? I don’t doubt this of course, but for citation purposes it would still be nice to have a better quote. The one by Lawvere from the first paragraph of “Taking categories seriously”, which is more pronouncedly paraphrased in hist first answer in the 2007 interview (here) is fairly good.
Lawvere in his metric spaces paper identifies “generalized logic” with certain systems of adjoint functors. He writes (p.142)
Since logic signifies formal relationships which are general in character, we may more precisely identify logic with this scheme of interlocking adjoints and then observe that all of logic applies directly to structures valued in an arbitrary closed category…
we may more precisely identify logic with this scheme of interlocking adjoints
That’s interesting in light of how LS and LSR adjoint logic express all the basic connectives of all different sorts of logic as (multivariable) adjoints expressible in an appropriate doctrine.
Isn’t Lawvere in that passage from “Metric spaces, generalized logic, and closed categories” referring to the observation of Adjointness in Foundations, regarding systems of adjoint triples given by existential and universal quantification? Where he wrote in 1969 that: “One of the aims of this paper is to give evidence for the universality of the concept of adjointness…?”
And isn’t the base change/quantifier adjunction business precisely that part which is currently missing from those LSx formulations of adjoint logic?
Of course Lawvere’s main point there (p. 142), as the quotation in #25 goes on to say, is that valuable concepts emerge by interpreting the ’scheme of interlocking adjoints’ by varying the associated closed category: truth values, quantities, abstract sets, abelian groups,… Is there any scope for some new ’generalized adjoint logic’?
Is there any scope for some new ’generalized adjoint logic’?
But isn’t that just what hyperdoctrines etc. is about, all the stuff we have been discussing here for years? Maybe I am missing a point.
Regarding adjoint logic: The thought that keeps haunting me is whether, in view of the “dominant” role of adjunctions, it is maybe a serious design flaw of dependent type theory not to make the adjoint triples in dependent sum, context extension and dependent product manifest, say syntactically.
Maybe there should be foundations of mathematics that really is founded on the concept of adjunction. Maybe adjunctions should be a more primitive notion than dependent sum and dependent product in dependent type theory. Maybe there could be a type theory which is adjoint-to-the-roots that would be able to more seamlessly admit implementation of progressions of adjoint modalities as needed for super-differential cohesion.
Urs #27: no, he’s talking about those but also about the connectives as adjoints, e.g. implication, additive disjunction, additive conjunction, and I think he’s also referring to the comprehension scheme (as discussed here; cf. comprehension in a hyperdoctrine) in terms of adjoints, and then generalizing all of this traditional logic by allowing the base category to change, as David was saying.
Anyway, I was trying to give you a more explicit quote re the dominance of adjunctions, which is what I thought you wanted. Lawvere sees all of logic in terms of interlocking systems of adjoints.
And isn’t the base change/quantifier adjunction business precisely that part which is currently missing from those LSx formulations of adjoint logic?
You mean, because the two papers we’ve written so far are only about propositional logic? Yes, of course, the 3-theories involving quantifiers are still work in progress. But the point I was making is that the central role of adjunctions, in general, in logic is front and center.
whether, in view of the “dominant” role of adjunctions, it is maybe a serious design flaw of dependent type theory not to make the adjoint triples in dependent sum, context extension and dependent product manifest
What do you find insufficiently “manifest” about ? And what do you find insufficiently “seamless” about modal dependent type theory?
Re #29, thinking about what I was reaching for in #28, perhaps a good way to express it is that I’m wondering how the kind of enrichment Lawvere discusses in ’Generalized Logic’ interacts with Mike’s latest thinking about ’logic’, the -theories account.
In a nutshell, why the choice of the “canonical” in
The models of an -theory in the -category are the semantic -theories in that -theory?
Say we were dealing with an enriched 2-category of enriched categories. Would we just treat these as models of a (rather complicated) ordinary 2-theory in , or can we think about models of a simpler 2-theory in an enriched 2-category?
Right, better be doing something else, but a brief browse showed me glimpses of the enriched world I’d forgotten about, such as Mike’s Enriched categories as a free cocompletion with its equipments of equipment enriched categories.
I came across myself 5 years ago asking him for something as surprising as Lawvere’s metric spaces. That makes for an example: isn’t the enriched account preferable to casting the theory of generalized metric spaces as having models which are sets with a distance… ?
What do you find insufficiently “manifest” about ?
Hm? What I said is that this adjunction is not manifest in dependent type theory. DTT has a bunch of rules that look nothing like this. After the dust has settled, we recognize that the rules for dependent sum, dependent product and context extension may be understood as an adjoint triple.
It makes me wonder, I said, if maybe there should be a different way to set up DTT, a way where the concept of adjunction is native to the formal language, and primary to dependent sum and dependent product, and where instead and are declared in terms of adjunctions.
The rules for and look to me fairly manifestly like left and right adjoints to weakening respectively. I’m not sure what more you would like to see.
More generally, the perspective of LSR is that all (nonrecursive) type formers are essentially by definition specified as multivariable adjoints.
he’s talking about those but also about the connectives as adjoints, e.g. implication, additive disjunction, additive conjunction
All right, I’d say these are special cases of the other, no?
I was trying to give you a more explicit quote re the dominance of adjunctions
Thanks, I appreciate that. What I kept wondering if these are not actually pointers that re-amplify the statement of Adjointness in Foundations [1969] about the base change adjoint triple:
One of the aims of this paper is to give evidence for the universality of the concept of adjointness, which was first isolated and named in the conceptual sphere of category theory, but which also seems to pervade logic. Specifically, we describe in section III the notion of cartesian closed category, which appears to be the appropriate abstract structure for making explicit the known analogy (sometimes exploited in proof theory) between the theory of functionality and propositional logic. The structure of a cartesian closed category is entirely given by adjointness, as is the structure of a “hyperdoctrine”, which includes quantification as well. Precisely analogous “quantifiers” occur in realms of mathematics normally considered far removed from the province of logic or proof theory.
Mike, is DTT a special case (or example or implementation, or whatever it will be called) of the framework in your article?
Not the existing articles, no, but yes for the one in preparation that I talked about at HoTTEST.
Would we just treat these as models of a (rather complicated) ordinary 2-theory in , or can we think about models of a simpler 2-theory in an enriched 2-category?
I think either one. Just as a ring can be defined either as a model of the theory of rings in or as a model of the theory of monoids in .
Not the existing articles, no, but yes for the one in preparation
All right, thanks for the information. Then you did know what more one might want to see, after all.
Spotted one typo in LSR:
p. 2: “concepts such state”
Perhaps along the lines Urs was thinking of, I could imagine a syntax in which categorical notions such as adjoints were expressed directly. In other words, one could ’program directly in a certain doctrine’. So one has some syntax for arrows (say a - >b), can apply an adjoint to them, (say ! (a - > b) or *! (a -> b)), one can compose them, etc.
Then you did know what more one might want to see, after all.
Yes, that’s what I said back in #32.
Mike, #32 sounds like it refers to having adjunctions in DTT, not like having DDT be implemented itself on a backdrop of a syntax of adjunctions.
To be clear, Urs, you think dependent type 2-theory (as outlined in Mike’s HoTTEST talk) isn’t sufficiently ’adjoint-to-the-roots’?
Since only Mike can know what it says in his unwritten articles, I won’t try to second guess. The rough idea which I had voiced seems to be evident enough to me, but apparently something is impeding its communication. But it’s not so important. We’ll wait for Mike to write and make available his article, and then we can try to talk about it in the language introduced there.
I hope to see Felix Wellen and Dan Licata and his tutorial talk tomorrow in Bonn (here), if the dysfunctional DB permits. Maybe that will help me speak a language that may be understood.
I can try to say a bit more about why I think the LSR programme (i.e. not just the two extant papers) can be viewed as “type theory implemented on a backdrop of a syntax of adjunctions”. It’s simplest to see for unary type theory. The mode theory is a syntax for a 2-category, but we can view it as a version of the 2-category of categories and adjunctions, so that it is “a syntax for adjunctions”. This is because each morphism in that 2-category gives rise to two type forming operations and which are adjoint. The more expressive 3-theories enhance this by incorporating dependency and by allowing multivariable adjunctions as well; thus for simple type theories the mode theory is a “syntax for multivariable adjunctions”, and in the dependent case it is some kind of “syntax for dependently typed multivariable adjunctions”.
Re #38: I’m not sure what you mean. You can have a hyperdoctrine with the usual quantification adjoints to substitution maps (as mentioned in #27), but without additive disjunction (= coproducts) in the “fibers”. So within a specific hyperdoctrine, I wouldn’t say that additive disjunction is necessarily a special case of existential quantification.
If all you mean is that additive disjunction is an example of a Kan extension, and that Kan extensions are adjoints to certain types of substitution maps, then of course I agree with that.
Re #48
some kind of “syntax for dependently typed multivariable adjunctions”,
do you have some examples of such adjunctions appearing “in nature”?
Maybe indexed adjunctions?
Hi Mike, I am reading LSR. I have trouble matching the text of the first two paragraphs of section 2.2 to Figure 2, which supposedly they should be referring to.
Could you check? In the text, does “the first judgement” and “the second judgement” refer to the top left two items in figure 2? Could you explain how? Even the symbol names don’t seem to match.
I generally find type theory hard to read, but isn’t it just that the first line of Fig. 2 records the first kind of judgement concerns assignments of modes to types, followed by generating rules for mode assignment, starting with propositions . Then the second line records the second kind of judgement concerns assignments of mode contexts to contexts, followed by generating rules, starting with the empty context being assigned the empty mode context.
Oh, I see now: The text at the beginning of 2.2 is referring to the boxed items in Fig. 2.2.
Spotted another typo: In the first displayed equation in the proof of theorem 6.7 on p. 31, “” should be “”.
And if I were an editor I’d remark:
In the statement of theorem 6.7, expand “the syntax” to say which syntax exactly.
add a table of contents
Okay, this morning I heard Dan Licata’s very nice talk (here) on LSR and followup developments. Towards the end it had something about the “Modal theory of Dependent type theory”, which seems to be exactly the kind of thing I was expressing hope, above, should exist, and should help with defining adjoint modalities in DTT.
I don’t quite understand now the way the discussion worked out here (apparently various misunderstandings) but I am very happy to see this take shape!
Type theory seems to have that effect.
By the way, where you hope in #29
Maybe there could be a type theory which is adjoint-to-the-roots that would be able to more seamlessly admit implementation of progressions of adjoint modalities as needed for super-differential cohesion.
I asked something to that effect on the blog, and Mike pointed out that the minimality aspect of the progression couldn’t be represented in 2-DTT.
the minimality aspect of the progression couldn’t be represented in 2-DTT.
Is there any mathematical use for that minimality?
I’m glad Dan’s talk was helpful, Urs!
Ignoring the Hegelese, is this not a mathematical use of minimality at Aufhebung?
…the Aufhebung of is necessarily given by a dense subtopos . Since the double negation topology is the unique largest dense topology it follows in general that , in particular in the case that happens to be essential and hence happens to be a level, the minimality condition on the Aufhebung of the initial opposition means that is, in particular, a Boolean topos.
Well, density is something that can be expressed internally.
I still want to know in the progression of the modalities why jets rather than germs?. Should minimality tell us which?
Do you mean a specific entry, or is it the Lab in general that does not display properly on your system?
I just checked the entry category theory, and – except for some bad whitespaces, which I have fixed now – it renders properly on my system.
Raymond, if you have javascript disabled and are not using a browser such as Firefox which can render MathML, you may encounter this. To render mathematics one needs one of the two.
added publication data for
added ISBN to
and DOI to
added pointer to:
added pointer to:
added pointer to
and re-arranged the other items around it into chronological order (here)
added pointer to:
added pointer to:
In the “History”-section (here), below
The concepts of category, functor and natural transformation were introduced in
- Samuel Eilenberg, Saunders MacLane, General Theory of Natural Equivalences, Transactions of the American Mathematical Society Vol. 58, No. 2 (Sep., 1945), pp. 231-294 (JSTOR)
I have added (thanks to Thomas Holder’s edit here):
apparently (see there) taking inspiration from:
- Hans Freudenthal, Entwicklungen von Räumen und ihren Gruppen, Comp. Math. 4 (1937) 145-234. [numdam]
added pointer to:
have added publication data to this item:
expanded the publication data for Hilton 1969 and Pareigis 1970
added these pointers:
Jean-Pierre Marquis, What is Category Theory?, in G. Sica (ed.) What is Category Theory?, Polimetrica (2006) 221-256 [pdf, semanticscholar]
Jean-Pierre Marquis, From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory, Springer (2009) [doi:10.1007/978-1-4020-9384-5]
added pointer to:
1 to 86 of 86