Filled part 3 (2/3)

Report/M2Report.tex

@@ -89,7 +89,7 @@
 		$\dots$
 	\end{tabular}
 	
-	This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}, although they didn't prove it.
+	This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. Filippo Sestini noticed that in his thesis \cite{SestiniPhD}:
 	
 	\begin{quote}
 		Many instances of multi-sorted IITs [IITs are a variant of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and	consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
@@ -234,14 +234,14 @@
 		
 		\paragraph{$K$ functor}
 		
-		We define a helper functor $K : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
+		We define a helper functor $K_A : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
 		\[
-		K_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
+		K_A(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
 		\]
 		The morphisms are translated as-is.
 		
 		\begin{remark}
-			This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$
+			This functor can be constructed using the formal construction of the Grothendieck construction of $\TSet \cong (X: \Set) \times (\Set/X)$ as a pullback in the category of categories $\Cat$
 		\end{remark}
 	
 	\subsection{Initialization}
@@ -283,6 +283,8 @@
 		\]
 		and where $H_i$ is the specific functor described above.
 		
+		This way of constructing the category has formerly been described by Altenkirsch and al. \cite{Altenkirch2018}, with the only difference of the equivalence $\Set/H_i(X) \simeq \Set^{H_i(X)}$.
+		
 		\paragraph{An example of $H_i$ functors}
 		Let us now give an example of those $H_i$ objects for our type theory example.
 		
@@ -305,7 +307,6 @@
 		Then, we take the functor $H_2(X) = X_\Con$, corresponding to the sort declaration above. This functor means that types need \emph{one} context to be built.
 		
 		Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model $X$ is a family of sets $\left(X_\Ty(\Gamma)\right)_{\Gamma \in X_\Con}$, as expected.
-		
 		\[
 			\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}
 		\]
@@ -516,7 +517,7 @@
 		
 		The proof is that statement is given in \autoref{apx:FG-refl}.
 			
-	\subsection{Inductive step: $\tl^i$}
+	\subsection{Inductive step: Constructing $\tl^i$}
 	
 		\label{sec:coproductConstr}
 		
@@ -602,58 +603,170 @@
 
 		And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism.
 	
-	\section{Misc}
+	\section{Other Properties}
 	
+	\subsection{Fibration of the category $\CC_i$}
 	
+	In the formal proof, we defined $\CC_i$ as an inductive Grothendieck construction as in Altenkirsch and al. papers \cite{Altenkirch2018}.
 	
-	\subsection{Fiore's Category - Fibration of the category of sorts}
+	But there is an other way \cite{Fiore2008} of building the category $\CC_i$ which is equivalent to the one presented above.
 	
-	Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories (i.e. countable categories where all the arrows follow an unique direction and hom-sets are finite). The models of a GAT then are the presheaves over that category $S$: $\left[S,\Set\right]$.
+	With this other method, a sort specification is described by a countable simple direct category $S$ (i.e. a countable category where all the arrows follow an unique direction, and $\Hom$-sets are finite). The models of the sort specification are therefore the presheaves over the category $S$ called $\left[S,\Set\right]$.
 	
-	One can understand the correspondance between those categories and sort specifications as follows:
+	\paragraph{Constructing $S$ as a sequence}
-	\begin{itemize}
+	In order to fall back on the definition we gave in the formal proof, we will build the final countable simple direct category $S$ as a sequence $\emptyset = S_0,S_1,\dots,S_i$ where $S_i$ is the category describing the sort specification limited to the $i$ first sort declarations.
-		\item An object of the category is a sort of the specification.
-		\item An arrow $x$ from an object $s$ to an object $s'$ is a parameter of the sort declaration of $s$ of the for $(x : s' \dots)$.
-		\item The parameter $y$ of a parameter $x$ of a sort specification (i.e. the sort declaration parameter has the form $(x: s' \dots \left[y=z\right] \dots)$) is given by $z = x \circ y$.
-	\end{itemize}
 	
-	\begin{remark}
+	The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$.
-		We ignore in this definition identity arrows, and we will do so in the rest of this document. Identities are the only arrows that are not «directed» in the direct category.
-		
-		Interpreting the identity arrow would mean having a parameter of type $s$ to construct the sort $s$. which loops in a self-dependency.
-		
-		You can assume in the rest of the document that the formalizations \enquote{all arrows} or \enquote{the arrows} pointing to/from exclude identity arrows.
-	\end{remark}
 	
-	\todo{Éventuellement changer tous les paramètres par la forme complète, exemple 
+	We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
-		\[
-		\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty \left[\Gamma=\Gamma\right]) \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Tm \left[\Gamma=\Gamma\right] \left[A=A\right] \to \Ty \left[\Gamma=\Gamma\right]
-		\]
-		C'est bien plus verbeux et en pratique pas utilisé, mais permet de mieux voir la «composition» dans la catégorie de Fiore.}
-	\todo{Est-ce qu'on fait une notation \enquote{arrow*} pour dire «flèche qui n'est pas l'identité» pour plus de rigueur ?}
 	
-	For example the category version of the specification of sorts of Type Theory given above is defined as:
+	Avec le formalisme de la construction de Grothendieck, on peut formaliser la construction de la nouvelle catégorie comme cela:
+	\[
+		S_i = S_{i-1} \times 
+	\]
 	
-	\begin{itemize}
+	The final category is simply $S = \bigcup S_i$.
-		\item There is three objects called $\Con$,$\Ty$, and $\Tm$.
-		\item The arrows are defined as
-		\begin{itemize}
-			\item There is no arrow going out of $\Con$
-			\item There is one arrow going out of $\Ty$: $\Gamma$ pointing to $\Con$.
-			\item There is two arrows going out of $\Tm$: $\Delta$ pointing to $\Con$ and $\Gamma$ pointing to $\Ty$.
-		\end{itemize} 
-		\item The $\Gamma$ parameter of $\Ty$ in the parameter $A$ of $\Tm$ is $\Delta$. Therefore, we have $\Delta = A \circ \Gamma$.
-	\end{itemize}
 	
-	The category is pictured below:
+	In our type theory example, the category $S$ is constructed as follows:
 	
 	\begin{center}
-		% YADE DIAGRAM B1.json
+	\begin{tabular}{c|c|c}
-		% GENERATED LATEX
+		$\boxed{\Con : \Set}$ &
-		\input{graphs/B1.tex}
+		$\boxed{\Ty : (\Gamma : \Con) \to \Set}$ &
-		% END OF GENERATED LATEX
+		$\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ \\
+		$S_1 = \qquad \Con$	&
+		$S_2 = \qquad \Con \leftarrow \Ty$ &
+		$S_3 = \qquad \Con \leftarrow \Ty \leftarrow \Tm$ \\
+		$\left[S_1,\Set\right] \simeq \CC_1$ &
+		$\left[S_2,\Set\right] \simeq \CC_2$ &
+		$\left[S_3,\Set\right] \simeq \CC_3$
+	\end{tabular}
 	\end{center}
 	
+	\begin{remark}
+		This definition is reversable (up to the order of the sorts), and therefore, one can define a sequence of $\Gamma_i$ functors from any countable simple direct category.
+	\end{remark}
+	
+	\paragraph{Falling back on the formal proof}
+	
+		In the formal proof, we used categories $\CC_i$ and functors $H_i : \CC_i \to \Set$. We now undertand that the categories $\CC_i$ are defined on top of the categories $S_i$ with $\CC_i := \left[S_i,\Set\right]$.
+		
+		In the same way, the functors $H_i : \CC_{i-1} \to \Set$ are defined on top of the functors $\Gamma_i$ with the following relation:
+		\[
+			H_i(X) := \Hom_{\left[S_{i-1},\Set\right]}\left(\Gamma_i,X\right)
+		\]
+	
+	\subsection{Creating semantics object from the syntax}
+		\label{sec:HiFromSyntax}
+		
+		In this part, we will see how the functors $\Gamma_i$ given above can be constructed from the syntax of a sort specification. The previous subsection gives us a way of constructing the $H_i$ functors from the $\Gamma_i$ functors, and thus one can make the complete proof with the definition below.
+		
+		\paragraph{Verbose sort specification}
+		We will take a verbose version of a sort specification, where when \enquote{implementing} a sort, we gave the name of the parameter and the name of the term. For example, our type theory example becomes the following verbose version:
+		
+		\begin{center}
+		\renewcommand\arraystretch{1.5}
+		\begin{tabular}{l}
+			$\Con : \Set$\\
+			$\Ty : (\Gamma : \Con) \to \Set$ \\
+			$\Tm : (\Delta : \Con) \to (A : \Ty \left[\Gamma \mapsto \Delta\right]) \to \Set$
+		\end{tabular}
+		\end{center}
+		\vspace{1em}
+		The only sort declaration that changes is that of $\Tm$ as it is the only one for which one of its parameter is a sort with parameters.
+		
+		With that verbose definition, a generic sort specification is a list of sort declarations indexed by $\mathbb{T}$, the fully ordered set of all sorts. The sort declarations are as follow, for a sort $T \in \mathbb{T}$
+		
+		\[
+			T : \left[x_a^T : U_T(a) \left[x^{U_T(a)}_{b} \mapsto x^T_{v_T(a,b)}\right]_{b\leq I_{U_T(a)}}\right]_{a \leq I_T} \to \Set
+		\]
+		
+		Where
+		\begin{itemize}
+			\setlength\itemsep{-.2em}
+			\item $I_T$ is the number of parameters of the sort $T$
+			\item $x^T_a$ is the $a$-th parameter of the sort $T$
+			\item $U_T(a)$ is the sort of the $a$-th parameter of the sort $T$ (we have $U_T(a) < T$)
+			\item $I_{U_T(a)}$ is the number of parameters of the sort $U_T(a)$ i.e. the number of arguments we have to give to make an object of sort $U_T(a)$
+			\item $x^{U_T(a)}_b$ is the $b$-th parameter of the sort $U_T(a)$
+			\item $v_T(a,b)$ is the index of the parameter of the sort $T$ given as the $b$-th parameter of the $a$-th parameter of the sort $T$ (we have $v_T(a,b) < a$)
+			\item The types of parameters have to be respected, therefore we must have the equality
+			\[
+				U_T(v_T(a,b)) = U_{U_T(a)}(b)
+			\]
+		\end{itemize}
+		
+		For example, for the above sort declaration, we would have
+		\begin{itemize}
+			\setlength\itemsep{-.2em}
+			\item $\mathbb{T} = \left\{\Con < \Ty < \Tm\right\}$
+			\item $I_\Con = 0$, $I_\Ty = 1$, $I_\Tm = 2$
+			\item $x^\Ty_1 = "\Gamma"$, $x^\Tm_1 = "\Delta"$, $x^\Tm_2 = "A"$
+			\item $U_\Ty(1) = \Con$, $U_\Tm(1) = \Con$, $U_\Tm(2) = \Ty$
+			\item $v_\Tm(2,1) = 1$ such that $x^\Tm_{v_\Tm(2,1)} = "\Delta"$ (associated to $x^\Ty_{b=1} = "\Gamma"$)
+		\end{itemize}
+		
+		\paragraph{Describing the category $S$}
+			
+			We will then describe what is the category $S$ corresponding to a given sort specification $(\mathbb{T},I,U,v)$
+			
+			Its objects are simply the sorts, i.e. the elements of $\mathbb{T}$.
+			
+			Morphisms from a sort $T_x$ to a different sort $T_y$ are described by $U$ and correspond to the parameters of the sort $T_x$ that are of sort $T_y$. In other words:
+			
+			\[
+				\Hom_{S}(T_x,T_y) = \left\{x^{T_x}_a\middle| a \leq I_{T_x} \text{ and } U_{T_x}(a) = T_y\right\}
+			\]
+			
+			We can see that the category is direct, because of the rule $U_T(a) < T$ i.e. if $T_x < T_y$ then $\Hom_S(T_x,T_y) = \emptyset$.
+			For every sort $T$, we define $\Hom_S(T,T)$ to contain only the identity morphism $\id_T$, for which composition rules are already defined.
+			
+			Composition is described by $v$, corresponding to\enquote{parameters of parameters}.
+			Let's take two morphisms $x^{T_x}_b : T_x \to T_y$ and $x^{T_y}_a : T_y \to T_z$. Their composition is defined by
+			\[
+				x^{T_y}_a \circ x^{T_x}_b = x^{T_x}_{v_{T_x}(a,b)}
+			\]
+			
+			This composition is well-defined as 
+			\[
+				U_{T_x}(v_{T_x}(a,b)) = U_{U_{T_x}(a)}(b) = U_{T_y}(b) = T_z
+			\]
+			
+			For our type theory example, the category $S$ is as follows
+			
+			\begin{center}
+				% YADE DIAGRAM TyThExampleSCat.json
+				% GENERATED LATEX
+				\input{graphs/TyThExampleSCat.tex}
+				% END OF GENERATED LATEX
+			\end{center}
+		
+		\paragraph{Creating the functor $\Gamma_i$}
+		
+			We know we can create the functors $\Gamma_i$ directly from a complete category $S$, but we will look more in detail what those functors mean related to the syntax.
+			
+			If we are given the category $S_{i-1}$ with objects corresponding to the $i-1$ sorts already defined.
+			
+			We want to build a finite functor $\Gamma_i : S_{i-1} \to \Set$ corresponding to the following sort declaration of a new sort $T_i$
+		
+			We will build $\Gamma_i$ as follows:
+			
+			\[
+				\Gamma_i(T_x) = \left\{x^{T_i}_a\middle| a \leq I_{T_i} \text{ and } U_{T_i}(a) = T_x\right\}
+			\]
+			
+			\[
+				\Gamma_i(x_b^{T_x} : T_x \to T_y)(x^{T_i}_a \in \Gamma_i(T_x)) = x^{T_i}_{v_{T_i}(a,b)}
+			\]
+			
+			This definition is redundant with that of the last paragraph, but it has the advantage of directly creating the functor $\Gamma_i$ that are used to create the functors $H_i$ and all the rest of the proof.
+	
+	\subsection{Non-recursive definitions}
+	
+	\subsubsection{Redefinition of $\BB_i$}
+	\subsubsection{Redefinition of $G_i$ and $F_i$}
+	\subsubsection{Non-direct base category}
+	
 	\subsection{Infinite construction of $\BB_i$}
 	\[
 	\BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right)
@@ -695,46 +808,6 @@
 	
 	\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
 	
-	
-	\subsection{Adding 2-transformation of constructors}
-	\label{sec:constructors2trans}
-	\todo{Describe the process}
-	
-	\subsection{Overview}
-	
-	\subsubsection{$\CC$ as presheaf category}
-	\label{sec:CtoSSetFiore}
-	We use the specification of sorts definition of Fiore \cite{Fiore2008}.
-	
-	A specification of sorts is given by a sequence of functors $\Gamma_i : S_{i-1} \to \Set$. We construct the category $S_{i+1}$ by adding a single object $\alpha_{i+1}$ to the category $S_{i}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
-	
-	We have define a sequence of direct categories $\emptyset = S_0 \subset S_1 \subset S_2 \subset \dots$ (with inclusions functors $I_i : S_{i+1} \to S_i$). We define the \enquote{final} direct category as $S = \bigcup S_i$
-	
-	This definition is an isomorphism, so we can define a GAT categorically as any locally finite direct category.
-	
-	Then the semantics of the GAT is described as the category of presheaves over $S$, written $[S, \Set]$.
-	
-	Altenkirsch has another way of constructing the semantics of a specification of sorts \cite{Altenkirch2018}, and he also describes a way to describe constructors.
-	
-	So we can construct the base category, which is that of families of sets.
-	
-	
-	In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : S_{i-1} \to \Set$ describing entirely the sort declaration.
-	
-	This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$.
-	
-	Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities 
-	$s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$.
-	
-	\begin{remark}
-		We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.\inlinetodo{C'est sûr la deuxième partie ?}
-		
-		This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category.
-	\end{remark}
-	
-	\subsection{Consructing the $H_i$ functors from the syntax}
-	\label{sec:HiFromSyntax}
-	
 	\section{Summary}
 		
 		\lipsum[2-3]
@@ -1017,5 +1090,6 @@
 
 
 
+
 
 

Report/graphs/TyThExampleSCat.json

@@ -0,0 +1 @@
+{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":2,"id":3,"label":{"kind":"normal","label":"\"A\"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"\"\\Gamma\"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"\"\\Delta\" \\;=\\; \\Gamma \\circ A","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}