agda - 如果没有 funext，是否有可能证明不等于无关紧要？

Question

我可以简单地证明不等于与函数可扩展性无关:

open import Relation.Binary.PropositionalEquality using (_≢_)
open import Relation.Binary using (Irrelevant)
open import Relation.Nullary.Negation using (contradiction)
open import Axiom.Extensionality.Propositional using (Extensionality)

postulate
  fun-ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂

≢-irrelevant : ∀ {a} {A : Set a} → Irrelevant {A = A} _≢_
≢-irrelevant {x} {y} [x≉y]₁ [x≉y]₂ = fun-ext (λ x≈y → contradiction x≈y [x≉y]₁)

当 A 是多态时，如果没有 funext，这似乎无法证明，但当 A = ℕ 或 A = Bool 时，这是否可能？

Answer 1

如果没有 funext，这是无法证明的。我们做了consider changing the definition of the empty type使这些可证明，但它被认为是一种过于侵入性的改变。