Equal indexed inductive types implies equal indices

Question

Let's have an inductive type foo indexed by x : X.

Parameter X : Type.

Inductive foo : X -> Type :=
| constr : forall (x : X), foo x.

I'm curious, if foo x = foo y implies x = y. I'm out of ideas how to prove this.

Lemma type_equality_implies_index_equality : forall (x y : X), foo x = foo y -> x = y.

If this can't be proven, why?

Answer 1

It cannot be proved. Consider the following special case of the theorem, when we set X := bool:

foo true = foo false -> true = false

Given that true and false are different, if the theorem were provable, it should be possible to show that foo true and foo false are different. The problem is that these two types are isomorphic:

Inductive foo : bool -> Type :=
| constr : forall (x : bool), foo x.

(* An isomorphism between foo true and foo false *)
Definition foo_t_f (x : foo true) : foo false := constr false.
Definition foo_f_t (x : foo false) : foo true := constr true.

(* Proofs that the functions are inverses of each other *)
Lemma foo_t_fK x : foo_f_t (foo_t_f x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

Lemma foo_f_tK x : foo_t_f (foo_f_t x) = x.
Proof. unfold foo_f_t, foo_t_f. now destruct x. Qed.

In Coq's theory, it is not possible to show that two isomorphic types are different without assuming extra axioms. This is why an extension of Coq's theory such as homotopy type theory is sound. In HoTT, isomorphic types can be shown to be equal, and if it were possible to prove your theorem, HoTT would be inconsistent.