Skip to content
Snippets Groups Projects
Commit 917ee033 authored by ghondet's avatar ghondet
Browse files

Diagram for proof irrelevance

parent e98ca1cc
No related branches found
Tags phdSlides@v1
No related merge requests found
......@@ -492,34 +492,25 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
% \end{thebibliography}
\end{frame}
\begin{frame}
\frametitle{Proof irrelevance in \lpmr}
\onslide<+->
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{exampleblock}{}
Assume
\begin{itemize}
\item \(z_1 = \tapp{\epair, 0, h_1}: \tapp*{\El, \tapp{\epsub, \N, P}}\),
\item \(z_2 = \tapp{\epair, 0, h_2}: \tapp*{\El, \tapp{\epsub, \N, P}}\)
\end{itemize}
\end{exampleblock}
\end{column}
\begin{column}{0.5\textwidth}
\onslide<+->
If \(h_1 \ne h_2\), then \(\alert{z_1 \ne z_2}\)
\end{column}
\end{columns}
\onslide<+->
\vfill
\begin{block}{Embedding proof irrelevance}
\begin{center}
\( \tapp*{\epair, 0, h_1} \onslide<+->{\rw \tapp*{\epair*, 0} \wr} \tapp*{\epair, 0, h_2} \)
\end{center}
\end{block}
\begin{frame}{Proof irrelevance in \lpmr}
\begin{center}
\begin{tikzpicture}[node distance = 2cm and 4cm]
\node (pcert-left) {\(\tapp*{\tpair, v, g}\)};
\node [right = of pcert-left] (pcert-right) {\(\tapp*{\tpair, v, h}\)};
\node [below = of pcert-left] (lpcert-left) {\(\tapp*{\epair, [v], [g]}\)};
\node [below = of pcert-right] (lpcert-right) {\(\tapp*{\epair, [v], [h]}\)};
\draw [->] (pcert-left) -- (lpcert-left);
\draw [->] (pcert-right) -- (lpcert-right);
\onslide<2->
\draw [<->, double] (pcert-left) -- (pcert-right);
\onslide<3->
\node [below = of lpcert-left] (lpcert-left-virt) {};
\node [below = of lpcert-right] (lpcert-right-virt) {};
\path (lpcert-left-virt) -- (lpcert-right-virt) node[midway] (lpcert-pair-p) {\(\tapp*{\epair*, v}\)};
\draw [->] (lpcert-left) -- (lpcert-pair-p);
\draw [->] (lpcert-right) -- (lpcert-pair-p);
\end{tikzpicture}
\end{center}
\end{frame}
\begin{frame}{Preservation of typing}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment