adding standard rules for isProp

Anonymous

]]>added links to subsingleton, subterminal object, and propositional truncation

Anonymous

]]>adding rules for isProp which does not involve product types

Anonymous

]]>adding natural deduction syntax rules for isProp; not sure how to define these without product types

Anonymous

]]>I don’t know a particularly slick way.

]]>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?

]]>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’.

]]>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.

]]>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. (-:

]]>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’ve merged them.

]]>No, a (-2)-groupoid is a concept in category theory, whereas a contractible type is a concept in type theory.

]]>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.

]]>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 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.

]]>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-propositionas well as that of(-1)-truncated homotopy typeand(-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.

]]>None.

]]>What's the difference between this and an h-proposition?

]]>an entry for *mere proposition* had been missing. Created a minimum, just so as to satisfy links.