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 added the HoTT introduction rule for ’the’, then added a speculative remark on why say things like
The Duck-billed Platypus is a primitive mammal that lives in Australia.
That sounds rather dubious, though. Do people really believe that any two duck-billed platypodes are equivalent? I’m also informed that the use of definite articles varies quite a bit between languages; purportedly Arabic uses ‘al-’ rather more than English uses ‘the’.
That sounds rather dubious, though. Do people really believe that any two duck-billed platypodes are equivalent?
Maybe. I like the idea, however, that generalized ’the’ has left its trace in natural language. Beyond the obvious case of a 0-type (i.e., set) with precisely one element, the next step would be a connected groupoid with singleton homsets.
Do people really believe that any two duck-billed platypodes are equivalent?
So any platypus finds itself in a number of different categories. But if I define an equivalence relation over animals according to species, then the class of platypuses (I can’t bring myself to write your Greek plural) is a contractible groupoid. Is it so very different to say ’The duck-billed platypus’ compared to ’The product of sets A and B’, alluding to a general representative known to have all essential features?
Yes, it would be interesting to look at other languages, e.g.,
Je vais souvent à la piscine le vendredi (I often go to the pool on Fridays).
I could convince myself that’s another equivalence class/connected groupoid.
Quick small edit: I disentabgled the technical statement about the formalization in HoTT from the discussion of examples by moving the last paragraph up and adding section headers.
Here the term t is one witness for the contractibility of the type A.
Might it be worth pointing out that, since IsContr(A) is itself contractible, one could say “(generalized) the witness for the contractibility of the type A”? Maybe that’s why we drop any trace of it in ordinary language.
I see the analogy, but I think it makes more sense to regard the “generic the” in natural language as an idiomatic way of making a statement about a type, rather than about an inhabitant of that type. To take your example, while it may currently be the case that there are no living platypuses outside of Australia, at some times in the past there have been such and in the future there might be again. Yet at such times I would still say “The duck-billed platypus lives in Australia” even though it is not the case of all platypuses; the statement is about the species rather than about all its inhabitants.
I guess the acid test is whether we use ’the’ in situations where we describe properties of the collective. “The kangaroo can be found throughout Australia.” “The average weight of the kangaroo is X kg.” (Even so, I might have opted for ’kangaroos’ in the first, and ’a kangaroo’ in the second.)
Anyway, I’ll scrap it.
Just for convenience: the
So strictly we shouldn’t say the set of cardinality 3 because the type of sets of cardinality 3 is not contractible? But the set of cardinality 1 is fine, in the same way that the terminal object in is fine?
I guess that’s like a situation with three intersecting lines on a plane. How many triangles are there? Would it matter if the triangle(s) were equilateral? Presumably that would depend on the way the type of triangles is introduced.
I can’t think of a realistic situation where someone says “the set of cardinality 3” (except where clear which set is being referred to). It definitely sounds strange.
Well, I guess I take that back in a sense: people do say, e.g., “the field of cardinality 25”, which I would declare wrong. (Notice “the field of cardinality 5” is fine.) “The field of complex numbers” is somewhat more ambiguous since it’s not obvious without some context that people aren’t thinking of the complex numbers as a topological field on which one does analysis, or as carrying a distinguished real subfield.
I think a slight abuse of “the” is unavoidable in field theory, because algebraic closures are only unique up to non-canonical isomorphism. However, once an algebraic closure is fixed, some things really do become well-defined up to unique isomorphism. For instance, given an algebraic closure of , there is a unique (up to equality) subfield of cardinality , for any positive integer . So that’s one sense in which really is “the” field of order .
Zhen: I agree completely with what you say after the first sentence. My impression is that the more careful writers (Serre, perhaps, or Lang when he is being careful) avoid “the algebraic closure of ”, before agreeing on one such as given.
Incidentally, David: I was very impressed by what you wrote here. I hope philosophers like Jeffrey take this in.
Re #13, thanks Todd. I wonder which group will learn quickest. Philosophers of maths exposed to how mathematics uses ’the’, ’same’, ’equality’, etc., or philosophers of physics exposed to configuration spaces really being groupoids.
Re #10: It’s very common to hear someone refer to “the cyclic group of order 3”, which as far as I can see is just as wrong (or as right, depending on your perspective) as referring to “the field of cardinality 25”, but is in my experience less likely to be pointed out as such.
Unless by “cyclic group” you mean a group equipped with a single generator.
True, though I’ve never heard anyone define it that way. (Which isn’t to say that that isn’t what they really mean, of course.)
Along those lines, one can cheat and say that “the set of cardinality ” is really a set equipped with a bijection to a distinguished -element set, say the von Neumann ordinal …
I’d actually like to see specific examples of what Mark is referring to, to have something to stare at and ponder.
If I heard anyone say “the set of cardinality ”, I’d almost have to assume they have in mind what Zhen Lin said in his last comment! :-)
How about at the level of categories? Are there common cases of ’The category of s’ where the category has nontrivial autoequivalences?
All the time! “The category of abelian groups” has an inner automorphism (), “the category of simplicial sets” has an outer automorphism ()…
And here, groups no, monoids yes.
Is anyone sensitive enough to this issue to be happy with ’the category of groups’, but not with ’the category of monoids’?
Re #20: I think I need more convincing that there’s an issue here. The category of abelian groups seems roughly comparable to the set , which I don’t have any problem with.
To put my comment in #23 a little more thoughtfully, here are some thoughts. None of which, if cogent, would be news to anyone here.
I don’t think existence of automorphisms is the precise issue. At bottom is the game we play: “two objects , are the same”. “The same how?” If and are judged (externally) to be the same set , then the answer to “same how” is of course by the identity morphism. If we have two sets , of cardinality that are not judged (externally) to be the same but simply have the same cardinality, then the question “same how” doesn’t have a distinguished answer: there is no distinguished element of . Thus “the set of cardinality ” rightfully sounds weird to us.
As for the category of abelian groups, it could be helpful to think of this as an Eilenberg-Moore object for a monad on , i.e., something universal with respect to appropriate data . That is, when people talk of the category of abelian groups, they really do mean (I think) not just the category given abstractly, but a concrete category equipped with some algebraic structure on , e.g., people always talk about the underlying set functor on abelian groups without turning a hair. Then the universal property of Eilenberg-Moore objects makes sense of the “the”.
This observation could be put more forcefully in the context of Morita theory. When we speak of the category of vector spaces over a field , we really do mean a concrete category; we don’t (perversely) mean the category of modules over the algebra , which gives an equivalent category of course but not concretely equivalent.
Todd, that makes sense. Perhaps rather like specifying which root of is in a complex plane.
By the way, was the category of abelian groups mentioned in #21 a good example? Aren’t I reading Peter Freyd on p. 31 of Abelian Categories to be saying that it has no non-trivial auto-equivalences? If so, we could think of the category of small categories instead.
Todd, you can find lots of examples of what I was referring by googling the phrase “cyclic group of order”, including this nice little paper. For many of the search results you can make a case that the cyclic groups are implicitly equipped with a single generator, but I don’t think that’s the case for all of them.
Thanks, Mark! I think I might have even glanced at that very paper in the context of a recent MO discussion (could have been MSE).
I suppose my reaction is just to smile at that. It’s a cute and pithy result after all, and somehow it doesn’t bother me to mentally supply “unique” with “(up to non-unique isomorphism)”, but maybe I need to pay closer attention to that reaction. Part of it may be that I see such a result as something cute but isolated, and not part of some bigger important structure theory. But I might be wrong about that.
I do want to think more seriously at some point about things like the representation ring of the symmetric groups, which looms large in mathematics but which, I think, largely elides over the issues under current discussion by passing straightaway to isomorphism classes of representations.
It’s just a question of whether the existential in the definition of cyclic group should be read as or . Mathematicians are used to thinking of “there exists” as meaning mere existence (), but I’ve argued elsewhere that that’s not always the most appropriate interpretation of what we actually do.
By the way, I agree entirely with Todd #23. Just like “the cyclic group of integers” is unproblematic, or for that matter “the automorphism group of ” whenever we know what is.
@David #25
You misunderstand. That only implies that every autoequivalence of is isomorphic to . But every inner automorphism is of this form, by definition.
I think I’m lost. I thought we were wondering whether or not is contractible.
I suppose at hlevel , we should say ’the’ of a proposition iff it is true. At least we say then
The fact that…
What Freyd shows is that is connected, not that it is contractible!
Returning to #31, if we adopt the line that to say ’the ’ of a type that we first require a witness to its contractibility, this should hold for a type which is a proposition. This may strike us as odd given the form of many propositions: ’The cat sat on the mat’, ’Paris is the capital of France’, etc. It hardly seems that we’d want to form ’The the cat sat on the mat’ or ’The Paris is the capital of France’, once we had a proof that the cat did this or that Paris has that status.
Hence the suggestion in #31 to opt for ’The fact that the cat sat on the mat’ and ’The fact that Paris is the capital of France’. But then, according to the schema, the types should have been ’Fact that…’.
Maybe it would help to think of a mathematical example, perhaps one where the bracket type operation has been applied. Let’s say I’d formed the type for two hsets. I then form the bracket type . From a judgement , I can form in the bracket type, and know that any other term of that type is equal to it.
What would be the natural language version of all this? is the type of isomorphisms between and . So how should I say ? ’ is isomorphic to ’ suffers from the problem above that we can’t prefix with ’the’. Is it better then as ’Fact that and are isomorphic’ or ’’s being isomorphic to ’ or something else?
The first of these would at least allow ’The’ in front, while the second would require us to modify the ’generalized the’ rule to pass from to .
Am I really inclined to say of that it’s ’The fact that and are isomorphic’?
Odd that such a simple case doesn’t appear to have a simple resolution.
Regarding your first lines, it would seem to me that there is no problem if one understands – as you had in fact been highlighting – that most sentences we speak are implicitly in some context.
For instance when in France one may easily say “Paris is the capital” with the qualifier “of France” implicitly understood. And since there is precisely one capital of France, with that qualification the use of “the” seems to fit the proposed formalization here.
Of course, there’s no problem with ’The capital of France’ since ’Capital of France’ is contractible. I was wondering what to do with a proposition, i.e., declarative sentence. Or do I misunderstand your point?
’The’ is straightforward for a type which is a singleton set, or a contractible groupoid (e.g., the type of products of A and B), but seems odd applied to propositions. I have a feeling there’s something relating to the initially odd feeling of applying necessity and possibility to general types, when they feel most at home with propositions. Although we readily descend 2-groupoid, groupoid, set, proposition, it somehow feels different the last of these stages.
To pose my problem another way, let’s take the type ’Cat’. How should I speak of its bracket type? It’s by definition a proposition. Given
I also have a term
According to what we have at generalized the, we should say
(not bothering about unnecessary witnesses to [Cat]’s contractibility to isinhab(tibbles)).
So now how can I write that equation in natural language?
Ah, now I see what you are after.
I’d describe it like this: Let’s consider a type and have be a -dependent type. Then saying “the capital” while it is understood that we are in France means not making the global statement
(where I leave the dependent sum notationally implicit) but means making the statement-in-context
Re #26
you can make a case that the cyclic groups are implicitly equipped with a single generator, but I don’t think that’s the case for all of them.
when thinking about modular curves, one considers the moduli spaces which are elliptic curves with a specified cyclic subgroup of order , but, importantly, without a generator. Equivalently, it can be seen as the space of elliptic curves equipped with an injective map . Such a thing has a -action given by precomposing with an automorphism of .
By the way, there is an Lab entry on this at level structure on an elliptic curve (though the section for the case “Over general rings” consists only of pointers to references, for the moment)
Re #36, I don’t think you’ve got my point yet. At generalized the we say
The notion of a “generalized the” can be formalized and treated uniformly in homotopy type theory. Here one can define an introduction rule for the as follows:
My point is that this rule as stated applies to any true proposition.
But it sounds odd to say
Is there anything you could put in for “” that wouldn’t sound odd in ordinary language?
Oh, I see, sorry.
But what’s wrong with saying, as you suggested above, “Fact that ” for the propositon , such as to have its essentially unique witness naturally read “The fact that ”?
This “Fact that ” is an “escaping” just like “ is true” and, as we discussed the other day, by propositional extensionality they are equivalent and may be freely interchanged.
Re #40 No, but that in a way is my difficulty when trying to convince colleagues of the h levels hierarchy’s way of considering propositions to slot in neatly below sets, which are themselves below some things they haven’t heard of, called 1-groupoids. I can awaken them to the idea that contractible groupoids warrant the use of ’the’ as in ’the product of A and B’, as a generalisation of ’the’ used in the context of singleton sets. Then when I turn to true propositions, things seem different. Why can’t I tell them how to say in familiar fashion the unique term when it comes to those things they feel they know best of all, namely, propositions?
I can’t even settle on a reading of . I think I persuaded Urs to change his term for the bracket of the dependent sum of paths in dcct from ’there is a path’ to ’that there is a path’ (p. 480 of latest version):
- in logic it means “that there is a path”;
- in type theory it means “the collection of all paths”;
- in homotopy-type theory it means “the collection of all paths with gauge transformations accounted for”;
- finally in linear homotopy-type theory it means “the sum of the phases of all possible paths”.
Was that for the best?
Once propositions don’t seem like they belong to the family, why should they buy into our extension of from -dependent propositions to general -dependent types. Sure terms of type , for world-dependent sets , do seem to resemble their beloved ’rigid designators’, and perhaps I could push ’Nixon’ as a ’necessary person’ if there are counterparts in all worlds. Maybe even one can glimpse the necessity of group invariants in the context of the looped group. But does all this really resemble the simple ’It is necessary that…’, applied to a (world-dependent) proposition?
So there’s my bind. Why should they believe my positioning of propositions in the hierarchy when we seem to treat the level, which they feel they know best, differently from the others?
Re #41, ah I had loosely felt there is something similar to the ’name of’ or constructions. “Fact that P” could of course be uninhabited, preventing us from forming “The fact that P”.
As a mathematician, of course, it seems odd to me that people would get hung up on what is essentially a linguistic issue, depending on accidents of the historical development of human language, that has nothing to do with the underlying structures. But I suppose not everyone is a mathematician. (-:
“Fact that” (or similar constructions such as “witness that” or “proof that” or “reason that”) has the additional virtue of according with the standard type-theoretic convention (often observed in the breach) that the name of a type should be the singular noun designating its elements, e.g. for the universe (rather than something like or ). I guess that’s also why it works with the rule for generalized the.
It seems that David is after something in the spirit of the “informal HoTT”-program, where the goal is to match established informal language as nicely as possible to the formal language. While this is not part of the maths but part of the mathematicians (as linguistic historical creatures) it may still be useful.
And, for whatever it’s worth, doesn’t it work nicely in the case at hand with “The fact that…”? One could imagine combining it with the analogous informal-HoTT from the book, such as in saying things like: “Since is a mere proposition, the fact that it is true in this context serves to witness … (this or that).”.
But I suppose not everyone is a mathematician. (-:
Blame Frege and Russell and other for imagining that logic could resolve confusing natural language expressions.
Lots of topics to pass to now, though you mathematicians might want to look away. For instance, what of negative facts, those facts that make negative statements true? E.g., what kind of fact makes ’Mike is a philosopher’ false.
I guess that from the type ’Fact that P’ and its corresponding , we also have ’Fact that not P’ and .
Hmm, from here
A fact … is taken to be some kind of existent in the world… . But … can it really be a fact in the world that there is no hippopotamus in the room? This sounds like an absence of a fact, and an absence is nothing at all. (2007, 46)
So form dependent sum ’Hippopotamus in the room’, then bracket type ’There is a hippo in the room’, then [There is a hippo in the room, ] = There is no hippo in the room, a perfectly good proposition. Taking , this is ’Fact that there is no hippo in the room’. So a term of this type is a function taking a witness of there being a hippo in the room to a term of the empty type. That doesn’t sound like an absence.
A fact that there is no hippopotamus in the room doesn’t sound to me at all like the absence of a fact. There’s no reason that “fact that not” should be the same as “not fact that”, any more than “proof that not” is the same as “not proof that”. A constructivist point of view may be helpful; saying that we can’t prove or assert something is not the same as saying that we can prove it false or deny it. And as you pointed out, the type-theoretic perspective bears that out; a “fact than not” is a real thing, a reason why the truth of such a statement would be contradictory. (One might also bring in the occasional constructive necessity for “positive” versions of facts that are classically negative, e.g. apartness.)
’Conditional facts’ are also the subject of debate, but taking negation the constructive way, places them together.
I guess a lot of proofs of propositions are projections from higher up the hierarchy. I mean rather than look for a reason why the truth of a bracket type is contradictory, we look for a map from the original type to the empty type, then project.
So is the same as .
I don’t understand your notation.
The bracket type of a function type for two types, and , is the function type for their bracket types. Hmm now I’m starting to think that might not be right.
But anyway the general wondering was about ways of proving propositions via truncation from functions.
Oh! I see: you were using the notation for the function-type and also the notation for the bracket-type. Bleh! (-: I would write that question as “is the same as ?” And in general, I’m pretty sure the answer is no, although I don’t have a counterexample off the top of my head. However, it is true if is already a proposition (such as ), since in that case we have and , and the universal property of truncation .
Off topic, but… a friend of mine met Jacob Lurie back in the 90’s at an event related to the Intel Science Talent Search competition that Lurie won, and he remembers Lurie for 2 reasons: 1. b/c he was smart 2. b/c he introduced himself (or signed some paper) as “Jacob The Lurie”.
It’s not true that the formation of bracket types commute with the formation of function types. For instance, consider the slice over , take to be , and take to be the connected double cover of . Then has no global elements, whereas does.
@Zhen, I think what you say is not sufficient for a counterexample, since might have a global element even though does not. And indeed, since is (in the slice over ) the terminal object, we have , and as well.
Ah, of course: is equivalent to the propositional axiom of choice, . In particular, it is implied by LEM, hence holds in and any slice of it; but it fails for instance if the world’s simplest AC fails.
Back to #1 and ’generic the’:
How about characterising this to fall under our the introduction rule by using bracket types? Some properties applicable to wombats won’t hold for all wombats, or in other words a map need not factor through . However, properties that do apply generically to all wombats do so factor.
is a singleton, as is an extant species, and any specific wombat provides its element, . Then perhaps when we say ’The wombat is noctural’, ’the wombat’ is formed by ’the introduction’,
for a proof of contractibility. Convincing?
I still find #6 more convincing. Maybe we could subsume that under “the-introduction” by considering the type as the (unique) inhabitant of the universe of all “types of wombats”…
I guess we do tend to use different words with the two ’thes’. From here:
And
On the other hand, perhaps the use of different language in #59 is telling. The second sentence in each case does really seem to be about the type not any specific or generic element. Turing performed type formation. So then why use the same language ambiguously for an individual and a type?:
5.43. A generic sg [singular] with the definite article is very frequent, though in itself ambiguous: the origin of the ballad may refer both to the individual ballad we are just discussing, and to ballads in general as a literary species; in the latter case the ballad stands as a (typical) representative of the whole class. (Jespersen (1954, Part II, §5.43)
Hmm, ’the ballad’ seems more like ’the computer’. I should have thought Jespersen could have made a better case for the ’typical representative’ idea for animal species, etc. – ’the tiger has stripes’.
Then what of ’A tiger has stripes’? Does anything correspond to the inhabitant of the bracket type?
But with M-theory being cracked and a new dependent type 2-theory emerging, perhaps there are bigger fish to fry.
Yeah… this sort of thing is fun, but I have limited brain cycles to spend on trying to fit the quirks of natural language into mathematics… (-:
For all the concepts of theoretical knowledge constitute merely an upper stratum of logic which is founded upon a lower stratum, that of the logic of language. (Cassirer 1925, p. 28)
Language and Myth, 1925, translated by S. Langer, Dover 1953.
re the Cassirer quote: Language, sure, but not our “natural” language! That would be like building a skyscraper on a foundation of slum huts. You want to remove the contamination by the random, the biological, the historical from language, and retain only its essence. At least if you are interested in type theory as such, as a formal language. Instead of trying to squeeze the quirks of common English into dependent type theory, what, I think, you’d rather want to do is practice dependent type theory as a new language for philosophy; not a subordinate translation of the ill-suited natural English (or other), but as the new native language, the analogue of what modern mathematics has become for, say, geometry. The goal would be to practice philosophy in terms of DTT the same way that we practice differential geometry in terms of tensor calculus; and then to turn the insights into natural English only for the purpose of prefacing your publications or for talking to the journalists.
Well, I rather rather think that depends on what you take the tasks of philosophy to be. It was unfair of me to quote Cassirer out of context. He certainly doesn’t imagine you building your M-theory on structures we find in natural language. He does have the idea of mathematical ideas taking their point of departure from everyday cognition, and says some interesting things on the Erlanger Program as a certain culmination of a departure in thought from common capacities to perceive invariance in the world (object size, colour under varying light, etc.)
But this wouldn’t exhaust his interest in language that DTT, say, could be seen as a purified and extended calculus with seeds in natural language. He sets himself the task of charting all of our ’symbolic forms’ - myth, language, art, science, history, technology, religion - and their relations. The book I’m quoting from looks to understand how language and mythical thought could ever emerge.
May I ask what you had in mind in the following, David?
But with M-theory being cracked and a new dependent type 2-theory emerging, perhaps there are bigger fish to fry.
May I also ask about your own view on the following, and how you see your thinking about natural language as fitting into it?
Well, I rather rather think that depends on what you take the tasks of philosophy to be.
looks to understand how language and mythical thought could ever emerge.
I rather like the following passage from the Zhuangzi, in the translation of Gia-Fu Feng and Jane English.
Among the ancients, knowledge was very deep. What is meant by deep? It reached back to the time when nothing existed. It was so deep, so complete, that nothing could be added to it. Then came men who distinguished between things but did not give them names. Later they labeled them but did not choose between right and wrong. When right and wrong appeared, Tao declined. With the fall of Tao, desire arose. Is there really rise and fall? When there is rise and fall, Chao Wen plays the lute. When there is no rise and fall, Chao Wen does not play the lute.
Chao Wen played the lute, Shia Kuang kept time with a baton, and Hui Tsu leaned on a stump and debated. Each of these three masters was nearly perfect in their own art. Their names will be remembered forevermore. Because they excelled, they were distinguished from others. Because they excelled, they wanted to enlighten others through their art. They tried to teach what could not be taught. This resulted in obscure discussions as to the nature of “hardness” and “whiteness”.
Re #65,
Just look at three texts published within the years 1927-29 and see if you can discern what philosophy is about:
All come from German-speaking countries. All meet in Davos in 1929, Cassirer and Heidegger to converse in public, while Carnap attended. Carnap later added to his book “Scheinprobleme in der Philosophie”, translated as “pseudoproblems in philosophy”, where Heidegger becomes a target.
Heidegger is still highly regarded in Continental Europe. Carnap more in the Anglophone world. Cassirer is rather neglected now.
Diversity doesn’t stop there. From a similar geographical background and time (though published later), we could add
Urs @ #63 could be Carnap reincarnated. I will always retain a fondness for Cassirer.
I should add, despite obvious comparisons:
The scientific world conception is characterised not so much by theses of its own, but rather by its basic attitude, its points of view and direction of research. The goal ahead is unified science. The endeavour is to link and harmonise the achievements of individual investigators in their various fields of science. From this aim follows the emphasis on collective efforts, and also the emphasis on what can be grasped intersubjectively; from this springs the search for a neutral system of formulae, for a symbolism freed from the slag of historical languages; and also the search for a total system of concepts. Neatness and clarity are striven for, and dark distances and unfathomable depths rejected. In science there are no ’depths’; there is surface everywhere: all experience forms a complex network, which cannot always be surveyed and, can often be grasped only in parts. (Wissenschaftliche Weltauffassung 1929)
and
You want to remove the contamination by the random, the biological, the historical from language, and retain only its essence. At least if you are interested in type theory as such, as a formal language,
there is also the Hegelian side of Urs, where the Logic is not just a neutral vehicle for expressing concepts, but the very source of the concepts we need to understand the world.
Thanks! I am familiar with the texts you mention of Heidegger and Wittgenstein, not with the others. But I don’t think there is any dispute that there is diversity in views of what philosophy is! I was asking more about your own view, and how your ruminations on language fit into that. Was the following your answer?
I will always retain a fondness for Cassirer.
There’s still a considerable industry in people trying to understand the ’logic’ of our natural language. I was never much into this, and was happy to go along with the followers of the later Wittgenstein that natural language is a highly flexible, context-dependent way of communicating, instructing, promising, etc., which no formalism was likely to capture. However, since the dash to dependent type theory around these parts, I’ve been interested to see whether it would fare better than first-order logic, and have come to think that indeed it does.
Who would have thought that in the use of such a basic word as ’and’ one could see dependent sum lurking - “It’s raining and heavily”? And there’s the seed of the idea of a fibre bundle. Instead of a point in the base space, and then a point in its fibre, we have a warrant that it is raining and then a warrant that the rain is heavy.
This tallies with Collingwood’s idea that we don’t have free-floating propositions, but only ones formed in some kind of context. Where Russell takes “The present King of France is bald” in a context free way, and so expects a Yes or No, we can say with Collingwood, that the question ’Is the King of France bald?’ doesn’t arise, since there isn’t such a person to ask this question about. The context structure of dependent type theory, and its formation, introduction, elimination rules, makes good sense again of how we think and speak.
Although we were looking to spare Mike’s brain cycles (#61), let’s see if I can engage them some more. This isn’t just about something wholly non-mathematical – you spend your lives speaking about mathematics in informal ways, and presumably expect that it should possible to make what you say rigorous.
A referee for my ’the structure of’ paper suggested that when we say “the cyclic group of order 6 has an element of order 3”, we are using the generic ’the’, i.e., the one used in ’The wombat is nocturnal’, where I was pressing for a definite description. If he’s right, whose generic ’the’ do we prefer?
Recall we have
Definite ’the’: For a contractible , ’the ’ is the unique element of .
Generic ’the’: Two HoTT possibilities:
(a) ’the ’ refers to the type (definite description of the type)
(b) , where may have many members (definite description of the generic element of the bracket type)
So what do we have in the following?
Turing invented the computer
Turing repaired the computer
Griess discovered the monster group
The first seems to be Generic (a), suggesting that the third is too. And you might take the following as both Generic (a):
There are two bears in Alaska: the grizzly bear and the black bear.
There are two groups of order 6: the cyclic group and the symmetric group on 3 objects
But then why did we go to the bother of defining definite ’the’ as the unique element of a contractible type? Why not always think in terms of Generic (a)? Isn’t it because there are times when we seem to be speaking about elements not types:
Types don’t hibernate or have vertices, its their members which do. Generic (b) allows something closer to this, and coincides with Definite ’the’ for a contractible type.
“There are two bears in the zoo”
So that’s ambiguous between there being two animals which are bears, and there being examples of two species of bear found in the zoo.
I think that referee is wrong. (-:
I have streamlined and slightly expanded the wording in the second paragraph of the Idea-section.
In John’s edit, I have hyperlinked also “James Dolan” and moved the item to the top of the list of references.
in version #23 “chicksgold” added spam links in the added text (down in the redirects)
Spanish Version by ChicksGold
in version #24 “Rosselyn Evies” edited that text to add a period.
I removed that spam. Also Rosselyn had added spam to first uncountable ordinal which Urs removed. However “test” has recently added that spam back which I will fix next.
EDIT: “Dr.Wilson” was also involved in this spam effort but didn’t leave any lasting damage.
Dr Wilson also had fiddled with the page on Nicola Gambino. An ‘also’ had been added. I rolled back the entry.
1 to 77 of 77