Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory lie lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorEric
    • CommentTimeOct 26th 2009

    I removed some spam on category theory.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 22nd 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2013

    Added the recent

    to the references at category theory.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2013
    • (edited Oct 2nd 2013)

    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)

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2014

    added a pointer to

    which Todd had kindly pointed out as a nice enthusiastic lecture. Apparently the speaker mentions the nLab at some point.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 5th 2014

    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.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2014

    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.)

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 5th 2014

    I decided to put LaGatta’s talk under a new heading, Videos. The Catsters have now been entered under that heading as well.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2014

    Thanks, Todd!

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMar 12th 2016

    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?

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 7th 2018
    • (edited Apr 7th 2018)

    added pointer to Fong-Spivak 18:

    diff, v232, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2018
    • (edited Jun 2nd 2018)

    added to the previous quote by Freyd, concerning that categories were introduced to define functors, which were introduced in order to define natural transformations, also a second more pronounced quote

    diff, v233, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2018
    • (edited Jun 2nd 2018)

    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?

    • CommentRowNumber14.
    • CommentAuthorThomas Holder
    • CommentTimeJun 2nd 2018
    • (edited Jun 2nd 2018)

    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.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2018

    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
    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 2nd 2018

    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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJun 2nd 2018

    Hm, Lawvere [1963], [1964]? Not 1969?

    I guess [1963] is “Functorial semantics”? Is that so much about adjunctions? What’s Lawvere [1964]?

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 2nd 2018

    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.

    • CommentRowNumber19.
    • CommentAuthorTim_Porter
    • CommentTimeJun 2nd 2018

    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.

    • CommentRowNumber20.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 3rd 2018

    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 CatCat one needs adjunctions.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 4th 2018

    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.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJun 4th 2018

    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”?

    • CommentRowNumber23.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 4th 2018

    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.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJun 4th 2018
    • (edited Jun 4th 2018)

    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.

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 4th 2018

    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…

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    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.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJun 4th 2018
    • (edited Jun 4th 2018)

    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?

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 4th 2018

    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’?

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJun 4th 2018
    • (edited Jun 4th 2018)

    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.

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 4th 2018

    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.

    • CommentRowNumber31.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 4th 2018

    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.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    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 ΣsubstΠ\Sigma \dashv subst \dashv \Pi? And what do you find insufficiently “seamless” about modal dependent type theory?

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 5th 2018

    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 nn-theories account.

    In a nutshell, why the choice of the “canonical” nCatn Cat in

    The models of an (n+1)(n+1)-theory in the (n+1)(n+1)-category nCatn Cat are the semantic nn-theories in that (n+1)(n+1)-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 CatCat, or can we think about models of a simpler 2-theory in an enriched 2-category?

    • CommentRowNumber34.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 5th 2018

    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… ?

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018
    • (edited Jun 5th 2018)

    What do you find insufficiently “manifest” about ΣsubstΠ\Sigma \dashv subst \dashv \Pi?

    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 Σ\Sigma and Π\Pi are declared in terms of adjunctions.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    The rules for Σ\Sigma and Π\Pi look to me fairly manifestly like left and right adjoints to weakening respectively. I’m not sure what more you would like to see.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    More generally, the perspective of LSR is that all (nonrecursive) type formers are essentially by definition specified as multivariable adjoints.

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018

    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.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018
    • (edited Jun 5th 2018)

    Mike, is DTT a special case (or example or implementation, or whatever it will be called) of the framework in your article?

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    Not the existing articles, no, but yes for the one in preparation that I talked about at HoTTEST.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    Would we just treat these as models of a (rather complicated) ordinary 2-theory in CatCat, 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 SetSet or as a model of the theory of monoids in AbAb.

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018
    • (edited Jun 5th 2018)

    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”

  1. 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.

    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    Then you did know what more one might want to see, after all.

    Yes, that’s what I said back in #32.

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2018

    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.

    • CommentRowNumber46.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 6th 2018

    To be clear, Urs, you think dependent type 2-theory (as outlined in Mike’s HoTTEST talk) isn’t sufficiently ’adjoint-to-the-roots’?

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2018
    • (edited Jun 6th 2018)

    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.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeJun 6th 2018

    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 AdjAdj of categories and adjunctions, so that it is “a syntax for adjunctions”. This is because each morphism α\alpha in that 2-category gives rise to two type forming operations F αF_\alpha and U αU_\alpha 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”.

    • CommentRowNumber49.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 6th 2018

    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.

    • CommentRowNumber50.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2018
    • (edited Jun 7th 2018)

    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?

    • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2018

    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.

    • CommentRowNumber52.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2018

    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 PP. 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.

    • CommentRowNumber53.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2018
    • (edited Jun 7th 2018)

    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, “β m\beta_m” should be “β m/x m\beta_m/x_m”.

    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

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2018

    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!

    • CommentRowNumber55.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2018

    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.

    • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    the minimality aspect of the progression couldn’t be represented in 2-DTT.

    Is there any mathematical use for that minimality?

    • CommentRowNumber57.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    I’m glad Dan’s talk was helpful, Urs!

    • CommentRowNumber58.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2018

    Ignoring the Hegelese, is this not a mathematical use of minimality at Aufhebung?

    …the Aufhebung of *\emptyset\dashv \ast is necessarily given by a dense subtopos j\mathcal{E}_j. Since the double negation topology ¬¬\neg\neg is the unique largest dense topology it follows in general that ¬¬ j\mathcal{E}_{\neg\neg}\subseteq\mathcal{E}_j , in particular in the case that ¬¬\mathcal{E}_{\neg\neg} happens to be essential and hence happens to be a level, the minimality condition on the Aufhebung of the initial opposition means that j= ¬¬\mathcal{E}_j = \mathcal{E}_{\neg\neg} is, in particular, a Boolean topos.

    • CommentRowNumber59.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    Well, density is something that can be expressed internally.

    • CommentRowNumber60.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2018

    I still want to know in the progression of the modalities why jets rather than germs?. Should minimality tell us which?

    • CommentRowNumber61.
    • CommentAuthorMike Shulman
    • CommentTimeAug 3rd 2018

    Add link to Grandis’s textbook

    diff, v236, current

    • CommentRowNumber62.
    • CommentAuthorAlexisHazell
    • CommentTimeNov 2nd 2018

    Mention additional non-mathematical applications of CT; reference ’applied category theory’ page.

    diff, v237, current

    • CommentRowNumber63.
    • CommentAuthorGuest
    • CommentTimeMar 8th 2019
    Problem: some/most symbolic expressions remain in Latex(-like) form.
    Can this be corrected?
    Regards,
    Raymond Boute
    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeMar 8th 2019
    • (edited Mar 8th 2019)

    Do you mean a specific entry, or is it the nnLab 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.

    • CommentRowNumber65.
    • CommentAuthorMarc
    • CommentTimeMar 8th 2019

    replaced the dead link to Barr-Wells TTT with a link to the TAC reprint. Also I wonder why it is listed under “other texts”.

    diff, v241, current

    • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeMar 8th 2019

    I have removed the “other texts”-label.

    diff, v242, current

  2. 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.

    • CommentRowNumber68.
    • CommentAuthorThomas Holder
    • CommentTimeMay 27th 2019

    Added a reference to lectures on category theory by Peter Johnstone.

    diff, v244, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)