Not signed in (Sign In)

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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2015

    I fixed the first sentence at doctrine. It used to say

    A doctrine, as the word was originally used by Jon Beck, is a categorification of a “theory”.

    I have changed it to

    The concept of doctrine, as the word was originally used by Jon Beck, is a categorification of the concept of “theory”.

    If you see what I mean.

    Then I added to the References-section this:

    Willian Lawvere, 23 Mar 2006:

    The word “doctrine” itself is entirely due to Jon Beck and signifies something which is like a theory, except appropriate to be interpreted in the category of categories, rather than, for example, in the category of sets; of course, an important example of a doctrine is a 2-monad, and among 2-monads there are key examples whose category of “algebras” is actually a category of theories in the set-interpretable sense. Among such “theories of theories”, there is a special kind whose study I proposed in that paper. This kind has come to be known as “Kock-Zoeberlein” doctrine in honor of those who first worked out some of the basic properties and ramifications, but the recognition of its probable importance had emerged from those discussions with Jon.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2015
    • (edited Sep 4th 2015)

    I have added to doctrine the reference

    • William Lawvere, Ordinal sums and equational doctrines, Lecture Notes in Math., Vol. 80 (Springer, Berlin, 1969).

    This is the origin of the concept, in print, according to page 2 of

    • Michael Makkai, Gonzalo Reyes, Completeness results for intuitionistic and modal logic in a categorical setting, Annals of Pure and Applied Logic 72 (1995) 25-101
    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 20th 2018

    Now we have type 2-theories and type 3-theories (from slide 30 of Mike’s HOTTEST talk), at some point we may want to modify doctrine and perhaps more significantly higher doctrine.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 20th 2018

    Let’s see if I have the numbering of layers right.

    So we might choose to work in the type 3-theory which is dependent type theory, then choose to work in it with a specific type 2-theory with specific type constructors, say Martin-Löf dependent type theory.

    Then we may choose to specify some type and term generators and axioms they satisfy for a 1-theory in our 2-theory. Finally we can choose an interpretation of our 1-theory as a model, which may be called a 0-theory.

    So if ’simple type theory’ and ’dependent type theory’ are each examples of a type 3-theory (slide 33). What kind of theory then is ’dependent type 2-theory’ (slide 45)? Or ’simple type 3-theory’ (slide 29)?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeApr 20th 2018

    By “simple type 3-theory” on slide 29 I meant the same as “simple type theory” regarded as a 3-theory (as on slide 33). I guess that slide 45 should probably have been “dependent type 3-theory”, meaning the same as “dependent type theory” regarded as a 3-theory as on slide 33. I’m not sure this is the best terminology though. Even once having the idea of what a 0-theory, 1-theory, 2-theory, 3-theory means in general, it’s hard to give good names to particular ones because historically the plain word “theory” has been used indiscriminately at several levels.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 21st 2018

    Physics hasn’t fared any better with such indiscriminate use - theory (physics).

    Great talk by the way. I think that’s the first time I heard you talking since Minneapolis in 2004. Funnily enough at that meeting I remember trying to work out a way of associating categorical levels to logical theories with John Baez. If I recall, it was based on the kind of nn-groupoid that a theory’s models constituted: so a set of models of propositional logic, a groupoid of models of a first-order theory, and there was some thought of modal logic being at the next level with a 2-groupoid of models.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 21st 2018

    Why were ’comprehension categories’ given that name? And ’category with attributes’?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeApr 21st 2018

    Wow, Minneapolis was a long time ago. I’m pretty sure I didn’t give any talks at that meeting though — I was just a first-year grad student trying to figure out what it was all about. Or did you just mean “heard my voice”? I might have screwed up my courage to ask a question or two.

    Re #7, I can’t say for sure, but I’ve always figured that comprehension categories were named because the operation TC T\to C^\to is a “comprehension” in a similar sense to Lawvere’s (though not identical – I think a fibration with Lawvere comprehension is automatically a comprehension category, but not conversely). No ideas about “category with attributes”.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 22nd 2018

    Yes, “heard your voice”. I think maybe you were there at an impromptu talk that James Dolan gave to a handful of people.

    We should have an nLab conference one day. I met Todd once in the last millennium. Aside from Urs, I don’t think I’ve met anyone else here.

    • CommentRowNumber10.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 22nd 2018
    • (edited Apr 22nd 2018)

    We should have an nLab conference one day.

    This is the sort of the thing I imagine might be able to be funded if we were to obtain a grant, as discussed for instance in #14-#19 here.

    Were you able to speak with Steve Awodey at the meeting, Mike? If not, how shall we proceed? I would have thought we should begin preparing something and applying sooner rather than later.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeApr 23rd 2018

    An nLab conference would be awesome.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 24th 2018

    My life circumstances put heavy constraints on my ability to travel to conferences, but I’d definitely make an effort to attend an nLab conference.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 7th 2024

    Added something on the treatment in terms of double categories here:

    diff, v20, current

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 7th 2024

    I see we don’t have an entry for ’cartesian double category’. If we do, there are some notes by Mike here.