\newcommand{\timpl}[3]{#1 \typea #2 : #3}
\newcommand{\subimpl}[5]{#1 \typec #2 : #3 \suba #4 : #5}

\def\WfEmptyI{
  \UAX{WfEmpty}
  {}
  {$\wf []$}
  {}
}  
  
\def\WfVarI{
  \UAX{WfVar}
  {$\timpl{`G}{A}{s}{`G'}{A'}{s}$}
  {$\wf `G', x : A'$}
  {$s `: \{ \Set, \Prop, \Type \}$}
}

\def\PropSetI{
  \UAX{PropSet}
  {$\wf `G'$}
  {$\timpl{`G}{s}{\Type(0)}{`G'}{s}{\Type}$}
  {$s `: \{ \Prop, \Set \}$} 
}

\def\TypeTypeI{
  \UAX{Type}
  {$\wf `G "~>" \wf `G$}
  {$\timpl{`G}{\Type(i)}{\Type(i + 1)}{`G'}{\Type(i)}{\Type(i + 1)}$}
  {}
}

\def\VarI{
  \BAX{Var}
  {$\wf `G'$}
  {$x : A' `: `G'$}
  {$\timpl{`G}{x}{A}{`G'}{x}{A'}$}
  {}
}

\def\ProdI{
  \BAX{Prod}
  {$\timpl{`G}{T}{s_1}{`G'}{T'}{s_1}$}
  {$\timpl{`G, x : T}{U}{s_2}{`G', x : T'}{U'}{s_2}$}
  {$\timpl{`G}{\Pi x : T.U}{s_3}{`G'}{\Pi x : T'.U'}{s_3}$}
  {$(s_1, s_2, s_3) `: \mathcal{R}$}
}

\def\AbsI{
  \BAX{Abs}
  {$\timpl{`G}{\Pi x : T. U}{s}{`G'}{\Pi x : T'. U'}{s}$}
  {$\timpl{`G, x : T}{M}{U}{`G', x : T'}{M'}{U'}$}
  {$\timpl{`G}{\lambda x : T. M}{\Pi x : T.U}
    {`G'}{\lambda x : T'. M'}{\Pi x : T'.U'}$}
  {}
}

\def\AppI{
  \QAX{App}
  {$\timpl{`G}{f}{T}{`G'}{f'}{T'}$}
  {$\mu~T' `= (\pi, \Pi x : V'. W')$}
  {$\timpl{`G}{u}{U}{`G'}{u'}{U'}$}
  {$\subimpl{`G'}{c}{U'}{V'}$}
  {$\timpl{`G}{f u}{W[u/x]}{`G'}{(\pi~f')~(c~u')}{W'[ c~u' / x ]}$}
  {}
}

\def\LetInI{
  \BAX{LetIn}
  {$\timpl{`G}{t}{T}{`G'}{t'}{T'}$}
  {$\timpl{`G, x : T}{v}{V}{`G', x : T'}{v'}{V'}$}
  {$\timpl{`G}{\letml~x = t~\inml~v}{V[t / x]}
    {`G'}{\letml~x = t'~\inml~v'}{V'[t' / x]}$}
  {}
}

\def\SigmaRI{
  \BAX{Sigma}
  {$\timpl{`G}{T}{s}{`G'}{T'}{s}$}
  {$\timpl{`G, x : T}{U}{s}{`G', x : T'}{U'}{s}$}
  {$\timpl{`G}{\Sigma x : T.U}{s}{`G'}{\Sigma x : T'.U'}{s}$}
  {$s `: \{ \Prop, \Set \} `^ x `; `G$}
}


\def\SumInfI{
  \TAXWide{SumInf}
  {$\timpl{`G}{t}{T}{`G'}{t'}{T'}$}
  {$\timpl{`G}{u}{U}{`G'}{u'}{U'}$}
  {$\timpl{`G}{\Sigma \_ : T.U}{s}{`G'}{\Sigma \_ : T'.U'}{s}$}
  {$\timpl{`G}{(t, u)}{\Sigma \_ : T.U}{`G'}{(t', u')}{\Sigma \_ : T'.U'}$}
  {}
}

\def\SumDepI{
  \TAXWide{SumDep}
  {$\timpl{`G}{t}{T}{`G'}{t'}{T'}$}
  {$\timpl{`G}{u}{U[t/x]}{`G'}{u'}{U'[t'/x]}$}
  {$\timpl{`G}{\Sigma x : T.U}{s}{`G'}{\Sigma x : T'.U'}{s}$}
  {$\timpl{`G}{(x \coloneqq t, u : U)}{\Sigma x : T.U}{`G'}{(t', u')}{\Sigma x : T'.U'}$}
  {}
}
 
\def\LetSumI{
  \BAX{LetSum}
  {$\timpl{`G}{t}{\Sigma x : T. U}{`G'}{t'}{\Sigma x : T'.U'}$}
  {$\timpl{`G, x : T, u : U}{v}{V}{`G, x : T', u : U'}{v'}{V'}$}
  {$\timpl{`G}{\letml~(x, u) = t~\inml~v}{V}
    {`G'}{\letml~(x, u) = t'~\inml~v'}{V'}$}
  {}
}

\def\SubsetI{
  \BAX{Subset}
  {$\timpl{`G}{U}{\Set}{`G'}{U'}{\Set}$}
  {$\timpl{`G, x : U}{P}{\Prop}{`G', x : U'}{P'}{\Prop} $}
  {$\timpl{`G}{\mysubset{x}{U}{P}}{\Set}{`G'}{\mysubset{x}{U'}{P'}}{\Set}$}
  {$$}
}

\def\marginleft{0em}

\def\typeiFig{
\begin{figure}[ht]
  \begin{center}
    \def\fCenter{\wf}
    \def\type{\typec}
    
    \WfEmpty\DP
    \quad$"~>"$\quad
    \WfEmptyI\DP

    \vspace{\infvspace}
    \WfVar\DP
    \quad$"~>"$\quad
    \WfVarI\DP
    
    \vspace{\infvspace}
    \PropSet\DP
    \quad$"~>"$\quad
    \PropSetI\DP
    
    \vspace{\infvspace}
    \Var\DP
    \quad$"~>"$\quad
    \VarI\DP
    
    \vspace{\infvspace}
    \Prod\DP
    \quad$"~>"$\quad
    \ProdI\DP
    
    \vspace{\infvspace}
    \Abs\DP
    \quad$"~>"$\quad
    \AbsI\DP
    
    \vspace{\infvspace}
    \App\DP
    \quad$"~>"$\quad
    \AppI\DP

%     \vspace{\infvspace}
%     \LetInI\DP
    
    \vspace{\infvspace}
    \SigmaR\DP
    \quad$"~>"$\quad
    \SigmaRI\DP

%     \vspace{\infvspace}
%     \SumInfI\DP

    \vspace{\infvspace}
    \SumDepA\DP
    \quad$"~>"$\quad
    \SumDepI\DP
    
    \vspace{\infvspace}
    \LetSum\DP
    \quad$"~>"$\quad
    \LetSumI\DP
    
    \vspace{\infvspace}
    \Subset\DP
    \quad$"~>"$\quad
    \SubsetI\DP
  \end{center}
  \caption{Réécriture du typage vers \CCI}
  \label{fig:typing-impl-rules}
\end{figure}
}

\def\typeiFigC{
\begin{figure}
  \begin{center} 
    \vspace{\infvspace}
    \App\DP
    \quad$"~>"$\quad
    \AppI\DP
    
    \vspace{\infvspace}
    \SumDepA\DP
    \quad$"~>"$\quad
    \SumDepI\DP
  \end{center}
  \caption{Réécriture du typage vers \CCI}
  \label{fig:typing-impl-rules-changed}
\end{figure}
}


\def\typemuiFig{
\begin{figure}[ht]
  \begin{eqnarray*}
    \muimplprim{\mysubset{x}{U}{P}}   & "=>" & \letml~(f, t) = \muimplprim{\hnf{U}}~\inml~(f `o
    \pi_1, t) \\
    \muimplprim{T}                        & "=>"  & (\sref{id}, T) \\
    \\
    \muimpl{T} & = & \muimplprim{\hnf{T}}
  \end{eqnarray*}
  \caption{Définition de $\muimpl$}
  \label{fig:muimpl-definition}
\end{figure}
}

\newcommand{\teqone}[5]{#1 \typea #2 : #3 "->"_{\beta\rho} #4 : #5}

\newcommand{\teq}[5]{#1 \typea #2 : #3 \eqbr #4 : #5}

\newcommand{\VarTeq}{
  \UAX{VarTeq}
  {}
  {$\teq{`G}{x}{X}{x}{X}$}
  {}
}

\newcommand{\SortTeq}{
  \UAX{SortTeq}
  {}
  {$\teq{`G}{s}{\Type}{s}{\Type}$}
  {$s `: \setprop$}
}

\newcommand{\BetaTeq}{
  %\AXC{$\talgo{`G, x : X}{v}{T'} \quad T'[e/x] \sub T \quad T \sub U$}
  %\AXC{$\talgo{`G}{e}{E} \quad X \sub E$}
  \UAX{BetaTeq}
  {$\subalgo{`G}{U}{T}$}
  {$\teq{`G}{(\lambda x : X.v)~e}{T}{v[e/x]}{U}$}
  {}
}

\newcommand{\PiLeftTeq}{
  \UAX{PiLeftTeq}
  {$\subalgo{`G}{U}{T}$}
  {$\teq{`G}{\pi_1~\pair{\Sigma x : T.V}{e_1}{e_2}}{T}{e_1}{U}$}
  {}
}

\newcommand{\PiRightTeq}{
  \UAX{PiRightTeq}
  {$\subalgo{`G}{U}{T}$}
  {$\teq{`G}{\pi_2~\pair{\Sigma x : V.T}{e_1}{e_2}}{T}{e_2}{U}$}
  {}
}

\newcommand{\LambdaTeq}{
  \BAX{LambdaTeq}
  {$\teq{`G}{X}{s_1}{X'}{s_1}$}
  {$\teq{`G, x : X'}{v}{Y}{v'}{Y'}$}
  {$\teq{`G}{\lambda x : X.v}{\Pi x : X.Y}{\lambda x : X'.v'}{\Pi x : X'.Y'}$}
  {}
}

\newcommand{\AppTeq}{
  \QAX{AppTeq}
  {$\teq{`G}{M}{S}{M'}{T}$}
  {$\mualgo{S} = \Pi x : A.B \quad \mualgo{T} = \Pi x : C.D$}
  {$\teq{`G}{N}{U}{N'}{V} \quad \subalgo{`G}{U}{A}$}
  {$\subalgo{`G}{V}{C}$}
  {$\teq{`G}{M~N}{B[N/x]}{M'~N'}{D[N'/x]}$}
  {}
}

\newcommand{\PairTeq}{
  \SAX{PairTeq}
  {$\teq{`G}{e_1}{A'}{e_1'}{C'}$}
  {$\teq{`G, x : A'}{e_2}{B'}{e_2'}{D'}$}
  {$\subalgo{`G}{A'}{A} \quad \subalgo{`G}{C'}{C}$}
  {$\subalgo{`G}{B'}{B[e_1/x]}$}
  {$\subalgo{`G}{D'}{D[e_1/x]}$}
  {$\teq{`G}{\pair{\Sigma x : A.B}{e_1}{e_2}}{\Sigma x : A.B}{\pair{\Sigma x :
        C.D}{e_1'}{e_2'}}{\Sigma x : C.D}$}
  {}
}

\newcommand{\PiTeq}{
  \BAX{PiTeq}
  {$\teq{`G}{C}{s_1}{A}{s_1}$}
  {$\teq{`G, x : A}{B}{s_2}{D}{s_2}$}
  {$\teq{`G}{\Pi x : A.B}{s_3}{\Pi x : C.D}{s_3}$}
  {}
}

\newcommand{\SigmaTeq}{
  \BAX{SigmaTeq}
  {$\teq{`G}{A}{s_1}{C}{s_1}$}
  {$\teq{`G, x : A}{B}{s_2}{D}{s_2}$}
  {$\teq{`G}{`S x : A.B}{s_3}{`S x : C.D}{s_3}$}
  {}
}

\newcommand{\SubsetTeq}{
  \BAX{SubsetTeq}
  {$\teq{`G}{T}{\Set}{A}{\Set}$}
  {$\teq{`G, x : T}{P}{\Prop}{P'}{\Prop}$}
  {$\teq{`G}{\mysubset{x}{T}{P}}{\Set}{\mysubset{x}{U}{P'}}{\Set}$}
  {}
}

\newcommand{\teqfig}{
  \begin{figure}[ht]
    \begin{center}
      \VarTeq\DP

      \vspace{\infvspace}
      \SortTeq\DP

      \vspace{\infvspace}
      \BetaTeq\DP
      
      \vspace{\infvspace}
      \PiLeftTeq\DP

      \vspace{\infvspace}
      \PiRightTeq\DP

      \vspace{\infvspace}
      \LambdaTeq\DP

      \vspace{\infvspace}
      \AppTeq\DP

      \vspace{\infvspace}
      \PairTeq\DP

      \vspace{\infvspace}
      \PiTeq\DP

      \vspace{\infvspace}
      \SigmaTeq\DP

      \vspace{\infvspace}
      \SubsetTeq\DP
    \end{center}
    \caption{Définition du jugement $\teq{`G}{t}{T}{u}{U}$}
  \label{fig:teq-rules}
\end{figure}

}

\newcommand{\interpfig}[1][Interprétation dans \CCI{}]{
\begin{figure}[ht]
  \[\begin{array}{lcll}
    \ip{x}{`G} & = & x & \\
    \\
    \ip{s}{`G} & = & s & s `: \setproptype\\
    \\
    \ip{\Pi x : T.U}{`G} 
    & = & \Pi x : \ip{T}{`G}.\ip{U}{`G, x : T} & \\
    & \\
    \ip{\lambda x : `t.v}{`G} 
    & = & \letml~`t' = \ip{`t}{`G}~\inml & \\
    & & \letml~v' = \ip{v}{`G, x : `t}~\inml & \\
    & & (\lambda x : `t'. v') & \\
    & \\
    \ip{f~u}{`G} 
    & = & \letml~F~=\typeafn{`G}{f}~\andml~U = \typeafn{`G}{u}~\inml & \\
    & & \letml~(\Pi x : V.W) = \mualgo{F}~\inml & \\
    & & \letml~\pi = \coerce{`G}{F}{(\Pi x : V.W)}~\inml & \\
    & & \letml~c = \coerce{`G}{U}{V}~\inml & \\
    & & (\pi[\ip{f}{`G}])~(c[\ip{u}{`G}]) & \\
    & \\
    \ip{\Sigma x : T.U}{`G} 
    & = & \Sigma x : \ip{T}{`G}.\ip{U}{`G, x : T} & \\
    & \\
    \ip{\pair{\Sigma x : T.U}{t}{u}}{`G}
    & = & \letml~t' = \ip{t}{`G}~\inml & \\
    & & \letml~T' = \typeafn{`G}{t}~\inml& \\
    & & \letml~ct = \coerce{`G}{T'}{T}~\inml& \\
    & & \letml~U' = \typeafn{`G}{u}~\inml& \\
    & & \letml~u' = \ip{u}{`G}~\inml & \\
    & & \letml~cu = \coerce{`G}{U'}{U[t/x]}~\inml & \\
    & & \pair{\ip{\Sigma x : T.U}{`G}}{ct[t']}{cu[u']} & \\
    & \\
    \ip{\pi_i~t}{`G} 
    & = & \letml~t' = \ip{t}{`G}~\inml & i `: \{ 1, 2 \} \\
    & & \letml~T = \typeafn{`G}{t}~\inml & \\
    & & \letml~\Sigma x : V.W = \mualgo{T}~\inml & \\
    & & \letml~c = \coerce{`G}{T}{(\Sigma x : V.W)}~\inml & \\
    & & \pi_i~c[t'] & \\
    & \\
    \ip{\mysubset{x}{U}{P}}{`G}
    & = & \mysubset{x}{\ip{U}{`G}}{\ip{P}{`G, x : U}}
  \end{array}\]
  \caption{#1}
  \label{fig:interp}
\end{figure}
}
\newcommand{\interparr}{
  \[\begin{array}{lcll}
    \ip{x}{`G} & = & x \\
    \ip{s}{`G} & = & s \hfill s `: \setproptype \\
    \ip{\Pi x : T.U}{`G} 
    & = & \Pi x : \ip{T}{`G}.\ip{U}{`G, x : T} \\
    \ip{\mysubset{x}{U}{P}}{`G}
    & = & \mysubset{x}{\ip{U}{`G}}{\ip{P}{`G, x : U}} \\
    \ip{\Sigma x : T.U}{`G} 
    & = & \Sigma x : \ip{T}{`G}.\ip{U}{`G, x : T} \\
    \ip{\lambda x : `t.v}{`G} 
    & = & (\lambda x : \ip{`t}{`G}. \ip{v}{`G, x : `t}) \\
    & \\
    \ip{f~u}{`G} 
    & = & \letml~F~=\typeafn{`G}{f}~\andml~U = \typeafn{`G}{u}~\inml  \\
    & & \letml~(\Pi x : V.W) = \mualgo{F}~\inml  \\
    & & \letml~\pi = \coerce{`G}{F}{(\Pi x : V.W)}~\inml  \\
    & & \letml~c = \coerce{`G}{U}{V}~\inml  \\
    & & (\pi[\ip{f}{`G}])~(c[\ip{u}{`G}]) \\
    & \\
    \ip{\pair{\Sigma x : T.U}{t}{u}}{`G}
    & = & \letml~T' = \typeafn{`G}{t}~\inml \\
    & & \letml~ct = \coerce{`G}{T'}{T}~\inml \\
    & & \letml~U' = \typeafn{`G}{u}~\inml \\
    & & \letml~cu = \coerce{`G}{U'}{U[t/x]}~\inml  \\
    & & \pair{\ip{\Sigma x : T.U}{`G}}{ct[\ip{t}{`G}]}{cu[\ip{u}{`G}]} \\
    & \\
    \ip{\pi_i~t}{`G} 
    & = & \letml~T = \typeafn{`G}{t}~\inml \hfill i `: \{ 1, 2 \} \\
    & & \letml~\Sigma x : V.W = \mualgo{T}~\inml  \\
    & & \letml~c = \coerce{`G}{T}{(\Sigma x : V.W)}~\inml \\
    & & \pi_i~c[\ip{t}{`G}]
  \end{array}\]}

\newcommand{\interpfigs}[1][Interprétation dans \CCI{}]{
\begin{figure}[ht]
  \interparr
  \caption{#1}
  \label{fig:interp}
\end{figure}
}
\newcommand{\ccqeqarr}{
  \[\begin{array}{llcll}
    (\beta) & (\lambda x : X.e)~v & `= & e[v/x] & \\
    (\pi_i) & \pi_i~\pair{T}{e_1}{e_2} & `= & e_i & \\
    (\sigma_i) & \sigma_i~(\elt{E}{P}{e_1}{e_2}) & `= & e_i & \\
    (\eta) & (\lambda x : X.e~x) & `= & e & \sidecond{$x `; FV(e)$} \\ % et $e : \Pi x : X.Y$} \\
    (\rho) & \pair{\Sigma x : X.Y}{\pi_1~e}{\pi_2~e} & `= & e & \sidecond{$e : \Sigma x : X. Y$} \\
    (\tau) & \elt{E}{P}{(\eltpit~e)}{(\eltpip~e)} & `= & e & \sidecond{$e : \mysubset{x}{E}{P}$} \\
    (\sigma) & \elt{E}{P}{t}{p} & `= & \elt{E}{P}{t'}{p'} & \sidecond{$t `= t'$}
  \end{array}\]}

\newcommand{\ccqeqfig}[1][Théorie équationnelle de \CCq{}]{
\begin{figure}[ht]
  \[\begin{array}{llcll}
    (\beta) & (\lambda x : X.e)~v & `= & e[v/x] & \\
    (\pi_i) & \pi_i~\pair{T}{e_1}{e_2} & `= & e_i & \\
    (\sigma_i) & \sigma_i~(\elt{E}{P}{e_1}{e_2}) & `= & e_i & \\
    (\eta) & (\lambda x : X.e~x) & `= & e & \sidecond{$x `; FV(e)$} \\ % et $e : \Pi x : X.Y$} \\
    (\rho) & \pair{\Sigma x : X.Y}{\pi_1~e}{\pi_2~e} & `= & e & \sidecond{$e : \Sigma x : X. Y$} \\
    (\tau) & \elt{E}{P}{(\eltpit~e)}{(\eltpip~e)} & `= & e & \sidecond{$e : \mysubset{x}{E}{P}$} \\
    (\sigma) & \elt{E}{P}{t}{p} & `= & \elt{E}{P}{t'}{p'} & \sidecond{$t `= t'$}
  \end{array}\]
  \caption{#1}
  \label{fig:eqccq}
\end{figure}
}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "subset-typing"
%%% LaTeX-command: "TEXINPUTS=\"style:$TEXINPUTS\" latex"
%%% End: