Minor improvements to the section on sorts.

2 files changed, 15 insertions, 12 deletions

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 12fd038fb6..b0ef792bd1 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -361,6 +361,7 @@ it is an atomic universe (i.e. not an algebraic max() universe).
    to the sort :g:`Set` and only collapses floating universes between
    themselves.
 
+.. _explicit-universes:
 
 Explicit Universes
 -------------------
@@ -387,7 +388,7 @@ to universes and explicitly instantiate polymorphic definitions.
          Polymorphic Universe @ident
 
    In the monorphic case, this command declares a new global universe
-   named :g:`ident`, which can be referred to using its qualified name
+   named :token:`ident`, which can be referred to using its qualified name
    as well. Global universe names live in a separate namespace. The
    command supports the :attr:`universes(polymorphic)` attribute (or
    the ``Polymorphic`` prefix) only in sections, meaning the universe
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 03581b95dd..3517d70005 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -30,14 +30,16 @@ 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.
+proofs of :math:`M`. An object :math:`m` belonging to :math:`M`
+:term:`witnesses <witness>` the fact that :math:`M` is
+provable. An object of type :math:`\Prop` is called a :gdef:`proposition`.
 We denote propositions by :n:`@form`.
 This constitutes a semantic subclass of the syntactic class :n:`@term`.
 
 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.
+equal). Objects of type :math:`\SProp` are called
+:gdef:`strict propositions <strict proposition>`.
 See :ref:`sprop` for information about using
 :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
 considerations.
@@ -66,12 +68,12 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by:
 
    \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`.
+Their properties, such as :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
+:math:`\Type(i):\Type(i+1)`, are described in :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
+referring to the universe :math:`\Type(i)`. One only writes `Type`. The system
+itself generates for each instance of `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
@@ -81,8 +83,8 @@ 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
+implemented using algebraic universes.
+An :gdef:`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
@@ -94,6 +96,6 @@ 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.
+results in a :exn:`Universe inconsistency` error.
 
-.. seealso:: :ref:`printing-universes`.
+.. seealso:: :ref:`printing-universes`, :ref:`explicit-universes`.