Improving text

paper/paper.tex

@@ -646,7 +646,7 @@ \subsection{Intuition for our formal construction\label{sec:intuition}}
 
 To assign types to $X_0, X_1, X_2, \ldots$ in the above indexed representation, we give a recursive definition relying on the building blocks which we call $\framep$, $\layer$, and $\painting$. A $\framep$ is a boundary of a standard form (simplex, cube, etc.), which we decompose into $\layer$, and a $\painting$ corresponds to a filled $\framep$. Some $\framep$ are full and we call them $\fullframe$: they represent matching objects.
 
-To every $X_n$ is uniformly assigned a type of the form $\fullframe[n] \rightarrow \U$. Compared to the informal description given in section~\ref{sec:rel-param}, e.g. $X_1 : X_0 \rightarrow X_0 \rightarrow \U$, this amounts to apply the isomorphisms between $A \rightarrow B \rightarrow C$ and $A \times B \rightarrow C$, or between $\Pi a: A.\, (B a \rightarrow C)$ and $(\Sigma a: A.\, B a) \rightarrow C$ so as to get the expected form $\fullframe[n] \rightarrow \U$.. In particular, $\fullframe[n]$ is a ``telescope'', i.e. a nesting of $\Sigma$-types.
+To every $X_n$ is uniformly assigned a type of the form $\fullframe[n] \rightarrow \U$. Compared to the informal description given in section~\ref{sec:rel-param}, this amounts to applying the isomorphisms between $A \rightarrow B \rightarrow C$ and $A \times B \rightarrow C$, or between $\Pi a: A.\, (B a \rightarrow C)$ and $(\Sigma a: A.\, B a) \rightarrow C$ so as to get the expected form $\fullframe[n] \rightarrow \U$. In particular, $\fullframe[n]$ is a ``telescope'', i.e. a nesting of $\Sigma$-types.
 
 Let us now illustrate how we recursively build $\fullframe[n]$. To begin, let us set $\fullframe[0] = \unittype$, so that the type $\U$ given to $X_0$ in section~\ref{sec:rel-param} can be equivalently formulated as $\unittype \rightarrow \U$. Then, more generally, we let each $\fullframe[n]$ consist of $n$ layers, written $\layer[n][p]$ with $p < n$, that we stack in order, starting from the $\unittype$ type and writing $\framep[n][p]$ for the $p$ first layers of a $\fullframe[n]$, so that $\fullframe[n]$ is $\framep[n][n]$. For instance, $X_1$ is made of one layer, so that it can be written as a $\Sigma$-type of an inhabitant of the $\unittype$ and $\layer[1][0]$, as shown below. The figure also mentions how the type of $X_2$ is structured.