Empty functions are equal in Agda (without functional extensionality)

user_13122298 0
Viewed 136

Can I prove that two empty functions (functions from the empty domain) are equal?

More concretely, is it possible to prove in Agda the following: eqf : ∀ {A : Set} (f g : ⊥ → A) → f ≡ g

Edit: as @Sassa-NF points out in the comments, if extensionality is present, then this can be proven. I am interested in whether this can be proven without extensionality.

agda
1 Answers

No, this is not possible to prove in plain Martin-Löf Type Theory (and hence should also be unprovable in Agda without extra assumptions). The paper "The Next 700 Syntactic Models of Type Theory" (https://hal.inria.fr/hal-01445835/file/main.pdf) describes a general technique to construct models of type theory that refute claims like this.

user_28825160
Related