CODEWITHSUNDEEP
agdaplfa
Marko Grdinić
Marko Grdinić

Reputation: 4062

Is functional extensionality with dependent functions consistent?

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

I know that the above definition is consistent, but what if a little twist on it is made?

postulate
  extensionality' : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

I had to define this in order to solve one of the PLFA book exercises, but I am not sure if I did the right thing by doing that. I think this should be consistent, but I do not have a good way of reasoning this out at the moment so I want to ask here.

Upvotes: 3

Views: 363

Answers (1)

András Kovács
András Kovács

Reputation: 30103

Yes. With Axiom K, dependent function extensionality is easily derivable from the non-dependent one. Perhaps this also works --without-K; I haven't tried or looked if it's in the literature.

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))))

In any case, dependent function extensionality is validated by many models, including set-theoretical ones, univalent ones, relational ones, etc. Models which don't support function extensionality are not common.

Upvotes: 5

Related Questions