Commit 742146ee by Michael Kohlhase

### tweaks

 \begin{mhmodnl}[creators=miko]{cartesian-closed-category}{en} \begin{definition} A \trefi[category]{category} $\cC$ is called \defii[name=CCC]{Cartesian}{closed} (a \defi{CCC}) , iff it satisfies the following three properties: \defi{CCC}), iff it satisfies the following three properties: \begin{itemize} \item $\cC$ has a \trefi[initerminal]{terminal} \trefi[category]{object}. \item Any two \trefis[category]{object} $X$ and $Y$ of $\cC$ have a ... ...
 ... ... @@ -5,7 +5,7 @@ \mtrefi[category?arrow]{morphisms} $\catfun{\catprodprojectionFN1}X{X_1}$ and $\catfun{\catprodprojectionFN2}X{X_2}$ the \defi{product} of $X_1$ and $X_2$ and write it as $\catobjprod{X_1,X_2}$ if it satisfies the following universal property:\\ \begin{minipage}{7cm} \begin{minipage}{7.3cm} For every object $Y$ and \trefi[pair]{pair} of \mtrefi[category?arrow]{morphisms} $\catfun{f_1}Y{X_1}$ and $\catfun{f_2}Y{X_2}$ there exists a unique \mtrefi[category?arrow]{morphism} $\catfun{f}Y{\catobjprod{X_1,X_2}}$ such that ... ... @@ -13,7 +13,7 @@ \end{minipage} \begin{minipage}{4cm} \mhtikzinput{tikz/product} \end{minipage} \end{minipage}\\ The unique morphism $f$ is called the \defiii{product}{of}{morphisms} $f_1$ and $f_2$ and is denoted $\catmorprod{f_1,f_2}$. The morphisms $\catprodprojectionFN1$ and $\catprodprojectionFN2$ are called the ... ...
 ... ... @@ -5,13 +5,13 @@ \item A \trefi[class]{class} $\catObj\cC$ of \defis{object}. \item A \trefi[class]{class} $\catMorOp\cC$ of \defis{arrow} (also called \defis[name=arrow]{morphism} or \defis[name=arrow]{map}). \item For each \trefi{arrow} $f$, two \trefis{object} which are called \defi{domain} of $f$; $\catdomain{f}$ and \defi{codomain}; $\catcodomain{f}$. We write \item For each \trefi{arrow} $f$, two \trefis{object} which are called \defi{domain} $\catdomain{f}$ and \defi{codomain} $\catcodomain{f}$ of $f$. We write $\catfun{f}{\catdomain{f}}{\catcodomain{f}}$ and call two \trefis{arrow} $f$ and $g$ \defi{composable}, iff $\catdomain{f}=\catcodomain{g}$. \item An \trefi[semigroup]{associative} \trefi[magma]{operation} $\catcompOp$ called \defi{composition} assigning to each \trefi[pair]{pair} $\pair{f}g$ of \trefi{composable} \trefis{arrow} another \trefi{arrow}; $\catcomp{g,f}$ such that \trefi{composable} \trefis{arrow} another \trefi{arrow} $\catcomp{g,f}$ such that $\catdomain{\catcomp{g,f}} = \catdomain{f}$ and $\catcodomain{\catcomp{g,f}} = \catcodomain{g}$, i.e. $\catfun{\catcomp{g,f}}{\catdomain{f}}{\catcodomain{g}}$. ... ...
 ... ... @@ -7,7 +7,7 @@ \begin{tikzpicture}[xscale=1.8,yscale=1.2] \node (x1) at (-1,0) {$X_1$}; \node (x12) at (0,0) {$\catobjprod{X_1,X_2}$}; \node (x2) at (1,0) {$X_1$}; \node (x2) at (1,0) {$X_2$}; \node (y) at (0,1) {$Y$}; \draw[->] (x12) -- node[below]{$\pi_1$}(x1); \draw[->] (x12) -- node[below]{$\pi_2$}(x2); ... ...