------------------------------------------------------------------------ -- The Agda standard library -- -- Results concerning function extensionality for propositional equality ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Axiom.Extensionality.Propositional where open import Function.Base open import Level using (Level; _⊔_; suc; lift) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core ------------------------------------------------------------------------ -- Function extensionality states that if two functions are -- propositionally equal for every input, then the functions themselves -- must be propositionally equal. Extensionality : (a b : Level) Set _ Extensionality a b = {A : Set a} {B : A Set b} {f g : (x : A) B x} (∀ x f x g x) f g -- A variant for implicit function spaces. ExtensionalityImplicit : (a b : Level) Set _ ExtensionalityImplicit a b = {A : Set a} {B : A Set b} {f g : {x : A} B x} (∀ {x} f {x} g {x}) {x} f {x}) {x} g {x}) ------------------------------------------------------------------------ -- Properties -- If extensionality holds for a given universe level, then it also -- holds for lower ones. lower-extensionality : {a₁ b₁} a₂ b₂ Extensionality (a₁ a₂) (b₁ b₂) Extensionality a₁ b₁ lower-extensionality a₂ b₂ ext f≡g = cong h Level.lower h lift) \$ ext (cong (lift { = b₂}) f≡g Level.lower { = a₂}) -- Functional extensionality implies a form of extensionality for -- Π-types. ∀-extensionality : {a b} Extensionality a (suc b) {A : Set a} (B₁ B₂ : A Set b) (∀ x B₁ x B₂ x) (∀ x B₁ x) (∀ x B₂ x) ∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂ ... | refl = refl -- Extensionality for explicit function spaces implies extensionality -- for implicit function spaces. implicit-extensionality : {a b} Extensionality a b ExtensionalityImplicit a b implicit-extensionality ext f≡g = cong _\$- (ext x f≡g))