Теорема Кантора в теории типов

Теорема Кантора утверждает, что

Для любого множества A множество всех подмножеств A имеет строго большую мощность, чем само A.

Можно ли кодировать что-то подобное, используя только типы / предложения, не обращаясь к наборам ZFC? Код или псевдокод для кодирования этого предложения на зависимо типизированном языке приветствуется.

Краткий ответ: да! Вам не нужно столько машин, чтобы получить доказательства, чтобы пройти.

Одна тонкость: на первый взгляд кажется, что используется исключенная середина: каждый строит набор $D$ и номер $d$и показывает, что либо $d\in D$ или $d\not\in D$что приводит к противоречию. Но есть лемма, истинная в интуиционистской логике, которая гласит:

Этого достаточно вместе с обычным доказательством. Обратите внимание, что в общем случае «сюрприз» может иметь некоторый тонкий нюанс в конструктивной / интуиционистской логике (без выбора), поэтому вместо этого вы должны отдать должное «правильной обратимой».

Очень стандартное доказательство в Coq (которое по какой-то причине я не смог найти в Интернете) может выглядеть следующим образом:

Inductive right_invertible {A B:Type}(f : A->B):Prop :=
| inverse: forall g, (forall b:B, f (g b) = b) -> right_invertible f.


Lemma case_to_false :  forall P : Prop, (P <-> ~P) -> False.
Proof.
  intros P H; apply H.
    - apply <- H.
      intro p.
      apply H; exact p.
    - apply <- H; intro p; apply H; exact p.
Qed.


Theorem cantor :  forall f : nat -> (nat -> Prop), ~right_invertible f.
Proof.
  intros f inv.
  destruct inv.
  pose (diag := fun n => ~ (f n n)).
  apply case_to_false with (diag (g diag)).
  split.
  - intro I; unfold diag in I.
    rewrite H in I. auto.
  - intro nI.
    unfold diag. rewrite H. auto.
Qed.

Конечно, «правильной» структурой, в которой нужно думать об этих материях, которую можно рассматривать как минимальные требования для прохождения этого доказательства, является теорема Лаврэра о неподвижной точке, которая утверждает, что теорема справедлива в каждой декартовой замкнутой категории (поэтому в в частности, в любой разумной теории типов).

Андрей Бауэр прекрасно пишет об этой теореме в статье « Теоремы о фиксированной точке в синтетической вычислимости» , и я подозреваю, что в этот ответ можно добавить несколько интересных вещей.