Correcting example part
This commit is contained in:
parent
19f72c6f51
commit
639dbfbc50
GPG Key ID:
0220AC4A3D6A328B
@ -112,54 +112,27 @@
|
||||
|
||||
\section{Example}
|
||||
|
||||
Before making the formal proof, we will construct and explain the objects on two examples.
|
||||
\subsection{Structure of the proof}
|
||||
Before making the formal proof, we will study our construction on three examples.
|
||||
|
||||
We will formalize the transformation for \emph{sort specifications} (i.e. lists of sort declarations).
|
||||
|
||||
This proof will be an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}).
|
||||
\paragraph{Structure of the proof}
|
||||
The formal proof will be an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}).
|
||||
|
||||
At the $i$-th recursion step, we will build the following objects :
|
||||
\begin{itemize}
|
||||
\setlength\itemsep{-1ex}
|
||||
\item The category of models of the GAT $\CC_i$
|
||||
\item The category of models of the transformed GAT $\BB_i$
|
||||
\item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$.
|
||||
|
||||
Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$:
|
||||
\[
|
||||
R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
|
||||
\]
|
||||
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute:
|
||||
\label{sec:tlUniversalProperty}
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversal.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversal.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
where $\en_0^i$ is the following composition:
|
||||
|
||||
\[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\]
|
||||
|
||||
And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds.
|
||||
|
||||
The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$.
|
||||
|
||||
\item A functor $F_i : \BB_i \to \CC_i$
|
||||
\item A functor $G_i : \CC_i \to \BB_i$
|
||||
\item An adjunction between them $F_i \vdash G_i$
|
||||
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
||||
\item A proof that $F_i\inj_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$
|
||||
\end{itemize}
|
||||
|
||||
We will now present those objects on three specific examples in order to help getting an understanding of the logic behind the formal proof.
|
||||
|
||||
\subsection{The empty sort specification}
|
||||
|
||||
Our proof will we an induction on the number of sorts, and so the first step will be creating the objects for the empty sort specification.
|
||||
|
||||
Therefore we will build the following objects
|
||||
Our first example is the empty sort specification. As our proof will we an induction on the number of sorts, its first step will always be creating the objects for this empty sort specification.
|
||||
|
||||
\paragraph{Category of models of the empty sort specification}
|
||||
|
||||
@ -194,16 +167,14 @@
|
||||
With this formalisation, a model of this sort specification is a functor $X : \TT \to \Set$, such that
|
||||
\begin{itemize}
|
||||
\item $X_\UU$ is the set of the \enquote{sort objects}
|
||||
\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^{-1}(\{\Gamma\}) \subset X_\El$
|
||||
\item For each sort object $A \in X_\UU$, the set of objects corresponding to the sort object is $X_p^{-1}(\{A\}) \subset X_\El$
|
||||
\end{itemize}
|
||||
|
||||
We will denote this category of models of the empty sort specification as $\BB_0$.
|
||||
|
||||
We notice that the category $\BB_0$ has a coproduct that we will denote as $\tl^0$. The two injectors of this coproduct will be denoted as $\inj_1^0$ and $\inj_2^0$.
|
||||
|
||||
\paragraph{Functors}
|
||||
|
||||
We want to show that there is a reflection between those two categories $\BB_0$ and $\CC_0$ as follows:
|
||||
We want to show that there is a coreflection between those two categories $\BB_0$ and $\CC_0$ as follows:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM AdjunctionLevel0.json
|
||||
@ -214,14 +185,14 @@
|
||||
|
||||
$F_0 : \TSet \to \one$ is simply the terminal functor of $\Cat$, i.e. the functor sending all objects to $\star$, the only object of $\one$, and all morphisms to $\id_\star$.
|
||||
|
||||
$G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ (such that $G_0$ preserves colimits)
|
||||
$G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ (i.e. such that $G_0$ preserves colimits)
|
||||
|
||||
We can check that those two functors create an adjunction, as
|
||||
\[
|
||||
\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)
|
||||
\]
|
||||
|
||||
We also have that they create a coreflection, as $F_0G_0$ goes from $\one$ to $one$, and so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$. So $F_0G_0$ is an isofunctor.
|
||||
We also have that they create a coreflection, as $F_0G_0$ goes from $\one$ to $\one$, and so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$. So $F_0G_0$ is an isofunctor.
|
||||
|
||||
\subsection{Type theory example}
|
||||
|
||||
@ -259,7 +230,7 @@
|
||||
|
||||
\paragraph{Category of models}
|
||||
|
||||
We have seen in the introduction how was a model of the type theory sort specification. We will rebuild that inductively, adding one sort at a time.
|
||||
We have seen in the introduction a description of a model of the type theory sort specification. We will rebuild the category of those models inductively, adding one sort at a time.
|
||||
|
||||
In order to construct those categories in a generic way, we will define functors $H_X : \CC_{X-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration.
|
||||
|
||||
@ -363,7 +334,12 @@
|
||||
\]
|
||||
|
||||
The codomain of this constructor means \enquote{Every object of $X_\El$ that are associated to the $\Con$ object of $X_\UU$ i.e. the object $\Cstr^X_\Con$}
|
||||
This codomain is quite verbose, but we have another way of expressing it. In the final proof, we will have already constructed the functor $F_1 : \BB_1 \to \CC_1$, and we had a functor $H_\Ty : \CC_1 \to \Set$ that described the parameters of the sort declaration of $\Ty$ for the category $\CC_1$. Well, it turns out that $H_\Ty \circ F_1 : \BB_1 \to \Set$ describes exactly the codomain expressed above.
|
||||
This codomain is quite verbose, but we have another way of expressing it. In the final proof, we will have already constructed the functor $F_1 : \BB_1 \to \CC_1$, and we had a functor $H_\Ty : \CC_1 \to \Set$ that described the parameters of the sort declaration of $\Ty$ for the category $\CC_1$. It turns out that $H_\Ty \circ F_1 : \BB_1 \to \Set$ describes exactly the codomain expressed above.
|
||||
\[
|
||||
(H_\Ty \circ F_1) (X,\Cstr^X_\Con) = X_p^{-1}\left(\Cstr^X_\Con\right)
|
||||
\]
|
||||
|
||||
The fact that $H_X \circ F_{X-1}$ describes exactly the codomain of the constructor we want to add will hold for every sort declaration we can add.
|
||||
|
||||
Therefore, the category $\BB_2$ consists of a pair of
|
||||
\begin{itemize}
|
||||
@ -371,7 +347,7 @@
|
||||
\item A constructor $\Cstr^X_\Ty : H_iF_{i-1}(X,\Cstr^X_\Con) \to X_\UU$
|
||||
\end{itemize}
|
||||
|
||||
One again, morphism $f$ from $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ to $(X',\Cstr^{X'}_\Con,\Cstr^{X'}_\Ty)$ are simply morphisms of $\BB_1$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ that respect the $\Cstr_\Ty$ constructor, i.e. that verifies, for every $\Gamma$ in $H_iF_{i-1}(X,\Cstr^X_\Con)$ that
|
||||
One again, a morphism $f$ from $(X,\Cstr^X_\Con,\Cstr^X_\Ty)$ to $(X',\Cstr^{X'}_\Con,\Cstr^{X'}_\Ty)$ is simply a morphism of $\BB_1$ from $(X,\Cstr^X_\Con)$ to $(X',\Cstr^{X'}_\Con)$ that does respect the $\Cstr_\Ty$ constructor, i.e. that verifies, for every $\Gamma$ in $H_iF_{i-1}(X,\Cstr^X_\Con)$ that
|
||||
\[
|
||||
f_\UU(\Cstr^X_\Ty(\Gamma)) = \Cstr^{X'}_\Ty(f_\El(\Gamma))
|
||||
\]
|
||||
@ -396,7 +372,7 @@
|
||||
We want to make functors connecting those two categories
|
||||
\[
|
||||
\begin{array}{l|l}
|
||||
Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\
|
||||
Y : \mathbf{\CC_3} & X : \mathbf{\BB_3} \\\hline
|
||||
& X : \TSet\\
|
||||
Y_\Con : \Set & \Cstr^X_\Con : X_\UU \\
|
||||
\left(Y_\Ty(\Gamma)\right)_{\Gamma \in Y_\Con} &
|
||||
@ -409,11 +385,11 @@
|
||||
Let's first look at the first component of the «result» $X = G_3(Y)$. It will be a functor of $\TSet$. We recall how $\TSet$ corresponds to the sort specification $(\mathcal{O},\El)$:
|
||||
\begin{itemize}
|
||||
\item $X_\UU$ is the set of all sorts
|
||||
\item $X_\El$ is the set of all «objects» of those sorts
|
||||
\item $X_\El$ is the set of all objects of those sorts
|
||||
\item $X_p$ sends an object of a sort to the sort it corresponds to
|
||||
\end{itemize}
|
||||
|
||||
Therefore, we will construct $X_\UU$ to be the disjoint union of all the indices of the sets inside $Y$, $X_\El$ will be the disjoint union of all the sets inside $Y$, and $X_p$ will keep track of what is the indice of a set.
|
||||
Therefore, we will construct $X_\UU$ to be the disjoint union of all the indices of the sets inside $Y$, $X_\El$ will be the disjoint union of all the sets inside $Y$, and $X_p$ will keep track of what is the index of a set.
|
||||
|
||||
\[\begin{array}{ccccccc}
|
||||
|
||||
@ -425,7 +401,7 @@
|
||||
X_\UU & = &
|
||||
1 & \oplus &
|
||||
Y_\Con & \oplus&
|
||||
\displaystyle\coprod_{\Gamma \in Y_\Con}Y_\Ty(\Gamma)
|
||||
\displaystyle\coprod_{\Delta \in Y_\Con}Y_\Ty(\Delta)
|
||||
\end{array}\]
|
||||
where $\operatorname{proj}_1 : \coprod_{a\in A}B(a) \to A$ is the first projector of the coproduct, and $\operatorname{proj}_{2,1}$ get the index $ \coprod_{a \in A}B(a)$ of a double coproduct $\coprod_{a \in A}\coprod_{b\in B(a)} C(a,b)$
|
||||
\vspace{.2ex}
|
||||
@ -439,11 +415,15 @@
|
||||
|
||||
where $\inj_i$ is the $i$-th injector of the direct sum $\oplus$.
|
||||
|
||||
\begin{remark}
|
||||
With this functor, every element of $X_\UU$ is reached by some constructor. And therefore, every object of $X_\El$ points to a sort that is reached by some constructor.
|
||||
\end{remark}
|
||||
|
||||
\todo{Parler des morphismes ? Est-ce nécessaire ?}
|
||||
|
||||
\paragraph{Constructing $F_i$}
|
||||
|
||||
Now we will try to create an object $Y = F_i X$ of $\CC_3$ from an object $X$ of $\BB_3$.
|
||||
We will now create an object $Y = F_i X$ of $\CC_3$ from an object $X$ of $\BB_3$.
|
||||
|
||||
\begin{itemize}
|
||||
\item $Y_\Con$ should be the set of all objects of sort $\Con$. In the transformed GAT, it means all objects of $\El$ which have been created with the sort $\Cstr^X_\Con$. Therefore we have
|
||||
@ -485,21 +465,19 @@
|
||||
|
||||
Therefore, both morphism are only descriptions of actions on constructible sorts into constructible sorts. That's how we create the isomorphism.
|
||||
|
||||
Morphisms of $\BB_3$ from $G_3Y$ to $X$ are morphisms of $\TSet$ that respect constructors. It means that
|
||||
|
||||
\paragraph{A coreflection}
|
||||
|
||||
If we look at $F_3G_3 Y$ for a model $Y$ of $\CC_3$, we remark that
|
||||
\[\begin{array}{lcl}
|
||||
F_3G_3(Y)_\Con &=& G(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Con\})\\
|
||||
&=& G(Y)_p^{-1}(\{\inj_1 \star\}) \\
|
||||
F_3G_3(Y)_\Con &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Con\})\\
|
||||
&=& G_3(Y)_p^{-1}(\{\inj_1 \star\}) \\
|
||||
&=& Y_\Con
|
||||
\end{array}\]
|
||||
and
|
||||
\[\begin{array}{lcl}
|
||||
F_3G_3(Y)_\Ty(\Gamma) &=& G(Y)_p^{-1}(\{\Cstr^{G(Y)}_\Ty(\Gamma)\})\\
|
||||
&=& G(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
|
||||
&=& proj_1^{-1}(\Gamma) \\
|
||||
F_3G_3(Y)_\Ty(\Gamma) &=& G_3(Y)_p^{-1}(\{\Cstr^{G_3(Y)}_\Ty(\Gamma)\})\\
|
||||
&=& G_3(Y)_p^{-1}(\{\inj_2 \Gamma\}) \\
|
||||
&=& \operatorname{proj}_1^{-1}(\Gamma) \\
|
||||
&=& \left\{(\Gamma',A) \in \coprod_{\Gamma' \in Y_\Con}Y_\Ty(\Gamma') \middle| \Gamma' = \Gamma\right\}\\
|
||||
&\simeq& Y_\Ty(\Gamma)
|
||||
\end{array}\]
|
||||
@ -510,8 +488,48 @@
|
||||
|
||||
And therefore $F_3G_3 \equiv \Id_{\CC_3}$.
|
||||
|
||||
\subsection{Another sort specification}
|
||||
\todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»}
|
||||
|
||||
\section{Constructing the coreflection}
|
||||
|
||||
The proof will take form of an induction on the number of sorts taken into account. At each induction step, we will build the following objects:
|
||||
|
||||
\begin{itemize}
|
||||
\setlength\itemsep{-1ex}
|
||||
\item The category of models of the GAT $\CC_i$
|
||||
\item The category of models of the transformed GAT $\BB_i$
|
||||
\item A forgetful functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$.
|
||||
|
||||
Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$:
|
||||
\[
|
||||
R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
|
||||
\]
|
||||
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute:
|
||||
\label{sec:tlUniversalProperty}
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversal.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversal.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
where $\en_0^i$ is the following composition:
|
||||
|
||||
\[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\]
|
||||
|
||||
And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds.
|
||||
|
||||
The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$.
|
||||
|
||||
\item A functor $F_i : \BB_i \to \CC_i$
|
||||
\item A functor $G_i : \CC_i \to \BB_i$
|
||||
\item An adjunction between them $F_i \vdash G_i$
|
||||
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
||||
\item A proof that $F_i\inj_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$
|
||||
\end{itemize}
|
||||
|
||||
Here is a figure that describes the recursive construction of some of the above objects
|
||||
\begin{center}
|
||||
% YADE DIAGRAM GlobalRecursiveConstruction.json
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user