我能证明两个空函数(来自空域的函数(相等吗？
更具体地说，是否可以在Agda中证明以下内容：eqf : ∀ {A : Set} (f g : ⊥ → A) → f ≡ g
编辑：正如@Sassa NF在评论中指出的那样，如果存在可扩展性，那么这是可以证明的。我感兴趣的是，这是否可以在没有可扩展性的情况下被证明。
不，这在普通的Martin-Löf型理论中是不可能证明的(因此在没有额外假设的情况下，在Agda中也应该是不可证明的(。论文"类型理论的下700个句法模型"(https://hal.inria.fr/hal-01445835/file/main.pdf)描述了一种构建类型理论模型的通用技术，以反驳此类说法。