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.
an entry for mere proposition had been missing. Created a minimum, just so as to satisfy links.
What's the difference between this and an h-proposition?
None.
I had said that explicitly at h-proposition but apparently not at mere proposition. Have added now the following:
This is the same concept as that of h-proposition as well as that of (-1)-truncated homotopy type and (-1)-groupoid (if these are understood in the general context of geometric homotopy types).
The terminology “mere proposition” is meant to better work in informal language in view of the propositions as types interpretation, where every type $X$ “is” a proposition in a way, or rather represents a proposition, namely the mere proposition which is its (-1)-truncation isInhab (X).
I seem to remember that the h-level terminology got sort of deprecated. In any case, we have similarly duplicating entries for (-2)-truncation (true, unit type, contractible type). I’d think it’s okay, but of course if anyone feels like rather merging these entries, I won’t object.
The duplicating entries for (-2)-truncation actually mean different things, e.g. the unit type is a particular type with a particular definition, whereas being contractible is a property of an arbitrary type. But h-proposition and mere proposition are synonyms, so I think the pages should be merged.
That's my thought as well, but I wasn't sure whether it was true that they are synonyms, so I'm glad that you answered that.
The difference between -2-groupoid and contractible type is quite similarly not in the technical meaning but more in which reader my end up looking for which term.
But if you have strong editorial feelings about this then you probably have the energy to reorganize it.
No, a (-2)-groupoid is a concept in category theory, whereas a contractible type is a concept in type theory.
I’ve merged them.
Hey Mike, I am not sure if we should stage arguments in this form over what are less than trivialities. Please have it your way, you are welcome. I suppose you have a strong feeling of ownership of this topic and its incarnation in words.
As you know, there were once people who titled their article “Types are omega-groupoids”, there are equivalences justifying this language, there are good reasons to emphasize the equivalence over the superficial differences. There are different styles of talking, but as long as there is no substantial issue, maybe we can relax a bit?
I’m not angry or annoyed, sorry if I gave that impression. I just have less time than usual to spend carefully phrasing my comments to avoid unintentionally giving offense. Sorry. (-:
The point I’m making, if it matters any more, is that “mere proposition” and “h-proposition” mean literally the same thing by definition, which is not the case for any of the other pairs of concepts you’ve mentioned.
To me, it also matters that ‘mere proposition’ and ‘h-proposition’ are used by the same people in the same context, which isn't so for ‘$(-2)$-groupoid’ and ‘contractible type’.
I can convince myself that $\prod_{x\colon A} \prod_{y\colon A} (x=y)$ and $\prod_{x\colon A} \prod_{y\colon A} isContr(x=y)$ are equivalent, but is there a nice slick way to show this?
I don’t know a particularly slick way.
added links to subsingleton, subterminal object, and propositional truncation
Anonymous
1 to 20 of 20