In homotopy type theory, if the identity type A=B is non-empty, can we conclude that A and B are also non-empty? If not what constarints can be put on the identity type or A and B in order that the above statement becomes true for them.
Update: As Andrej Bauer has mentioned in the answer below, a better variation of this question would be: if the identity type A=B is inhabited, can we conclude that A and B are also inhabited?
In other words, assume we know that A=B is inhabited. What constraint can be put on A=B in order that we can conclude A is inhabited? If there are such constraints then what will be the minimum constraint that is sufficient to draw the conclusion that A is inhabited? By constraint I mean things like A=B having at least two distinct elements or A=B being infinite and alike.