Mysaa/M2Internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Suppression des slides superfules

Browse Source
This commit is contained in:
Samy Avrillon 2024-09-03 11:35:58 +02:00
parent c36520f1a3
commit a7df1d8369
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
2 changed files with 52 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

72
Report/M2Diapo.tex
View File

@ -17,11 +17,6 @@
\maketitle \maketitle
\end{frame} \end{frame}
\section*{Table of contents}
\begin{frame}{Plan of the presentation}
\tableofcontents[hidesubsections]
\end{frame}
\section{GATs and 2-sortification} \section{GATs and 2-sortification}
\begin{frame}{What is a GAT ?} \begin{frame}{What is a GAT ?}
\begin{itemize} \begin{itemize}
@ -404,7 +399,52 @@
\end{remark} \end{remark}
\end{frame} \end{frame}
\section{The complete proof \& Discoveries} \section{Conclusion}
\begin{frame}{Conclusion}
\begin{center}
\hspace{2ex}$\CC$ \hspace{3.5cm} $\BB$
\vspace{.5cm}
\includesvg[scale=.4]{graphs/diagrammeFG.svg}
\end{center}
\end{frame}
\begin{frame}{Future work}
\begin{itemize}
\item Complete GAT (term constructors + equalities)
\item Proof Assistant Formalization
\item $S_i$ non-direct
\end{itemize}
\end{frame}
\begin{frame}
\begin{center}
\Large Thank you for your attention
\end{center}
\end{frame}
\appendix
\begin{frame}
\[\begin{array}{lcl}
F_3G_3(Y)_\Con &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Con\})\\
&=& G_3(Y)_p^{-1}(\{\inj_1 \star\}) \\
&=& Y_\Con
\end{array}\]
and
\[\begin{array}{lcl}
F_3G_3(Y)_\Ty(\Gamma) &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Ty(\Gamma)\})\\
&=& G_3(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
&=& \operatorname{proj}_1^{-1}(\Gamma) \\
&=& \left\{(\Gamma',A) \in \coprod_{\Gamma' \in Y_\Con}Y_\Ty(\Gamma') \middle| \Gamma' = \Gamma\right\}\\
&\simeq& Y_\Ty(\Gamma)
\end{array}\]
and finally, with the same method, we get that
\[
F_3G_3(Y)_\Tm(\Delta,A) \simeq Y_\Tm(\Delta,A)
\]
\end{frame}
\begin{frame}{Structure of the global proof} \begin{frame}{Structure of the global proof}
\begin{itemize} \begin{itemize}
@ -429,26 +469,6 @@
\end{frame} \end{frame}
\section{Conclusion}
\begin{frame}{Conclusion}
\end{frame}
\begin{frame}{Future work}
\begin{itemize}
\item Complete GAT (term constructors + equalities)
\item Proof Assistant Formalization
\item $S_i$ non-direct
\end{itemize}
\end{frame}
\begin{frame}
\begin{center}
\Large Thank you for your attention
\end{center}
\end{frame}
\end{document} \end{document}

2
Report/headerDiapo.tex
View File

@ -171,7 +171,7 @@
\hypersetup{pdfpagemode=FullScreen} \hypersetup{pdfpagemode=FullScreen}
% Transition en fade-in par défaut % Transition en fade-in par défaut
\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{} %\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}
\addtobeamertemplate{frametitle}{ \addtobeamertemplate{frametitle}{
\let\insertframetitle\insertsubsectionhead}{} \let\insertframetitle\insertsubsectionhead}{}