Zulip Chat Archive

Stream: new members

Topic: nonempty vs inhabited

Winston Yin (Jun 11 2021 at 06:30):

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

Winston Yin (Jun 11 2021 at 06:31):

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 (Jun 11 2021 at 06:57):

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 (Jun 11 2021 at 09:02):

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

Last updated: Dec 20 2023 at 11:08 UTC