Identity type between A and B being non-empty implies non-emptiness of A and B? 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.
 A: The empty type is equal to itself, i.e., $\mathsf{refl}_0 : 0 = 0$, so the answer to your question is negative.
We could consider several other variants of your question. NB: A type $A$ is empty if $A \to 0$ has an element; it is non-empty if $(A \to 0) \to 0$ has an element; it is ihabited if $A$ has an element. Also, in type theory there is no difference between "there exists an element" and "we can construct an element".

Variant 1: Suppose $A = B$ contains two distinct elements. Does it follow that $A$ is non-empty?

If $A = B$ and $A$ is empty then so is $B$ (because it is equal to $A$), hence $A = B$ is equal to $0 = 0$ which contains exactly one element $\mathsf{refl}_0$. Thus, if $A = B$ contains two distinct elements, $A$ and $B$ are non-empty.

Variant 2: Suppose $A = B$ contains two distinct elements. Does it follow that $A$ contains an element?

This is a better variant than the first one. I do not have an answer at the moment.

Variant 3: Suppose $A = b$ contains two distinct elements. Does it follow that $A$ contains two distinct elements?

No it does not, consider $S^1 = S^1$ where $S^1$ is the circle (as a higher inductive type).
