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