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, 2015 at 2:08

1 Answer 1

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, 2015 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, 2015 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, 2015 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, 2015 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, 2015 at 14:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .