関数外延性公理(function extensionality axiom)はすべての関数型が関数外延性を満たすことを要請する。