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.
Just had a look at functor (homotopytypetheory). I understand that this is just a first beginning, but some comments:
These entries should at least point to their corresponding nLab entries, for context and background. I have now added such pointer, by adding a line of an Idea-section right at the top. But feel free to edit for style.
Since currently the entry is written completely “informally”, it is a little hard to see what makes it stand alongside the nLab entry functor in the first place. I suggest there should be something recognizably type-theoretic in all entries on the HoTT-web. Ideally the corresponding nLab entry should be able to point to its HoTT-wiki companion with the words “For details on the formalization of this concept in type theory, see ….” and then the HoTT-web entry should provide more than the implicit suggestion that the type theoretic formalization is straightforward for the experts.
The pointer to the HoTT-Book (or any other reference) should really contain at least a chapter number, ideally a definition/proposition number!
I suggest there should be something recognizably type-theoretic in all entries on the HoTT-web
I’ve suggested it before, but wherever possible I think it would be great with actual code as well, which compiles.
Urs, I will have to disagree with you here. I agree that we should have links to the nlab version, but it shoudn’t be part of the main body of text. All the things I have talked about in the definition have specific type theoretic definitions (which as the wiki is young are not included as of yet). If we linked to the nlab in the main references, the page might as well be its own nlab article.
The page for functor doesn’t need to stand aside the nlab page precisely because it serves a different purpose: A reference about HoTT for people using or doing HoTT. It doesn’t need to reference classical mathematics and that is part of the point.
On the informality of the text. I am following the philosophy of the HoTT book that mathematics in HoTT can be done informally to a rigourous standard. These arguements are all from the HoTT book, they are very easily translated into your favorite proof assistant. Whether or not we include that here is a seperate matter.
Obviously many of the notions I have written up thus far are heavily inspired (and are in most cases direct copies of,) by classical mathematics. If you take a look at the Univalent categories paper by Ahrens, Kapulkin and Shulman, you will see a similar language.
One final thing to say: I think what distinguishes this wiki from the nlab is that the nlab can talk about HoTT, but this wiki is in HoTT.
it shoudn’t be part of the main body of text.
No, and I didn’t say that. But a pointer should be somewhere. The canonical places are 1) In the Idea-section (which should give an informal quick idea of what is to follow, and put things in perspective) or 2) In a list of entries labeled “Related entries” or maybe “See also”.
they are very easily translated into your favorite proof assistant.
I know, that’s why I spoke about the implicit suggestion that the formalizaton is straightforward for the experts. But it seems at least a missed opportunity if a public wiki entry on “functor” in HoTT reads verbatim and exclusively like any other such entry, on Wikipedia or the nLab.
Keep in mind is that the people perusing a wiki entry are typically those who are not expert yet, but want to become experts. Lend them a hand!
I like to imagine myself as somebody who has picked up the HoTT book, and read some of it. I am now inspired and intuiged about what I have just read and I wish to find out more. The average person will click on the nlab and think: “Wow this looks difficult and confusing”. Wheras what I believe the HoTT wiki should be aiming for is essentially a continutation of the philosophy of the book to show the world how mathematics is done in HoTT.
This isn’t a critisism of the nlab. You must believe me when I say that the nlab is an indespensible reference. But it isn’t for everybody. Part of what the HoTT book and this wiki are trying to addresss is the acessability of mathematics we are presenting. One of the key ideas of the HoTT book philisophy is that the informal mathematics isn’t so different from the formal/formalised mathematics.
To your last comment:
I see your point. I will try to take your points into account. My current goals at the moment are to soldify the pages as a reference then I will go and add thoughts and ideas later on. The latter requires me to read a few research papers and talk to some more people.
Sorry if I have sounded a bit rantish I will blame the coffee.
added pointer to the original reference Ahrens-Kapulkin-Shulman 13 as well as to the corresponding Coq-source.
added the corresponding formal definition, here
Alizter,
hope you don’t mind the addition of the formal definition.
I have to admit that I don’t quite understand #6. It sounds as if you are saying that people interested in type theory should not be bothered with type theory. They should just find the standard informal lore and trust that a type theory formalization exists. Maybe you don’t mean it that way, but #6 does sound that way.
In any case, good practice should be the following (as for any piece of computer code, I would think): Every thought on the HoTT wiki should be voiced in two steps: First it should say something informally, in order to appeal to the human being in the reader, then it should provide at least some indication as to the actual formalization, in order to appeal to the type theorist.
You can give these two steps two different subsections, if you are afraid that readers will be confused by seeing formal code (?!)
I do not think that the definition I have given is in fact informal. I will claim that it can be unambiguously translated into a formal bunch of dependent and inductive types, which would be expressable in any proof assistant (hopefully soon). That’s why I think that adding the Coq code is unnecessery. Computer code changes, in ten years time I will be suprised if we are still using Coq and agda. The ideas however do not.
Another point is that HoTT isn’t about formalisation, it can be formalised (which should be a whole seperate article in itself as it is a useful skill) but you can also do HoTT without having a care in the world how it is implemented. This is not too different from set theoretic foundations: The only people who really care about what the objects you are actually playing around with are set theorists. If we expressed everything in set theoretic terms much of mathematics would become unbearable.
If I type theorist wants to study this article for example, they should have no trouble: Simply read the (to be) article on translating informal statements into type theory, and you will have a mess of sigma and pi types which if they really want to study that they can.
I guess the point I keep grappling at but I just can’t seem to express is that this wiki is about doing mathematics (and what mathematics you can do) in HoTT.
So in a sense #6 is exactly how you say it is. Although I am claiming that there will be an article showing how all this (carefully) written “informal” language is actually sigma and pi types in diguise. So #6 isn’t really as bad as you make it sound.
This is about the third time I have rewritten this post so if any points don’t make sense please let me know.
Alizter,
thanks. I don’t want to be trouble, just trying to share some experience with wikis.
If you insist, feel free to remove the code again, it’s “your” wiki. But I do suggest to keep at least the pointer to the github repository, for readers who do want to see it.
I admit that I find the attitude of the type theory community confusing, these days. On the one hand the community is now questionig the ancient idea of categorical semantics of type theory as not being proven to a satisfactory formal level; on the other hand there is this attitude that it’s not only a done deal but so trivial as to not even requiring or even deserving mentioning.
Urs I don’t think you are any trouble at all in fact I openly welcome all discussion on this matter.
I want to make it clear that formalisation will definietly be an important part of this wiki, but it won’t be everywhere. I began with the HoTT book because it is definitely mostly formalised, which means it is simple to add notes to an article detailing how it may have been implemented in coq etc.
I understand your confusion. This “implicit formality” has been the method of mathematicians for many years now so there is nothing new there. The only new thing is that we actually have evidence to show that it can be formalised. In fact I am willing to bet that in 20 years we will have programs capable of translating the natural language of “math speak” into formalised computer code. Part of the difficulty with set theory is that we had no way of “checking our program”. Take Russels work for example, nobody can actually sit down and check it. The difference with HoTT is that anybody could theoretically press run on their computer.
I am not personally all that convinced that categorical semantics developed enough to be useful from a type theory point of view. Take Haskell for example: it is a wonderfully expressive language with many useful (type theoretic) ideas however there is a lingering notion of “this is so because of category theory” which in most cases is completely nonsense. There is definitely cross polination going on but the full potential of such an interaction is definitely not realised (yet). I have heard Mike say that the “potential of HoTT is not fully realised”.
Similar to how the average analyst does not question set theory, I believe there are many people who just don’t care about foundational issues with HoTT etc. I think one of the main goals of this wiki will be to show how to do mathematics in HoTT. Not if the mathematics they are doing is consistent etc. How do we know that this is worth doing? Take a look at synthetic homotopy theory, there is currently an explosion of research in this area with new non-trivial viewpoints of classical results being realised. I think that this would be motivation enough for any mathematican to look at how to do their favorite mathematics in HoTT.
In general I’m with Alizter here. Type theory is a formal system (or rather, a collection of formal systems), but one doesn’t have to get “all the way to the metal” of those formal systems in order to do mathematics with a type-theoretic foundation, just as mathematicians do mathematics based on set theory informally without reference all the way down to ZFC. The whole point of the HoTT Book was to advance this point of view, and I like the idea of continuing it on the HoTT Wiki.
That said, the formal systems of type theory are also part of the subject of HoTT and should not be neglected. But I would rather not drop huge chunks of code from a particular proof assistant into the middle of entries. For one thing, such code is hard to read plain; it’s better-understood when interacted with interactively. For another, it privileges one proof assistant over another for no reason. If we want to include “more formal” versions of things (which is reasonable), I think we should just write them with the pencil-and-paper version of formal type-theoretic syntax with and , which looks like mathematics rather than code. We should of course include links to code when available.
I also don’t think it should be the task of the HoTT wiki to explain “ordinary” notions from mathematics. If even the basic idea of a notion is specific to HoTT, then of course we should explain it. But we shouldn’t spend time explaining what a functor is intuitively or giving lots of examples; if the reader doesn’t know that they should read about it elsewhere (e.g. on the main nLab, or in a category theory textbook). The point of functor (homotopytypetheory) should be to explain what’s special about the definition of functor in HoTT, from a HoTT perspective.
Also, I think we should be careful about pointing to the main nLab when it would be more appropriate to point to another page on the HoTT wiki, even if the latter page doesn’t yet exist. For instance, I think there ought to be a HoTT Wiki page about Coq, so we should point there even if it makes a gray link rather than to the main nLab page on Coq. Of course, we can and should point to main nLab pages when we want a reference explaining the “classical” point of view on something, either for the benefit of readers who may not be familiar with it, or to contrast with the HoTT version, or simply when discussing classical things (for instance, a page on categorical semantics might be using a classical metatheory).
Just a quick suggestion: could the Lemmas from the HoTT book be indicated more clearly as being such? Otherwise the numbering is a bit confusing if one stumbles upon the page, I would think?
1 to 18 of 18