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've seen two meanings for this term, and they are both at limit point, along with a family of other terms for various arity classes.
Nice! Unfortunately, though, is not an arity class – arity classes have to contain 1. Maybe this is somewhere where you really do want a regular cardinal rather than an arity class?
Why ’indexed subset’ rather than ’family’?
Finally, for the HoTT book we settled on ’disequality’ as a name for negated equality, on the grounds that ’inequality’ is commonly used to refer instead to and . Apparently ’disequality’ is not uncommon among type theorists. We might want to consider this issue for the nlab.
Actually, it’s not obvious to me why you even want to exclude singular cardinals. Not that I have any idea what use the notion would be for cardinals larger than , but at least it doesn’t seem to collapse into triviality or anything at a singular cardinal. Does it?
Unfortunately, though, is not an arity class – arity classes have to contain 1. Maybe this is somewhere where you really do want a regular cardinal rather than an arity class?
H'm, yeah, that should be the arity class , only that doesn't give us the correct result. (It gives us that is an accumulation point of if it is an adherent point, I think, which is not an interesting condition.)
Why ’indexed subset’ rather than ’family’?
More likely to be immediately understood, and implying that repetition is irrelevant.
for the HoTT book we settled on ’disequality’ as a name for negated equality
In constructive mathematics, I see ‘inequality’ a lot. But this is a generic term, not necessary negated equality (which is called ‘the denial inequality’). In general, an inequality could be any irreflexive symmetric relation, although one often restricts to tight inequalities.
it’s not obvious to me why you even want to exclude singular cardinals
I was thinking that you turn a -ary family of -ary families into a single -ary family, so may as well assume that is regular, but maybe not.
I’ve never heard of an “indexed subset” before, but I know what a “family” is.
But ‘family’ is ambiguous; what if I say ‘indexed family’?
Is there a “non-indexed” kind of family? I’ve never heard of one.
Yeah, I often see ‘family’ used to just mean a set (or class, or subset, whatever). It's an informal usage, along with ‘collection’ (and ‘class’, sometimes, when that's not being used for size distinctions). More careful people use it in the indexed sense.
I think Toby means ’indexed family’ in the context of a collection of families indexed by another set.
Huh. (-:
I was thinking that you turn a -ary family of -ary families into a single -ary family, so may as well assume that is regular,
This is indeed wrong. Given a -ary family of -ary families, each family has an element out of it, giving a -ary family of these exceptions (using choice!), which then has its own exception, but that need not be out of the union of the original families, so regularity is not relevant. (I already changed the text to deemphasize arity classes.)
The definition of accumulation point was wrong, so I had to redesign things slightly. It should be working now.
1 to 12 of 12