У меня наивный вопрос:
Почему бы нам не добавить эту аксиому в Coq:
Axiom type_extensionality : forall (A B:Type)
(f:A->B) (invf:B->A) (H1: forall b, (f (invf b)) = b)
(H2: forall a, (invf (f a)) = a), A = B.
Хорошо, это позволило бы такие неконструктивные теоремы, как (nat-> Prop) = (nat-> bool) и (A \ / B) -> (A + B) (доказательства здесь ).
Но в стандартной библиотеке Coq уже есть много неконструктивных аксиом.
Приведет ли это к противоречию? (Если так, где я могу прочитать доказательство?)
Или просто еще не доказано, что аксиома не приведет к противоречию? Может быть, это просто бесполезно?
Возможно, именно поэтому библиотека HoTT переопределяет типы путей в https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v.
Эта аксиома "type_extensionality" менее сильна, чем аксиома однолистности.
Последнее потерпит неудачу при наличии ProofIrrelevance, PropositionExtensionality. (bool эквивалентен самому себе двумя различными способами, тогда как bool = тип bool состоит только из одного элемента).