1
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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, $\endgroup$ Dec 21 '15 at 2:08
1
$\begingroup$

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

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Oak
    Dec 20 '15 at 23:18
  • $\begingroup$ 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. $\endgroup$ Dec 20 '15 at 23:51
  • $\begingroup$ 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? $\endgroup$
    – Oak
    Dec 21 '15 at 6:25
  • 1
    $\begingroup$ I would recommend that you ask such questions on the HoTT Cafe group, which is devoted to HoTT beginners. $\endgroup$ Dec 21 '15 at 9:40
  • $\begingroup$ For the record, Mike Shulman answered the question at the HoTT Cafe group at groups.google.com/forum/#!topic/hott-cafe/7vVdLfzZP90. $\endgroup$ Dec 22 '15 at 14:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.