From b8ed28e8e4d184c2f3433b7bf91e9e4bb6af785b Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Tue, 3 Sep 2024 18:22:20 +0200 Subject: [PATCH] Quick fixes --- Report/M2Diapo.tex | 190 +++++++++++++++----------- Report/graphs/diagrammeFG.svg | 101 +++++++++++--- Report/graphs/diagrammeFGmini.svg | 216 ++++++++++++++++++++++++++++++ Report/graphs/diagrammeFmini.svg | 190 ++++++++++++++++++++++++++ Report/graphs/diagrammeGmini.svg | 190 ++++++++++++++++++++++++++ Report/headerDiapo.tex | 6 +- 6 files changed, 792 insertions(+), 101 deletions(-) create mode 100644 Report/graphs/diagrammeFGmini.svg create mode 100644 Report/graphs/diagrammeFmini.svg create mode 100644 Report/graphs/diagrammeGmini.svg diff --git a/Report/M2Diapo.tex b/Report/M2Diapo.tex index 462b2c3..c598b0c 100644 --- a/Report/M2Diapo.tex +++ b/Report/M2Diapo.tex @@ -2,6 +2,7 @@ \DocumentMetadata{} \documentclass[12pt,xcolor={dvipsnames},aspectratio=169]{beamer} + \input{./headerDiapo.tex} \title[Semantics of 2-sortification]{Categorical semantics of the reduction of GATs to two-sorted GATs. @@ -20,8 +21,8 @@ \section{GATs and 2-sortification} \begin{frame}{What is a GAT ?} \begin{itemize} - \item A dependent \textbf{type theory} - \item[\ding{220}] Enables to create sorts, object of those sorts, equalities between those objects + \item A \textbf{list} of declarations + \item[\ding{220}] Enables to declare sorts, objects of those sorts and equalities between those objects \item A \textbf{syntactic object} \item[\ding{220}] Type judgements are defined with induction rules \item Describes \textbf{models} @@ -35,10 +36,10 @@ \begin{columns} \begin{column}{.6\textwidth} \renewcommand\arraystretch{1.5} - \begin{tabular}{l} - $A : \Set$ \\ - $B : \Set$ \\\hline - $\operatorname{exec} : A \to B$ + \begin{tabular}{ll} + $A : \Set$&\multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{sorts}$}\\ + $B : \Set$&\\\hdashline + $\operatorname{exec} : A \to B$&$\}\text{constructors}$ \end{tabular} \end{column} \begin{column}{.4\textwidth} @@ -52,18 +53,19 @@ \begin{frame}{A GAT for an bijective function in Set} \begin{tcolorbox} \begin{columns} - \begin{column}{.6\textwidth} + \begin{column}{.7\textwidth} \renewcommand\arraystretch{1.5} - \begin{tabular}{l} - $A : \Set$ \\ - $B : \Set$ \\\hline - $\operatorname{exec} : A \to B$ \\ - $\operatorname{invexec} : B \to A$\\\hline - $\operatorname{isol} : (x : A) \to \operatorname{invexec}(\operatorname{exec}\;x) = x$\\ - $\operatorname{isor} : (y : B) \to \operatorname{exec}(\operatorname{invexec}\;y) = y$\\ + \begin{tabular}{ll} + $A : \Set$ & \multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{sorts}$}\\ + $B : \Set$ &\\\hdashline + $\operatorname{exec} : A \to B$ &\multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{constructors}$}\\ + $\operatorname{invexec} : B \to A$&\\\hdashline + $\operatorname{isol} : (x : A) \to \operatorname{invexec}(\operatorname{exec}\;x) = x$& + \multirow{2}{*}{$\left.\begin{array}{c}\\\\\end{array}\right\}\text{equalities}$}\\ + $\operatorname{isor} : (y : B) \to \operatorname{exec}(\operatorname{invexec}\;y) = y$&\\ \end{tabular} \end{column} - \begin{column}{.4\textwidth} + \begin{column}{.3\textwidth} Models: triples (A,B,f) @@ -80,12 +82,12 @@ \renewcommand\arraystretch{1.5} \begin{tabular}{l} $\Obj : \Set$ \\ - $\Hom : \Obj \to \Obj \to \Set$ \\\hline + $\Hom : \Obj \to \Obj \to \Set$ \\\hdashline $\id : (A : \Obj) \to \Hom\;A\;A$ \\ - $\operatorname{comp} : (A\;B\;C:\Obj) \to \Hom\;B\;C \to\Hom\;A\;B \to \Hom\;A\;C$ \\\hline - $\operatorname{idl}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \operatorname{comp} (\id\;B) \sigma = \sigma$\\ - $\operatorname{idr}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \operatorname{comp} \sigma (\id\;A) = \sigma$\\ - $\operatorname{comp-trans}: \dots$\\ + $\circ : (A\;B\;C:\Obj) \to \Hom\;B\;C \to\Hom\;A\;B \to \Hom\;A\;C$ \\\hdashline + $\operatorname{idl}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \circ\;(\id\;B)\;\sigma = \sigma$\\ + $\operatorname{idr}: (A B : \Obj) \to (\sigma : \Hom\;A\;B) \to \circ\;\sigma\;(\id\;A) = \sigma$\\ + $\operatorname{\circ-trans}: \dots$\\ \end{tabular} \end{column} \begin{column}{0.2\textwidth} @@ -105,7 +107,7 @@ \begin{tabular}{l} $\Con : \Set$ \\ $\Ty : \Con \to \Set$ \\ - $\Tm : (\Gamma : \Con) \to \Ty\;\Gamma \to \Set$ \\\hline + $\Tm : (\Gamma : \Con) \to \Ty\;\Gamma \to \Set$ \\\hdashline $\operatorname{empty}: \Con$ \\ $\operatorname{ext}: (\Gamma:\Con)\to(A:\Ty\;\Gamma)\to\Con$ \\ $\operatorname{implies} : (\Gamma:\Con) \to \Ty\;\Gamma \to \Ty\;\Gamma \to \Ty\;\Gamma$ \\ @@ -129,12 +131,17 @@ \end{tcolorbox} \end{frame} - \begin{frame}{2-sortification} + \begin{frame}{Subject of my internship}{2-sortification of GATs} \begin{center} {\large Transform a GAT into a GAT with only two sorts} - - \ding{229} Simplify a study of GATs \end{center} + \vspace{3ex} + + \ding{229} Process observed since at least 2021 + + \ding{229} Never formally studied + + \ding{229} Studying all GATs by only studying GATs with two sorts ? \end{frame} \begin{frame}{2-sortification of the Set Function GAT} \begin{tcolorbox} @@ -142,7 +149,7 @@ \begin{tabular}{llrcl} \pause $\mathcal{O} : \Set$ & \color{RoyalBlue} \text{sorts} & $o:\mathcal{O}$ &$\leftrightarrow$&$o$ is a sort \\ - $\El : \mathcal{O} \to \Set$ & \color{RoyalBlue}\text{objects of that sort} & \qquad $x : \El\;o$ & $\leftrightarrow$ & $x : \mathcal{O}$ \pause\\\hline + $\El : \mathcal{O} \to \Set$ & \color{RoyalBlue}\text{objects of that sort} & \qquad $x : \El\;o$ & $\leftrightarrow$ & $x : o$ \pause\\\hline $A : \mathcal{O}$ &&\multicolumn{1}{l}{\color{teal}$A : \Set$}&&\\ $B : \mathcal{O}$ &&\multicolumn{1}{l}{\color{teal}$B : \Set$}&&\\ $\operatorname{exec} : \El\;A \to \El\;B$&&\color{teal}$\operatorname{exec} : A \to B$&& @@ -171,7 +178,7 @@ \ding{229} Can one study all GATs by studying only GATs with two sorts \vspace{1ex} - {\large How to state this fact} + {\large How to state this fact ?} \ding{229} Semantical proof @@ -185,10 +192,11 @@ \section{One Example} - \begin{frame}{Constructing the categories} + \begin{frame}{Categories of models} \begin{center} + \renewcommand{\ULthickness}{2.4pt} \only<1>{GAT = sorts + constructors + equalities} - \only<2>{GAT = sorts + \sout{constructors} + \sout{equalities}} + \only<2>{GAT = \textbf{sorts} + \sout{constructors} + \sout{equalities}} \end{center} \pause[2] \begin{center} @@ -202,7 +210,7 @@ & $\begin{array}{l} \mathcal{O} : \Set\\ - \El : \mathcal{O} \to \Set \\\hline + \El : \mathcal{O} \to \Set \\\hdashline \underline{\Con} : \mathcal{O} \\ \underline{\Ty} : \El\;\underline{\Con} \to \mathcal{O} \\ \underline{\Tm} : (\Gamma : \El\;\underline{\Con}) \to \El(\underline{\Ty}\;\Gamma) \to \mathcal{O} @@ -222,27 +230,27 @@ \end{center} \end{frame} - \begin{frame}{Category of Models \& Generalization} + \begin{frame}{Categories of Models}{of the original GAT} \begin{tabular}{lcp{0.5\textwidth}} $\boxed{()}$ & $\CC_0 :=$ & $\one$ \\ $\boxed{\Con : \Set}$ & $\CC_1 := $& - \only<1>{$\left[X_\Con\right]$} - \only<2>{$\left[X_\Con : \Set\right]$} + \only<1>{$\left(X_\Con\right)$} + \only<2>{$\left(X_\Con : \Set\right)$} \only<3>{$(\bullet : \CC_0) \times \left(\Set\right)$} \only<4>{$\left(X : \CC_0\right) \times \Set^{H_1(X)}$} \\ $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ & $\CC_2 := $& - \only<1>{$\left[X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}\right]$} - \only<2>{$\left[X_\Con : \Set, X_\Ty : \Set^{X_\Con}\right]$} + \only<1>{$\left(X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}\right)$} + \only<2>{$\left(X_\Con : \Set, X_\Ty : \Set^{X_\Con}\right)$} \only<3>{$\left(X_\Con : \CC_1\right) \times \left(\Set^{X_\Con}\right)$} \only<4>{$\left(X : \CC_1\right) \times \Set^{H_2(X)}$} \\ $\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ & $\CC_3 :=$& - \only<1>{$\left[X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con},\right.$} - \only<2>{$\left[X_\Con : \Set, X_\Ty : \Set^{X_\Con},\right.$} + \only<1>{$\left(X_\Con, \left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con},\right.$} + \only<2>{$\left(X_\Con : \Set, X_\Ty : \Set^{X_\Con},\right.$} \only<3>{$\left((X_\Con,X_\Ty) : \CC_2\right) \times$} \only<4>{$\left(X : \CC_2\right) \times \Set^{H_3(X)}$} \\ && - \only<1>{$\left.\left(\left(X_\Tm(\Delta,A)\right)_{A \in \Ty(\Delta)}\right)_{\Delta \in X_\Con} \right]$} - \only<2>{\quad$\left.X_\Tm : \Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right]$} + \only<1>{$\left.\left(\left(X_\Tm(\Delta,A)\right)_{A \in \Ty(\Delta)}\right)_{\Delta \in X_\Con} \right)$} + \only<2>{\quad$\left.X_\Tm : \Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right)$} \only<3>{\quad$\left(\Set^{\prod_{\Delta:X_\Con}X_\Ty(\Delta)}\right)$} \end{tabular} @@ -254,7 +262,7 @@ \end{array}\] \end{frame} - \begin{frame}{Category of Models of transformed GAT} + \begin{frame}{Category of Models}{of the transformed GAT} \[ \begin{array}{|c|} \hline @@ -277,55 +285,70 @@ \end{frame} - \begin{frame}{Adding transformed sort declarations} + \begin{frame}{Category of Models}{of the transformed GAT} \begin{center} + \color{blue}{ \begin{tabular}{ll} $X_\UU$:& Sorts \\ $X_\El(o)$:& Objects of sort $o$\\ - \end{tabular} + \end{tabular}} \end{center} \begin{center} \renewcommand\arraystretch{1.4} \begin{tabular}{lrp{0.4\textwidth}} $\boxed{\mathcal{O} : \Set\quad\El : \mathcal{O} \to \Set}$ & $\BB_0 =$ & $(X_\UU,X_\El)$ \\ - $\boxed{\Con : \mathcal{O}}$ & $\Cstr_\Con :$ & + $\boxed{\Con : \mathcal{O}}$ & $\XCon_X :$ & \only<1>{$X_\UU$} \only<2>{$H_1F_0(X) \to X_\UU$} \\ - $\boxed{\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}}$ & $\Cstr_\Ty :$& - \only<1>{$\left(\Gamma \in X_\El(\Cstr_\Con)\right) \to X_\UU $} - \only<2>{$H_2F_1(X,\Cstr_\Con) \to X_\UU$} \\ - $\boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}}$ & $\Cstr_\Tm : $ & - \only<1>{\rule[6ex]{0pt}{0pt}\renewcommand\arraystretch{0.9}$\begin{array}{c}\left(\Delta \in X_\El(\Cstr_\Con)\right) \to\\ \left(A \in X_\El(\Cstr_\Ty(\Delta))\right) \to\\ X_\UU\end{array}$} - \only<2>{$H_3F_2(X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU$} + $\boxed{\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}}$ & $\XTy_X :$& + \only<1>{$\left(\Gamma \in X_\El(\XCon_X)\right) \to X_\UU $} + \only<2>{$H_2F_1(X,\XCon_X) \to X_\UU$} \\ + $\boxed{\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}}$ & + $\XTm_X : $ & + \only<1>{\rule[6ex]{0pt}{0pt}\renewcommand\arraystretch{0.9}$\begin{array}{c}\left(\Delta \in X_\El(\XCon_X)\right) \to\\ \left(A \in X_\El(\XTy_X(\Delta))\right) \to\\ X_\UU\end{array}$} + \only<2>{$H_3F_2(X,\XCon_X,\XTy_X) \to X_\UU$} \end{tabular} \end{center} + \pause + \begin{center} + \includesvg[scale=.4]{graphs/diagrammeFGmini.svg} + \end{center} \end{frame} - \begin{frame}{Constructing the functors} + \begin{frame}{Constructing $F$ and $G$} + + \begin{center} + \includesvg[scale=.4]{graphs/diagrammeFGmini.svg} + \end{center} \[ \begin{array}{l|l} Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline & X_\UU : \Set \quad X_\El : \Set^{X_\UU}\\ - Y_\Con : \Set & \Cstr_\Con : X_\UU \\ + Y_\Con : \Set & \XCon_X : X_\UU \\ \left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} & - \Cstr_\Ty : H_2 F_{1} (X,\Cstr_\Con) \to X_\UU \\ + \XTy_X : H_2 F_{1} (X,\XCon_X) \to X_\UU \\ \left(\left(Y_\Tm(\Delta,A)\right)_{A \in Y_\Ty(\Delta)}\right)_{\Delta \in Y_\Con} & - \Cstr_\Tm : H_3 F_{2} (X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU \\ + \XTm_X : H_3 F_{2} (X,\XCon_X,\XTy_X) \to X_\UU \\ \end{array} \] - - \begin{center} - \begin{tabular}{ll} - $X_\UU$:& Sorts \\ - $X_\El(o)$:& Objects of sort $o$\\ - \end{tabular} - \end{center} \end{frame} \begin{frame}{Constructing $G_3$} - + \begin{columns} + \begin{column}{.5\textwidth} + \begin{center} + \includesvg[scale=.4]{graphs/diagrammeGmini.svg} + \end{center} + \end{column} + \begin{column}{.5\textwidth} + \[ + Y = \left(Y_\Con,Y_\Ty,Y_\Tm\right) + \] + \end{column} +\end{columns} + \vspace{.5ex} \only<1>{ \[\begin{array}{ccl} X_\UU & = & \text{«sorts»}\\ @@ -335,8 +358,8 @@ \pause \[\begin{array}{ccccccc} X_\UU & = & - 1 & \oplus & - Y_\Con & \oplus& + \{\star\} & \uplus & + Y_\Con & \uplus& \displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta) \\ X_\El(\inj_1(\star)) & = & Y_\Con &&&&\\ @@ -348,37 +371,42 @@ \end{array}\] \pause \[\begin{array}{lcl} - \Cstr_\Con &=& \inj_1(\star)\\ - \Cstr_\Ty(\Gamma) &=& \inj_2(\Gamma) \\ - \Cstr_\Tm(\Delta,A) &=& \inj_3(\Delta,A) + \XCon_X &=& \inj_1(\star)\\ + \XTy_X(\Gamma) &=& \inj_2(\Gamma) \\ + \XTm_X(\Delta,A) &=& \inj_3(\Delta,A) \end{array}\] \pause - \begin{remark} - All sorts of $X_\UU$ are reached by some $\Cstr$ - \end{remark} + \vspace{-1.5ex} + \begin{tcolorbox} + All sorts of $X_\UU$ are in the image of some constructor $(\XCon_X,\XTy_X,\XTm_X)$ + \end{tcolorbox} \end{frame} \begin{frame}{Constructing $F_3$} - - \renewcommand\arraystretch{1.8} + \begin{center} + \includesvg[scale=.4]{graphs/diagrammeFmini.svg} + \end{center} + \vspace{-1ex} + \renewcommand\arraystretch{1.5} \[ \begin{array}{l|l} X : \mathbf{\BB_3} & Y = F_3(X): \mathbf{\CC_3}\\\hline X_\UU : \Set\quad X_\El : \Set^{X_\UU} &\\ - \Cstr_\Con : X_\UU & Y_\Con = - \uncover<2->{\ensuremath{X_\El(\Cstr^X_\Con)}}\\ - \Cstr_\Ty : H_2 F_{1} (X,\Cstr_\Con) \to X_\UU & + \XCon_X : X_\UU & Y_\Con = + \uncover<2->{\ensuremath{X_\El(\XCon_X)}}\\ + \XTy_X : H_2 F_{1} (X,\XCon_X) \to X_\UU & Y_\Ty(\Gamma) = - \uncover<3->{\ensuremath{X_\El(\Cstr^X_\Ty(\Gamma))}}\\ - \Cstr_\Tm : H_3 F_{2} (X,\Cstr_\Con,\Cstr_\Ty) \to X_\UU & + \uncover<3->{\ensuremath{X_\El(\XTy_X(\Gamma))}}\\ + \XTm_X : H_3 F_{2} (X,\XCon_X,\XTy_X) \to X_\UU & Y_\Tm(\Delta,A) = - \uncover<4->{\ensuremath{X_\El(\Cstr^X_\Tm(\Delta,A))}} \\ + \uncover<4->{\ensuremath{X_\El(\XTm_X(\Delta,A))}} \\ \end{array} \] \pause[5] - \begin{remark} - Each object of $Y$ are associated by $X_\El$ to some $\Cstr$ - \end{remark} + \vspace{-.5ex} + \begin{tcolorbox} + Each object of $Y$ are associated by $X_\El$ to some constructor + \end{tcolorbox} \end{frame} @@ -389,11 +417,11 @@ \pause \begin{remark} - All sorts of $G_3Y$ are reached by some $\Cstr$ of $G_3Y$ + All sorts of $G_3Y$ are reached by some constructor of $G_3Y$ \uncover<3>{\ding{220}$\Hom_{\BB_3}\left(G_3Y,X\right)$ transforms constructible into constructible} - Each object of $F_3X$ are associated by $X_\El$ to some $\Cstr$ of $X$ + Each object of $F_3X$ are associated by $X_\El$ to some constructor of $X$ \uncover<3>{\ding{220}$\Hom_{\CC_3}\left(Y,F_3X\right)$ transforms constructible into constructible} \end{remark} diff --git a/Report/graphs/diagrammeFG.svg b/Report/graphs/diagrammeFG.svg index d1af201..2f3fd68 100644 --- a/Report/graphs/diagrammeFG.svg +++ b/Report/graphs/diagrammeFG.svg @@ -24,15 +24,15 @@ inkscape:deskcolor="#d1d1d1" inkscape:document-units="mm" showgrid="false" - inkscape:zoom="1.6819304" - inkscape:cx="395.37902" - inkscape:cy="181.04197" - inkscape:window-width="1680" - inkscape:window-height="978" + inkscape:zoom="1.4810357" + inkscape:cx="413.22434" + inkscape:cy="132.00222" + inkscape:window-width="1920" + inkscape:window-height="1008" inkscape:window-x="0" - inkscape:window-y="15" + inkscape:window-y="0" inkscape:window-maximized="1" - inkscape:current-layer="layer1" /> + inkscape:current-layer="text625" /> + + + + id="g1316" + transform="translate(12.700002)"> + transform="translate(-3.1325529,1.1054134)"> + + style="font-weight:bold;font-size:8.46667px;font-family:'Josefin Sans';-inkscape-font-specification:'Josefin Sans Bold';text-align:center;text-anchor:middle;opacity:0.75462;stroke-width:1.296" + transform="translate(12.700002)"> @@ -357,19 +385,54 @@ + style="font-weight:bold;font-size:8.46667px;font-family:'Josefin Sans';-inkscape-font-specification:'Josefin Sans Bold';text-align:center;text-anchor:middle;opacity:0.75462;stroke-width:1.296" + transform="translate(12.700002)"> + + + + + + + + + + + + + diff --git a/Report/graphs/diagrammeFGmini.svg b/Report/graphs/diagrammeFGmini.svg new file mode 100644 index 0000000..6601f7a --- /dev/null +++ b/Report/graphs/diagrammeFGmini.svg @@ -0,0 +1,216 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Report/graphs/diagrammeFmini.svg b/Report/graphs/diagrammeFmini.svg new file mode 100644 index 0000000..06476e1 --- /dev/null +++ b/Report/graphs/diagrammeFmini.svg @@ -0,0 +1,190 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Report/graphs/diagrammeGmini.svg b/Report/graphs/diagrammeGmini.svg new file mode 100644 index 0000000..8d8003f --- /dev/null +++ b/Report/graphs/diagrammeGmini.svg @@ -0,0 +1,190 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Report/headerDiapo.tex b/Report/headerDiapo.tex index 435f4fa..9072d22 100644 --- a/Report/headerDiapo.tex +++ b/Report/headerDiapo.tex @@ -31,6 +31,7 @@ \usepackage[backend=biber,style=numeric]{biblatex} \usepackage{hyperref} \usepackage{array} +\usepackage{arydshln} \usepackage[lighttt]{lmodern} \usetikzlibrary{shapes.geometric,positioning,backgrounds} @@ -84,6 +85,9 @@ \newcommand\Con{{\ensuremath{\operatorname{Con}}}} \newcommand\Ty{{\ensuremath{\operatorname{Ty}}}} \newcommand\Tm{{\ensuremath{\operatorname{Tm}}}} +\newcommand\XCon{{\ensuremath{\operatorname{\mathbf{Con}}}}} +\newcommand\XTy{{\ensuremath{\operatorname{\mathbf{Ty}}}}} +\newcommand\XTm{{\ensuremath{\operatorname{\mathbf{Tm}}}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} \newcommand\Rtsc{{\ensuremath{\operatorname{\mathcal{R}tsc}}}} \newcommand\Cat{{\ensuremath{\operatorname{\mathcal{C}at}}}} @@ -186,4 +190,4 @@ \pdfpcnote{#1} \tableofcontents[currentsection,hideothersubsections,sections=\value{section}] \end{frame} -} \ No newline at end of file +}