Agda中的空函数相等（无函数可扩展性）

Question

我可以证明两个空函数（来自空域的函数）相等吗？

更具体地说，是否可以在Agda中证明以下内容：eqf : ∀ {A : Set} (f g : ⊥ → A) → f ≡ g

编辑：正如@ Sassa-NF在评论中指出，如果存在可扩展性，则可以证明这一点。我对是否可以证明without可扩展性感兴趣。

Answer 1

不，这不可能用简单的马丁·洛夫类型理论来证明（因此，在没有额外假设的情况下，在阿格达也无法证明）。论文“接下来的700个类型理论的句法模型”（https://hal.inria.fr/hal-01445835/file/main.pdf）描述了一种构建类型理论模型的通用技术，该模型可以反驳这样的主张。