diff --git a/Report/Bilibibio.bib b/Report/Bilibibio.bib index e9b3781..ff2f6de 100644 --- a/Report/Bilibibio.bib +++ b/Report/Bilibibio.bib @@ -1,21 +1,12 @@ @InProceedings{Fiore2008, - author={Fiore, Marcelo}, - booktitle={2008 23rd Annual IEEE Symposium on Logic in Computer Science}, - title={Second-Order and Dependently-Sorted Abstract Syntax}, - year={2008}, - volume={}, - number={}, - pages={57-68}, - keywords={Algebra;Computer science;Mathematical model;Logic functions;Laboratories;MONOS devices;Sorting;abstract syntax;second-order syntax;dependently-sorted syntax;alpha-equivalence;variable binding;substitution;metavariable;meta-substitution;categorical algebra}, - doi={10.1109/LICS.2008.38} } @@ -24,7 +15,7 @@ editor={"Baier, Christel and Dal Lago, Ugo"}, title={"Quotient Inductive-Inductive Types"}, booktitle={"Foundations of Software Science and Computation Structures"}, - year={"2018"}, + year = 2018, publisher={"Springer International Publishing"}, address={"Cham"}, pages={"293--310"}, @@ -40,7 +31,7 @@ series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, - year = {2023}, + year = 2023, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, @@ -55,10 +46,33 @@ journal = {Annals of Pure and Applied Logic}, volume = {32}, pages = {209-243}, - year = {1986}, + year = 1986, issn = {0168-0072}, doi = {https://doi.org/10.1016/0168-0072(86)90053-9}, url = {https://www.sciencedirect.com/science/article/pii/0168007286900539}, author = {John Cartmell} } +@phdthesis{SestiniPhD, + author = {Filippo Sestini}, + title = {Bootstrapping Extensionality}, + school = {University of Nottingham}, + year = 2023, + month = mar +} + +@misc{AmbrusSzumiXie2sort, + author = {Ambrus Kaposi}, + title = {Message to the Agda mailing list}, + howpublished = {\url{https://lists.chalmers.se/pipermail/agda/2019/011176.html}}, + year = 2019 +} + +@misc{nlab:reflective_subcategory, + author = {{nLab authors}}, + title = {reflective subcategory}, + howpublished = {\url{https://ncatlab.org/nlab/show/reflective+subcategory}}, + note = {\href{https://ncatlab.org/nlab/revision/reflective+subcategory/116}{Revision 116}}, + month = jul, + year = 2024 +} \ No newline at end of file diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 1610f42..f7c3c45 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -3,6 +3,10 @@ \input{./header.tex} +% po4a: environment remark +% po4a: environment tikzpicture +% po4a: environment property + \title{Categorical semantics of the reduction of GATs to two-sorted GATs. \\[1ex] \large Notes on my 4.5-month internship at the Laboratoire d'Informatique de l'École Polytechnique (Palaiseau, France)} \hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}} @@ -43,8 +47,8 @@ A model of this category is a triple \begin{itemize} \item A set $X_\Con : \Set$ - \item A function $X_\Ty : X_\Con \to \Set$ - \item A function $X_\Tm : \displaystyle\coprod_{\Gamma : X_\Con} X_\Ty(\Gamma) \to \Set$ + \item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$ + \item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$ \end{itemize} \paragraph{Constructor specification} @@ -72,13 +76,15 @@ \paragraph{Two-sortification} - There is a process that allows us to transform a GAT into a GAT with only two sorts. This process is applied for example by Philippo Sestini \inlinetodo{manque une citation}, who asserts that one can build back an initial model + There is a process that allows us to transform a GAT into a GAT with only two sorts. This process is used by Philippo Sestini in his thesis \cite{SestiniPhD} refering the work of Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}: + + \begin{quote} + Many instances of multi-sorted IITs [IITs are another type 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. + \end{quote} - this transformation preserves the existence of the initial model. + The goal of this document is to prove semantically that this transformation makes sense. More specifically, we prove that this transformation is a left adjunct functor of a coreflection. This is enough to prove what Sestini conjectured, i.e. that the initial object in the 2-sort category creates back the initial object of the primary category \cite[5. General]{nlab:reflective_subcategory}. - The goal of this document is to prove semantically that this transformation creates an adjunction, and more precisely a reflective adjunction between the categories of models (and therefore preserving the existence of an initial model). - - We will now present this transformation. The sort specification of the GAT is always the same, and contains two sort declarations (as planned): + We will now present this transformation. The sort specification of the transformed GAT is always the same, and contains two sort declarations (as planned): \vspace{1em} \begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}} @@ -87,7 +93,7 @@ \end{tabular} \vspace{1em} - Category of models of this two-sort specification are intuitively the category of families of set $\FamSet$, composed of pairs $\left(X_0:\Set,X_1: X_0 \to \Set\right)$ (or $\coprod_{X : \Set}\Set$ in type theory). + Category of models of this two-sort specification are intuitively the category of families of set $\FamSet$, composed of pairs $\left(X_0:\Set,X_1: X_0 \to \Set\right)$. Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every parameter. For example, the Type Theory GAT presented above becomes that which follows: @@ -98,64 +104,16 @@ $\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ & For each object $\Gamma$ corresponding to the sort object $\Con$, and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called \enquote{$\Tm\;\Gamma\;A$}\\ - $\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & + $\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ & For each object $\Gamma$ corresponding to the sort object $\Con$, an object called \enquote{$\operatorname{unit} \Gamma$} corresponding to the sort object $\Ty\;\Gamma$\\ - $\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty\;\Gamma) \to$ \newline - $\qquad\Tm\;\Gamma A \to \Tm\;\Gamma A \to \Ty\;\Gamma$ & + $\operatorname{eq}: (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Gamma}) \to$ \newline + $\qquad\underline{\Tm\;\Gamma A} \to \underline{\Tm\;\Gamma A} \to \underline{\Ty\;\Gamma}$ & $\dots$ \end{tabular} - \paragraph{Fiore's categories} - 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]$. - - One can understand the correspondance between those categories and sort specifications as follows: - \begin{itemize} - \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} - 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 - \[ - \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: - - \begin{itemize} - \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: - - \begin{center} - % YADE DIAGRAM B1.json - % GENERATED LATEX - \input{graphs/B1.tex} - % END OF GENERATED LATEX - \end{center} - - \paragraph{Fiore's category of the 2-sorts specification} - - If compute the small category associated to the two-sort specification described above, we obtain the simple category with two objects and one arrow between them. We call this category $\TT$ and write the objects as follows: + \paragraph{$\FamSet$ as functors} + In the rest of the document, we will denote the simple category containing two elements and one non-identity arrow between them as $\TT$. The objects and arrow of this category are pictured below. \begin{center} % YADE DIAGRAM G0.json @@ -164,11 +122,21 @@ % END OF GENERATED LATEX \end{center} - The category of presheaves over this category is equivalent to the category $\FamSet$. + The functors over this categories are equivalent to families of sets, using the following mapping : + + \[ + \begin{array}{l|l} + X_\UU = X_0 & X_0 = X_\UU \\ + X_\El = \displaystyle\coprod_{A\in X_0}X_1(A) & X_1 = A \mapsto X_p^{-1}(\{A\})\\ + X_p = (A,B) \mapsto A & + \end{array} + \] + + Therefore the categories of sorts of the transformed GATs will be built atop of the category $\TSet$ rather than atop of the category $\FamSet$ as it makes the formal proofs more elegant. \paragraph{Goal} - The goal of this document is to make a relation between the category of models of the GAT $\left[S,\Set\right]$ and the category of models of the two-sortified GAT $\BB$. This relation will be an adjunction $F \vdash G$ that we will prove to be a coreflection. + The goal of this document is to make a relation between the category of models of the GAT $\CC$ and the category of models of the two-sortified GAT $\BB$. This relation will be an adjunction $F \vdash G$ that we will prove to be a coreflection. The category $\BB$ is built with an adjunction $R \vdash L$ to the category of models of the simple two-sort specification of sorts $\TSet$. @@ -181,100 +149,93 @@ \subsection{Constructing the categories} - We will construct both categories $S$ and $\BB$ recursively, adding new sorts one by one. - The categories $S_i$ are described as in Fiore's paper \cite{Fiore2008}, and the categories $\BB_i$ are constructed atop of the category $\TSet$ with a method inspired by the category of models described by Altenkirch et al. \cite{Altenkirch2018}. - - The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\TSet = \BB_0$ and $\left[S_0,\Set\right] = \left[\emptyset,\Set\right] = 1$. - - Then we construct the category $S_i$ as a full supercategory of $S_{i-1}$ (and so we have a ff injection functor $I_i : S_{i-1} \to S_i$). - - We construct at the same time the category $\BB_i$ along with an adjunction $R_{i-1}^i \vdash L_{i-1}^i$ with $\BB_{i-1}$. - - The construction is summarized in the following diagram: - - \begin{center} - % YADE DIAGRAM G1.json - % GENERATED LATEX - \input{graphs/G1.tex} - % END OF GENERATED LATEX - \end{center} - - - \subsubsection{Fiore's category} - - 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 ?} + We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one. + The categories $\CC_i$ are described as in Fiore's paper \cite{Fiore2008}, and the categories $\BB_i$ are constructed atop of the category $\TSet$ with a method inspired by the category of models described by Altenkirch et al. \cite{Altenkirch2018}. - This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category. - \end{remark} - - \subsubsection{2sort category} - - To start our series of categories, we use the category of models of the two-sort specification of sorts $\BB_0 := \TSet$. - - Then, we recursively add constructors, constructing categories $\BB_1$,$\BB_2$, etc. - - For the $i$-th constructor, we define the objects of $\BB_i$ as pairs of - - \begin{itemize} - \item an object $X$ of $\BB_{i-1}$ - \item a \enquote{sort constructor} $\Cstr_i$ as a function $\Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU$ - \newline - where $\Gamma_i$ is the functor $S_{i-1} \to \Set$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\left[S_{i-1}, \Set\right] \to \BB_{i-1}$ that we are defining recursively at the same time. - \end{itemize} - - - Morphisms $(X,\Cstr_i) \to (X',\Cstr'_i)$ in $\BB_i$ are morphisms $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. - - \begin{center} - % YADE DIAGRAM D1.json - % GENERATED LATEX - \input{graphs/D1.tex} - % END OF GENERATED LATEX - \end{center} - - Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. -seeing - We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjunct} of another functor we call $L_{i-1}^i$. - - As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions. - \[ - R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j} - \] - \[ - L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1} - \] - - We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$. - - - - We know that this category has a coproduct, that we will denote $\oplus_i$ or just $\oplus$ when there is no ambiguity. We will also denote as $\inj_1^i : X \to X \oplus Y$ (resp. $\inj_2^i : Y \to X \oplus Y$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphisms $f : X \to Z$ and $g : Y \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$. - - \begin{remark} - This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}\Gamma_i \to G_{i-1}\Gamma_i \oplus L_0^{i-1} y\UU$. - \end{remark} - - \subsubsection{Summary} - - Here is a graph summarizing the categories and functors. - We have constructed two chains of categories $\BB_0$,$\BB_1$,... and $S_0$,$S_1$,... - - The categories $\BB_{i-1}$ and $\BB_{i}$ are in an adjunction written $R_{i-1}^i \vdash L_{i-1}^i$. - - We will give in the next part the construction of the adjunction $F_i \vdash G_i$ at the step $i$. The functor $G_{i-1}$ is used in the definition of $\BB_i$, so the two recurrences have to be done at the same time. - - + The overall construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below. + + \begin{center} + % YADE DIAGRAM G1.json + % GENERATED LATEX + \input{graphs/G1.tex} + % END OF GENERATED LATEX + \end{center} + + The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$. + + \subsubsection{Constructing $\CC_i$} + + We construct the category $\CC_i$ as the following pair: + \[ + \CC_i = (X : \CC_{i-1}) \times \Set^{\Hom(O_i,X)} \qquad\text{(this is a dependent coproduct)} + \] + where $O_i$ is a specific object of the category $\CC_{i-1}$, such that $\Hom(O_i,X)$ is the set of parameters for the construction of the new sort. + + For example, for our type theory example, we first have + \[ + O_1 = \star \in \operatorname{Obj}(\CC_0) = \operatorname{Obj}(1) + \] + so $\Hom(O_1,X) = 1$, which corresponds to the fact that $\Con$ takes no parameter. + + Therefore $\CC_1 = 1 \times \Set^1 = \Set$ + + Then, we take the singleton object $O_2 = 1$ (this means, that types need \emph{one} context to be built), and so, for a set $X_\Con$, $\Hom(O_2,X_\Con) \cong X_\Con$, which corresponds to the fact that $\Ty$ take one $\Con$ as a parameter. + + Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$. + + Finally, we take the object $O_3 = (1, \lambda \star . 1)$ (this means that terms need \emph{one} context, and \emph{one} type of that context). With this object, for a pair $(X_\Con,X_\Ty)$ in $\CC_2$, we have $\Hom(O_3,(X_\Con,X_\Ty)) \cong \left(\Gamma: X_\Con, A: X_\Ty(\Gamma)\right)$. + + The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$ + + \begin{remark} + There is a way of getting the object $O_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}. + \end{remark} + + \subsubsection{Constructing $\BB_i$} + + \paragraph{The category} We construct the category $\BB_i$ as follows. + + An object of $\BB_i$ is + \begin{itemize} + \item an object $X$ of $\BB_{i-1}$ + \item a \enquote{sort constructor} $\Cstr_i$ as a function $\Hom_{\BB_{i-1}} (G_{i-1}O_i,X) \to (R_0^{i-1}X)_\UU$ + \newline + where $O_i$ is the object of $\CC_{i-1}$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\CC_{i-1} \to \BB_{i-1}$ that we are defining recursively at the same time. + \end{itemize} + + + A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ of $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. + + \begin{center} + % YADE DIAGRAM D1.json + % GENERATED LATEX + \input{graphs/D1.tex} + % END OF GENERATED LATEX + \end{center} + + Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. + + \paragraph{The adjunction} + We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjunct} of another functor we call $L_{i-1}^i$. + + As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions. + \[\begin{array}{c} + R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j}\\ + L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1} + \end{array}\] + + We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$. + + \paragraph{The coproduct} + For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$. + \begin{remark} + This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$. + \end{remark} \subsection{Constructing the adjunction} + We will now construct the adjunction $F_i \vdash G_i$ at the step $i$. \subsubsection{Hypotheses} @@ -508,7 +469,58 @@ seeing \subsection{Proof of H3} - \subsection{Infinite construction of $\BB_i$} + + \section{Misc} + + \subsection{Fiore's Category - Fibration of the category of sorts} + + 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]$. + + One can understand the correspondance between those categories and sort specifications as follows: + \begin{itemize} + \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} + 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 + \[ + \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: + + \begin{itemize} + \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: + + \begin{center} + % YADE DIAGRAM B1.json + % GENERATED LATEX + \input{graphs/B1.tex} + % END OF GENERATED LATEX + \end{center} + + \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) \] @@ -569,6 +581,8 @@ seeing \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$. @@ -583,6 +597,20 @@ seeing 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} + \section{Summary} \lipsum[2-3] @@ -704,3 +732,7 @@ seeing \end{document} + + + + diff --git a/Report/graphs/D1.json b/Report/graphs/D1.json index 5b4efb6..98e5a3c 100644 --- a/Report/graphs/D1.json +++ b/Report/graphs/D1.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"isPullshout":false,"label":"R_0^i X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"isPullshout":false,"label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i(X))","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i( X'))","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":11} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\Cstr^X","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":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/G1-0.json b/Report/graphs/G1-0.json index 9f360bb..bb1e164 100644 --- a/Report/graphs/G1-0.json +++ b/Report/graphs/G1-0.json @@ -1 +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\\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":0,"id":5,"label":{"isPullshout":false,"label":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"isPullshout":false,"label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":7,"label":{"isPullshout":false,"label":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":8,"label":{"isPullshout":false,"label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left[S,\\Set\\right]","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\TSet","pos":[300,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\vdash","pos":[301,203.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\bot","pos":[395,100.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file +{"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\\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":0,"id":3,"label":{"kind":"normal","label":"F","style":{"alignment":"right","bend":0.20000000000000004,"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":"G","style":{"alignment":"right","bend":0.20000000000000004,"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":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":6,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":8,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\TSet","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index 40f41bc..cfd7c3d 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -102,6 +102,7 @@ \newcommand\BB{{\ensuremath{\mathcal{B}}}} \newcommand\TT{{\ensuremath{\mathcal{T}}}} \newcommand\UU{{\ensuremath{\mathcal{U}}}} +\newcommand\CC{{\ensuremath{\mathcal{C}}}} \newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} \newcommand\ii{{\ensuremath{\mathbf{i}}}} \newcommand\Con{{\ensuremath{\operatorname{Con}}}} diff --git a/Report/yade-preamble.tex b/Report/yade-preamble.tex index 306efba..8c6f169 100644 --- a/Report/yade-preamble.tex +++ b/Report/yade-preamble.tex @@ -2,6 +2,7 @@ \newcommand\BB{{\ensuremath{\mathcal{B}}}} \newcommand\TT{{\ensuremath{\mathcal{T}}}} \newcommand\UU{{\ensuremath{\mathcal{U}}}} +\newcommand\CC{{\ensuremath{\mathcal{C}}}} \newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} \newcommand\ii{{\ensuremath{\mathbf{i}}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} diff --git a/Report/yade.sty b/Report/yade.sty index c887f07..854e110 100644 --- a/Report/yade.sty +++ b/Report/yade.sty @@ -27,53 +27,53 @@ \usetikzlibrary{backgrounds} \usetikzlibrary{quotes} \pgfkeys{/pgf/.cd, - arity/.initial=4, + arity/.initial=4, } \def\twocell{% - \@ifnextchar[{\twocell@i}{\twocell@i[.4]}% + \@ifnextchar[{\twocell@i}{\twocell@i[.4]}% } \def\twocell@i[#1]{% - \@ifnextchar[{\twocell@ii[#1]}{\twocell@ii[#1][#1]}% + \@ifnextchar[{\twocell@ii[#1]}{\twocell@ii[#1][#1]}% } \def\twocell@ii[#1][#2]{% - \deuxcellule{#1}{#2}% + \deuxcellule{#1}{#2}% } % A TikZ style for curved arrows, inspired by AndréC's. \tikzset{curve/.style={settings={#1},to path={ - let \p1 = ($(\tikztostart) - (\tikztotarget)$) in - (\tikztostart) -.. controls -($(\tikztostart)!\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*1pt}!270:(\tikztotarget)$) -and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*1pt}!270:(\tikztotarget)$) -.. (\tikztotarget)\tikztonodes}}, -settings/.code={\tikzset{yade/.cd,#1} -\def\pv##1{\pgfkeysvalueof{/tikz/yade/##1}}}, -yade/.cd,pos/.initial=0.35,ratio/.initial=0} + let \p1 = ($(\tikztostart) - (\tikztotarget)$) in + (\tikztostart) + .. controls + ($(\tikztostart)!\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!270:(\tikztotarget)$) + and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!270:(\tikztotarget)$) + .. (\tikztotarget)\tikztonodes}}, + settings/.code={\tikzset{yade/.cd,#1} + \def\pv##1{\pgfkeysvalueof{/tikz/yade/##1}}}, + yade/.cd,pos/.initial=0.35,ratio/.initial=0} \newcommand{\deuxcellule}[8]{% - \node[coordinate] (a) at (#3) {} ; % - \node[coordinate] (b) at (#4) {} ; % - \node[coordinate] (c) at (#5) {} ; % - \node[coordinate] (d) at (#6) {} ; % - \path let - \p1= ($(b) - (a)$) , % - \p2= ($(d) - (c)$), % - \n1={veclen(\x1,\y1)}, % - \n2={veclen(\x2,\y2)}, % - \p3=($(\x1/\n1,\y1/\n1)$),% - \p4=($(\x2/\n2,\y2/\n2)$),% - \n3={#1 * \n1},% - \p5=($(\n3 * \x3, \n3 * \y3)$),% - \n3={#2 * \n2},% - \p6=($(\n3 * \x4, \n3 * \y4)$) in% - (a) ++ (\p5) node[coordinate] (x) {} %% - (c) ++ (\p6) node[coordinate] (y) {} %% - ; - \draw[#7] (x) -| (y) ; % + \node[coordinate] (a) at (#3) {} ; % + \node[coordinate] (b) at (#4) {} ; % + \node[coordinate] (c) at (#5) {} ; % + \node[coordinate] (d) at (#6) {} ; % + \path let + \p1= ($(b) - (a)$) , % + \p2= ($(d) - (c)$), % + \n1={veclen(\x1,\y1)}, % + \n2={veclen(\x2,\y2)}, % + \p3=($(\x1/\n1,\y1/\n1)$),% + \p4=($(\x2/\n2,\y2/\n2)$),% + \n3={#1 * \n1},% + \p5=($(\n3 * \x3, \n3 * \y3)$),% + \n3={#2 * \n2},% + \p6=($(\n3 * \x4, \n3 * \y4)$) in% + (a) ++ (\p5) node[coordinate] (x) {} %% + (c) ++ (\p6) node[coordinate] (y) {} %% + ; + \draw[#7] (x) -| (y) ; % } % Old macros, for compatibility @@ -81,177 +81,177 @@ yade/.cd,pos/.initial=0.35,ratio/.initial=0} \newcommand{\twocellright}[5][.4]{\twocell[#1]{#2}{#3}{#4}{#5}{}{cell=0,bend right}} \DeclareDocumentCommand{\twocelll}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[left]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[left]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellbr}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below right]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below right]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellr}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[right]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[right]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellb}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocella}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellal}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above left]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above left]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellar}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend left={#3},celllr=#4,label={[above right]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend left={#3},celllr=#4,label={[above right]{$\scriptstyle #9$}}}} \DeclareDocumentCommand{\twocellbl}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% -\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below left]{$\scriptstyle #9$}}}} + \deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below left]{$\scriptstyle #9$}}}} % Two cell bent right \def\twocellrb{% - \@ifnextchar[{\twocellrb@i}{\twocellrb@i[.4]}% + \@ifnextchar[{\twocellrb@i}{\twocellrb@i[.4]}% } \def\twocellrb@i[#1]{% - \@ifnextchar[{\twocellrb@ii[#1]}{\twocellrb@ii[#1][#1]}% + \@ifnextchar[{\twocellrb@ii[#1]}{\twocellrb@ii[#1][#1]}% } \def\twocellrb@ii[#1][#2]{% - \deuxcellulerb{#1}{#2}% + \deuxcellulerb{#1}{#2}% } \newcommand{\deuxcellulerb}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labeld={#6}}} \def\twocellra{% - \@ifnextchar[{\twocellra@i}{\twocellra@i[.4]}% + \@ifnextchar[{\twocellra@i}{\twocellra@i[.4]}% } \def\twocellra@i[#1]{% - \@ifnextchar[{\twocellra@ii[#1]}{\twocellra@ii[#1][#1]}% + \@ifnextchar[{\twocellra@ii[#1]}{\twocellra@ii[#1][#1]}% } \def\twocellra@ii[#1][#2]{% - \deuxcellulera{#1}{#2}% + \deuxcellulera{#1}{#2}% } \newcommand{\deuxcellulera}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelu={#6}}} \def\twocellral{% - \@ifnextchar[{\twocellral@i}{\twocellral@i[.4]}% + \@ifnextchar[{\twocellral@i}{\twocellral@i[.4]}% } \def\twocellral@i[#1]{% - \@ifnextchar[{\twocellral@ii[#1]}{\twocellral@ii[#1][#1]}% + \@ifnextchar[{\twocellral@ii[#1]}{\twocellral@ii[#1][#1]}% } \def\twocellral@ii[#1][#2]{% - \deuxcelluleral{#1}{#2}% + \deuxcelluleral{#1}{#2}% } \newcommand{\deuxcelluleral}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelal={#6}}} \def\twocellro{% - \@ifnextchar[{\twocellro@i}{\twocellro@i[.4]}% + \@ifnextchar[{\twocellro@i}{\twocellro@i[.4]}% } \def\twocellro@i[#1]{% - \@ifnextchar[{\twocellro@ii[#1]}{\twocellro@ii[#1][#1]}% + \@ifnextchar[{\twocellro@ii[#1]}{\twocellro@ii[#1][#1]}% } \def\twocellro@ii[#1][#2]{% - \deuxcellulero{#1}{#2}% + \deuxcellulero{#1}{#2}% } \newcommand{\deuxcellulero}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelo={#6}}} \def\twocellrl{% - \@ifnextchar[{\twocellrl@i}{\twocellrl@i[.4]}% + \@ifnextchar[{\twocellrl@i}{\twocellrl@i[.4]}% } \def\twocellrl@i[#1]{% - \@ifnextchar[{\twocellrl@ii[#1]}{\twocellrl@ii[#1][#1]}% + \@ifnextchar[{\twocellrl@ii[#1]}{\twocellrl@ii[#1][#1]}% } \def\twocellrl@ii[#1][#2]{% - \deuxcellulerl{#1}{#2}% + \deuxcellulerl{#1}{#2}% } \newcommand{\deuxcellulerl}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labell={#6}}} \def\twocellrr{% - \@ifnextchar[{\twocellrr@i}{\twocellrr@i[.4]}% + \@ifnextchar[{\twocellrr@i}{\twocellrr@i[.4]}% } \def\twocellrr@i[#1]{% - \@ifnextchar[{\twocellrr@ii[#1]}{\twocellrr@ii[#1][#1]}% + \@ifnextchar[{\twocellrr@ii[#1]}{\twocellrr@ii[#1][#1]}% } \def\twocellrr@ii[#1][#2]{% - \deuxcellulerr{#1}{#2}% + \deuxcellulerr{#1}{#2}% } \newcommand{\deuxcellulerr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelr={#6}}} \def\twocellrbr{% - \@ifnextchar[{\twocellrbr@i}{\twocellrbr@i[.4]}% + \@ifnextchar[{\twocellrbr@i}{\twocellrbr@i[.4]}% } \def\twocellrbr@i[#1]{% - \@ifnextchar[{\twocellrbr@ii[#1]}{\twocellrbr@ii[#1][#1]}% + \@ifnextchar[{\twocellrbr@ii[#1]}{\twocellrbr@ii[#1][#1]}% } \def\twocellrbr@ii[#1][#2]{% - \deuxcellulerbr{#1}{#2}% + \deuxcellulerbr{#1}{#2}% } \newcommand{\deuxcellulerbr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelbr={#6}}} % Two cell bent left \def\twocelllb{% - \@ifnextchar[{\twocelllb@i}{\twocelllb@i[.4]}% + \@ifnextchar[{\twocelllb@i}{\twocelllb@i[.4]}% } \def\twocelllb@i[#1]{% - \@ifnextchar[{\twocelllb@ii[#1]}{\twocelllb@ii[#1][#1]}% + \@ifnextchar[{\twocelllb@ii[#1]}{\twocelllb@ii[#1][#1]}% } \def\twocelllb@ii[#1][#2]{% - \deuxcellulelb{#1}{#2}% + \deuxcellulelb{#1}{#2}% } \newcommand{\deuxcellulelb}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labeld={#6}}} \def\twocellla{% - \@ifnextchar[{\twocellla@i}{\twocellla@i[.4]}% + \@ifnextchar[{\twocellla@i}{\twocellla@i[.4]}% } \def\twocellla@i[#1]{% - \@ifnextchar[{\twocellla@ii[#1]}{\twocellla@ii[#1][#1]}% + \@ifnextchar[{\twocellla@ii[#1]}{\twocellla@ii[#1][#1]}% } \def\twocellla@ii[#1][#2]{% - \deuxcellulela{#1}{#2}% + \deuxcellulela{#1}{#2}% } \newcommand{\deuxcellulela}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelu={#6}}} \def\twocelllal{% - \@ifnextchar[{\twocelllal@i}{\twocelllal@i[.4]}% + \@ifnextchar[{\twocelllal@i}{\twocelllal@i[.4]}% } \def\twocelllal@i[#1]{% - \@ifnextchar[{\twocelllal@ii[#1]}{\twocelllal@ii[#1][#1]}% + \@ifnextchar[{\twocelllal@ii[#1]}{\twocelllal@ii[#1][#1]}% } \def\twocelllal@ii[#1][#2]{% - \deuxcellulelal{#1}{#2}% + \deuxcellulelal{#1}{#2}% } \newcommand{\deuxcellulelal}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelal={#6}}} \def\twocelllo{% - \@ifnextchar[{\twocelllo@i}{\twocelllo@i[.4]}% + \@ifnextchar[{\twocelllo@i}{\twocelllo@i[.4]}% } \def\twocelllo@i[#1]{% - \@ifnextchar[{\twocelllo@ii[#1]}{\twocelllo@ii[#1][#1]}% + \@ifnextchar[{\twocelllo@ii[#1]}{\twocelllo@ii[#1][#1]}% } \def\twocelllo@ii[#1][#2]{% - \deuxcellulelo{#1}{#2}% + \deuxcellulelo{#1}{#2}% } \newcommand{\deuxcellulelo}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelo={#6}}} \def\twocellll{% - \@ifnextchar[{\twocellll@i}{\twocellll@i[.4]}% + \@ifnextchar[{\twocellll@i}{\twocellll@i[.4]}% } \def\twocellll@i[#1]{% - \@ifnextchar[{\twocellll@ii[#1]}{\twocellll@ii[#1][#1]}% + \@ifnextchar[{\twocellll@ii[#1]}{\twocellll@ii[#1][#1]}% } \def\twocellll@ii[#1][#2]{% - \deuxcellulell{#1}{#2}% + \deuxcellulell{#1}{#2}% } \newcommand{\deuxcellulell}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labell={#6}}} \def\twocelllr{% - \@ifnextchar[{\twocelllr@i}{\twocelllr@i[.4]}% + \@ifnextchar[{\twocelllr@i}{\twocelllr@i[.4]}% } \def\twocelllr@i[#1]{% - \@ifnextchar[{\twocelllr@ii[#1]}{\twocelllr@ii[#1][#1]}% + \@ifnextchar[{\twocelllr@ii[#1]}{\twocelllr@ii[#1][#1]}% } \def\twocelllr@ii[#1][#2]{% - \deuxcellulelr{#1}{#2}% + \deuxcellulelr{#1}{#2}% } \newcommand{\deuxcellulelr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelr={#6}}} \def\twocelllbr{% - \@ifnextchar[{\twocelllbr@i}{\twocelllbr@i[.4]}% + \@ifnextchar[{\twocelllbr@i}{\twocelllbr@i[.4]}% } \def\twocelllbr@i[#1]{% - \@ifnextchar[{\twocelllbr@ii[#1]}{\twocelllbr@ii[#1][#1]}% + \@ifnextchar[{\twocelllbr@ii[#1]}{\twocelllbr@ii[#1][#1]}% } \def\twocelllbr@ii[#1][#2]{% - \deuxcellulelbr{#1}{#2}% + \deuxcellulelbr{#1}{#2}% } \newcommand{\deuxcellulelbr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelbr={#6}}} @@ -259,20 +259,20 @@ yade/.cd,pos/.initial=0.35,ratio/.initial=0} \newbox\xrat@below \newbox\xrat@above \newcommand{\Xarrow}[3][]{% - \setbox\xrat@below=\hbox{\ensuremath{\scriptstyle #2}}% - \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #3}}% - \pgfmathsetlengthmacro{\xrat@len}{max(\wd\xrat@below,\wd\xrat@above)+.6em}% - \mathrel{\tikz [#1,baseline=-.75ex] - \draw (0,0) -- node[below=-2pt] {\box\xrat@below} - node[above=-2pt] {\box\xrat@above} - (\xrat@len,0) ;}} + \setbox\xrat@below=\hbox{\ensuremath{\scriptstyle #2}}% + \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #3}}% + \pgfmathsetlengthmacro{\xrat@len}{max(\wd\xrat@below,\wd\xrat@above)+.6em}% + \mathrel{\tikz [#1,baseline=-.75ex] + \draw (0,0) -- node[below=-2pt] {\box\xrat@below} + node[above=-2pt] {\box\xrat@above} + (\xrat@len,0) ;}} \newcommand{\xarrow}[2][]{% - \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #2\ }}% - \pgfmathsetlengthmacro{\xrat@len}{\wd\xrat@above+.8em}% - \mathrel{\tikz [baseline=-.75ex] - \draw (0,0) edge[#1] node[above=-2pt] {\box\xrat@above} - (\xrat@len,0) ;}} + \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #2\ }}% + \pgfmathsetlengthmacro{\xrat@len}{\wd\xrat@above+.8em}% + \mathrel{\tikz [baseline=-.75ex] + \draw (0,0) edge[#1] node[above=-2pt] {\box\xrat@above} + (\xrat@len,0) ;}} @@ -281,7 +281,7 @@ yade/.cd,pos/.initial=0.35,ratio/.initial=0} \newenvironment{net}{\begin{tikzpicture}[baseline=(current bounding box.center),text depth=.2em,text height=.8em,inner sep=1pt]}{\end{tikzpicture}} \newcommand{\ssf}[2]{% -\inetatom(#1){#2}% + \inetatom(#1){#2}% } \newcommand{\gimpll}{\ssf{Rien}{\impll}} @@ -299,107 +299,116 @@ yade/.cd,pos/.initial=0.35,ratio/.initial=0} \pgfdeclaredecoration{single line}{initial}{ - \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} - \state{final}{\pgfpathlineto{\pgfpointorigin}} + \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} + \state{final}{\pgfpathlineto{\pgfpointorigin}} } \pgfdeclaredecoration{single line backwards}{initial}{ - \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} - \state{final}{\pgfpathlineto{\pgfpointorigin}} + \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} + \state{final}{\pgfpathlineto{\pgfpointorigin}} } \tikzset{ - raise line/.style={ - decoration={single line, raise=#1}, decorate - } + raise line/.style={ + decoration={single line, raise=#1}, decorate + } } \tikzset{ -mod/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with { -\path[draw,-] (0,-3pt) -- (0,3pt); + mod/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with { + \path[draw,-] (0,-3pt) -- (0,3pt); }}}}} \tikzset{ -label/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\node[inner sep=2pt,outer sep=0] #1 ;} + label/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[inner sep=2pt,outer sep=0] #1 ;} }}}} \tikzset{ -labelo/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\node[circle,inner sep=0pt,fill=white] {$\scriptstyle #1$} ;} + labelo/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[circle,inner sep=0pt,fill=white] {$\scriptstyle #1$} ;} }}}} \tikzset{ -labelon/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\node[inner sep=1pt,fill=white] {$\scriptstyle #1$} ;} + labelon/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[inner sep=1pt,fill=white] {$\scriptstyle #1$} ;} }}}} \tikzset{ -labelonb/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\node[inner sep=0pt,fill={bg}] {$\scriptstyle #1$} ;} + labelonb/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[inner sep=0pt,fill={bg}] {$\scriptstyle #1$} ;} }}}} \tikzset{ -labelat/.style 2 args={postaction={ -decorate, -decoration={ -markings, -mark=at position #2 with {\node[inner sep=2pt] #1 ;} + labelat/.style 2 args={postaction={ + decorate, + decoration={ + markings, + mark=at position #2 with {\node[inner sep=2pt] #1 ;} }}}} \tikzset{ -labeloat/.style 2 args={postaction={ -decorate, -decoration={ -markings, -mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} + labeloat/.style 2 args={postaction={ + decorate, + decoration={ + markings, + mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} }}}} \tikzset{ -labelonat/.style 2 args={postaction={ -decorate, -decoration={ -markings, -mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} + labelonat/.style 2 args={postaction={ + decorate, + decoration={ + markings, + mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} }}}} +\tikzset{ + labelonatsloped/.style 2 args={postaction={ + decorate, + decoration={ + markings, + mark=at position #2 with {\node[inner sep=0.1pt,fill=white,transform shape] {#1} ;} +}}}} + + \tikzset{diagnode/.style={anchor=base,inner sep=5pt,outer sep=0pt}} \tikzset{diag/.style 2 args=% - { -matrix of math nodes,ampersand replacement=\&, % -text height=1.2ex, text depth=0.25ex, % -row sep={#1 cm,between borders}, % -column sep={#2 cm,between borders}} + { + matrix of math nodes,ampersand replacement=\&, % + text height=1.2ex, text depth=0.25ex, % + row sep={#1 cm,between borders}, % + column sep={#2 cm,between borders}} }% \tikzset{diagorigins/.style 2 args=% -{matrix of math nodes,ampersand replacement=\&, % -row sep={#1 cm,between origins}, % -column sep={#2 cm,between origins}} + {matrix of math nodes,ampersand replacement=\&, % + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins}} }% \tikzset{stringdiag/.style 2 args=% -{nodes={inner sep=1pt,outer sep=0pt},% - ampersand replacement=\&,% - row sep={#1 cm,between origins}, % - column sep={#2 cm,between origins}% + {nodes={inner sep=1pt,outer sep=0pt},% + ampersand replacement=\&,% + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins}% }}% \newcommand{\diaggrandhauteur}{1} \newcommand{\diaggrandlargeur}{2} @@ -407,310 +416,310 @@ column sep={#2 cm,between origins}} \newcommand{\diagpetitlargeur}{1.5} \tikzset{organigram/.style 2 args={matrix of nodes,ampersand replacement=\&, % -text height=1.7ex, text depth=0.25ex, % -row sep={#1 cm,between origins}, % -column sep={#2 cm,between origins} }} + text height=1.7ex, text depth=0.25ex, % + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins} }} \tikzset{graphe/.style 2 args={matrix of math nodes,ampersand replacement=\&, % - row sep={#1 cm,between origins}, % - column sep={#2 cm,between origins}, % - inner sep=-.1ex}} % + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins}, % + inner sep=-.1ex}} % \tikzset{ -two/.style 2 args={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with \node (#1) [#2] {} ; + two/.style 2 args={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with \node (#1) [#2] {} ; }}}} \tikzset{ -twocenter/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with \node (#1) {} ; + twocenter/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with \node (#1) {} ; }}}} \tikzset{ -twoon/.style 2 args={twocenter={#1},label={{$\scriptstyle #2$}}} + twoon/.style 2 args={twocenter={#1},label={{$\scriptstyle #2$}}} } \tikzset{ -twoo/.style={two={on},label={{$\scriptstyle #1$}}} + twoo/.style={two={on},label={{$\scriptstyle #1$}}} } \tikzset{ -twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} + twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} } \tikzset{ -twoleft/.style 2 args={two={#1}{right},label={[left]{$\scriptstyle #2$}}} + twoleft/.style 2 args={two={#1}{right},label={[left]{$\scriptstyle #2$}}} } \tikzset{ -twor/.style={two={r}{left},label={[right]{$\scriptstyle #1$}}} + twor/.style={two={r}{left},label={[right]{$\scriptstyle #1$}}} } \tikzset{ -tworight/.style 2 args={two={#1}{left},label={[right]{$\scriptstyle #2$}}} + tworight/.style 2 args={two={#1}{left},label={[right]{$\scriptstyle #2$}}} } \tikzset{ -twou/.style={two={u}{below},label={[above]{$\scriptstyle #1$}}} + twou/.style={two={u}{below},label={[above]{$\scriptstyle #1$}}} } \tikzset{ -twoa/.style={two={a}{below},label={[above]{$\scriptstyle #1$}}} + twoa/.style={two={a}{below},label={[above]{$\scriptstyle #1$}}} } \tikzset{ -twoup/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} + twoup/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} } \tikzset{ -twoabove/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} + twoabove/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} } \tikzset{ -twod/.style={two={d}{above},label={[below]{$\scriptstyle #1$}}} + twod/.style={two={d}{above},label={[below]{$\scriptstyle #1$}}} } \tikzset{ -twob/.style={two={b}{above},label={[below]{$\scriptstyle #1$}}} + twob/.style={two={b}{above},label={[below]{$\scriptstyle #1$}}} } \tikzset{ -twodown/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} + twodown/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} } \tikzset{ -twobelow/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} + twobelow/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} } \tikzset{ -twoal/.style={two={al}{right},label={[above left]{$\scriptstyle #1$}}} + twoal/.style={two={al}{right},label={[above left]{$\scriptstyle #1$}}} } \tikzset{ -twoaboveleft/.style 2 args={two={#1}{above},label={[above left]{$\scriptstyle #2$}}} + twoaboveleft/.style 2 args={two={#1}{above},label={[above left]{$\scriptstyle #2$}}} } \tikzset{ -twoar/.style={two={ar}{left},label={[above right]{$\scriptstyle #1$}}} + twoar/.style={two={ar}{left},label={[above right]{$\scriptstyle #1$}}} } \tikzset{ -twoaboveright/.style 2 args={two={#1}{above},label={[above right]{$\scriptstyle #2$}}} + twoaboveright/.style 2 args={two={#1}{above},label={[above right]{$\scriptstyle #2$}}} } \tikzset{ -twobr/.style={two={br}{left},label={[below right]{$\scriptstyle #1$}}} + twobr/.style={two={br}{left},label={[below right]{$\scriptstyle #1$}}} } \tikzset{ -twobelowright/.style 2 args={two={#1}{left},label={[below right]{$\scriptstyle #2$}}} + twobelowright/.style 2 args={two={#1}{left},label={[below right]{$\scriptstyle #2$}}} } \tikzset{ -twobl/.style={two={bl}{right},label={[below left]{$\scriptstyle #1$}}} + twobl/.style={two={bl}{right},label={[below left]{$\scriptstyle #1$}}} } \tikzset{ -twobelowleft/.style 2 args={two={#1}{right},label={[below left]{$\scriptstyle #2$}}} + twobelowleft/.style 2 args={two={#1}{right},label={[below left]{$\scriptstyle #2$}}} } \tikzset{ -twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} + twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} } \tikzset{ -labell/.style={label={[left]{$\scriptstyle #1$}}} + labell/.style={label={[left]{$\scriptstyle #1$}}} } \tikzset{ -labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} + labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labelr/.style={label={[right]{$\scriptstyle #1$}}} + labelr/.style={label={[right]{$\scriptstyle #1$}}} } \tikzset{ -labelrat/.style 2 args={labelat={[right]{$\scriptstyle #1$}}{#2}} + labelrat/.style 2 args={labelat={[right]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labelar/.style={label={[above right]{$\scriptstyle #1$}}} + labelar/.style={label={[above right]{$\scriptstyle #1$}}} } \tikzset{ -labelarat/.style 2 args={labelat={[above right]{$\scriptstyle #1$}}{#2}} + labelarat/.style 2 args={labelat={[above right]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labelbr/.style={label={[below right]{$\scriptstyle #1$}}} + labelbr/.style={label={[below right]{$\scriptstyle #1$}}} } \tikzset{ -labelbrat/.style 2 args={labelat={[below right]{$\scriptstyle #1$}}{#2}} + labelbrat/.style 2 args={labelat={[below right]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labelu/.style={label={[above]{$\scriptstyle #1$}}} + labelu/.style={label={[above]{$\scriptstyle #1$}}} } \tikzset{ -labeluat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} + labeluat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} } \tikzset{ - labela/.style={label={[above]{$\scriptstyle #1$}}} + labela/.style={label={[above]{$\scriptstyle #1$}}} } \tikzset{ -labelaat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} + labelaat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} } \tikzset{ - loina/.style={label={[above=.5em]{$\scriptstyle #1$}}} + loina/.style={label={[above=.5em]{$\scriptstyle #1$}}} } \tikzset{ -labeld/.style={label={[below]{$\scriptstyle #1$}}} + labeld/.style={label={[below]{$\scriptstyle #1$}}} } \tikzset{ -labelb/.style={label={[below]{$\scriptstyle #1$}}} + labelb/.style={label={[below]{$\scriptstyle #1$}}} } \tikzset{ -labelbat/.style 2 args={labelat={[below]{$\scriptstyle #1$}}{#2}} + labelbat/.style 2 args={labelat={[below]{$\scriptstyle #1$}}{#2}} } \tikzset{ -loinb/.style={label={[below=.5em]{$\scriptstyle #1$}}} + loinb/.style={label={[below=.5em]{$\scriptstyle #1$}}} } \tikzset{ -labelal/.style={label={[above left]{$\scriptstyle #1$}}} + labelal/.style={label={[above left]{$\scriptstyle #1$}}} } \tikzset{ -labelalat/.style 2 args={labelat={[above left]{$\scriptstyle #1$}}{#2}} + labelalat/.style 2 args={labelat={[above left]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labelbl/.style={label={[below left]{$\scriptstyle #1$}}} + labelbl/.style={label={[below left]{$\scriptstyle #1$}}} } \tikzset{ -labelblat/.style 2 args={labelat={[below left]{$\scriptstyle #1$}}{#2}} + labelblat/.style 2 args={labelat={[below left]{$\scriptstyle #1$}}{#2}} } \tikzset{ -labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} + labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} } \newcommand{\cs}[2][draw,->]{ % - \path[#1] (#2-1-1) -- (#2-1-2) ; % - \path[#1] (#2-1-3) -- (#2-1-2) ; % + \path[#1] (#2-1-1) -- (#2-1-2) ; % + \path[#1] (#2-1-3) -- (#2-1-2) ; % } \newcommand{\cospan}{\cs{m}} \newcommand{\vdoublecs}[2][draw,->]{ - \foreach \i in {1,2,3} % - {% - \path[#1] (#2-1-\i) -- (#2-2-\i) ;% - \path[#1] (#2-3-\i) -- (#2-2-\i) ; % - } ; % + \foreach \i in {1,2,3} % + {% + \path[#1] (#2-1-\i) -- (#2-2-\i) ;% + \path[#1] (#2-3-\i) -- (#2-2-\i) ; % + } ; % } \newcommand{\hdoublecs}[2][draw,->]{ - \foreach \i in {1,2,3} % - {% - \path[#1] (#2-\i-1) -- (#2-\i-2) ;% - \path[#1] (#2-\i-3) -- (#2-\i-2) ; % - } ; % + \foreach \i in {1,2,3} % + {% + \path[#1] (#2-\i-1) -- (#2-\i-2) ;% + \path[#1] (#2-\i-3) -- (#2-\i-2) ; % + } ; % } \newcommand{\vdoubleisos}[1]{ - \foreach \i in {1,2,3} % - {% - \isopath{#1-1-\i}{#1-2-\i} % - \isopath{#1-2-\i}{#1-3-\i} % - } ; % + \foreach \i in {1,2,3} % + {% + \isopath{#1-1-\i}{#1-2-\i} % + \isopath{#1-2-\i}{#1-3-\i} % + } ; % } \newcommand{\hdoubleisos}[1]{ - \foreach \i in {1,2,3} % - {% - \isopath{#1-\i-1}{#1-\i-2} % - \isopath{#1-\i-2}{#1-\i-3} % - } ; % + \foreach \i in {1,2,3} % + {% + \isopath{#1-\i-1}{#1-\i-2} % + \isopath{#1-\i-2}{#1-\i-3} % + } ; % } \newcommand{\doublecs}[2][draw,->]{% - \vdoublecs[#1]{#2} % - \hdoublecs[#1]{#2} % + \vdoublecs[#1]{#2} % + \hdoublecs[#1]{#2} % } \newcommand{\doublecospan}{\doublecs{m}} \newcommand{\sq}[4]{% - (m-1-1) edge[twou={#1}] (m-1-2) % - (m-1-1) edge[twol={#2}] (m-2-1) % - (m-1-2) edge[twor={#3}] (m-2-2) % - (m-2-1) edge[twod={#4}] (m-2-2) % + (m-1-1) edge[twou={#1}] (m-1-2) % + (m-1-1) edge[twol={#2}] (m-2-1) % + (m-1-2) edge[twor={#3}] (m-2-2) % + (m-2-1) edge[twod={#4}] (m-2-2) % } \newcommand{\sqpath}[6]{ - \draw[->,#6,rounded corners] - (#1) -- +(#2:#3ex) -- node(#4) {} ($(#5) + (#2:#3ex)$) -- (#5) % - ; % - } + \draw[->,#6,rounded corners] + (#1) -- +(#2:#3ex) -- node(#4) {} ($(#5) + (#2:#3ex)$) -- (#5) % + ; % +} \newcommand{\celltoangle}[5]{ - \path[draw] ($(#1)+(#2:#3ex)$) edge[celllr={0}{0},#5] ($(#1)+(#2:#4ex)$) ; % + \path[draw] ($(#1)+(#2:#3ex)$) edge[celllr={0}{0},#5] ($(#1)+(#2:#4ex)$) ; % } \newcommand{\pbkdefault}{1.4em} \newcommand{\pbkmargin}{1pt} \DeclareDocumentCommand{\pullbackk}{O{\pbkdefault} O{\pbkdefault} D(){2pt} m m m m}{% - \node[coordinate] (a) at (#4) {} ; % - \node[coordinate] (b) at (#5) {} ; % - \node[coordinate] (c) at (#6) {} ; % - \node[coordinate] (a') at ($(b)!#1!(a)$) {} ; % - \node[coordinate] (c') at ($(b)!#2!(c)$) {} ; % - \node[coordinate] (d) at (barycentric cs:a'=1,c'=1,b=-1) {} ; % - \node[coordinate] (aup) at ($(a')!#3!(d)$) {}; - \node[coordinate] (cup) at ($(c')!#3!(d)$) {}; - \path[#7] (aup) -- (d) -- (cup) ; % + \node[coordinate] (a) at (#4) {} ; % + \node[coordinate] (b) at (#5) {} ; % + \node[coordinate] (c) at (#6) {} ; % + \node[coordinate] (a') at ($(b)!#1!(a)$) {} ; % + \node[coordinate] (c') at ($(b)!#2!(c)$) {} ; % + \node[coordinate] (d) at (barycentric cs:a'=1,c'=1,b=-1) {} ; % + \node[coordinate] (aup) at ($(a')!#3!(d)$) {}; + \node[coordinate] (cup) at ($(c')!#3!(d)$) {}; + \path[#7] (aup) -- (d) -- (cup) ; % } \newcommand{\pullback}[5][\pbkdefault]{\pullbackk[#1][#1]{#2}{#3}{#4}{#5}} \newcommand{\pbk}[4][\pbkdefault]{% - \pullbackk[#1][#1]{#2}{#3}{#4}{draw,-} } + \pullbackk[#1][#1]{#2}{#3}{#4}{draw,-} } \newcommand{\stdpbk}{\pbk{m-2-1}{m-1-1}{m-1-2}} \newcommand{\stdpo}{\pbk{m-2-1}{m-2-2}{m-1-2}} \newcommand{\onepbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } + \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } \newcommand{\ptwpbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } + \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } \newcommand{\wpbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,dashed} } + \pullback[#1]{#2}{#3}{#4}{draw,dashed} } \newcommand{\pbkk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{cell=0} } + \pullback[#1]{#2}{#3}{#4}{cell=0} } \newcommand{\laxpbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,->,cell=0} } + \pullback[#1]{#2}{#3}{#4}{draw,->,cell=0} } \newcommand{\oplaxpbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,<-,cell=0} } + \pullback[#1]{#2}{#3}{#4}{draw,<-,cell=0} } \newcommand{\poleftg}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45-} } + \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45-} } \newcommand{\porightg}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45 reversed-} } + \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45 reversed-} } \newcommand{\dpbk}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45} } + \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45} } \newcommand{\dpbkrev}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45 reversed} } + \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45 reversed} } \newcommand{\dpbkblack}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,-triangle 45} } + \pullback[#1]{#2}{#3}{#4}{draw,-triangle 45} } \newcommand{\dpbkblackrev}[4][\pbkdefault]{% - \pullback[#1]{#2}{#3}{#4}{draw,triangle 45-open triangle 45} } + \pullback[#1]{#2}{#3}{#4}{draw,triangle 45-open triangle 45} } \tikzset{shortenlr/.style 2 args={shorten <={#1 ex},shorten >={#2 ex}}} \tikzset{ -back/.style={densely dotted} + back/.style={densely dotted} } \tikzset{ -fore/.style 2 args={preaction={draw={white},-,line width=4pt,shorten <=#1cm,shorten >=#2cm}}, -fore/.default={0.2}{0.2} + fore/.style 2 args={preaction={draw={white},-,line width=4pt,shorten <=#1cm,shorten >=#2cm}}, + fore/.default={0.2}{0.2} } \tikzset{ -foretwo/.style={preaction={draw=white,-,line width=6pt}} + foretwo/.style={preaction={draw=white,-,line width=6pt}} } \tikzset{twocell/.style = {double equal sign distance,double,-implies,shorten <= .15cm,shorten >=.15cm,draw}} \tikzset{ -cell/.style = {double equal sign distance,double,-implies,shorten <= #1 cm,shorten >=#1 cm,draw} + cell/.style = {double equal sign distance,double,-implies,shorten <= #1 cm,shorten >=#1 cm,draw} } \tikzset{celllr/.style 2 args = {double equal sign distance,double,-implies,shorten <= #1 ex,shorten >=#2 ex,draw}} \tikzset{identity/.style = {double equal sign distance,double,-,draw}} \tikzset{iso/.style = {label={[below=0em,sloped]{$\scriptstyle -$}},label={[above=-.2em,sloped]{$\scriptstyle \sim$}}}} \tikzset{equi/.style = {label={[above=-.2em,sloped]{$\scriptstyle \sim$}}}} \tikzset{isotwo/.style = postaction={ - decorate, - decoration={ - markings, - mark=at position .5 with {\node[inner sep=2pt,outer sep=0,above=-.2em,sloped] {$\scriptstyle \sim$} ;} - }}} + decorate, + decoration={ + markings, + mark=at position .5 with {\node[inner sep=2pt,outer sep=0,above=-.2em,sloped] {$\scriptstyle \sim$} ;} +}}} \tikzset{isor/.style = {labelr={\iso}}} \tikzset{isol/.style = {labell={\iso}}} \tikzset{isod/.style = {labeld={\iso}}} @@ -738,33 +747,33 @@ cell/.style = {double equal sign distance,double,-implies,shorten <= #1 cm,short \tikzset{adj/.default={.1cm}{0cm}} \tikzset{iff/.style = {double equal sign distance,double,-implies,draw,shorten <= #1cm}} \tikzset{ -mod/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\draw[-] (0pt,-2pt) -- (0pt,2pt);} -}}}, -negate/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\node[transform shape] (tempnode) {$/$};} -}}}, -mapsto/.style={|->}, -otspam/.style={<-|}, -pro/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position #1 with {\draw[-,fill] (0pt,0pt) circle (1.5pt);} -}}}, -pro/.default={.5}, -glob/.style={postaction={ -decorate, -decoration={ -markings, -mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} -}}} + mod/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\draw[-] (0pt,-2pt) -- (0pt,2pt);} + }}}, + negate/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[transform shape] (tempnode) {$/$};} + }}}, + mapsto/.style={|->}, + otspam/.style={<-|}, + pro/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position #1 with {\draw[-,fill] (0pt,0pt) circle (1.5pt);} + }}}, + pro/.default={.5}, + glob/.style={postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} + }}} } \newcommand{\idto}{\mathbin{\tikz[baseline] \draw[identity] (0pt,.5ex) -- (3ex,.5ex);}} @@ -772,17 +781,17 @@ mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} \newcommand{\fibto}[1]{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[fib,labelu={\scriptstyle #1}] (3ex,.5ex);}} \newcommand{\fibot}[1]{\mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[fib,labelu={\scriptstyle #1}] (0pt,.5ex);}} \newcommand{\dfibto}{ - \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (3ex,.5ex);}} + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (3ex,.5ex);}} \newcommand{\xdfibto}[1]{ - \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib,labelu={\scriptstyle #1}] (3ex,.5ex);}} + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib,labelu={\scriptstyle #1}] (3ex,.5ex);}} \newcommand{\shortdfibto}{ - \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (1.5ex,.5ex);}} + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (1.5ex,.5ex);}} \newcommand{\shortdfibot}{ - \mathbin{\tikz[baseline] \draw (1.5ex,.5ex) edge[dfib] (0,.5ex);}} + \mathbin{\tikz[baseline] \draw (1.5ex,.5ex) edge[dfib] (0,.5ex);}} \newcommand{\xxto}[2]{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[->,labelu={\scriptstyle #1},labelb={\scriptstyle #2}] (3ex,.5ex);}} \newcommand{\dfibot}[1][]{ - \mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[dfib,labelu={\scriptstyle #1}] (0pt,.5ex);}} + \mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[dfib,labelu={\scriptstyle #1}] (0pt,.5ex);}} \newcommand{\modto}{\mathbin{\tikz[baseline] \draw[->,mod] (0pt,.5ex) -- (3ex,.5ex);}} \newcommand{\proto}{\mathbin{\tikz[baseline] \draw[->,pro] (0pt,.5ex) -- (3ex,.5ex);}} \newcommand{\shortproto}{\mathbin{\tikz[baseline] \draw[->,pro] (0pt,.5ex) -- (1.5ex,.5ex);}} @@ -795,34 +804,34 @@ mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} \newcommand{\cellule}[3][]{ % - \path (#3) +(#2:-.4cm) [twocell,#1] -- +(#2:.4cm) ; % + \path (#3) +(#2:-.4cm) [twocell,#1] -- +(#2:.4cm) ; % } \newcommand{\celluled}[2]{ % - \cellule[labell={#2}]{-90}{#1} % + \cellule[labell={#2}]{-90}{#1} % } \newcommand{\celluler}[2]{ % - \cellule[labelu={#2}]{0}{#1} % + \cellule[labelu={#2}]{0}{#1} % } \newcommand{\isopath}[2]{% - \path % - (#1) -- node[sloped] {$\iso$} (#2) ; % + \path % + (#1) -- node[sloped] {$\iso$} (#2) ; % } \newcommand{\adjtemplate}[6][1]{% - \begin{tikzpicture}[baseline=(m-1-1.base)] % - \matrix (m) [diag={1}{#1}, - column sep={#1 cm,between borders}]{ % - |[adj]| #2 % - \& #6 % - \& |[adj]| #3 \\ - } ; % - \path[->] % - (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % - (m-1-3.base west) edge[labeld={#5},bend left=15] (m-1-1.base east) % - ; % - \end{tikzpicture} % + \begin{tikzpicture}[baseline=(m-1-1.base)] % + \matrix (m) [diag={1}{#1}, + column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& #6 % + \& |[adj]| #3 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.base west) edge[labeld={#5},bend left=15] (m-1-1.base east) % + ; % + \end{tikzpicture} % } \newcommand{\adj}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\bot}} @@ -831,107 +840,107 @@ mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} \newcommand{\catiso}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\cong}} \newcommand{\adjunction}[4]{% - \path[->] % - (#1) edge[twou={#3},bend left=15] (#2) % - (#2) edge[twod={#4},bend left=15] (#1) % - ; % - \path (u) -- node[pos=.5,sloped] {$\dashv$} (d) ; % - } + \path[->] % + (#1) edge[twou={#3},bend left=15] (#2) % + (#2) edge[twod={#4},bend left=15] (#1) % + ; % + \path (u) -- node[pos=.5,sloped] {$\dashv$} (d) ; % +} \newcommand{\ladjunction}[4]{% - \path[->] % - (#1) edge[twou={#3},bend left=15] (#2) % - (#2) edge[twod={#4},bend left=15] (#1) % - ; % - \path (u) -- node[pos=.5,sloped] {$\vdash$} (d) ; % - } + \path[->] % + (#1) edge[twou={#3},bend left=15] (#2) % + (#2) edge[twod={#4},bend left=15] (#1) % + ; % + \path (u) -- node[pos=.5,sloped] {$\vdash$} (d) ; % +} \newcommand{\adjs}[8][1]{% - \begin{tikzpicture} % - \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % - |[adj]| #2 % - \& \bot % - \& |[adj]| #3 - \& \bot % - \& |[adj]| #6 \\ - } ; % - \path[->] % - (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % - (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % - (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % - (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % - ; % - \end{tikzpicture} % + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& \bot % + \& |[adj]| #3 + \& \bot % + \& |[adj]| #6 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % + (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % + ; % + \end{tikzpicture} % } \newcommand{\coadjs}[8][1]{% - \begin{tikzpicture} % - \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % - |[adj]| #2 % - \& \top % - \& |[adj]| #3 - \& \top % - \& |[adj]| #6 \\ - } ; % - \path[->] % - (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % - (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % - (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % - (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % - ; % - \end{tikzpicture} % + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& \top % + \& |[adj]| #3 + \& \top % + \& |[adj]| #6 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % + (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % + ; % + \end{tikzpicture} % } \newcommand{\retr}[5][1]{% - \begin{tikzpicture} % - \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % - |[anchor=east,text height=.1cm,text depth=-.1cm]| #2 % - \& |[anchor=center]| \triangleleft % - \& |[anchor=west,text height=.1cm,text depth=-.1cm]| #3 \\ - } ; % - \path[->] % - (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % - (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % - ; % - \end{tikzpicture} % + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[anchor=east,text height=.1cm,text depth=-.1cm]| #2 % + \& |[anchor=center]| \triangleleft % + \& |[anchor=west,text height=.1cm,text depth=-.1cm]| #3 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + ; % + \end{tikzpicture} % } \newcommand{\doublecell}[9]{ - \diag{% - |(X)| {#1} \& |(Y)| {#2} \\ % - |(U)| {#3} \& |(V)| {#4} % - }{% - (X) edge[labelu={#5}] (Y) % - edge[pro,twol={#6}] (U) % - (Y) edge[pro,twor={#7}] (V) % - (U) edge[labeld={#8}] (V) % - (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % - } + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[labelu={#5}] (Y) % + edge[pro,twol={#6}] (U) % + (Y) edge[pro,twor={#7}] (V) % + (U) edge[labeld={#8}] (V) % + (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % + } } \newcommand{\doublecellpro}[9]{ - \diag{% - |(X)| {#1} \& |(Y)| {#2} \\ % - |(U)| {#3} \& |(V)| {#4} % - }{% - (X) edge[labelu={#5}] (Y) % - edge[pro,twol={#6}] (U) % - (Y) edge[pro,twor={#7}] (V) % - (U) edge[labeld={#8}] (V) % - (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % - } + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[labelu={#5}] (Y) % + edge[pro,twol={#6}] (U) % + (Y) edge[pro,twor={#7}] (V) % + (U) edge[labeld={#8}] (V) % + (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % + } } \newcommand{\vdoublecell}[9]{ - \diag{% - |(X)| {#1} \& |(Y)| {#2} \\ % - |(U)| {#3} \& |(V)| {#4} % - }{% - (X) edge[twou={#5}] (Y) % - edge[labell={#6}] (U) % - (Y) edge[labelr={#7}] (V) % - (U) edge[twod={#8}] (V) % - (u) edge[cell=.4,labelr={\scriptstyle #9}] (d) % - } + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[twou={#5}] (Y) % + edge[labell={#6}] (U) % + (Y) edge[labelr={#7}] (V) % + (U) edge[twod={#8}] (V) % + (u) edge[cell=.4,labelr={\scriptstyle #9}] (d) % + } } \newcommand{\Vdots}{|[anchor=center,text height=.1cm]| \vdots} @@ -942,19 +951,19 @@ mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} \newcommand{\mkdots}[2]{ \path - (#1) -- - node[pos=.4] {.} - node[pos=.5] {.} - node[pos=.6] {.} - (#2) - ;} + (#1) -- + node[pos=.4] {.} + node[pos=.5] {.} + node[pos=.6] {.} + (#2) + ;} \newcommand{\mkdotsshrink}[2]{ \path - (#1) -- - node[pos=.3] {.} - node[pos=.5] {.} - node[pos=.7] {.} - (#2) - ;} + (#1) -- + node[pos=.3] {.} + node[pos=.5] {.} + node[pos=.7] {.} + (#2) + ;} \endinput