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

## Discussion Tag Cloud

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

• 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:

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 $n$-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 $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 23rd 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.

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)