last proof reading

Time to sleep!

Author: MevenBertrand

Manuscript/Todo.md

@@ -1,3 +1,2 @@
 - hack continued floats for references
-- once chapter 6 is written: refer to it in the note on names at the beginning of chapter 3
-- title caps
+- once chapter 6 is written: refer to it in the note on names at the beginning of chapter 3

Manuscript/appendix.tex

@@ -1,64 +1,70 @@
-\chapter{On Names for Type Systems}
+\chapter{Names for Type Systems}
 \label{chap:names}
 
 \subsection*{MLTT and CIC}
 
-Dependent type theory is a vast field, and as in any other field there are numerous
-variations in the objects considered, both due to advances in their understanding,
-and to diverging purposes and techniques. In the end, when 
-choosing a particular type system to investigate, there are many more parameters to 
-fix than names available for them, so that the same name is bound to be used for
-different systems.
+% Dependent type theory is a vast field, and as in any other field there are numerous
+% variations in the objects considered, both due to advances in their understanding,
+% and to diverging purposes and techniques. In the end, when 
+% choosing a particular type system to investigate, there are many more parameters to 
+% fix than names available for them, so that the same name is bound to be used for
+% different systems.
 
-In the dependently typed setting, I think we can safely delineate two main schools,
+In the field of dependently types, I think we can safely delineate two main schools,
 with different histories and cultures. The first goes back to Martin-Löf –
 in particular \sidetextcite{MartinLoef1972} –, and is strongly linked to the \kl{Agda}
-proof assistant. The second is tied to the proof assistant \kl{Coq}, in the filiation of
+proof assistant. The second is related to the proof assistant \kl{Coq}, in the filiation of
 Coquand and Huet – since \sidetextcite{Coquand1988}.
 The umbrella name “MLTT”, for Martin-Löf Type Theory is the one usually used for systems
 in the first school, while ones in the second tend to use “CIC” – Calculus of Inductive
 Constructions –, or variants thereof.
 
-This separation is not a strict one, and researchers from both schools interact, exchange
+This separation is of course not a strict one,
+and researchers from both schools interact, exchange
 theoretical and implementation ideas, and move forward together. But still, this cultural
 difference is not anecdotal, as seemingly small differences between the approaches on both
-sides lead to wildly different behaviours between the systems, so that  some techniques
+sides lead to wildly different behaviours between the systems, so that some techniques
 that are very successful on one side can prove unusable on the other.
 
-I tried to prompt the community of proof assistants%
+I tried to probe the community of proof assistants%
 \sidenote{Using a \href{https://proofassistants.stackexchange.com/questions/267/what-are-the-differences-between-mltt-and-cic}{question} on the proof assistant
-stack exchange.}
-which led to quite different answers. I tried to summarize them in \cref{fig:mltt-cic},
+Stack Exchange.}
+as to what they consider the more important differences between the two schools,
+which led to quite different answers,
 although this is very approximate: \kl{Agda} has a general scheme for inductive types
 (including cubical ones in the cubical library) while many articles on \kl{CIC} only
-consider a few example inductive types – as was the case in parts of this thesis, etc.
-The one feature which is maybe the more prominent in the distinction between MLTT and
-CIC is the presence of an impredicative sort of propositions, which immensely augments the
-logical power of the theory, and makes it much harder to prove normalization.
+consider a few example inductive types – as was the case in parts of this thesis –, etc.
+So this should be read as “this tradition is more prone to taking that approach”.
+The results are summarized in \cref{fig:mltt-cic}.
 
 \begin{figure*}[h]
   \begin{tabular}{cccccc}
-    \rule{0pt}{4ex} & Philosophy & Universes & Inductive Types & Pattern-matching & Conversion \\
+    \rule{0pt}{4ex} & Universes & Inductive Types & Pattern-matching & Philosophy & Conversion \\
     \hline
-    MLTT \rule{0pt}{4ex} & Constructivism & Predicative hierarchy & $0$, $1$, $W$ and $Id$ & Top-level clauses & Typed \\
-    CIC \rule{0pt}{4ex} & None/Formalism & Impredicative $\Prop$ & General scheme & First-class terms & Untyped
+    MLTT \rule{0pt}{4ex} & Predicative hierarchy & $0$, $1$, $W$ and $Id$ & Top-level clauses & Constructivism & Typed \\
+    CIC \rule{0pt}{4ex} & Impredicative $\Prop$ & General scheme & First-class terms & None/Formalism & Untyped
   \end{tabular}
   \caption{General characteristics of MLTT and CIC}
   \label{fig:mltt-cic}
 \end{figure*}
 
 \subsection*{Why “CIC”?}
 
-Despite the inclusion of propositions, I chose to use the name \kl{CIC} in this thesis, for
-multiple reasons. First, regarding all other columns in the table, the system fits more
+The one feature which came out maybe as the more prominent in the distinction between MLTT and
+CIC is the presence of an impredicative sort of propositions, which immensely augments the
+logical power of the theory, and makes it much harder to prove normalization.
+Despite the exclusion of propositions by default, I still chose to use the name \kl{CIC}
+in this thesis, for multiple reasons.
+
+First, regarding all other columns in the table, the system fits more
 in the bottom line than the top one. In particular, the general spirit of studying
 conversion using tools from rewriting theory which appears as a repeated pattern throughout
 the thesis is incompatible – or, at the very least, must be heavily amended –
 with a typed conversion.
 Moreover, apart from \arefpart{gradual}, the absence of
 treatment of $\Prop$ on the paper presentation was done mostly due to simplification concerns
-than to theoretical issues, as the formalization of \kl{PCUIC} as a whole illustrates.
-This also applies to \cref{chap:bidir-gradual-elab}, even though the models quickly presented
+than to theoretical limitations, as the formalization of \kl{PCUIC} as a whole illustrates.
+This also applies to \cref{chap:bidir-gradual-elab}, even though the models presented
 in \cref{chap:beyond-gcic} do not scale to $\Prop$, meaning that the target
 of \cref{chap:bidir-gradual-elab} would then be on a precarious foundation.
 
@@ -67,14 +73,15 @@ \subsection*{Why “CIC”?}
 \kl{Agda}/MLTT and \kl{Coq}/CIC. The former have used the bidirectional ideas for a long
 time in order to allow for a lightweight syntax using Curry-style abstractions,
 at the cost of losing completeness of typing on non-normal forms.%
-\sidenote{This was a deliberate trade-off, at least in the case of \kl{Agda}
+\sidenote{This is a deliberate trade-off, at least in the case of \kl{Agda}
   \cite[p.~19]{Norell2007}.}%
 \margincite{Norell2007}
 The latter insist on keeping enough annotations in the kernel syntax by using Church-style
-abstractions, and using a mechanism of implicit arguments to lighten the weight of
-for users.
-This means that the completeness theorem \cref{thm:compl-ccomega} does \emph{not} apply
-to any of the standard presentations of MLTT, while it does to CIC’s, as this thesis shows.
+abstractions to let every term infer,
+and use a mechanism of implicit arguments during elaboration to lighten the weight of for users.
+This means that the completeness theorem as stated in \cref{thm:compl-ccomega}
+does \emph{not} hold in any of the standard presentations of MLTT,
+while it does to CIC’s, as this thesis shows.
 
 % \chapter{\kl{MetaCoq} Contributors}
 % \label{chap:meta-contrib}

Manuscript/beyond-gcic.tex

@@ -188,7 +188,7 @@ \subsection{The monotone model}
 
 
 
-\section{What is the issue with indices? Gradual vectors and equalities}
+\section{The issue with indices: gradual vectors and equalities}
   [Gradual vectors and equalities]
 \label{sec:indices-issue}
 
@@ -319,7 +319,7 @@ \subsection{Solutions for vectors}
 but is too permissive with invalid index assertions. It fails very late when such invalid
 assertions are made, meaning that error-reporting is bad.
 
-\paragraph{Direct support}
+\paragraph{Direct support.}
 
 In contrast to the two previously-exposed encodings that both have serious shortcomings, 
 extending \kl{CCIC} with direct support for indexed inductive types can provide a
@@ -447,7 +447,7 @@ \section{A Reasonably Gradual Type Theory}
 in this regard has not been developed. In particular, there is no clear characterization
 of a class of terms for which \kl{graduality} holds.
 
-\paragraph{A Refined Stratification of Precision} 
+\paragraph{A refined stratification of precision} 
 %
 \AP However, by refining the stratification of
 \kl{precision} we can develop a full account of graduality for an extension
@@ -473,7 +473,7 @@ \section{A Reasonably Gradual Type Theory}
 that conservatively extends \kl{CIC}, is normalizing,
 and satisfies graduality for a large and well-defined class of terms.
 
-\paragraph{Internalizing Precision, Reasonably}
+\paragraph{Internalizing precision, reasonably}
 While we could study graduality for \kl{CCICPrec} externally,
 we observe that we can exploit the expressiveness of the type-theoretic setting to
 internalize precision and its associated reasoning.
@@ -527,7 +527,7 @@ \section{A Reasonably Gradual Type Theory}
 define an internal notion of precision that is extensional and whose proofs
 cannot be trivialized with exceptional terms.
 
-\paragraph{Applications of Internal Precision}
+\paragraph{Applications of internal precision}
 
 In addition to supporting reasoning about the graduality of terms in a theory
 that is not globally gradual, \kl{internal precision} makes it possible