Равноиндексированные индуктивные типы подразумевают равные индексы

9

Давайте fooиндексировать индуктивный тип x : X.

Parameter X : Type.

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

Мне любопытно, если foo x = foo yподразумевается x = y. У меня нет идей, как это доказать.

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

Если это невозможно доказать, почему?

Том
источник

Ответы:

8

Это не может быть доказано. Рассмотрим следующий частный случай теоремы, когда мы устанавливаем X := bool:

foo true = foo false -> true = false

Учитывая, что trueи falseотличаются, если теорема доказуема, должно быть возможно показать, что foo trueи foo falseотличаются. Проблема в том, что эти два типа изоморфны :

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.

В теории Кока невозможно показать, что два изоморфных типа различны без допущения дополнительных аксиом. Вот почему такое расширение теории Кока, как теория гомотопического типа, является обоснованным. В HoTT можно показать, что изоморфные типы равны, и если бы можно было доказать вашу теорему, HoTT был бы несовместимым.

Артур Азеведо Де Аморим
источник
У меня болит голова, но я думаю, что понял. Если бы у вас была ссылка на утверждение «В теории Кока невозможно показать, что два изоморфных типа различны без допущения дополнительных аксиом». ?
Том
И можно ли это показать (x <> y) -> (foo x <> foo y)? Я действительно запутался в этом мире без принципа исключенного среднего.
Том
Лучшая ссылка, которую я знаю (хотя, возможно, не самая доступная), это статья Хофмана и Штрайхера «Групповая интерпретация теории типов». Как говорит Хофманн ( ncatlab.org/homotopytypetheory/files/HofmannDMV.pdf ), у нас может быть звуковое расширение теории типов Мартина-Лёфа, где изоморфные типы равны. Этот результат также относится к теории Кока.
Артур Азеведо Де Аморим
И нет, это не возможно показать контрацептив. Контрпример, который я дал с истиной и ложью, также противоречил бы этому утверждению.
Артур Азеведо Де Аморим