------------------------------------------------------------------------ -- INCREMENTAL λ-CALCULUS -- -- Postulate extensionality of functions. -- -- Justification on Agda mailing list: -- http://permalink.gmane.org/gmane.comp.lang.agda/2343 ------------------------------------------------------------------------ module Postulate.Extensionality where open import Relation.Binary.PropositionalEquality postulate ext : ∀ {a b} → Extensionality a b -- Convenience of using extensionality 3 times in a row -- (using it twice in a row is moderately tolerable) ext³ : ∀ {A : Set} {B : A → Set} {C : (a : A) → B a → Set } {D : (a : A) → (b : B a) → C a b → Set} {f g : (a : A) → (b : B a) → (c : C a b) → D a b c} → ((a : A) (b : B a) (c : C a b) → f a b c ≡ g a b c) → f ≡ g ext³ fabc=gabc = ext (λ a → ext (λ b → ext (λ c → fabc=gabc a b c)))