Thanks again, Mike.

I tried to explain this in the paragraph which follows:

Right, I should spend more time looking into this. The trouble is that I am really doing something else and just following the type theory development with half an eye.

I want to get to the point where I can clearly understand the relation to -groupoids. I certainly get the basic idea that an identity type is like an -groupoid of paths or of equivalences between two objects. But eventually I want to understand this on a more formal level, for myself.

But not right now. I need to take care of some Cartesian fibrations now...

]]>Back on the original subject, I added some more explicit explanation to context about morphisms of contexts in terms of type theory. I'm not sure I put it in the right place, though.

]]>Actually, I think type theory is more like machine code, since it's more directly connected to first-order logic. Material set theory is just a particular first-order theory that lives inside a type theory. (-:

And why on earth would you believe that material set theory is like machine code? That would mean that somehow the integer 2 "really is" the von Neumann ordinal (or maybe a different set), but the type theory doesn't know it. It's much more reasonable to say that 2 is an element of the type of natural numbers, which in turn can be modeled in material set theory by the set of finite von neumann ordinals, but also in lots of other ways.

]]>The whole point of foundations is not to build on top of another foundation. Sure you can build a model of ETCS or SEAR from ZFC, but that is not necessary what you want to do. The point is to extract the necessary structure (i.e. the category) and throw away , which allows the construction of stupid questions (like is ?).

]]>I think that we should build structural set theory on top of material set theory. This is extremely easy to do and feels more natural in a sense. For instance, a lot of the complicated definitions from type theory can be stated more easily using a material set theory.

Think of it this way: material set theory is like machine code or binary, while type theory gives us a higher-level language to deal with things.

]]>Harry, my problem with material set theory is not that it's complicated (it's not, really, in its own right) but that the process of coding mathematics into it is unnatural, introduces superfluous data, enables meaningless questions, and discards important typing information. Also, structural set theory and type theory have a much more natural categorical semantics, while type theory also has important connections to computability and automated proof. I freely admit that type theory is more complicated than set theory (at a basic level, anyway); its advantages lie elsewhere.

]]>Zoran, I'm not disagreeing with any of that, I just don't think the word "abuse" is appropriate. In fact, I think that often things labeled "abuses" of notation are actually not ambiguous at all. For instance, if is a group, we always write to mean that is an element of the *underlying set* of . People call this an abuse of notation, but since only has one underlying set, there is really nothing ambiguous about it. (Unless one insists that a group is really a Kuratowski ordered triple, in which case might have a totally different meaning, but that's just silly.)

This seems just as complicated as material set theory.

(I was going to delete my comment, but mike answered it, so I've put it back the best I could.)

]]>Urs, the subsections look good. You're right that is a context; I think is pretty universally used to denote an arbitrary context, so sometimes I may forget to mention what it means.

The "big rule" is defining a term constructor called J. I tried to explain this in the paragraph which follows: J(...) is a new term, with some specified type, which the identity type rule allows us to form.

Finally, if I understand you correctly, the first half of the lower line copies the first part of the upper line because they are two different assertions in the same context. The first hypothesis asserts that in some context we have a type , while the conclusion asserts that in that same context we have a *term* belonging to the type , namely .

and powerful type inference procedures exist to resolve ambiguity

But those must be probabilistic in general (Edit: in cases which go beyond comparativley simple overloading in programming languages). These algorithms are for more special and simple situations than in human mathematical comunication in which we are on daily basis witnesses in seminars where the informal shortcuts confuse listeners. This is an economy which does lead to occasional errors, hence there is a feature which is not perfect. That does not say that imperfect objects are not often useful, but they are imperfect and stepping down from more unambiguous to more ambigous notation is hence a kind of abuse. Even higher level of ambiguity is in the natural language discourse, and the level of disambiguation of deixis has not been radically raised in last 30 years, as it would require so much of the context and real artificial intelligence that mere algorithm improvement and speed does not help that much. I have some sizeable hands on experience on both the computational linguistics and the compiler construction.

]]>Armed with my improved understanding, I am now looking at identity type again.

I still don't follows this, though.

]]>Okay.

I couldn't stop myself and edited a bit more, still:

where dependent types are being introduced I expanded a bit more and mentioned the new notation

then I added some subsection titles, since this part is becoming fairly long now. What do you think how the new toc looks? I like it better this way.

@Urs: looks good, I did a bit more editing.

]]>@Urs: Mike has said before that SEAR is just type theory in a disguise.

So.. How about the theory of unramified types....

]]>I further edited type theory:

I went to the paragraph that talks about dependent types and in an analogous manner as before tried to unwind everything into the underlying categorical language.

Please have a look!

]]>@Urs, thanks! I like how it is now.

Okay, good. I like the notation, now that I fully understand how it is meant to be read. I feel like it should have been obvious to me without asking.

In fact, this categorical semantics notation and language already appears in structural set theory, as in Todd's discussion ot ETCS, of course. It is really the language that says that each morphism in a category is a natural map of sets of generalized elements. So it's really the language that describes all the ingredients of a category after their Yoneda embedding into .

Just for the sake of it, I added a sentence to this extent to type theory:

]]>So the notation is a direct reflection of the description of the morphism under the Yoneda embedding . Since the Yoneda embedding is a full and faithful functor, this is indeed an entirely equivalent characterization of the morphism .

@Toby, good point. It is true, though, that you only need dependent sums if you also have dependent types -- otherwise, finite product types suffice. Of course in both cases there is then also the question of equalizers and more general subobjects, and at some point we have to figure out exactly what was meant by the words "correspond to" in the phrase "types correspond to objects." But I think in the overview, the "(with various subtleties)" is probably sufficient where currently placed.

@Urs, thanks! I like how it is now.

]]>@Zoran: But overloaded operators and polymorphism are ubiquitous in computer science, and powerful type inference procedures exist to resolve ambiguity. I'm not saying that such simplified notations aren't *harder* for a computer to parse (and occasionally may require additional annotation from the user), but I don't think that makes them "wrong" or "not true."

@Harry: I completely agree that notation should be introduced, and indexed.

]]>The Wikipedia page actually gives a pretty good idea of how it's generally meant in the mathematical community.

In written work as well, noting abuses of notation when they're first introduced can save a lot of time and pain for the reader. That's why when you introduce a definition, you should give it a formal definition and then note that there is an abuse of notation going on. This way, if the reader looks up the definition in the index, he/she will also be able to find the conventions! (For example, I was reading Michael Spivak's book on Differential geometry, and I could not figure out for the life of me what meant. Needless to say, it was due to an abuse of notation. (It's not actually a pushforward at all)).

]]>I do object to calling such uses of notation "abuses" since it gives the impression there is something wrong with them

The wrong thing is that it spoils theoretical uniquness of the notation by using shortcuts which are overloaded and hence can be misinterpreted if a computer would analyse it automatically. Anybody who was programming artificial intelligence knows the pains of the abuse of notation. I find the expression cute and the very fact that it is standard and accepted implies that the abuse is OK from practical mathematical point of view as long as the people communicating mathematics do feel so. The fact that it is labelled as nongenuine can, in the cases of misunderstanding, give the right to the listener to call the speaker to go back to the true underlying formal or more formal expression.

]]>Thanks Mike, thanks Toby!

That helps. I have turned the query boxes at Categorical semantics into genuine text, using replies here and Toby's replies there. Please check if this is correct now.

]]>Although not all type theories *have* dependent sums. And then this simplification, in which we identify objects of the category with types, breaks down; we really have to identify objects with contexts.

Yes, I know it's standard, but I still object to it. (-:

Actually, after thinking about it some more, I think that the "abuse" really flows the other way. That is, the dependent type should be regarded as containing all the information of an object of the slice category , namely a morphism together with its domain. The abuse is in referring to the domain alone by the same letter used for the dependent type; really we should notate the morphism as something like .

And in fact, both the domain and the morphism already have names within the type theory. The domain, considered as an object of the category in its own right, is the dependent sum type , and the morphism from this to is the projection onto the indexing type of the dependent sum.

]]>"Abuse of notation" is a standard term. It was not meant as a slight! =)

]]>