# 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.

• I am sure that others understand your question. In my case I would need a clearer formulation. I know the homotopy equivalence but otherwise I am in logical dark, Dec 21 '15 at 2:08

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).

• Thank you so much! Variant 4: Suppose A=B contains more than one element. Does it follow that A contains elements determined by the elements of A=B i.e. if x and y are two distinct elements of A=B then x implies the existence of a in A and y implies the existence of c in A such that a is not equal to c?
– Oak
Dec 20 '15 at 23:18
• It is possible for $A = B$ to have infinitely many different elements, but for all $x, y : A$ we have $\lnot (\lnot (x = y))$. The circle is an example. Dec 20 '15 at 23:51
• Thank you! do you think it is a good idea to ask variant 2 as a separate question here on math.stackexchange or on mathoverflow? Also I am interested to know on which condition A=B's being inhabited, can imply that A is inhabited with infinitely many elements. I mean putting which condition on A=B can guarantee that A will have infinitely many elements? Does such a condition exist?
– Oak
Dec 21 '15 at 6:25
• I would recommend that you ask such questions on the HoTT Cafe group, which is devoted to HoTT beginners. Dec 21 '15 at 9:40
• For the record, Mike Shulman answered the question at the HoTT Cafe group at groups.google.com/forum/#!topic/hott-cafe/7vVdLfzZP90. Dec 22 '15 at 14:56