Plan complet

Report/M2Diapo.tex

@@ -106,7 +106,7 @@
 			\only<3>{\quad$\left(\Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right)$}
 		\end{tabular}
 		
-		\pause[3]
+		\pause[4]
 		\[\begin{array}{rcl}
 			H_1(\bullet) &=& 1_\Set \\
 			H_2(X_\Con) &=& X_\Con \\
@@ -247,6 +247,50 @@
 		\]
 	\end{frame}
 	
+	\begin{frame}{Adjunction $F \vdash G$}
+		
+	\end{frame}
+	
+	\begin{frame}{$FG \cong \Id$}
+		
+	\end{frame}
+	
+	\begin{frame}{Structure of the proof}
+		\begin{itemize}
+			\item $\CC_i$
+			\item $\BB_i$
+			\item $R_{i-1}^i : \BB_i \to \BB_{i-1}$
+					$R_0^i : \BB_i \to \BB_0$
+			\item $\tl^i : \BB_i \times \BB_0 \to \BB_i$
+					$\inj_1^i : X \to X \tl^i Y$
+					$\inj_2^i : Y \to R_0^i(X \tl^i Y)$
+			\item $F_i : \BB_i \to \CC_i : G_i$
+			\item $F_i \vdash G_i$
+			\item $F_iG_i \cong \Id_{\CC_i}$
+			$F_i\inj_1^i$
+			\item $(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}
+	
+	\begin{frame}{Conclusion}
+		
+	\end{frame}
+	
+	\begin{frame}{Future work}
+		\begin{itemize}
+			\item Complete GAT
+			\item Proof Assistant Formalization
+			\item $S_i$ non-direct
+		\end{itemize}
+	\end{frame}
 	
 \end{document}