Create new file on sorts.

1 files changed, 76 insertions, 0 deletions

diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
new file mode 100644
index 0000000000..3fa5f826df
--- /dev/null
+++ b/doc/sphinx/language/core/sorts.rst
@@ -0,0 +1,76 @@
+.. _Sorts:
+
+Sorts
+~~~~~~~~~~~
+
+The types of types are called :gdef:`sort`\s.
+
+All sorts have a type and there is an infinite well-founded typing
+hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop`
+and :math:`\Set`.
+
+The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a
+logical proposition then it denotes the class of terms representing
+proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is
+provable. An object of type :math:`\Prop` is called a proposition.
+
+The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
+:math:`\SProp` are known to have irrelevant proofs (all proofs are
+equal). Objects of type :math:`\SProp` are called strict propositions.
+See :ref:`sprop` for information about using
+:math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
+considerations.
+
+The sort :math:`\Set` intends to be the type of small sets. This includes data
+types such as booleans and naturals, but also products, subsets, and
+function types over these data types.
+
+:math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms.
+Consequently they also have a type. Because assuming simply that :math:`\Set`
+has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of
+|Cic| has infinitely many sorts. There are, in addition to the base sorts,
+a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`.
+
+Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as
+booleans, natural numbers, as well as products, subsets and function
+types over small sets. But, unlike :math:`\Set`, they also contain large sets,
+namely the sorts :math:`\Set` and :math:`\Type(j)` for :math:`j<i`, and all products, subsets
+and function types over these sorts.
+
+Formally, we call :math:`\Sort` the set of sorts which is defined by:
+
+.. math::
+
+   \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\}
+
+Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
+:math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`.
+
+The user does not have to mention explicitly the index :math:`i` when
+referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system
+itself generates for each instance of :math:`\Type` a new index for the
+universe and checks that the constraints between these indexes can be
+solved. From the user point of view we consequently have :math:`\Type:\Type`. We
+shall make precise in the typing rules the constraints between the
+indices.
+
+
+.. _Implementation-issues:
+
+**Implementation issues** In practice, the Type hierarchy is
+implemented using *algebraic
+universes*. An algebraic universe :math:`u` is either a variable (a qualified
+identifier with a number) or a successor of an algebraic universe (an
+expression :math:`u+1`), or an upper bound of algebraic universes (an
+expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression
+:math:`0`) which corresponds, in the arity of template polymorphic inductive
+types (see Section
+:ref:`well-formed-inductive-definitions`),
+to the predicative sort :math:`\Set`. A graph of
+constraints between the universe variables is maintained globally. To
+ensure the existence of a mapping of the universes to the positive
+integers, the graph of constraints must remain acyclic. Typing
+expressions that violate the acyclicity of the graph of constraints
+results in a Universe inconsistency error.
+
+.. seealso:: :ref:`printing-universes`.