@@ -334,16 +334,25 @@ importing ``Data.Fin``, or can be declared as follows:
334334 FZ : Fin (S k)
335335 FS : Fin k -> Fin (S k)
336336
337+From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
338+So this is not a set in the sense of a collection that is a container of objects,
339+rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
340+Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
341+``n`` is the argument used to instantiate the ``Fin`` type.
342+For example, ``Fin 5`` can be thought of as the type of integers between 0 and 4.
343+
344+Let us look at the constructors in greater detail.
345+
337346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
338347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
339348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
340−of elements in the set. Obviously we can’t construct an element of an
341−empty set, so neither constructor targets ``Fin Z``.
349+of elements in the set. Since we can’t construct an element of an
350+empty set, neither constructor targets ``Fin Z``.
342351
343−A useful application of the ``Fin`` family is to represent bounded
352+As mentioned above, a useful application of the ``Fin`` family is to represent bounded
344353natural numbers. Since the first ``n`` natural numbers form a finite
345−set of ``n`` elements, we can treat ``Fin n`` as the set of natural
346−numbers bounded by ``n``.
354+set of ``n`` elements, we can treat ``Fin n`` as the set of integers
355+greater than or equal to zero and less than ``n``.
347356
348357For example, the following function which looks up an element in a
349358``Vect``, by a bounded index given as a ``Fin n``, is defined in the
@@ -359,7 +368,7 @@ This function looks up a value at a given location in a vector. The
359368location is bounded by the length of the vector (``n`` in each case),
360369so there is no need for a run-time bounds check. The type checker
361370guarantees that the location is no larger than the length of the
362−vector.
371+vector, and of course no less than zero.
363372
364373Note also that there is no case for ``Nil`` here. This is because it
365374is impossible. Since there is no element of ``Fin Z``, and the