cartesianas.tex

\chapter{Categorías cartesianamente cerradas}
\section{Exponencial}
Si $\cat$ tiene productos binarios, entonces el \newterm{exponencial} de los objetos $B$ y $C$ de $\cat$ es el objeto
\[ C^B \]
y un morfismo:
\[ \varepsilon \colon C^B \times B \to C \]
tal que para todo objeto $A$ y morfismo
\[ f \colon A \times B \to C \]
hay un único morfismo
\[ \lambda_f \colon A \to C^B \]
tal que el siguiente diagrama conmuta:

\[
\begin{tikzcd}
C^B \times B \arrow[rr,"\varepsilon"] & & C \\\\
A \times B \arrow[uu,"\lambda_f\times\id_B"]  \arrow[uurr,"f"]
\end{tikzcd}
\]

El morfismo $\varepsilon$ se denomina \newterm{evaluación}.
El morfismo $\lambda_f$ se denomina \newterm{transposición} o \newterm{currificación} de $f$.

Obsérvese que
\begin{align*}
\lambda \colon C(A \times B, C) & \to C(A,C^B)\\
f & \mapsto \lambda_f
\end{align*}
es un isomorfismo por la existencia e unicidad de $\lambda_f$ por cada $f$.

En programación funcional, la currificación resulta de gran utilidad.
En Haskell, por ejemplo, se usa la función \code{curry} de tipo:
\begin{minted}{haskell}
curry :: ((a, b) -> c) -> a -> b -> c
\end{minted}
Su inversa es \code{uncurry}, de tipo:
\begin{minted}{haskell}
uncurry :: (a ->  b -> c) -> (a, b) -> c
\end{minted}

\section{Categorías cerradas cartesianas}
\begin{definition}
Decimos que una categoría es \index{categoría!cartesianamente cerrada}\emph{cartesianamente cerrada} si cumple las siguientes condiciones:
\begin{enumerate}
\item Tiene productos finitos.
\item Tiene el exponencial de dos objetos cualesquiera.
\end{enumerate}
Si además tiene coproductos finitos, se denomina \index{categoría!bicartesianamente cerrada}\emph{bicartesianamente cerrada}
\end{definition}

\begin{example}
Consideramos la categoría $Pos$ de conjuntos parcialmente ordenados donde los morfismos son funciones monótonas del que hablamos en \ref{ejemplo-producto-pos}.
Sean $P$ y $Q$ posets, veamos que $Q^P = \{ f \colon Q \to P \mid f \text{ monótona}\}$ con el orden:
\[ f \leq g \sii f(p) \leq g(p) \text{ para todo }p \in P \]
El morfismo evaluación es:
\[ \varepsilon (f,p) = f(p) \]
Veamos que efectivamente $\varepsilon$ es un morfismo.
Supongamos que $(f,p) \leq (f',p')$, entonces:
\begin{align*}
\varepsilon(f,p) & = f(p) & \\
& \leq f(p') & \text{ por ser }f\text{ monótona y }p\leq p'\\
& \leq f'(p') & \text{ por ser }f \leq f'\\
& = \varepsilon(f',p')
\end{align*}
Luego $\varepsilon$ es un morfismo $Pos$.
Sea $f \colon X \times P \to Q$ monótona y sea $x \leq x'$.
\begin{align*}
\lambda_f(x)(p) & = f(x,p) & \\
& \leq f(x',p) & \text{pues }(x,p) \leq (x',p)\\
& \leq f'(x',p) & \text{pues }f \leq f'\\
& = \lambda_f(x')(p)
\end{align*}
\end{example}

\begin{lemma}
En una categoría cartesianamente cerrada $\cat$, la exponenciación por un objeto fijo es un functor.
\end{lemma}
\begin{proof}
Queremos probar que la exponenciación:
\[ -^Z \colon \cat \to \cat \]
para un objeto fijo $Z$ es un endofunctor.
Como $\cat$ es cartesianamente cerrada, la exponenciación de $A^Z$ está bien definida para todo objeto $A$ de $\cat$.
Consideremos ahora un morfismo $f \colon A \to B$, tenemos que definir $f^Z \colon A^Z \to B^Z$.
Primero observamos que:
\[ \varepsilon \colon A^Z \times Z \to A \]
Luego:
\[ f \circ \varepsilon \colon A^Z \times Z \to B\]
Transponiendo:
\[ \lambda_{f \circ \varepsilon} \colon A^Z \to B^Z \]
Así que definimos $f^Z$ como $\lambda_{f \circ \varepsilon}$.

Tenemos el siguiente diagrama conmutativo consecuencia de la transposición:
\[
\begin{tikzcd}
B^Z \times Z \arrow[rr,"\varepsilon"] & & B \\\\
A^Z \times Z \arrow[uu,"\lambda_{f\circ \varepsilon}\times\id_Z"]  \arrow[uurr,"f \circ \varepsilon"]
\end{tikzcd}
\]

Luego considerando $(\id_A)^Z$:
\[
\begin{tikzcd}
A^Z \times Z \arrow[rr,"\varepsilon"] & & A \\\\
A^Z \times Z \arrow[uu,"(\id_A)^Z\times\id_Z"]  \arrow[uurr,"\varepsilon"]
\end{tikzcd}
\]
Como $\id_{A^Z}$ cumple también el anterior diagrama y tenemos que el morfismo que cumple el diagrama es único, $(\id_A)^Z = \id_{A^Z}$.

Por otro lado, si tenemos morfismos: $f \colon A \to B$ y $g \colon B \to C$, tenemos que $(g \circ f)^Z$ es el único que conmuta el diagrama:
\[
\begin{tikzcd}
C^Z \times Z \arrow[rr,"\varepsilon"] & & C \\\\
A^Z \times Z \arrow[uu,"(g \circ f)^Z \times\id_Z"]  \arrow[uurr,"g \circ f \circ \varepsilon"]
\end{tikzcd}
\]
Sin embargo, observamos que también conmuta:
\[
\begin{tikzcd}
C^Z \times Z \arrow[rr,"\varepsilon"] & & C\\\\
B^Z \times Z \arrow[rr,"\varepsilon"] \arrow[uu,"g^Z \times \id_Z"] \arrow[uurr,"g \circ \varepsilon"] & & B \\\\
A^Z \times Z \arrow[uu,"f^Z \times\id_Z"]  \arrow[uurr,"f \circ \varepsilon"]
\end{tikzcd}
\]
Podemos reemplazar la flecha diagonal $g \circ \varepsilon$ obteniendo:
\[
\begin{tikzcd}
C^Z \times Z \arrow[rr,"\varepsilon"] & & C\\\\
B^Z \times Z \arrow[rr,"\varepsilon"] \arrow[uu,"g^Z \times \id_Z"] & & B \arrow[uu,"g"] \\\\
A^Z \times Z \arrow[uu,"f^Z \times\id_Z"]  \arrow[uurr,"f \circ \varepsilon"]
\end{tikzcd}
\]
Finalmente, este diagrama implica que:
\[
\begin{tikzcd}
C^Z \times Z \arrow[rr,"\varepsilon"] & & C\\\\
A^Z \times Z \arrow[uu,"(g^Z \circ f^Z) \times\id_Z"]  \arrow[uurr,"g \circ f \circ \varepsilon"]
\end{tikzcd}
\]
conmuta, luego prueba por unicidad que $(g \circ f)^Z = g^Z \circ f^Z$.

Esto demuestra que $-^Z$ es un endofunctor.
\end{proof}

%Más atrás, consideramos la categoría de functores entre dos categorías $\cat$ y $\mathcal{D}$.
%Consideramos ahora la \index{categoría!{de categorías pequeñas}}\emph{categoría de categorías pequeñas}, denominada \index{Cat@$\Cat$|see {categoría de categorías pequeñas}}$\Cat$, con functores como morfismos.

% TODO: Vamos a ver que $\Cat$ es cartesianamente cerrada.

\section{Lógica}
\begin{definition}
Un \newterm{sistema deductivo} es un grafo:
\begin{enumerate}
\item Con flechas $A \xrightarrow{1_A} A$
\item Con una operación binaria sobre flechas $A \xrightarrow{1_A} A$:

\AxiomC{$A \xrightarrow{f} B$}
\AxiomC{$B \xrightarrow{g} C$}
\BinaryInfC{$A \xrightarrow{gf} C$}
\DisplayProof
\end{enumerate}
\end{definition}

Los nodos de los grafos de un sistema deductivo se denominan \emph{fórmulas} y las flechas, \emph{pruebas}.

Hasta aquí es evidente que el concepto de sistema deductivo es equivalente a categoría.

\begin{definition}
Un \newterm{cálculo de conjunción} es un sistema deductivo donde existe una fórmula $\top$, una operación binaria $\land$ llamada conjunción y las siguientes reglas:
\begin{enumerate}
  \item $A \xrightarrow{O_A} \top$.
  \item $A \land B \xrightarrow{\pi^1_{A,B}} A$.
  \item $A \land B \xrightarrow{\pi^2_{A,B}} B$.
  \item
  
  \AxiomC{$C \xrightarrow{f} A$}
  \AxiomC{$C \xrightarrow{g} C$}
  \BinaryInfC{$C \xrightarrow{\langle f,g \rangle} A \land B$}
  \DisplayProof
\end{enumerate}
\end{definition}

\begin{proposition}
Una categoría con productos finitos es un cálculo de conjunción donde $\top$ es el objeto terminal y $\land$ es el producto de objetos.
\end{proposition}
\begin{proof}
Tomamos $O_A$ como el morfismo $A \to \top$.
Igualmente, tomamos $\pi^1$ y $\pi^2$ como las proyecciones del objeto producto $A \times B$ a sus factores.
Para dos morfismo $f \colon C \to A$ y $g \colon C \to B$, sabemos que existe un único morfismo $f \colon C \to A \times B$, que se corresponde con $\langle f,g \rangle$.
\end{proof}

\begin{definition}
Un \newterm{cálculo proposicional intuicionista positivo} es un cálculo de conjunción con una operación binaria $\Rightarrow$ sobre fórmulas y:
\begin{enumerate}
\item $(A \Rightarrow B) \land A \xrightarrow{\varepsilon_{A,B}} B$.
\item 

  \AxiomC{$C \land A \xrightarrow{h} B$}
  \UnaryInfC{$C \xrightarrow{h^*} A \Rightarrow B$}
  \DisplayProof
\end{enumerate} 
\end{definition}
\begin{proposition}
Una categoría cartesianamente cerrada es un cálculo proposicional intuicionista positivo donde $\Rightarrow$ se corresponde con la exponenciación.
\end{proposition}
\begin{proof}
El morfismo $\varepsilon \colon B^A \times A \to B$ de la evaluación de la exponenciación sirve como $\varepsilon_{A,B}$.
Por otro lado $h^*$ se corresponde con la currificación $\lambda_h$.
\end{proof}

\begin{definition}
Una \newterm{cálculo intuicionista} es un cálculo proposicional intuicionista positivo con una fórmula $\bot$, una operación disyunción $\lor$ sobre fórmulas y unas flechas:
\begin{enumerate}
\item $\bot \xrightarrow{!} A$.
\item $A \xrightarrow{\kappa^1_{A,B}} A \lor B$
\item $B \xrightarrow{\kappa^2_{A,B}} A \lor B$
\item 

\AxiomC{$A \xrightarrow{f} C$}
\AxiomC{$B \xrightarrow{g} C$}
\BinaryInfC{$A \lor B \xrightarrow{[f,g]} C$}
\DisplayProof
\end{enumerate}
\end{definition}
\begin{proposition}
Una categoría bicartesianamente cerrada es un cálculo intuicionista donde $\bot$ se corresponde con el objeto inicial y $\lor$ se corresponde con el coproducto.
\end{proposition}
\begin{proof}
Las primera regla es consecuencia de la definición de objeto inicial.
Las otras tres reglas están dadas por las propiedades del coproducto.
\end{proof}

Este vínculo entre lógica intuicionista y categorías bicartesianamente cerradas nos permite movernos entre las dos teorías cuando queramos demostrar algún resultado, por ejemplo:
\begin{lemma}
En cálculo intuicionista proposicional hay como mucho una demostración $A \to \bot$ salvo equivalencia de pruebas.
\end{lemma}
\begin{proof}
En una categoría bicatersianamente cerrada $\cat$ con objeto inicial $0$, para cualquier par de objetos $A$ y $B$ cualesquiera:
\[ \cat(0 \times A, B) \cong \cat(0, B^A) \]
Como hay un único morfismo en $\cat(0, B^A)$ por ser $0$ inicial, entonces hay un único morfismo $0 \times A \to B$.
Luego $0 \times A$ es objeto inicial.
Supongamos que hubiera un morfismo $f \colon A \to 0$.
Como también hay un morfismo $\id_A$, debe haber un morfismo $h \colon A \to 0 \times A$ por la definición de objeto producto.
Si $\pi_2 \colon 0 \times A \to A$ es la segunda proyección, entonces $\pi_2 \circ h = \id_A$ por la definición de producto y $h \circ \pi_2 = \id_{0 \times A}$ porque sólo hay un morfismo $0 \times A \to 0 \times A$.
Por lo tanto $A \cong 0$ y sólo $f$ es el único morfismo.
\end{proof}

Ahora que hemos construido en paralelo un sistema lógico intuicionista y una categoría equivalente, nos podemos preguntar si podemos dar un paso más y llegar a la lógica clásica.
Para ello hay que añadir el principio del tercero excluso, que es equivalente a la regla de eliminación de doble negación.
Para ello, definimos $\neg A$ como la fórmula $A \Rightarrow \bot$.
\begin{prooftree}
\AxiomC{$\neg \neg A$}
\UnaryInfC{A}
\end{prooftree}
¿Qué ocurriría si hubiera un isomorfismo $\neg \neg A \to A$ en una categoría bicartesianamente cerrada?
Primero observémos que $\neg \neg A$ es equivalente a $0^{0^A}$.

\begin{theorem}
Sea $\cat$ una categoría cartesianamente cerrada con objeto inicial $0$.
Si para todo objeto $A$ se tiene $0^{0^A} \cong A$, entonces $\cat$ es fina, es decir, tiene como mucho un morfismo entre dos objetos.
\end{theorem}
\begin{proof}
Por definición, para objetos $B$ y $C$:
\[ \cat(B, 0^C) \cong \cat(B \times C, 0) \]
Como hay como mucho un morfismo en $\cat(B \times C, 0)$, entonces hay como mucho un morfismo $B \to 0^C$.
Tomando $C = 0^A$, se tiene que hay como mucho un morfismo $B \to 0^{0^A} \cong A$.
\end{proof}

Por lo tanto, cuando añadimos la regla de eliminación de doble negación perdemos la capacidad de distinguir entre distintas pruebas en nuestra categoría.
Esto vuelve poco interesante estudiar categorías de este tipo. 

Por otro lado, la \newterm{correspondencia de Curry-Howard} establece una equivalencia entre el cálculo intuicionista y el $\lambda$-cálculo con tipos simples.
Las fórmulas se corresponden con tipos y una fórmula es cierta (en un sentido intuicionista) si está habitada, es decir, si existe algún término con dicho tipo.
Esto resulta importante para nosotros, pues Haskell implementa $\lambda$-cálculo con tipos simples.
Por lo tanto, podemos hacer deducciones en cálculo intuicionista con Haskell.

De hecho, tenemos la siguiente tabla de equivalencias:
\begin{center}
\begin{tabular}{ c | c | c }
  Lógica & Categoría & Haskell\\
  \hline
  $\bot$ & 0 & \code{Empty} \\
  $\top$ & 1 & \code{()} \\
  $\neg$ & $0^{-}$ & \code{a -> Empty} \\
  $p \land q$ & $A \times B$ & \code{(a, b)} \\
  $p \lor q$ & $A + B$ & Either a b \\
\end{tabular}
\end{center}

Con esto en mente, podemos hacer algunas demostraciones sencillamente escribiendo una función que habite el tipo correspondiente.
\begin{minted}{haskell}
modus_ponens :: a -> (a -> b) -> b
modus_ponens x f = f x

prueba_por_negacion :: (a -> Empty) -> Not a
prueba_por_negacion f = f

de_morgan :: Either (Not a) (Not b) -> Not (a, b)
de_morgan (Left f) = \(x, y) -> f x
de_morgan (Right f) = \(x, y) -> f y

otro_ejemplo :: (a -> (b -> c)) -> (a -> b) -> (a -> c)
otro_ejemplo f g = \x -> f x (g x)
\end{minted}

\section{Referencias}
\begin{itemize}
  \item Awodey, S. (2006). \emph{Category Theory}, Capítulo 6.
  \item Lambek, J. (1986). \emph{Introduction to Higher Order Categorical Logic}, Parte I.
  \item Low, Z.L. (2011). \emph{Bicartesian closed categories and logic}.
\end{itemize}