Remove more contractions

chapters/coq-orders.tex

@@ -122,7 +122,7 @@ \section{Constructive setting}
   end.
 \end{minted}
 It does not like the \mintinline{coq}{S n} bit in the recursive call.
-I'm cheating a bit because it can still be defined by telling \Coq that
+I am cheating a bit because it can still be defined by telling \Coq that
 \mintinline{coq}{S n} here is indeed a subterm of the matched term.
 \begin{minted}{coq}
 Fixpoint fib n :=

chapters/coq-positions.tex

@@ -375,7 +375,7 @@ \section{Ordering positions}
 the term, something which you cannot do indefinitely, you are bound to reach a
 leaf at some (finite) point.
 
-If you think about it dually, I'm merely explaining that the structural order on
+If you think about it dually, I am merely explaining that the structural order on
 terms is well-founded, so why bother?
 The interesting part is that the order on positions can be more flexible than
 the subterm relation in that it allows us to compare `going left' with

chapters/elim-conclusion.tex

@@ -6,7 +6,7 @@ \section{Limitations and Axioms}
 \label{sec:axioms}
 
 \marginnote[0.2cm]{
-  I'd like to use a minimal representation of derivations that does not contain
+  I would like to use a minimal representation of derivations that does not contain
   everything that can be inferred automatically for one.
 }
 Currently, the representation of terms and derivations and the

chapters/elim-reflection-framework.tex

@@ -785,7 +785,7 @@ \subsection{Typing of \acrshort{WTT}}
   %
 \end{mathpar}
 
-You can notice that I'm cheating a little bit here. Indeed, I am already using
+You can notice that I am cheating a little bit here. Indeed, I am already using
 heterogeneous equality (\(\cong\)) in the typing rules. If you would indulge me,
 you can imagine that the definition for heterogeneous equality is \emph{inlined}
 in the typing rules. That way it is a much more convenient read (and it is

chapters/elim-reflection-intro.tex

@@ -21,7 +21,7 @@ \chapter{What I mean by elimination of reflection}
 This work gave rise to a publication~\sidecite[0.2cm]{winterhalter:hal-01849166} that
 focused on translating \acrshort{ETT} to \acrshort{ITT}.
 However, with Simon Boulier we worked on another version translating directly to
-\acrshort{WTT} which I'm going to present here.
+\acrshort{WTT} which I am going to present here.
 
 \section{Nature of the translation}
 

chapters/flavours.tex

@@ -396,7 +396,7 @@ \subsection{Inductive types}
 \emph{cumulative inductive types}~\sidecite{timany2018cumulative}
 (\acrshort{CIC}---and even \acrshort{CoC}---already has cumulativity).
 The idea is to extend the cumulativity relation beyond sorts to inductive types
-as well. I'm going to use the same example than the paper introducing them:
+as well. I am going to use the same example than the paper introducing them:
 a record~\sidenote{Exploiting the fact that (non-primitive) records are actually
 inductive types with one constructor in \Coq.} definition of categories:
 \[

chapters/translations.tex

@@ -248,7 +248,7 @@ \section{Other translations}
 Sometimes, the empty context itself is not translated to the empty context
 as is the case in the forcing translation~\sidecite{jaber2016definitional} and
 such an encoding becomes impossible.
-Even worse, in this document, in \arefpart{elim-reflection}, I'm going to
+Even worse, in this document, in \arefpart{elim-reflection}, I am going to
 present a translation that is not even syntactic! Indeed, sometimes the
 translation can only be conducted at the derivation level: derivations in \cS
 are sent to derivations in \cT. It often reflects the fact that terms in \cS are