@@ -334,7 +334,7 @@ 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 data type that takes a ``Nat``, and produces a type.
337+From the signature, we can see that this is a type constructor that takes a ``Nat``, and produces a type.
338338So this is not a set in the sense of a collection that is a container of objects,
339339rather it is the canonical set of unnamed elements, as in "the set of 5 elements," for example.
340340Effectively, it is a type that captures integers that fall into the range of zero to ``(n - 1)`` where
@@ -346,8 +346,8 @@ Let us look at the constructors in greater detail.
346346``FZ`` is the zeroth element of a finite set with ``S k`` elements;
347347``FS n`` is the ``n+1``\ th element of a finite set with ``S k``
348348elements. ``Fin`` is indexed by a ``Nat``, which represents the number
349−of elements in the set. Obviously we can’t construct an element of an
350−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``.
351351
352352As mentioned above, a useful application of the ``Fin`` family is to represent bounded
353353natural numbers. Since the first ``n`` natural numbers form a finite