modalities.tex

\chapter{Higher modalities}
\label{chap:modalities}

\epigraph{There is no one fundamental logical notion of {\em
    necessity}, not consequently of {\em possibility}. If this
  conclusion is valid, the subject of modality ought to be vanished
  from logic, since propositions are simply true or false.}{Bertrand Russel}

As said in the introduction, the main purpose of our work is to build,
from a model $\mathfrak M$ of homotopy type theory, another model
$\mathfrak M'$ satisfying new principles. Of course, $\mathfrak M'$
should be describable {\em inside} $\mathfrak M$. In set theory, it
corresponds to building {\em inner models} (\cite{kunen}). 
%
In type theory, it can be rephrased in terms of left-exact modalities:
it consists of an operator $\modal$ on types such that for any type
$A$, $\modal A$ satisfies a desired property. If the operator has a
``good'' behaviour, then it is a modality, and, with a few more
properties, the universe of all types satisfying the chosen property
forms a new model of homotopy type theory.

Modalities are actually a generalization of {\em modal logics}~\cite{goldblatt-modal} and
{\em modal type theories}~\cite{moggi-monad}. At the time we write this
thesis, the only references for modalities
are~\cite{shulman-higher-modalities} and~\cite[Section
7.7]{hottbook}. 
Most of the results presented here either are taken from the book,
either are paper versions of results formalized in~\cite[{Folder
  \code{Modalities}}]{hottlib}.

Egbert Rijke, Mike Shulman and Bas Spitters
are writing a paper~\cite{RijkeShulmanSpitters} extending greatly what is said in the HoTT book,
and probably in this thesis.


\section{Modalities}
\label{sec:modalities}

\begin{defi}
  \label{def:modality}
  A left exact modality is the data of
  \begin{enumerate}[(i)]
  \item A predicate $P:\Type \to \HProp$
  \item For every type $A$, a type
    $\modal A$ such that $P(\modal A)$
  \item For every type $A$, a map $\eta_A:A \to
    \modal A$
  \end{enumerate}
  such that
  \begin{enumerate}[(i)]
    \setcounter{enumi}{3}
  \item For every types $A$ and $B$, if $P(B)$ then
    \[ \left\{
        \begin{array}{rcl}
          (\modal A \to B) & \to & (A \to B) \\
          f & \mapsto & f \circ \eta_A
        \end{array} \right. \] %
    is an equivalence.
  \item for any $A:\Type$ and $B:A \to \Type$ such that $P(A)$
    and $\prod_{x:A} P(B x)$, then $P\left( \sum_{x:A} B(x)\right)$
  \item for any $A:\Type$ and $x,y:A$, if $\modal A$ is
    contractible, then $\modal (x=y)$ is contractible.
  \end{enumerate}
  Conditions (i) to (iv) define a {\em reflective subuniverse}, (i) to
  (v) a {\em modality}.
\end{defi}

\begin{nota}
  The inverse of $- \circ \eta_A$ from point {\itshape (iv)} will be
  denoted $\modal_{\mathrm{rec}}: (A\to B) \to (\modal A \to B)$, and its
  computation rule $\modal_{\mathrm{rec}}^\beta : \prodD f {A \to B} {\prodD x A
  {\modal_{\mathrm{rec}}(f) (\eta_A x) = f x}}$.
\end{nota}

If $\modal$ is a modality, the type of modal types will be denoted
$\Type^\modal$. Let us fix a left-exact modality $\modal$ for the rest
of this section. A modality acts functorialy on $\Type$, in the sense
that

\begin{lem}[Functoriality of modalities]
  Let $A,B:\Type$ and $f:A\to B$. Then there is a map $\modal f:\modal
  A \to \modal B$ such that 
  \begin{itemize}
  \item $\modal f \circ \eta_A = \eta_B \circ f$
  \item if $g:B\to C$, $\modal (g \circ f) = \modal g \circ \modal f$
  \item if $\IsEquiv f$, then $\IsEquiv \modal f$.
  \end{itemize}
\end{lem}

\begin{prop}\label{prop:mod_prop}
  Any left-exact modality $\modal$ satisfies the following
  properties\footnote{Properties needing only a reflective subuniverse
    are annoted by (R), a modality by (M), a left-exact modality by (L)}.
  \begin{itemize}
  \item[\labelitemi(R)] $A$ is modal if and only if $\eta_A$ is an equivalence.
  \item[\labelitemi(R)] $\one$ is modal.
  \item[\labelitemi(R)] $\Type^\modal$ is closed under dependent
    products, \ie{} $\prodD x A {B\, x}$ is modal as soon as all $B\,
    x$ are modal.
  \item[\labelitemi(R)] For any types $A$ and $B$, the map
    \[ \modal(A\times B) \to \modal A \times\modal B \]
    is an equivalence.
  \item[\labelitemi(R)] If $A$ is modal, then for all $x,y:A$, $(x=y)$
    is modal.
  \item[\labelitemi(M)] For every type $A$ and $B:\modal(A)\to\Type^\modal$, then
    \[ \fonction{-\circ\eta_A}{\prodD z {\modal A} {B\, x}}{\prodD a
        A {B(\eta_A\, a)}}{f}{f\circ \eta_A} \]
    is an equivalence.
  \item[\labelitemi(M)] If $A,B:\Type$ are modal, then so are $\IsType
    n A$, $A\simeq B$ and $\IsEquiv f$ for all $f:A\to B$.
  \item[\labelitemi(L)] If $A:\Type_n$, then $\modal A:\Type_n$.
  \item[\labelitemi(L)] If $A,B:\Type$ and $f:A\to B$, then the map
    \[ \modal \left( \fib f b\right) \to \fib{\modal f}{\eta_B
        b} \]
    is an equivalence, and the following diagram commutes
\[ \xymatrix{
  \fib f b \ar[r]^\eta \ar[d]_\gamma & \modal \left(\fib f b \right) \ar[dl]\\
  \fib{\modal f}{\eta_B b} & }\] 
  \end{itemize}
\end{prop}

\begin{nota}
  Again, the inverse of $- \circ \eta_A$ will be denoted
  $\modal_{\mathrm{ind}} : \prodD a A {B (\eta_A a)} \to \prodD z
  {\modal A} {B\, x}$, and its computation rule
  $\modal_{\mathrm{ind}}^\beta : \prodD f {\prodD a
        A {B(\eta_A\, a)}} {\prodD x A
        {\modal_{\mathrm{ind}}(f)(\eta_A x) }} = f x$
\end{nota}

\begin{proof}
  We only prove the last point.
  It is straighforward to define a map
  \[ \phi:\sumD x X  {f x = y}\to
    \sumD x {\modal X} {\modal f x = \eta_Y y},\]
  using $\eta$ functions.
  We will use the following lemma to prove that the function induced
  by $\phi$ defines an equivalence:
  \begin{lem}
    Let $A:\Type$, $B:\Type^\modal$ and $f:A\to B$. If for all $b:Y$,
    $\modal (\fib f b)$ is contractible, then $\modal A \simeq B$.
  \end{lem}
  % 
  Hence we just need to check that every $\modal$-fiber $\modal(\fib \phi {x;p})$ is contractible.
  Technical transformations allow one to prove
  \[ \fib\phi{x;p} \simeq \fib s {y;p^{-1}}\]
  for
  \[
    \fonction{s}{\fib{\eta_X}x}{\fib{\eta_Y}{\modal f\, x}}{(a,q)}{(f\, a,-)}
  \]
  But left-exctness allows to characterize the contractibility of fibers:
  \begin{lem}
    Let $A,B:\Type$. Let $f:A\to B$. If $\modal A$ and $\modal B$ are
    contractible, then so is $\fib f b$ for any $b:B$.
  \end{lem}
  Thus, we just need to prove that $\modal(\fib {\eta_X} a)$ and
  $\modal(\fib {\eta_Y} b)$ are contractible. But one can check that
  $\eta$ maps always satisfy this property.
  Finally, $\modal(\fib s{y;p^{-1}})$ is contractible, so $\modal(\fib \phi {x;p})$ also, and the result is proved.
  % \kq{Finish that}

  % \nt{Indeed, I can't follow the proof for the moment}
\end{proof}

Let us finish these properties by the following proposition, giving
an equivalent characterization of left-exactness.

\begin{prop}\label{prop:lex}
  Let $\modal$ be a modality. Then $\modal$ is left-exact if and only
  if
 % one of
 %  the following equivalent properties is satisfied
 %  \begin{itemize}
 %  \item $\modal$ preserves contractibility, \ie{}
 %    \[ \prodD A \Type {\prodD {x,y} A { \Contr(\modal A) \to \Contr
 %          (\modal (x=y))}}.\]
 %  \item $\modal$ preserves pullback, in the sense that if
 %    \[
 %      \xymatrix{
 %        A \ar[r] \ar[d] \times_B C \pullbackcorner& C \ar[d]^g\\
 %        A \ar[r]_f & B
 %      }
 %    \]
 %    is a pullback diagram, then
 %    \[
 %      \xymatrix{
 %       \modal A \ar[r] \ar[d] \times_{\modal B} \modal C
 %       \pullbackcorner& \modal C \ar[d]^{\modal g}\\
 %        \modal A \ar[r]_{\modal f} & \modal B
 %      }
 %    \]
 %    is too.
 %  \item
  $\modal$ preserves path spaces, \ie{}
    \[
      \prodD A \Type {\prodD {x,y} A {\IsEquiv (\modal (\ap{\eta_A}))}}
    \]
    where $\modal (\ap{\eta_A}) : \modal(x = y) \to \eta_A x = \eta_A
    y$.
  % \end{itemize}
\end{prop}
\begin{proof}
  We will rather prove something slighlty more general, using an
  encode-decode proof~\cite[Section 8.9]{hottbook} ; we will
  characterize, for a type $A$ and a fixed inhabitant $x:A$ the type 
  \[ \eta_A x = y \] 
  for any $y:\modal A$.
  
  \newcommand{\Cover}{\mathrm{Cover}}
  \newcommand{\Encode}{\mathrm{Encode}}
  \newcommand{\Decode}{\mathrm{Decode}}
  Let $\Cover:\modal A \to \Type^\modal$ be defined by induction by
  \[ \Cover(y) \defeq \modal_{\mathrm{rec}} (\lambda y,\,\modal (x =
    y)). \]
  Note that for any $y:\modal A$, $\Cover(y)$ is always modal.
  We will show that $\eta_A x = y \simeq \Cover(y)$.
  Now, let $\Encode : \prodD y {\modal A} {\eta_A x = y \to
    \Cover(y)}$ be defined by
  \[ \Encode(y,p) \defeq \transport_{\Cover}^p
    \left(\transport_{\idmap}^{\modal_{\mathrm{rec}}^\beta ((\lambda
        z,\,\modal (x = z)), x)} (\eta_{x=x} 1)\right) \]
  and $\Decode:\prodD y {\modal A} {\Cover(y) \to \eta_A x = y}$ by
  \[
    \Decode \defeq \modal_{\mathrm{ind}} \left(\lambda y\,p,\,
    \modal(\ap{\eta_A})  \left(\transport_{\idmap}^{\modal_{\mathrm{rec}}^\beta ((\lambda
        z,\,\modal (x = y)),y)} p\right)\right)
  \]
  Then one can show, using $\modal$-induction and path-induction, that
  for any $y:\modal A$, $\Encode(y,-)$ and $\Decode(y,-)$
  are each other inverses. Then, taking $y' = \eta_A y$, we have just
  shown that $\eta_A x = \eta_A y \simeq \Cover(\eta_A y)$, which is
  itself equivalent, by $\modal_{\mathrm{rec}}^\beta$, to $\modal
  (x=y)$.
  It is straightforward to check that the composition $\modal (x=y)
  \to \Cover(\eta_A y) \to \eta_A x = \eta_A y$ is exactly $\modal
  (\ap{\eta_A})$.
  
  Now, let us prove the backward implication. Let $A$ be a type such
  that $\modal A$ is contractible, and $x,y:A$. 
  As $\eta_A x,\eta_A y: \modal A$, we know that $\eta_A x = \eta_A y$
  is contractible. But as $\eta_A x = \eta_A y \simeq \modal (x=y)$ by
  assumption, $\modal (x=y)$ is also contractible.
\end{proof}

As this whole thesis deals with truncation levels, it should be
interesting to see how they are changed under a modality. 
We already know that if a type $T$ is $(-2)$-truncated, \ie{}
contractible, then it is unchanged by the reflector: \[\modal T \simeq
\modal \one \simeq \one \simeq T.\] Thus, $\Type_{-2}$ is closed by
any reflective subuniverse.
%
Now, let $T:\HProp$. To check that $\modal T$ is an h-proposition, it
suffices to check that \[\prodD {x,y} {\modal T} {x = y}\] 
For any $x:\modal T$, the type $\prodD y {\modal T} {x = y}$
is modal, as all $x=y$ are ; by the same argument, $\prodD x {\modal T} {x =
  y}$ is modal too for any $y:\modal T$. 
Using twice the dependent eliminator of $\modal$, it now suffices to
check that \[\prodD {x,y} T {\eta_T x = \eta_T y}.\]
As $T$ is supposed to be an h-proposition, this is true. It suffices
to state
\begin{lem}\label{lem:mod-hprop}
  For any modality, $\Type_{-1}$ is closed under the reflector
  $\modal$, \ie{} \[\prodD P \HProp {\IsHProp (\modal P)}.\]
\end{lem}

A simple induction on the truncation level, together with the
left-exactness property allows to state
\begin{lem}\label{lem:mod-istrunc}
  For any left-exact modality, all $\Type_p$ are closed under the
  reflector $\modal$, \ie{}
  \[\prodD P {\Type_p} {\IsType p (\modal P)}.\]
\end{lem}
We note that this is not a equivalent characterization of
left-exactness, as it is satisfied by truncations, and we will see
they are not left-exact.

% %\kq{Is the following usefull?}
% In the same way, left exact modalities preserve homotopy types.
% \begin{prop}
%   Let $k \leq n$.
%   If $P:\Type_k$, then $\modal \widehat P : \Type_k$, where $\widehat P$
%   is $P$ seen as a $n$-type.
% \end{prop}
% \begin{proof}
%   An $n$-truncated type $P$ can equivalently be described as a type for
%   which the unique map to $\one$ is with $n$-truncated fibers. Thus, the
%   property is a direct corollary of
%   Proposition~\ref{sec:defin-basic-prop} and the fact that $\modal \one =
%   \one$.
% \end{proof}
% \end{proof}



\section{Examples of modalities}
\label{sec:modalities-examples}

\subsection{The identity modality}
\label{ssec:id_mod}

Let us begin with the most simple modality one can imagine: the one
doing nothing. We can define it by letting $\modal A \defeq A$ for any type
$A$, and $\eta_A \defeq \idmap$. Obviously, the desired computation
rules are satisfied, so that the identity modality is indeed a
left-exact modality.

It might sound useless to consider such a modality, but it can be
precious when looking for properties of modalities: if it does not
hold for the identity modality, it cannot hold for an abstract one.


\subsection{Truncations}
\label{ssec:truncations}

The first class of non-trivial examples might be the {\em truncations}
modalities, seen in~\ref{ssec:trunc}.

\subsection{Double negation modality}
\label{ssec:notnot}

\begin{prop}
  The double negation modality $\modal A \defeq \lnot\lnot A$ is a
  modality.  
\end{prop}
\begin{proof}
  We define the modality with
  \begin{enumerate}[(i)]
  \item We will define the predicate $P$ later.
  \item $\modal$ is defined by $\modal A \defeq \lnot\lnot A$
  \item We want a term $\eta_A$ of type $A \to \lnot \lnot A$.
    Taking 
    \[ \eta_A\defeq \lambda \, x:A,\,\lambda\, y:\lnot A,\, y\, a\] 
    do the job.
    
    Now, we can define $P$ to be exactly $\prodD A \Type {\IsEquiv
      \eta_A}$.
  \item Let $A,B:\Type$, and $\varphi : A \to \lnot\lnot B$. We
    want to extend it into $\psi : \lnot\lnot A \to \lnot\lnot B$. Let
    $a:\lnot\lnot A$ and $b:\lnot B$.
    Then $a(\lambda\, x:A,\, \varphi\, x \, b) : \zero$, as
    wanted. One can check that it forms an equivalence.
  \item Let $A:\Type$ and $B:A\to\Type$ such that $P(A)$ and $\prodD a
    A {P(B\, a)}$. There is a map
    \[\sumD x A {B\, x} \to A \]
    thus by the preivous point, we can extend it into 
    \[\kappa:\lnot\lnot\sumD x A {B\, x} \to A.\]
    It remains to check that for any $x:\lnot\lnot\sumD x A {B\, x}$,
    $B(\kappa\, x)$.

    But the previous map can be easily extended to the dependent case,
    and thus it suffices to show that for all $x:\sumD x A{B\, x}$,
    $B(\kappa(\eta\, x)$. As $\kappa \circ \eta = \idmap$, the goal is
    solved by $\pi_2 x$.
  \end{enumerate}
\end{proof}

Unfortunately, it appears that the only type which can be modal are
h-propositions, as they are equivalent to their double negation which
is always an h-proposition. Thus, the type of modal types is consisted
only of h-proposition, which is not satisfactory. The main purpose of this
thesis, in particular chapter~\ref{chap:sheaf} is to extend this
modality into a better one.

% \section{New type theories}
% \label{sec:new-type-theories}

% \todo[inline]{New type theory: Enhance me.
% Actually, this might be better in the section ``Translation,èj,j,j''.
% }


% We suppose here that $\modal$ is a left-exact modality such that
% $\Type^\modal$ is modal.
% This is for example the case when the modality is {\em accessible}
% (see~\cite{hottlib} for definition and proof).

% \begin{prop}
%   The modal universe $\Type^\modal$ is non-trivial if the type $\modal
%   \zero$ is empty.
% \end{prop}
% \begin{proof}
  
% \end{proof}


% \todo[inline]{The translation might be clearer than this result\dots}
% \begin{prop}\label{prop:consistent}
%   A left exact modality $\modal$ induces a consistent type theory if
%   and only if $\modal \zero$ can not be inhabited in the initial type
%   theory. In that case, the modality is said to be consistent.
% \end{prop}
% \begin{proof}
%   By condition (iv) of Definition~\ref{def:modality},
%   $\modal \zero$ is an initial object of $\Type^\modal$, and thus
%   corresponds to false for modal mere proposition.
%   % 
%   As $\modal \one = \one$, $\Type^\modal$ is consistent when
%   $\modal \zero \neq \one$, that is when there is no proof of
%   $\modal \zero$.
% \end{proof}

\section{Truncated modalities}
\label{sec:trunc_modalities}

As for colimits, we define a truncated version of modalities, in order
to use it in chapter~\ref{chap:sheaf}. Basically, a truncated modality
is the same as a modality, but restricted to $\Type_n$. 

\begin{defi}[Truncated modality]
  \label{def:tr_mod}
  Let $n\geq -1$ be a truncation index. A left exact modality at level
  $n$ is the data of
  \begin{enumerate}[(i)]
  \item A predicate $P:\Type_n \to \HProp$
  \item For every $n$-truncated type $A$, a $n$-truncated type
    $\modal A$ such that $P(\modal A)$
  \item For every $n$-truncated type $A$, a map $\eta_A:A \to
    \modal A$
  \end{enumerate}
  such that
  \begin{enumerate}[(i)]
    \setcounter{enumi}{3}
  \item For every $n$-truncated types $A$ and $B$, if $P(B)$ then
    \[\left\{
      \begin{array}{rcl}
        (\modal A \to B) & \to & (A \to B) \\
        f & \mapsto & f \circ \eta_A
      \end{array} \right.\]
    is an equivalence.
  \item for any $A:\Type_n$ and $B:A \to \Type_n$ such that $P(A)$
    and $\prod_{x:A} P(B x)$, then $P\left( \sum_{x:A} B(x)\right)$
  \item for any $A:\Type_n$ and $x,y:A$, if $\modal A$ is
    contractible, then $\modal (x=y)$ is contractible.
  \end{enumerate}
\end{defi}

Properties of truncated left-exact modalities described
in~\ref{prop:mod_prop} are still true when restricted to $n$-truncated
types, except the one that does not make sense: $\Type_n^\modal$
cannot be modal, as it is not even a $n$-truncated type.

\section{Formalization}
\label{sec:mod-formalization}

Let us discuss here about the formalization of the theory of
modalities. General modalities are formalized in the Coq/HoTT
library~\cite{hottlib}, thanks to a huge work of Mike
Shulman~\cite{modules-modalities}. The formalization might seem to be
straightforward, but the universe levels (at least, their automatic
handling by Coq) are here a great issue. Hence, we have to explicitely
give the universe levels and their constraints in a large part of the
library. For example, the reflector $\modal$ of a modality is defined,
in~\cite{hottlib} as
\[ \modal : \Type^i \to \Type^i ;\]
it maps any universe to itself.

In chapter~\ref{chap:sheaf}, we will need a slighlty more general
definition of modality. The actual definitions stay the same, but the
universes constraints we consider change. The reflector $\modal$ will
now have type
\[ \modal : \Type^i \to \Type^j,\quad i \leqslant j ;\]
it maps any universe to a possibly higher one.
Other components of the definition of a modality are changed in the
same way. 

Fortunately, this change seems small enough for all properties of
modalities to be kept. Of course, the examples of modalities mapping
any universe to itself are still an example of generalized modality,
it just does not use the possibility to inhabit a higher
universe. This has been computer-checked, it can be found at 
\url{https://github.com/KevinQuirin/HoTT/tree/extended_modalities}.

We would like to have the same generalization for truncated
modalities. But there are a lot of new universe levels popping out,
mostly because in $\Type_n = \sumD T \Type {\IsType n T}$, $\IsType n$
come with its own universes. Hence, handling ``by hand'' so many
universes together with their constraints quickly go out of
control. One idea to fix this issue could be to use {\em resizing
  rules}~\cite{vv-resizing}, allowing h-propositions to live in the
smallest universe. We could then get rid of the universes generated by
$\IsType n$, and treat the truncated modality exactly as generalized
modalities.







\section{Translation}
\label{sec:translation}

In this section, we will explain how left-exact modalities allows to
perform model transformation, just as forcing does.  Actually, we can
to even better by exhibiting a {\em translation} of type theories,
from CIC into itself, as it has been done for
forcing~\cite{jaber2012extending,forcing2016}. Let us explain here how
this translation works.

Let $\modal$ be an accessible left-exact modality. We describe, for each term
constructor, how to build its translation. We denote $\pi_\modal(A)$
the proof that $\modal(A)$ is always modal.

\begin{itemize}
\item For types
\[
\begin{array}{lcl}
  \left[ \Type\right] &\defeq& (\Type^\modal,\pi_{\Type^\modal})
\end{array}
\]
where $\pi_{\Type^\modal}$ is a proof that $\Type^\modal$ is itself
modal.
To ease the reading in what follows, we introduce the notation  \[ 
  \Lbrack A \Rbrack \defeq \pi_1 \left[ A \right]\]

\item For dependent sums
\[
\begin{array}{lcl}
\left[ \sumD x A B \right] &\defeq&  \left( \sumD x{\Lbrack A \Rbrack}
                                  {\Lbrack B\Rbrack} , \pi_\Sigma^{[A],[B]}
                                \right)\\[0.5em]
  \left[  (x,y)\right] &\defeq& ([x],[y]) \\[0.5em]
  \left[  \pi_i t\right] &\defeq& \pi_i [t] \\[0.5em]
\end{array}
\]
where $\pi_{\Sigma}^{A,B}$ is a proof that $\sumD x A B$ is modal when
$A$ and $B$ are.
\item For dependent products
\[
\begin{array}{lcl}
 \left[ \prod_{x:A} B \right] &\defeq& \left( \prod_{x:\Lbrack A \Rbrack}
                                   \Lbrack B\Rbrack , \pi_{\Pi}^{[A],[B]}
                                  \right)\\[0.5em]
\left[  \lambda\, x:A,~M \right] &\defeq&\lambda\,x:\Lbrack A
                                     \Rbrack,~[ M ]
  \\[0.5em]
  \left[ t \, t' \right] &\defeq& [t] [t'] \\[0.5em]
\end{array}
\]
where $\pi_{\Pi}^{A,B}$ is a proof that $\prodD x A B$ is modal when $B$ is.
\item For paths
\[
\begin{array}{lcl}
\left[  x=_A y \right] &\defeq& \left( [x] =_{\Lbrack A\Rbrack} [y] , \pi_=^{[x],[y]}
                             \right)\\[0.5em]
\left[ 1 \right] &\defeq& 1\\[0.5em]
\left[ J \right] &\defeq& J \\[0.5em]
\end{array}
\]
where $\pi_{=}^{x,y}$ is a proof that $x=_A y$ is modal when $A$ is.
\item For positive types (we only treat the case of the sum as an example)
\[
\begin{array}{lcl}
\left[  A+B \right] &\defeq& \left( \modal(\Lbrack A \Rbrack + \Lbrack B
                        \Rbrack); \pi_\modal(\Lbrack A \Rbrack + \Lbrack B
                        \Rbrack)\right)\\[0.5em]
\left[  \mathrm{in}_\ell t \right] &\defeq& \eta (\mathrm{in}_\ell [t]) \\[0.5em]
\left[  \mathrm{in}_r t \right] &\defeq& \eta (\mathrm{in}_r [t]) \\[0.5em]
\left[ \langle f ,g\rangle\right] &\defeq& \modal_{\mathrm{rec}}^{\Lbrack A\Rbrack +
                                      \Lbrack B\Rbrack} \langle
                                      [f],[g]\rangle\\[0.5em]
\end{array}
\]
\item For truncations ($i\leqslant n$)
\[
\begin{array}{lcl}
  \left[  \|A\|_i \right] &\defeq& (\modal \| \Lbrack A\Rbrack  \|_i;
                                   \pi_\modal(\| \Lbrack A\Rbrack
                                   \|_i)) \\[0.5em]
  \left[ |t|_i \right] &\defeq& \eta |[t]|_i \\[0.5em]
  \left[ |f|_i \right] &\defeq& \modal_{\mathrm{rec}}^{\| \Lbrack
                                  A\Rbrack  \|_i} | [f] |_i
\end{array}
\]

\end{itemize}

Let us make it more explicit on inductive types. In Coq, inductive
types are all of the following form (we leave the mutual inductive
types, behaving in the same way):
\newcommand{\I}{\mathbb{I}}
\begin{align*}
  \I &~(a_1:A_1)\cdots (a_n:A_n)
  : \Type \defeq \\
     &| c_1 : \prodD{x_1}{X_1^1}{\cdots
       \prodD{x_{n_1}}{X_1^{n_1}}{\I(a_1^1,\ldots,a_1^n)}} \\
     & \qquad \qquad \vdots \\
     &| c_p : \prodD{x_1}{X_p^1}{\cdots
       \prodD{x_{n_1}}{X_p^{n_1}}{\I(a_p^1,\ldots,a_p^n)}} \\
\end{align*}
with technical conditions on the $X_i^j$ to avoid ill-defined types.
For every such inductive type, we build a new one 
\newcommand{\II}{\widehat \I}
$\II$ defined by
\begin{align*}
%  \todo[fancyline]{Insert a new delimiter here}
  \II &~(a_1:\Lbrack A_1\Rbrack)\cdots (a_n:\Lbrack A_n \Rbrack)
        : \Type \defeq \\
      &| \widehat{c_1} : \prodD{x_1}{\lceil X_1^1\rceil}{\cdots
        \prodD{x_{n_1}}{\lceil X_1^{n_1}\rceil}{\II([a_1^1],\ldots,[a_1^n])}} \\
      & \qquad \qquad \vdots \\
      &| \widehat{c_p} : \prodD{x_1}{\lceil X_p^1\rceil}{\cdots
        \prodD{x_{n_1}}{\lceil X_p^{n_1}\rceil}{\II([a_p^1],\ldots,[a_p^n])}} \\
\end{align*}
where $\lceil\bullet\rceil$ is
defined by
\[
  X = \left\{
  \begin{array}{lcl}
    \II([b_1],\ldots,[b_n]) & \text{ if }& X \text{ is } \I(b_1,\ldots,b_n)\\
    \Lbrack X \Rbrack & \text{ else}& 
  \end{array} \right.
\]
Then, the translation of $\I(a_1,\ldots,a_n)$ is defined as $\modal (\II([a_1],\ldots,[a_n]))$.

\begin{exm}
Consider the following inductive
\begin{align*}
  \mathrm{q} &~(A:\Type)
  : \Type \defeq \\
     &| \alpha : \mathrm q \two \\
     &| \beta : A \to \mathrm q\one \to \mathrm q A
\end{align*}
Then the inductive $\widehat{\mathrm{q}}$ is 
\begin{align*}
  \widehat{\mathrm{q}} &~(A:\Type^\modal)
  : \Type \defeq \\
     &| \widehat\alpha : \mathrm{q} (\modal\widehat\two) \\
     &| \widehat\beta : \pi_1A \to \widehat{\mathrm{q}}(\modal\widehat\one) \to
       \widehat{\mathrm q} A
\end{align*}  
and the translation of $\mathrm q A$ is thus $\modal(\widehat{\mathrm q}[A])$.
\end{exm}


Then, we translate contexts pointwise:
\begin{align*}
  [\emptyset] &\defeq \emptyset \\
  [\Gamma,x:A] &\defeq [\Gamma],x:\Lbrack A\Rbrack
\end{align*}

As in the forcing translation~\cite{jaber2012extending}, the main
issue is that convertibility might not be preserved. For
example, let $f:A \to X$ and $g:B\to X$. Then $\langle f,g\rangle
(\mathrm{in}_\ell t)$ is convertible to $f\,t$, but $[\langle f,g\rangle
(\mathrm{in}_\ell t)]$ reduces to $\modal_{\mathrm{rec}}^{\Lbrack A\Rbrack +
                                      \Lbrack
                                      B\Rbrack}\langle[f],[g]\rangle(\eta(\mathrm{in}_\ell
                                    t))$, which is only equal to $[f\,t]$.


Two solutions to this problem can come to our mind:
\begin{itemize}
\item We could use the eliminator $J$ of equality in the conversion
  rule, but this would require to use a type theory with explicit
  conversion in the syntax, like in~\cite{jaber2012extending}. Such
  type theories has been studied
  in~\cite{geuvers2004,van2013explicit}. We do not chose this
  solution, and thus do not give more details.
\item We can ask the modality $\modal$ to be a strict modality, in the
  sense that retraction in the equivalence of $(-\circ\eta)$ is conversion
  instead of equality, like for the closed modality. 
  That way, we keep the conversion rule, \ie{} if $\Gamma \vdash
  u \equiv v$, then $\Lbrack \Gamma \Rbrack \vdash [u] \equiv [v]$.
  That is the solution we chose.
\end{itemize}


We first want to show that the translation respects substitution:

\begin{prop}
  If $\Gamma \vdash A:\Type$, $\Gamma,x:A \vdash B:\Type$ and $\Gamma,x:A \vdash b:B$, then 
  \[ [b[a/x]] \equiv [b][[a]/x]. \]
\end{prop}
\begin{proof}
It can be shown directly by induction on the term $b$.
%   We prove it by induction on the term $b$.
%   \begin{itemize}
%   \item $b$ is a variable. Then if $b$ is $x$, $[b[a/x]] \equiv [a]
%     \equiv [b][[a]/x]$. If $b$ is not $x$, then $[b[a/x]] \equiv [b]
%     \equiv b \equiv [b][[a]/x]$.
%   \item $b$ is $\Type$. Then $x$ does not appear in $b$ or $[b]$.
%   \item $b$ is $\sumD u X B$. Then two cases arise:
%     \begin{itemize}
%     \item $x$ is $u$. Then $b[a/x] \equiv \sumD u {X[a/x]} B$, and
%       \begin{align*}
%         [b[a/x]] &\equiv \left[\sumD u {X[a/x]} B\right] \\
%                  &\equiv \left( \sumD u {[X[a/x]]} [B];
%                    \pi_\Sigma^{[X[a/x]],[B]}\right) \\
%                  &\equiv \left( \sumD u {[X][[a]/x]} [B];
%                    \pi_\Sigma^{[X][[a]/x],[B]}\right) \\
%                  &\equiv [b][[a]/x]
%       \end{align*}
%     \item The case when $x$ is not $u$ is similar.
%     \end{itemize}

% $b[a/x] \equiv \sumD u {X[a/x]} {B[a/x]}$


%   \item $b$ is $\lambda\, u:X,\,t$. If $x$ is not $u$, then $b[a/x]
%     \equiv \lambda\,u:X[a/x],\,t[a/x]$, so that 
%     \begin{align*}
%       [b[a/x]] &\equiv [\lambda\,u:X[a/x],\,t[a/x] \\
%                &\equiv \lambda\,u:[X[a/x]],\,[t[a/x]]\\
%                &\equiv \lambda\,u:\Lbrack X \Rbrack [[a]/x],\,[t][[a]/x]\\
%                &\equiv [b][[a]/x]
%     \end{align*}
%     If $x$ is $u$, the proof is similar.
%   \item $b$ is the application $u(v)$. Then $b[a/x] \equiv
%     u[a/x]v[a/x]$, so that
%     \begin{align*}
%       [b[a/x]] &\equiv [u[a/x]v[a/x]] \\
%                &\equiv [u[a/x]] [v[a/x]] \\
%                &\equiv [u][[a]/x] [v][[a]/x] \\
%                &\equiv [b][[a]/x]
%     \end{align*}
%   \end{itemize}
\end{proof}

The usual result we want about any translation is its soundness:
\begin{prop}[Soundness of the translation]
  Let $\Gamma$ is a valid context, $A$ a type and $t$ a term.
  If $\Gamma \vdash t : A$, then 
  \[\Lbrack \Gamma \Rbrack \vdash [t] : \Lbrack A \Rbrack. \]
\end{prop}
\begin{proof}
  We prove it by induction on the proof of $\Gamma \vdash t : A$. We
  use the name of rules as in~\cite[Appendix A]{hottbook}. We note $M$
  the predicate ``is modal''.
  
  \begin{itemize}
  \item $\Pi$-\textsc{form}: 
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack A \Rbrack : \Type$}
      \AxiomC{$[\Gamma,x:A]\vdash [B]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma,x:A] \vdash \Lbrack B \Rbrack : \Type$}
      \RightLabel{$\Pi$-\textsc{form}}
      \BinaryInfC{$[\Gamma] \vdash \prodD x {\Lbrack A \Rbrack}
        {\Lbrack B \Rbrack} : \Type$}
      \DisplayProof
    \end{center}
  }
  together with
  {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash [A]_2 : M(A)$}
      \AxiomC{$[\Gamma,x:A]\vdash [B]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma,x:A] \vdash [B]_2 : M(B)$}
      \BinaryInfC{$[\Gamma] \vdash \pi_{\Pi}^{[A]_2,[B]_2} :
        M\left(\prodD x {\Lbrack A \Rbrack}{\Lbrack B \Rbrack} \right)$}
      \DisplayProof
    \end{center}
  }
    yields 
    \[[\Gamma] \vdash \prodD x {\Lbrack A \Rbrack}{\Lbrack B \Rbrack}
      : [\Type] \]
    
  \item $\Pi$-\textsc{intro}:
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma,x:A] \vdash [b]:\Lbrack B \Rbrack$}
      \RightLabel{$\Pi$-\textsc{intro}}
      \UnaryInfC{$[\Gamma] \vdash \lambda\, x:\Lbrack A\Rbrack,\, [b]
        : \prodD x {\Lbrack A\Rbrack}{\Lbrack B\Rbrack}$}
      \DisplayProof
    \end{center}
  }
    
  \item $\Pi$-\textsc{elim}:
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [f] : \prodD x {\Lbrack
          A\Rbrack}{\Lbrack B\Rbrack}$}
      \AxiomC{$[\Gamma] \vdash [a]:\Lbrack A \Rbrack $}
      \RightLabel{$\Pi$-\textsc{elim}}
      \BinaryInfC{$[\Gamma] \vdash [f][a] : \Lbrack B \Rbrack [[a]/x]$}
      \DisplayProof
    \end{center}
  }
  \item As the translation go through dependent sums as well, the
    proof trees for $\Sigma$-\textsc{form}, $\Sigma$-\textsc{intro},
    $\Sigma$-\textsc{elim} and $\Sigma$-\textsc{comp} are similar.


  \item $\Pi$-\textsc{comp}:
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma,x:A] \vdash [b]:\Lbrack B\Rbrack$}
      \AxiomC{$[\Gamma] \vdash [a]:\Lbrack A\Rbrack$}
      \RightLabel{$\Pi$-\textsc{comp}}
      \BinaryInfC{$[\Gamma] \vdash (\lambda\,x:\Lbrack
        A\Rbrack,\,[b])([a]) \equiv [b][[a]/x] : \Lbrack B\Rbrack [[a]/x]$}
      \DisplayProof
    \end{center}
  }

  \item $+$-\textsc{form}:
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack A \Rbrack : \Type$}
      \AxiomC{$[\Gamma]\vdash [B]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack B \Rbrack : \Type$}
      \RightLabel{$+$-\textsc{form}}
      \BinaryInfC{$[\Gamma] \vdash {\Lbrack A \Rbrack} +
        {\Lbrack B \Rbrack} : \Type$}
      \RightLabel{$\pi_\modal^{{\Lbrack A \Rbrack} + {\Lbrack B \Rbrack}}$}
      \UnaryInfC{$[\Gamma] \vdash \modal\left({\Lbrack A \Rbrack} +
        {\Lbrack B \Rbrack}\right) : \Lbrack \Type \Rbrack$}
      \DisplayProof
    \end{center}
  }

  \item $+$-\textsc{intro${}_{1,2}$}:
    {\footnotesize
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack A \Rbrack : \Type$}
      \AxiomC{$[\Gamma] \vdash [B]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack B \Rbrack : \Type$}
      \AxiomC{$[\Gamma] \vdash [a]:\Lbrack A \Rbrack$}
      \RightLabel{$+$-\textsc{intro${}_1$}}
      \TrinaryInfC{$[\Gamma] \vdash \inl([a]) : \Lbrack A \Rbrack +
        \Lbrack B \Rbrack$}
      \UnaryInfC{$[\Gamma] \vdash \eta (\inl([a])) : \Lbrack A + B\Rbrack$}
      \DisplayProof
    \end{center}
  }

    and 
   
    {\footnotesize 
    \begin{center}
      \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack A \Rbrack : \Type$}
      \AxiomC{$[\Gamma] \vdash [B]:\Lbrack \Type \Rbrack$}
      \RightLabel{$\Sigma$-\textsc{elim}}
      \UnaryInfC{$[\Gamma] \vdash \Lbrack B \Rbrack : \Type$}
      \AxiomC{$[\Gamma] \vdash [b]:\Lbrack B \Rbrack$}
      \RightLabel{$+$-\textsc{intro${}_2$}}
      \TrinaryInfC{$[\Gamma] \vdash \inl([b]) : \Lbrack A \Rbrack +
        \Lbrack B \Rbrack$}
      \UnaryInfC{$[\Gamma] \vdash \eta (\inl([b])) : \Lbrack A + B\Rbrack$}
      \DisplayProof
    \end{center}
  }

 \item $+$-\textsc{elim}:
   We treat the non-dependent case.

   {\footnotesize
   \begin{center}
     \AxiomC{$[\Gamma]\vdash [C]:\Lbrack \Type \Rbrack$}
     \AxiomC{$[\Gamma] \vdash [f]:\Lbrack A \to C\Rbrack $}
     \AxiomC{$[\Gamma] \vdash [d]:\Lbrack B \to C\Rbrack $}
     \RightLabel{$+$-\textsc{elim}}
     \TrinaryInfC{$[\Gamma] \vdash \langle [f],[g]\rangle : \Lbrack A
       \Rbrack + \Lbrack B \Rbrack \to \Lbrack C\Rbrack$}
     \UnaryInfC{$[\Gamma] \vdash \modal_{\mathrm{rec}}^{\Lbrack A
       \Rbrack + \Lbrack B \Rbrack}  \langle [f],[g]\rangle :
     \modal \left( \Lbrack A
       \Rbrack + \Lbrack B \Rbrack \right) \to \Lbrack C \Rbrack$}
     % \AxiomC{$[\Gamma]\vdash [e]:\Lbrack A + B \Rbrack $}
     % \BinaryInfC{Foo}
     \DisplayProof
   \end{center}
 }

 \item $+$-\textsc{comp}${}_{1,2}$:
   Again, we only treat the non-dependent case.
   {\footnotesize
   \begin{center}
     \AxiomC{$[\Gamma]\vdash [C]:\Lbrack \Type \Rbrack$}
     \AxiomC{$[\Gamma] \vdash [f]:\Lbrack A \to C\Rbrack $}
     \AxiomC{$[\Gamma] \vdash [d]:\Lbrack B \to C\Rbrack $}
     \AxiomC{$[\Gamma] \vdash [a] : \Lbrack A \Rbrack$}
     \RightLabel{$+$-\textsc{comp}${}_1$}
     \QuaternaryInfC{$[\Gamma] \vdash \langle [f],[g]\rangle (\inl [a])
       \equiv [f][a] : \Lbrack C \Rbrack$}
     \RightLabel{$\modal_{\mathrm{strict}}$}
     \UnaryInfC{$[\Gamma] \vdash \modal_{\mathrm{rec}}^{\Lbrack A
       \Rbrack + \Lbrack B \Rbrack}  \langle [f],[g]\rangle (\eta(\inl
     [a])) \equiv [f][a] : \Lbrack C \Rbrack$}
     \DisplayProof
   \end{center}
 }
   $+$-\textsc{comp}${}_{2}$ is done in the same way.

 \item $=$-\textsc{form}:
   {\footnotesize
   \begin{center}
     \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
     \RightLabel{$\Sigma$-\textsc{elim}}
     \UnaryInfC{$[\Gamma] \vdash \Lbrack A \Rbrack : \Type$}
     \AxiomC{$[\Gamma] \vdash [a],[b]:\Lbrack A \Rbrack$}
     \RightLabel{$=$-\textsc{form}}
     \BinaryInfC{$[\Gamma] \vdash [a] = [b] : \Type$}
     \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
     \RightLabel{$\Sigma$-\textsc{elim}}
     \UnaryInfC{$[\Gamma] \vdash [A]_2 : M(A)$}
     \UnaryInfC{$[\Gamma] \vdash \pi_=^{[a],[b]} : M([a] = [b])$}
     \RightLabel{$\Sigma$-\textsc{intro}}
     \BinaryInfC{$[\Gamma] \vdash [a]=[b] : \Lbrack \Type \Rbrack$}
     \DisplayProof
   \end{center}
 }
    
 \item $=$-\textsc{intro}:
   {\footnotesize
   \begin{center}
     \AxiomC{$[\Gamma] \vdash [A]:\Lbrack \Type \Rbrack$}
     \AxiomC{$[\Gamma] \vdash [a]:\Lbrack A \Rbrack$}
     \RightLabel{$=$-\textsc{intro}}
     \BinaryInfC{$[\Gamma] \vdash 1_{[a]} : [a] = [a]$}
     \DisplayProof
   \end{center}
 }

 \item $=$-\textsc{elim}: 
   We only treat $\transport$.
   {\footnotesize
   \begin{center}
     \AxiomC{$[\Gamma,x:A] \vdash [P]:\Lbrack \Type \Rbrack $}
     \RightLabel{$\Sigma$-\textsc{elim}}
     \UnaryInfC{$[\Gamma,x:A] \vdash \Lbrack P \Rbrack : \Type$}
     \AxiomC{$[\Gamma] \vdash [a],[b]:\Lbrack A \Rbrack$}
     \AxiomC{$[\Gamma] \vdash [p] : [a] = [b] $}
     \AxiomC{$[\Gamma] \vdash [u] : \Lbrack P\, a\Rbrack$}
     \RightLabel{$=$-\textsc{elim}}
     \QuaternaryInfC{$[\Gamma] \vdash \transport_{\Lbrack P \Rbrack}^{[p]} [u] :
       [P][b]$}
     \DisplayProof
   \end{center}
 }
   

  \end{itemize}
\end{proof}

This allows to state the following theorem
\begin{thm}\label{prop:consistent}
  Let $\modal$ be a modality on $\Type$ such that
  \begin{itemize}
  \item $\modal$ is left-exact
  \item $\Type^\modal$ is itself modal
  \item For all $A,B,f,x$, $\modal_{\mathrm{rec}}^\beta (A,B,f,x)$ is
    a strict equality.
  \end{itemize}
  Then $\modal$ induces a new type theory.
\end{thm}


\begin{rmq}
Note that, for any (accessible) modality $\modal$, we can define an equivalent
strict modality, by defining an inductive family $\modal^S$ generated by
\[ \left.
    \begin{array}{lll}
      \eta^S & : & \prodD A \Type {A \to \modal^S A} \\
    \end{array}
    \right.
\]
with an axiom asserting that all $\modal^S A$ are $\modal$-modal, and
an induction principle restricted to $\modal$-modals types
{\large \[\textstyle{
  \prodD A \Type {%
    \prodD B {\modal^S A\to\Type^\modal}
      {\prodD a A {B(\eta^S_A a)} \to \prodD a {\modal^S A} {B\, a}%
      }%
    }%
}.\]}%
As in~\cite{shulman-localization}, we can change the axiom by the equivalent
\[
  \prodD A \Type {\IsEquiv (\eta_A : A \to \modal A)},
\] and unfold the definition of $\IsEquiv$ to see that $\modal^S$ is a
valid HIT.
We are actually building $\modal^S$ as the {\em
  localization}~\cite[Definition 5.2.7.2]{lurie} of $\modal$-modal
types. This idea is developed in~\cite{shulman-mod-hits}.

Then, it is
straightforward to see that $\modal^S$ is a strict modality,
equivalent to $\modal$.
\end{rmq}

According to the previous remark, the classical situation fulfilling
the requirements is when the modality $\modal$ is left-exact and
accessible. One example is the closed
modality~\cite[Modalities/Closed.v]{hottlib}.

Note that univalence axiom remains true in the new theory:
\begin{prop}\label{prop:univalence_modal}
  Let $\modal$ be as in theorem~\ref{prop:consistent}. Then the
  univalence axiom remains true in the new type theory.
\end{prop}
\begin{proof}

  \begin{lem}
    We begin by showing that for any arrow $f:A \to B$, $[\IsEquiv(f)]
    = \IsEquiv[f]$.
  \end{lem}
  \begin{prooflem}
    Let $A,B:\Type$ and $f:A\to B$. Then 
    \[\IsEquiv(f) \defeq \sumD g {B\to A} 
      {\sumD r {\prodD y B {f(g(y)) = y}}
        {\sumD s {\prodD x A {g(f(x)) = x}}
          {\prodD x A {\ap f r(x) = s(f x)}}}}.
    \]
    As the translation go through dependent product and sums, and
    through path elimination, it is straightforward that 
    $[\IsEquiv(f)] = \IsEquiv [f]$.
  \end{prooflem}

  Now, 
  \begin{align*}
    [\mathrm{idtoequiv}_{A,B}] 
    &= [\lambda\, (p:A=B),~\transport_{A\simeq \bullet}^p (\id)]  \\
    &= \lambda\, (p:\Lbrack A \Rbrack =\Lbrack B\Rbrack ),~\transport_{\Lbrack
      A\Rbrack \simeq \bullet}^p (\id) \\
    &= \mathrm{idtoequiv}_{\Lbrack A \Rbrack,\Lbrack B \Rbrack}
  \end{align*}
  As univalence is true in the original type theory, we have 
  $A:\Type,B:\Type \vdash \IsEquiv(\mathrm{idtoequiv}_{A,B})$. By the
  soundness theorem, we have
  \[A : \Type^\modal,B:\Type^\modal \vdash
    \IsEquiv(\mathrm{\mathrm{idtoequiv}}_{A_1,B_1}). \]
 

\end{proof}

\begin{rmq}
  We note that if the modality is not left-exact (or not accessible),
  like truncations
  modalities, then $\Type^\modal$ is not itself modal. It is although
  still possible to write a translation, but we can only define it on
  a type theory with only one universe. Indeed, the judgement $\Gamma
  \vdash \Type^i : \Type^j$ cannot be expressed, and thus cannot be
  translated to $\Lbrack \Gamma \Rbrack \vdash [\Type^i] :
  \Lbrack \Type^j \Rbrack$. 
\end{rmq}

An implementation of this translation has been made, in the form of a
Coq plugin, available at
\url{https://github.com/KevinQuirin/translation-mod/}. We give here a
brief description.
For each module, there is a table $T$ containing a list of pairs
consisting of constants $c$ (resp. inductive type $i$) together with
its translation $[c]$ (resp. another inductive type $[i]$). 
Each time we need the translation of a constant, the plugin read this
table to find it.
Then, we add two new commands in Coq: \texttt{Modal Definition} and
\texttt{Modal Translate}.

\texttt{Modal Definition} allows to give a definition in the reflective
subuniverse; 
\[\texttt{Modal Definition foo : bar using $\modal$}\]
open a new goal of type $[\texttt{bar}]$, waits for the user to give a
proof, and define a new term $\texttt{foo}^m:[\texttt{bar}]$ and a new
constant $\texttt{foo}:\texttt{bar}$ at the
\texttt{Defined} command. Then, it adds in $T$ a new pair
$(\texttt{foo},\texttt{foo}^m)$.

\texttt{Modal Translate} allows to translate automatically a
previously existing constant or inductive type.
If $\texttt{foo} \defeq \texttt{qux} : \texttt{bar}$ is a constant,
\[\texttt{Modal Translate foo using $\modal$}\]
computes the value of $[\texttt{foo}]$, and add in $T$ the pair
$(\texttt{foo},[\texttt{foo}])$.
If $I (x_1 : A_1) \cdots (x_n:A_n) : \Type$ is an inductive type with
$p$ constructors $C_i : T_i$, then the plugin builds a new inductive
type $I^m (x_1 : [A_1]) \cdots (x_n:[A_n]) : \Type$ with constructors 
$C_i^m : [T_i]$, and add $(I,I^m)$ in the table $T$. Then, the
translation of $I(t_1, \cdots, t_n)$ will be $\modal (I^m ([t_1], \cdots, [t_n]))$.



% \todo[inline]{Code the plugin, then plug it here}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: