formalism: Add some description for polymorphism syntax

formalism/polymorphism.tex

@@ -1,8 +1,20 @@
 \input{symbols/polymorphism}
 
 \subsection{Extension: polymorphism}
+In this section, we describe an extension of the marked lambda calculus for System F-style
+parametric polymorphism.
+
+Chiefly, the introduction of type variables and the possibility of unbound ones requires the
+distinction between unmarked and marked types. These are each governed by well-formedness judgments
+(alongside extensions of the original consistency, etc. judgments) and linked by a marking
+operation.
 
 \subsubsection{Syntax}
+The syntax of unmarked types is exactly that of the original types alongside additional forms for
+forall types and type variables. In marked types, we additionally have unbound type variables.
+Within unmarked expressions, there may be type abstractions and type applications. In marked
+expressions, marks corresponding to those of ordinary lambda abstractions are present.
+
 \[\begin{array}{rrcl}
   \TMName  & \TMV  & \Coloneqq & \cdots \mid \TForall{\TVarMV}{\TMV} \mid \TVarMV \\
   \MTMName & \MTMV & \Coloneqq & \cdots
@@ -15,6 +27,10 @@ \subsubsection{Syntax}
 \end{array}\]
 
 \subsubsection{Unmarked types}
+Type consistency is now parametrized by the type variable context $\tvarCtx$. Here (and similarly
+the extension of other judgments), we omit the rules for the old syntactic constructs, which may be
+straightforwardly derived from the original rules. \\
+
 \judgbox{\ensuremath{\tvarCtxConsistentU{\tvarCtx}{\TMV_1}{\TMV_2}}} $\TMV_1$ and $\TMV_2$ are consistent
 %
 \begin{mathpar}