Пустые функции в Агде равны (без функциональной расширенности)

Question

Могу ли я доказать, что две пустые функции (функции из пустой области) равны?

Более конкретно, возможно ли доказать в Agda следующее: eqf : ∀ {A : Set} (f g : ⊥ → A) → f ≡ g

Редактировать: как отмечает @ Sassa-NF в комментариях, если присутствует экстенсиональность, то это можно доказать. Меня интересует, может ли это быть доказано без экстенсиональности.

Answer 1

Нет, это невозможно доказать в простой теории типов Мартина-Лёфа (и, следовательно, должно быть недоказуемым в Агде без дополнительных предположений). В статье «Следующие 700 Syntacti c моделей теории типов» (https://hal.inria.fr/hal-01445835/file/main.pdf) описывается общая методика построения моделей теории типов, опровергающих подобные утверждения.