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.
Is the current arrangement optimal? We have ’setoid’ redirect to Bishop set, while the most said about them is in equivalence+relation#setoids.
Running about the loops of links, I can’t see a way to the thought that Bas made
An important advantage of HoTT is precisely that we do not need setoids anymore.
That presumably relates to “Our proof … avoids setoids by using pushouts and univalence” (HoTT book, p. 364) and quotient sets constructed via HITs.
Please somebody polish these entries. I remember I stopped editing them, way back, when some experts here complained about my text on Bishop sets.
Regarding that claim you cite: this is just the statement that I recently recorded at quotient type – From univalence: adding univalence to the type theory makes the long missing quotient types available, by the type-theoretic version of the old argument that a subobject classifier in a (what is it) regular category induces quotients.
This is one of the big points of why univalent HoTT is interesting, apart from its homotopy-theoretic semantics. I had once recorded this here, together with other facts at the entry called “homotopy type theory FAQ”.
That entry I stopped editing after receiving complaints about an expanded version of this claim here, complaints which I never understood, I guess they were of political nature, alas.
I still think this FAQ would be, or would have been, immensely useful to provide. Everywhere you turn on the web you see people confused about items that this FAQ was aiming to list the answers to. But maybe there is something intrinsic here that makes the communication impossible. Anyway, I am no longer looking into editing this. But it would be just the place to record answers such as to issues in #1.
When you touch on fundamental tenets of faith, I suppose these things are likely.
I’d rather we adopted a robust nPOV, with notes to the effect that other doctrinal interpretations are available. There have been other occasions where I’ve felt we let ourselves get somewhat overrun. E.g., necessity+and+possibility#the_s4_axioms was interposed without good nPOV rationale.
I fully agree regarding the necessity page. You could just revert that edit (maybe preserve it elsewhere). In principle I could, too, but then it might look like an edit war. But you are more neutral in this issue, and if you feel there is a way to improve the page by moving parts of it to where it finds a better home, then you should do it.
(Which “tenets of faith” are you referring to?)
I agree that setoid deserves its own page. I don’t quite understand/remember what the objection was at the necessity/possibility page though; everything there right now looks fine to me.
Regarding a HoTT FAQ, it occurs to me now that possibly the disagreement came partly from the fact that everything on the nLab has the nPOV, whereas HoTT has its own POV (in fact, a multiplicity of such POVs). So writing a FAQ about HoTT from the nPOV is one thing, but when you call the page “homotopy type theory FAQ” readers might easily be forgiven for missing the fact that this is just one POV on HoTT, leading them to object that their POV is not represented or respected.
My intention at the would-be-HoTT-FAQ was to give a perspective appealing to many different points of views, not just to one. That’s why each item had subsections
For laymen
For set theorists
For type theorists
For homotopy theorists.
I had thought it would be good to pick up each of these groups of people right where they are.
The problem arose when I added to the page under “Why should I case – For set theorists” some paragraphs on the beautiful fact that HoTT is conceptually simpler than set theory in the technical sense that instead of starting with FOL and then adding the set theory axioms to it, one remains at the level of FOL, just removes the restriction that all types are props, and then discovers sets without needing further axioms, besides UV.
I believe many people who care about foundations, as laymen or as prefessionals, would be delighted to learn about this fact.
But somehow me writing this into the Lab triggered you and Bas Spitters to complain. (The relevant discussion starts here). I never understood what the complaint was, except that I sensed you were afraid that voicing this truth might be politically incorrect . Finally I dug out a previous blog comment of yours where you said just the same (here). I just think if you would put that statement (or any wording of it that seems more appropriate) into a survey page like a HoTT-FAQ page on the Lab, you’d do humanity a considerable service. I won’t try anymore. But you really ought to do it.
Which “tenets of faith” are you referring to?
I mean those coming out of the various constructive traditions. The “meaning explanation” seems to derive from one of these traditions, though its importance is rather obscure to us nPOV-ers.
Regarding the necessity/possibility page, it doesn’t make much sense that it turns straight to S4 without motivation. I’ll move that to the logic S4(m) at some point.
Given the fact that you failed to understand the points we were making at the time (and to be fair, I failed to understand some of the points Bas was making myself), there doesn’t seem any point in trying to re-have the discussion now.
1 to 8 of 8