与依赖函数的函数外延性是否一致？

Question

postulate
  extensionality : ? {A B : Set} {f g : A ? B}
    ? (? (x : A) ? f x ? g x)
      -----------------------
    ? f ? g

我知道上面的定义是一致的，但是如果稍微改动一下呢？

postulate
  extensionality' : ? {A : Set} {B : A ? Set} {f g : (x : A) ? B x}
    ? (? (x : A) ? f x ? g x)
      -----------------------
    ? f ? g

为了解决 PLFA 书中的一个练习，我必须定义它，但我不确定这样做是否正确。我认为这应该是一致的，但我目前没有一个很好的方法来推理这一点，所以我想在这里问一下。

Answer 1

是的。使用公理 K，依赖函数的外延性很容易从非依赖函数中推导出来。也许这也有效--without-K；我没有尝试或查看它是否在文献中。

open import Relation.Binary.PropositionalEquality
import Relation.Binary.HeterogeneousEquality as H
open import Data.Product

postulate funext : ? {A B : Set}{f g : A ? B} ? (? x ? f x ? g x) ? f ? g

funext' : ? {A : Set}{B : A ? Set}{f g : ? a ? B a} ? (? x ? f x ? g x) ? f ? g
funext' {A}{B}{f}{g} h =
    H.?-to-? (H.cong (? f x ? proj? (f x)) (H.?-to-? (funext ? a ? cong (a ,_) (h a))))

无论如何，依赖函数的外延性得到了许多模型的验证，包括集合论模型、单价模型、关系模型等。不支持函数外延性的模型并不常见。