Tipos indutivos indexados iguais implica índices iguais

Vamos ter um tipo indutivo fooindexado por x : X.

Parameter X : Type.

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

Estou curioso, se foo x = foo yimplica x = y. Estou sem idéias de como provar isso.

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

Se isso não pode ser provado, por quê?

Isso não pode ser provado. Considere o seguinte caso especial do teorema, quando estabelecemos X := bool:

foo true = foo false -> true = false

Dado que truee falsesão diferentes, se o teorema for comprovável, deve ser possível mostrar isso foo truee foo falsesão diferentes. O problema é que esses dois tipos são isomórficos :

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.

Na teoria de Coq, não é possível mostrar que dois tipos isomórficos são diferentes sem assumir axiomas extras. É por isso que uma extensão da teoria de Coq, como a teoria dos tipos de homotopia, é sólida. No HoTT, pode-se mostrar que os tipos isomórficos são iguais e, se fosse possível provar seu teorema, o HoTT seria inconsistente.