Согласна ли функциональная расширяемость с зависимыми функциями? - PullRequest
Новая
       14

Согласна ли функциональная расширяемость с зависимыми функциями?

2 голосов
/ 25 мая 2019 
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

Я должен был определить это, чтобы выполнить одно из упражнений книги ЛПФА, но я не уверен, что поступил правильно.Я думаю, что это должно быть последовательным, но у меня нет хорошего способа объяснить это в данный момент, поэтому я хочу спросить здесь.

1 Ответ

3 голосов
/ 25 мая 2019

Да.С аксиомой 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))))

В любом случае расширяемость зависимых функций подтверждается многими моделями, включая теоретико-множественные, однолистные, реляционные и т. Д. Моделикоторые не не поддерживают расширенные функции поддержки.

...