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.
In section 3.5 of the HoTT book it considers
is a family of mere propositions
and then forms the dependent sum . Then as to whether to call this a subtype, it says
We may also refer to itself as a subset or subtype of ; this is actually more correct, since the type (3.5.2) [the dependent sum] in isolation doesn’t remember its relationship to .
What does ’in isolation’ mean here? Can the dependent sum be given without information about how it has been constructed, and so then with its projection to ?
I’m looking at this as I’m still tweaking my ’the structure’ paper, and was thinking that many uses of ’the’ arise when a above gives rise to a singleton (or contractible) .
Well, once we construct the dependent sum, it is just a type. Remembering how it was constructed is tantamount to remembering itself or the projection to .
For instance, every element of a set defines a singleton subset of that set. But as sets in isolation, each singleton is isomorphic to each other singleton. It’s only when we consider them together with their predicates or inclusions to the original set that they are distinguishable.
Ah good, thanks. That makes splendid contact with something that was said at the last Bristol conference on Philosophy and HoTT.
Recall that idea of mine that we might try to make sense of ’the structure of ’ as arising from a contractible type
Structure of := .
The objection was raised that this entails that all ’Structure of X’s are identical as each is contractible.
So I could have , . The dependent sum from this is my ’Structure of ’ and is contractible, hence we can introduce the element
the structure of : Structure of .
Returning to the ordinary language case of a singleton subtype. Say I have a type , and a predicate := Sitting on this mat’ which applies to only one cat. Then the dependent sum ’Cat sitting on the mat’ is a singleton, so a candidate for ’the introduction’.
But maybe I’d be better off remembering the projection to and arrange things so that ’the cat sitting on the mat’ is in fact an element of rather than of .
So a general rule for ’the introduction’ could be that when we have and the dependent sum is contractible as witnessed by , and (along with proof that any other element in the dependent sum is equal to , then
the that is := .
In the Structure case, this would give me ’the structure of ’ as an element of , and I can choose any type equivalent to .
Considering, say, the predicate on cats of being black. When I say ’The cat sitting on this mat is black’ am I coercing along the projection from the dependent sum, or is ’the cat sitting on this mat’ already just a cat?
Coercion is maybe quite common anyway, and I’m further mapping that cat to where Black is first defined.
Makes sense.
There probably isn’t a unique way to analyze any English sentence to decide which maps are coercions and which aren’t.
1 to 7 of 7