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 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.
I have added to doctrine the reference
This is the origin of the concept, in print, according to page 2 of
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.
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)?
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.
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.
Why were ’comprehension categories’ given that name? And ’category with attributes’?
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”.
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.
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.
An nLab conference would be awesome.
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.
Added something on the treatment in terms of double categories here:
I see we don’t have an entry for ’cartesian double category’. If we do, there are some notes by Mike here.
1 to 14 of 14