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
+}