.. _functions:

函数
====

到目前为止，本书研究的是数的性质（一个数是否为奇数、正数、素数；一个数是否被另一个数整除）以及数上的运算（加法、最大公因数）。

本章我们提升一个抽象层次，研究函数的性质以及函数上的运算。这些新性质包括：一个函数是否为*单射*、*满射*、*双射*；一个函数是否是另一个函数的*逆*；以及*复合*这一运算。

我们还把视野扩展到早期章节所处的数值类型（:math:`\mathbb{N}`、:math:`\mathbb{Z}`、:math:`\mathbb{Q}`、:math:`\mathbb{R}`）之外。现在我们开始处理范围更广的类型，包括函数类型、有限归纳类型和积类型。

.. include:: ch08_Functions/01_Injective_Surjective.inc
.. include:: ch08_Functions/02_Bijective.inc
.. include:: ch08_Functions/03_Composition.inc
.. include:: ch08_Functions/04_Product_Types.inc