<commit_before>
\section{Translation}
\label{sec:translation}

We need the following translations:
%
\begin{align}
  \label{lbl:ctx-ctr}
  \isctx{\G}
  &\quad\leadsto\quad
  \isctx{\G'}
  \\
  \label{lbl:ty-ctr}
  \G', (\istype{\G}{\A})
  &\quad\leadsto\quad
  \istype{\G'}{\A'}
  \\
  \label{lbl:ty-path}
  % the following is needed if we ever need to construct an equivalence given A',B' and A \equiv B
  (\istype{\G'}{\A'}), (\istype{\G}{\A})
  &\quad\leadsto\quad
  (\istype{\G'}{\A''}), (\G' \vdash \A' \simeq \A'')
  \\
  \label{lbl:term-ctr}
  (\G', A'), (\isterm{\G}{\uu}{\A})
  &\quad\leadsto\quad
  \isterm{\G'}{\uu'}{\A'}
  \\
  % the following is needed if we ever need to construct an equivalence given u', v' and u \equiv v
  % (which happens if we need to construct an equivalence given A',B' and A \equiv B)
  \label{lbl:term-path}
  (\isterm{\G'}{\uu'}{\A'}), (\isterm{\G}{\uu}{\A})
  &\quad\leadsto\quad
  (\isterm{\G'}{\uu''}{\A'}), (\G' \vdash \uu' \simeq \uu'' : \A')
  \\
  \G', (\issubst{\sbs}{\G}{\D})
  &\quad\leadsto\quad
  \issubst{\sbs'}{\G'}{\D'}
  \\
  (\issubst{\sbs'}{\G'}{\D'}), (\issubst{\sbs}{\G}{\D})
  &\quad\leadsto\quad
  (\issubst{\sbs''}{\G'}{\D''}), (\sbs' \simeq \sbs'')
  \\
  \label{lbl:eq-ctx-path}
  \G', (\eqctx{\G}{\D})
  &\quad\leadsto\quad
  (\isctx{\D'}), (\G' \simeq \D')
  \\
  \label{lbl:eq-ty-path}
  \G', \B', (\eqtype{\G}{\A}{\B})
  &\quad\leadsto\quad
  (\istype{\G'}{\A'}), (\G' \vdash \A' \simeq \B')
  \\
  \label{lbl:eq-term-path}
  \G', \A', \vv', (\eqterm{\G}{\uu}{\vv}{\A})
  &\quad\leadsto\quad
  (\isterm{\G'}{\A'}{\uu'}), (\G' \vdash \uu' \simeq \vv' : \A')
\end{align}
%
Remarks:
%
\begin{itemize}
\item \eqref{lbl:ty-path} must give the same result as~\eqref{lbl:eq-ty-path} applied to
  the reflexivity case. This is so that we can use the result of~\eqref{lbl:eq-ty-path} as
  if it were obtained through conversion.
\item \eqref{lbl:term-path} must give the same result as~\eqref{lbl:eq-term-path} applied
  to the reflexivity case, for similar reasons.
\item We will need to know that all the equivalences generated from the derivations of a
  given equation are equal (propositionally pointwise). This is where UIP will come into
  play, since such equivalences are compositions of structural acrobatics and transports
  along paths used in $\rl{eq-reflection}$.
\item We also need to know that translations of contexts have the same shape
  as the original context, and the same goes for translation of types up
  to context isomorphisms.
\item In the rules producing isomorphims, we actually assume that the center
  generated is the same as the one that would be generated by the corresponding
  ``simple'' rule.
\end{itemize}


\subsection{Proof of the translation}
\label{sec:proof-tran}

\Case{ctx-empty}
%
The derivation
%
\begin{equation*}
  \infer{ }{\isctx{\ctxempty}}
\end{equation*}
%
is translated into
%
\begin{equation*}
  \infer{ }{\isctx{\ctxempty}}
\end{equation*}


\Case{ctx-extend}
<commit_msg>Remark to have better assumptions when proving (4)<commit_after>
\section{Translation}
\label{sec:translation}

We need the following translations:
%
\begin{align}
  \label{lbl:ctx-ctr}
  \isctx{\G}
  &\quad\leadsto\quad
  \isctx{\G'}
  \\
  \label{lbl:ty-ctr}
  \G', (\istype{\G}{\A})
  &\quad\leadsto\quad
  \istype{\G'}{\A'}
  \\
  \label{lbl:ty-path}
  % the following is needed if we ever need to construct an equivalence given A',B' and A \equiv B
  (\istype{\G'}{\A'}), (\istype{\G}{\A})
  &\quad\leadsto\quad
  (\istype{\G'}{\A''}), (\G' \vdash \A' \simeq \A'')
  \\
  \label{lbl:term-ctr}
  (\G', A'), (\isterm{\G}{\uu}{\A})
  &\quad\leadsto\quad
  \isterm{\G'}{\uu'}{\A'}
  \\
  % the following is needed if we ever need to construct an equivalence given u', v' and u \equiv v
  % (which happens if we need to construct an equivalence given A',B' and A \equiv B)
  \label{lbl:term-path}
  (\isterm{\G'}{\uu'}{\A'}), (\isterm{\G}{\uu}{\A})
  &\quad\leadsto\quad
  (\isterm{\G'}{\uu''}{\A'}), (\G' \vdash \uu' \simeq \uu'' : \A')
  \\
  \G', (\issubst{\sbs}{\G}{\D})
  &\quad\leadsto\quad
  \issubst{\sbs'}{\G'}{\D'}
  \\
  (\issubst{\sbs'}{\G'}{\D'}), (\issubst{\sbs}{\G}{\D})
  &\quad\leadsto\quad
  (\issubst{\sbs''}{\G'}{\D''}), (\sbs' \simeq \sbs'')
  \\
  \label{lbl:eq-ctx-path}
  \G', (\eqctx{\G}{\D})
  &\quad\leadsto\quad
  (\isctx{\D'}), (\G' \simeq \D')
  \\
  \label{lbl:eq-ty-path}
  \G', \B', (\eqtype{\G}{\A}{\B})
  &\quad\leadsto\quad
  (\istype{\G'}{\A'}), (\G' \vdash \A' \simeq \B')
  \\
  \label{lbl:eq-term-path}
  \G', \A', \vv', (\eqterm{\G}{\uu}{\vv}{\A})
  &\quad\leadsto\quad
  (\isterm{\G'}{\A'}{\uu'}), (\G' \vdash \uu' \simeq \vv' : \A')
\end{align}
%
Remarks:
%
\begin{itemize}
\item \eqref{lbl:ty-path} must give the same result as~\eqref{lbl:eq-ty-path} applied to
  the reflexivity case. This is so that we can use the result of~\eqref{lbl:eq-ty-path} as
  if it were obtained through conversion.
\item \eqref{lbl:term-path} must give the same result as~\eqref{lbl:eq-term-path} applied
  to the reflexivity case, for similar reasons.
\item We will need to know that all the equivalences generated from the derivations of a
  given equation are equal (propositionally pointwise). This is where UIP will come into
  play, since such equivalences are compositions of structural acrobatics and transports
  along paths used in $\rl{eq-reflection}$.
\item We also need to know that translations of contexts have the same shape
  as the original context, and the same goes for translation of types up
  to context isomorphisms.
\item In the rules producing isomorphims, we actually assume that the center
  generated is the same as the one that would be generated by the corresponding
  ``simple'' rule.
\item Assume $\isterm{\G}{\uu}{\A}$ and $\theta : \G'' \simeq \G'$ and $\A'$
  is a translation of $\A$ (in $\G'$) then instead of
  $(\G'', \subst{\A'}{\theta})$ as input for~\eqref{lbl:term-ctr}, we can
  use $(\G',\A')$.
  Indeed, we would get $\isterm{\G'}{\uu'}{\A'}$ and then deduce
  $\isterm{\G''}{\subst{\uu'}{\theta}}{\subst{\A'}{\theta}}$.
  This means that we can always assume the type we get as input
  for~\eqref{lbl:term-ctr} to be of the same shape as the original type.
\end{itemize}


\subsection{Proof of the translation}
\label{sec:proof-tran}

\Case{ctx-empty}
%
The derivation
%
\begin{equation*}
  \infer{ }{\isctx{\ctxempty}}
\end{equation*}
%
is translated into
%
\begin{equation*}
  \infer{ }{\isctx{\ctxempty}}
\end{equation*}


\Case{ctx-extend}

{'fraction_non_alphanumeric': 0.21131089595819885, 'fraction_numerical': 0.0001536806516059628, 'mean_word_length': 3.270341207349081, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6368477', 'n_tokens_mistral': 2462, 'n_tokens_neox': 2459, 'n_words': 695}