nonempty vs inhabited

Stream: new members

[Winston Yin]

How should I decide to use nonempty or inhabited in general?

[Winston Yin]

In my current case, I'm trying to define "decomposability" of a representation by first defining decomposition r of some representation r as a structure containing an isomorphism to a direct sum representation, and then defining decomposability to be nonempty (decomposition r).

[Kevin Buzzard]

One is Prop-valued, one is Type-valued, right? I usually go for the Prop-valued one which minimises the chance of diamonds

[Eric Rodriguez]

and if you need the member, there's nonempty.some or inhabit (I think at representations, you're probably far past computability :b