From a7df1d8369103a006346ad66b416b573fd23cda6 Mon Sep 17 00:00:00 2001
From: Samy Avrillon <samy.avrillon@ens-lyon.fr>
Date: Tue, 3 Sep 2024 11:35:58 +0200
Subject: [PATCH] Suppression des slides superfules

---
 Report/M2Diapo.tex     | 82 ++++++++++++++++++++++++++----------------
 Report/headerDiapo.tex |  2 +-
 2 files changed, 52 insertions(+), 32 deletions(-)

diff --git a/Report/M2Diapo.tex b/Report/M2Diapo.tex
index 176384e..462b2c3 100644
--- a/Report/M2Diapo.tex
+++ b/Report/M2Diapo.tex
@@ -17,11 +17,6 @@
 		\maketitle
 	\end{frame}
 	
-	\section*{Table of contents}
-	\begin{frame}{Plan of the presentation}
-		\tableofcontents[hidesubsections]
-	\end{frame}
-	
 	\section{GATs and 2-sortification}
 	\begin{frame}{What is a GAT ?}
 		\begin{itemize}
@@ -404,35 +399,15 @@
 		\end{remark}
 	\end{frame}
 	
-	\section{The complete proof \& Discoveries}
-	
-	\begin{frame}{Structure of the global proof}
-		\begin{itemize}
-			\item Categories $\CC_i$ \quad $\BB_i$
-			\item Functors $F_i : \BB_i \to \CC_i : G_i$
-			\item Adjunction $F_i \vdash G_i$
-			\item Forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$
-			\item Operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ \quad
-					$\inj_1^i : X \to X \tl^i Y$ \quad
-					$\inj_2^i : Y \to R_0^i(X \tl^i Y)$
-			\item Coreflection $F_iG_i \cong \Id_{\CC_i}$
-			\item Isomorphism $F_i\inj_1^i$
-			\item Isomorphism $(R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$
-		\end{itemize}
-	\end{frame}
-	
-	\begin{frame}{Fibration of $\CC_i$}
-		
-	\end{frame}
-	
-	\begin{frame}{$S_i$ from syntax}
-		
-	\end{frame}
-	
 	\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}
@@ -449,6 +424,51 @@
 		\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{itemize}
+			\item Categories $\CC_i$ \quad $\BB_i$
+			\item Functors $F_i : \BB_i \to \CC_i : G_i$
+			\item Adjunction $F_i \vdash G_i$
+			\item Forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$
+			\item Operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ \quad
+			$\inj_1^i : X \to X \tl^i Y$ \quad
+			$\inj_2^i : Y \to R_0^i(X \tl^i Y)$
+			\item Coreflection $F_iG_i \cong \Id_{\CC_i}$
+			\item Isomorphism $F_i\inj_1^i$
+			\item Isomorphism $(R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$
+		\end{itemize}
+	\end{frame}
+	
+	\begin{frame}{Fibration of $\CC_i$}
+		
+	\end{frame}
+	
+	\begin{frame}{$S_i$ from syntax}
+		
+	\end{frame}
+	
 \end{document} 
 
 
diff --git a/Report/headerDiapo.tex b/Report/headerDiapo.tex
index 263a04c..435f4fa 100644
--- a/Report/headerDiapo.tex
+++ b/Report/headerDiapo.tex
@@ -171,7 +171,7 @@
 
 \hypersetup{pdfpagemode=FullScreen}
 % Transition en fade-in par défaut
-\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}
+%\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}
 
 \addtobeamertemplate{frametitle}{
 	\let\insertframetitle\insertsubsectionhead}{}