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.
Some reorganization and added material at type theory. In particular, I added some of the basic syntax of type theories, and also some comments about extensional vs. intensional type theories.
I'm really bothered by the lack of a definition. Surely we can define it formally using a Hilbert-style proof calculus, no? I mean, this isn't often covered, but in Ch.1 section 1 of book 1 of Bourbaki, they actually give a rigorous definition of a "mathmatical theory". I believe that this is flexible enough to encode type theories as well as set theories.
Let me save Urs the trouble and suggest you add it yourself.
I don't know anything about type theories. =(.
No worries :) You know a lot more about them than I do. You could always give it a shot and report back here, "I gave a shot at a definition for type theory. How is it? Did I completely mess up?"
I do that kind of thing all the time. Nothing like getting attention to a page by putting something wrong on it. Then the experts come in full force :)
Even better: put up a new page on the Bourbaki stuff, then waffle at type theory, and say it is something like the new page, only typey-er.
You can of course define any particular type theory formally. ButI've never seen a formal definition that includes all things called "type theories" and only things called "type theories." But I haven't tried very hard to produce one, either, so if you feel like trying, have a go, as long as you don't mind people coming along and poking holes in it. (-:
I don't write things unless I'm sure that they're either right, or wrong in an interesting way.
Then be interesting, and you won't have to worry about if you're right or wrong. :)
Out of curiosity, when Bourbaki define "mathematical theories", what does it amount to? E.g., is it necessarily a theory in first-order classical logic? Is it more broadly just any recursively enumerable collection? Do they give a criterion for equality of theories, and if so, how "presentation-free" is it? Etc.
It's just a language and a syntax in a very broad metamathematical sense. See here: http://books.google.com/books?id=IL-SI67hjI4C&lpg=PP1&ots=nahrxb7fLG&dq=theory%20of%20sets%20bourbaki&pg=PA15#v=onepage&q=&f=false
It doesn't assume any "logic" at all, at least in my understanding (it's certainly not classical, anyway). The logical axioms are only even defined in section 3 or 4. I'm pretty sure it's just a syntax with a few definitions.
True, but the next few sections don't attribute any meaning to the symbols, where they're really just defined syntactically.
I rearranged the section syntax of type theory to make it look more like a definition. Does that make you any happier?
Seeing the adjunction between semantics and syntax on the type theory page, reminded me of a comment of Lawvere's to the categories mailing list on 5 Jan 2010. What can we learn from this?:
Actually, the term 'syntax' refers NOT to small categories such as algebraic theories or rings, but rather to their PRESENTATION by signatures or by polynomial generators, et cetera. The process of presentation is an adjoint pair quite distinct from the semantical adjoint pair: both adjoint pairs have a category of theories or of rings in common but are otherwise quite independent.
In particular, syntax is NOT the adjoint of semantics. Cratylus, Chomsky, and their 21st century followers can be refuted by looking soberly at the actual practice of mathematics (wherein the construction of sequences of words and of diagrams is pursued with great care for the purpose of communication. That syntax is only remotely dependent on the structure of the content that is to be communicated).
Both of the functors
?----Syntax---> theories ----Semantics--->Large categories
are needed. The domain category of the first can be chosen in various useful ways: sketches or diagrams of signatures et cetera.
Hmm. I agree that "syntax" ideally refers not to small categories but to their presentations, which is of course the POV taken at type theory. However, I'm not sure it follows that syntax isn't the adjoint of semantics. I would tend to omit to write the inclusion of small categories in large ones, and consider as interesting the right adjoint of the functor from presentations to small categories.
Actually, I'm not sure how much I believe that 'syntax' and 'semantics' are really functors at all. I would be more inclined, intuitively, to regard 'syntax' as just referring to the presentations themselves, prior to any relationship with categories, and 'semantics' as referring to the entire adjoint pair.
I have added a pointer to Bob Harper’s book to type theory. In the course of this I ended up re-ordering the list of references there by type to make it clearer what to read why.
Experts please check and expand.
May I reiterate question on a related book: if somebody has a correct eletronic version of Taylor’s Practical foundations of mathematics (e.g. this does not render correctly, test case for your file will be lemma 6.5.3 and the text below). There are many electronic copies available online but neither of them renders typographically in formulas which are abundant.
P.S. it seems there is one now.
I think you can say that type theory is a precise syntactic language for describing theories (with “generators and relations”) in certain doctrines. It works better (or, at least, it is better known) for some doctrines than others. Theories in doctrines such as finite products, finite limits, regular categories, exact categories, coherent categories, Heyting categories, pretoposes, cartesian closed categories, elementary toposes, and locally cartesian closed categories are all well-described using type theories. With homotopy type theory, we can also handle locally cartesian closed -categories. Doctrines such as monoidal categories are not as well-described, although there exist type theories related to them such as “linear logic”.
Some aspects of what Mike just said are scattered about in entries related to type theory. But it would be nice to have a more comprehensive remark as #21 in the entry “type theory” itself.
Would you have time for that?
The usual notion of sketch doesn’t handle the doctrines of cartesian closed categories, locally cartesian closed categories, or elementary toposes. One might imagine a more general notion of sketch which does, but I don’t know if anyone has written one down.
Type theory also goes beyond merely defining a theory, but additionally gives a syntactic and computational presentation of the classifying category of the theory (the category that it “presents”), hence of a reasoning that is valid for any model of that theory in any category.
The pages internal logic and context have good descriptions of describing theories in type theory, such as the theory of groups.
I wasn’t saying that “the theory of cartesian closed categories” can’t be defined in the doctrine of, say, (2,1)-categories with finite products and involution (it can’t be defined in the doctrine of 2-categories with finite products, since the internal-hom is contravariant). What I was saying is that theories in the doctrine of cartesian closed categories cannot be presented by the standard notion of sketch.
The internal-hom of a cartesian closed category is a functor , in the same way that the cartesian product is a functor . The doctrine in which a theory is described specifies the allowable “arities” of the “operations” in that doctrine. Thus, in order to have a doctrine of cartesian closed categories, there must be some sort of “arity” for “binary operations with one covariant and one contravariant input”. The obvious way to model contravariance is to have an involution existing at the same level as the operation . Thus, the natural place in which to talk about “cartesian closed objects” is a 2-category with finite products and an involution — hence, the theory of cartesian closed categories lives in the doctrine of such 2-categories.
Perhaps the point is that a “subdoctrine” of a doctrine must also be itself a doctrine, not just an arbitrary subcategory of the category of theories in ?
@Zoran
P.S. it seems there is one now
where? Email me if it shouldn’t be advertised on a public forum.
I’ve always wanted to have a good browse, and the online version is so poor it isn’t worth trying.
EDIT: I take this back.
Defining cartesian categories as theories in the doctrine of cartesian 2-categories is not very useful, from my point of view, because we are eating our own functorial arm doing that, no? ;-)
You mean, because we used the word “cartesian” twice? I’m not sure what other doctrine you could define cartesian categories in. At some point, you’re going to need some input about what a “product” actually means. It doesn’t seem any better to me to define cartesian categories as a subcategory of using “the metalanguage of higher categories with limits” as you say — in both cases we’re using a notion of limit to define the theory of products.
What i would like to know is when a subcategory of the theories of a given doctrine form a doctrine. What kind of condition can we impose? It seems to me that when one is able to write down a condition with finitely many words, this should give a subdoctrine, but perhaps i am too optimistic.
Well, first of all, whether a subcategory forms a doctrine is going to depend on what eka-doctrine you want it to be a doctrine in. (By “eka-doctrine” I mean doctrine at one higher level up.) For instance, to take the example we’ve been looking at, cartesian categories (or, more precisely, cartesian objects) are a doctrine in the eka-doctrine of cartesian 2-categories, while the subcategory of cartesian closed categories is not a doctrine in that eka-doctrine, but it is one in some larger eka-doctrine (cartesian 2-categories with duality involution). Similarly, is the category of theories for the “doctrine of objects”, which exists in the simplest possible eka-doctrine, but if we want to be a sub-doctrine on we have to expand the eka-doctrine to at least cartesian 2-categories.
Since we know from experience that any condition we can write down in finitely many words can be described in first-order logic, it seems likely that if we are willing to expand the eka-doctrine to include all of first-order logic, then your guess would become correct.
There’s also the question of whether our subcategories of theories are full. The 2-category of cartesian closed categories, for instance, is not a full sub-2-category of the category of cartesian categories, since we want to consider only the functors that preserve internal-homs as well as products.
I think it will be very hard to give a presentation of every concretely given doctrine (like cartesian closed categories) as given by a higher finitary monad with arities on n-Cat.
I don’t think it will be that hard, once we have good machinery in place. It’s easy when and , where the machinery is pretty much already in place. People like Lurie have been working on the case , and maybe the machinery is basically in place there too, I’m not sure.
Also, beware that cartesian closed categories are not presented by a 2-monad on , only on (the (2,1)-category of categories, functors, and natural isomorphisms). This is due to contravariance again.
It seems to me that trying to give an explicit syntax for theories of a subdoctrine of n-Cat defined by limit and commuting diagram conditions (sketch approach) is like delooping the simple definition of the given theory
I don’t understand what it has to do with delooping. I see a sketch as basically an alternative way to describe the explicit syntax for a theory (in the case when the doctrine involves only limits and colimits). For instance, the explicit syntax of the theory of groups has one type and a binary operation (and some other stuff). When we describe that theory with a sketch, the type becomes an object of the sketch, and the operation becomes a morphism, with the arity of the morphism described by making its domain be an object stipulated to be the product .
The lego game of eka-doctrine looks quite interesting… I’m sure the situation is not far from being clarified by someone, about n-monads, and presentations of higher doctrines, but probably not by me, because this looks a bit hard.
At some point, you’re going to need some input about what a “product” actually means. It doesn’t seem any better to me to define >cartesian categories as a subcategory of using “the metalanguage of higher categories with limits” as you say — in both cases >we’re using a notion of limit to define the theory of products.
I think your are touching exactly the point that is problematic in a foundational perspective on doctrines. I don’t have a clever answer to the question: what is a product?
For me, a product is a universal cone for a finite discrete diagram: a limit. So categories with products are categories that have these kinds of limits for all finite diagrams. But i guess this is not foundational enough, and i understand that.
What is your prefered definition of a product, from a foundational perspective? :-)
For me, a product is a universal cone for a finite discrete diagram: a limit. So categories with products are categories that have these kinds of limits for all finite diagrams.
That seems perfectly foundational to me.
Some editorial points at type theory:
There is the following paragraph, which I guess contains a typo:
The description given below is a somewhat simplified one, in that we identify objects of the category with single objects, rather than contexts. This is strictly speaking only okay in type theories with a dependent sum operation, which allows us to reinterpret every context as a single type.
The highlighting is mine. And: the highlighted “objects” wants to by “types”, right?
In the References-section I renamed “Jean-Yves Giraud” to “Jean-Yves Girard”
The section An introduction to category theorists is pretty good.
I am wondering about strengthening it in the following ways:
Can we rename the section from “Introduction for category theorists” to something that more explicitly makes the point that type theory is not only something that category theorists can understand in their context, but that they also want to understand? Something like “Type theory as a formal language for category theory” or the like.
What would be references to support this section? I have added a link to a page Category theory and type theory by Paul Taylor, but I would like to give the reader more pointers to the literature here.
For instance that adjunction between type theories and categories: what is a reference, if any, that discusses this?
[edit: I have found more on this in Taylor’s book here]
Or, what’s a reference that discusses in detail the relation between type construction and universal properties in category theory? I would like to see an explicit discussion of the type-theoretic quadruple
related to category theory.
More on the first item in c): what I am after is more answers to those readers who may say the following:
I don’t care about teaching mathematics to a computer, or related applications of type theory. I am a category theorist or at least in my work I make heavy use of category theory, and I want to know: what can type theory do for me? If anything.
Maybe dependent type theory is telling me that I can prove better theorems about category theory or its applications if I emphasize the point of view of slice categories and base change between them over a more ’global’ point of view. But which theorems would that be? What do I gain, if anything, by reading your ’Introduction to type theory for category theorists’ if my motivation is not just to understand type theory for its own sake?
This is roughly a question that I am personally being confronted with, and I think it is a good question. I know partial replies to this. But I feel I could improve on those. All help would be appreciated.
For instance with the discussion at contractible type one can say to a higher category theorist: “Look, here is a neat way to reformulate (-1)-truncation in an -category which you had missed so far, because you didn’t systematically think in terms of . Similarly for statements about weak equivalences etc. This actually helps seeing some little facts that you had missed so far, so it’s good to know”.
Stuff like this. Eventually I would want a list or comprehensive account of answers to such “What can type theory actually do for (higher) category theory?” questions (as opposed to just: “Look, we can reformulate (higher) category theory. Isn’t this fun?”)
Re point d) above:
for instance Paul Taylor here (scroll down to section 2.5) asserts:
However, purely categorical textbooks cover many pages with diagrams expressing arguments that could be written much more briefly [in type theory].
I am not sure if the text fully supports this claim at this point. But this would be what I am after here: to make explicit where using type theory is genuinely useful as a tool in category theory or the like, as something that gives you insight or increases clarity in a way that couldn’t be achieved without.
a) yes, that’s a typo; I fixed it.
c1) Sure, how about just “As a formal language for category theory”?
c2) I would also like to see such an explicit discussion! Understanding introduction/elimination for positive/negative types quite generally in terms of universal properties for mapping out/in was a revelation to me precisely because I hadn’t read anyone explaining it well before. Which is to say, I don’t know good references. Bart Jacobs’ book is okay, but I find it too scattershot and doesn’t make the guiding principles explicit enough.
d) Yes, we should start collecting lists of these. One classical example I am fond of, which I used in my talks at Swansea, is that the proof that inverses in a group are unique works quite well in type theory and therefore internalizes to any finite product category. But if you try to prove by manipulating elements that the antipode of a Hopf algebra is unique, you are in for a world of pain.
There are some more classical examples in the Elephant, scattered throughout part D and a few places earlier as well.
There was a case here on the Forum a while back where some question about -limits came up that I found it easier to prove using homotopy type theory, maybe we could find it and cite it or copy it?
I also remember back when were discussing the pasting law for -pullbacks, you suggested that we could do it in homotopy type theory for an -topos, and then interpret it in any -category with pullbacks via the Yoneda embedding.
Thanks for these reactions!
Okay, good. So let’s start collecting such a list.
I did start such a page today, optimistically titled HoTT methods for homotopy theorists, but it is just a first rough place to contain some notes that I had time for today. I will try to expand on that tomorrow.
I’ll look again at your argument about uniqueness of inverses, that sounds like a great example.
Concerning that discussion of -limits you are alluding to, are you thinking of the discussion of stabilizer -groups about which you posted some impressive HoTT analysis here?
The pasting law of pullbacks is also a good example. I’ll include that in the above page. Maybe I’ll make some section “Basic facts of homotopy theory made even simpler in HoTT” or the like. Because, while very nice, I would like to separate that from facts that a homotopy theorist might actually consider news.
Mike, I looked again at your notes but I don’t seem to find it: where do you have that discussion of inverses in groups that you are referring to?
I have considerably expanded the Idea-section at type theory.
Hmm, maybe I only said it out loud. Anyway, what I said above is basically all there is.
(And yes, the stabilizer -groups is what I was thinking of.)
I have considerably expanded the Idea-section at type theory.
Maybe from type theory there could be pointers to positive type / negative type since in Swansea I got the impression that it is (at least didactically) good to know them.
Go ahead, Stephan, and add those pointers where it makes sense!
@Zoran
P.S. it seems there is one now
where? Email me if it shouldn’t be advertised on a public forum.
I’ve always wanted to have a good browse, and the online version is so poor it isn’t worth trying.
I am interested in this one, too.
Maybe from type theory there could be pointers to positive type / negative type since in Swansea I got the impression that it is (at least didactically) good to know them.
I linked the beginning of section As a formal language for category theory
”One way to look at type theory, from the point of view of a category theorist, is as a syntax for describing the construction of objects and morphisms in a category.”
This non existing page should then remark that one way of classifying types is via their ”construction” - or more precisely via their constructors. However the beginnings of positive type/negative type do not indicate that eliminators are type constructors but somehow suggest that ”constructor” and ”eliminator” are thought of complementary notions.
There is a potential confusion in that the word “constructor” can refer both to the formation rule by which we define new types (e.g. given types and there is a type ) and to the introduction rule by which we define terms belonging to those types (e.g. given and there is a term ). The latter case is what is dual/complementary to the elimination rule. Perhaps this should be clarified somewhere (or everywhere).
I added a link to the types mailing list to the page type theory.
1 to 48 of 48