is_zero_object

Stream: Is there code for X?

[Johan Commelin]

What is the best Prop-valued way of saying that an object in some category is a zero object. Do we already have an established way of saying that? Maybe something with subobjects?
cc: @Bhavik Mehta @Scott Morrison

[Bhavik Mehta]

You could say is_terminal X and is_initial X (I think these are prop-valued already)

[Johan Commelin]

is_initial : Π {C : Type u_4} [_inst_1 : category C], C → Type (max u_4 u_3)

[Bhavik Mehta]

My mistake! I have no objection to making these prop-valued since the data you get out of it is subsingleton anyway. Or, you can define is_zero_object X to mean nonempty (is_terminal X) and nonempty (is_initial X) - both options are good in my eyes.