typearithmeticyl.tex

% !TeX TXS-program:compile = txs:///pdflatex/[--shell-escape]
\documentclass[tikz]{beamer}


\usepackage{minted}
\usepackage[parfill]{parskip}    		
\usepackage{graphicx}				
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{bm}
\usepackage{tikz-cd}
\usepackage{enumerate}
\usepackage{xfrac}
\usepackage{hyperref}
\usepackage{graphicx} \graphicspath{ {./} }
\usepackage{xcolor}
\usepackage{bbold}


\newcommand{\cat}[1]{\bm{ \mathsf{#1} }}
\newcommand{\functor}[3]{#1 : \cat{#2} \to \cat{#3}}
\newcommand{\functordef}{\functor{F}{C}{D}}
\newcommand{\cc}{\cat{C}}
\newcommand{\dd}{\cat{D}}
\newcommand{\ee}{\cat{E}}
\newcommand{\subcat}[2]{\bm{ \mathsf{#1}}_{\bm{ \mathsf{#2}}}}
\newcommand{\op}[1]{#1^{\text{op}}}
\newcommand{\opc}{\op{\cc}}
\newcommand{\opd}{\op{\dd}}
\newcommand{\ope}{\op{\ee}}
\newcommand{\mono}{\rightarrowtail}
\newcommand{\epi}{\twoheadrightarrow}
\newcommand{\zero}{\bm{\mathbb{0}}}
\newcommand{\one}{\bm{\mathbb{1}}}
\newcommand{\two}{\bm{\mathbb{2}}}
\newcommand{\three}{\bm{\mathbb{3}}}
\newcommand{\bg}{\cat{BG}}
\newcommand{\bgg}{\cat{BG'}}
\newcommand{\nt}{\Rightarrow}
\newcommand{\ant}[2]{\alpha : F \nt G} 
\newcommand{\bnt}[2]{\beta : F \nt G} 
\newcommand{\anti}[2]{\alpha : F \cong G} 
\newcommand{\bnti}[2]{\beta : F \cong G} 
\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\mred}[1]{\textcolor{red}{$#1$}}
\newcommand{\blue}[1]{\textcolor{blue}{#1}}
\newcommand{\mblue}[1]{\textcolor{blue}{$#1$}}


\setbeamertemplate{navigation symbols}{\insertframenumber{}}
\colorlet{shadecolor}{gray!15}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\newcommand{\propnumber}{} % initialize
\newtheorem*{prop}{Proposition \propnumber}
\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]

\AtBeginSection[]{
  \begin{frame}
  \vfill
  \centering
  \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title}
    \usebeamerfont{title}\insertsectionhead\par%
  \end{beamercolorbox}
  \vfill
  \end{frame}
}


\title{Type Arithmetic and the Yoneda Perspective}
\author{Emily Pillmore}

\begin{document}

\frame{\titlepage}

\section[Outline]{}
\frame{\tableofcontents[hideallsubsections]}

\section{Introduction}
\subsection{Who am I?}

\frame
{
	My name is Emily Pillmore.
	
	I am a hopeful mathematician, and a moonlight programmer.
}

\frame
{
	\begin{itemize}
		\item Twitter (\href{https://twitter.com/emi1ypi}{@emi1ypi})
		\item Meetups in NYC: NY Homotopy Type Theory, NY Category Theory, and the NY Haskell User Group. 
		\item Discord: Haskell $\cap$ Dank Memes: \href{https://discord.gg/2x2fYSK}{https://discord.gg/2x2fYSK}. 
		\item Personal: All of my slides and meetup content are hosted at \href{https://github.com/cohomolo-gy}{cohomolo.gy}.
	\end{itemize}
	
	
	If you ever want to talk category theory or programming, I'm around to talk, help, or mentor (within reason).
}

\frame
{
	I got my start in Scala, with Runar's \textit{Functional Programming in Scala} (the \textcolor{red}{red one} - there is now a \textcolor{blue}{blue one})
	
}

\frame
{
	\begin{center}
		\includegraphics[scale=0.7]{screed}
	\end{center}
}

\frame
{ 
	I now work at a company called \textbf{Kadena}, designing a language and a couple of cool blockchains
	\begin{center}
		\includegraphics[scale=0.3]{kadena}
	\end{center}
	
}

\subsection{Why are we here?}

\frame
{ 
	Today, we're going to learn to \textbf{count}. Then we will learn to \textbf{add}, \textbf{multiple}, and even \textbf{take powers}. 
}

\frame
{ 
	...and we will do this with the language of Type Theory, Category Theory, and Constructive Logic. Hopefully you will be converted to Computational Trinitarianism by the time we're done.
}

\frame
{ 
	Many of you know these topics already without knowing the details. Much of it is folklore within the community. But there are new ways of thinking about it that I guarantee you haven't seen before, and some of it even translates into our work on Profunctor Optics! 
}

\subsection{What and How?}

\frame
{ 
	First, we'll start off with some exercises to illustrate the point, proving free theorems and basic facts about types (e.g. reasoning through why \red{$\forall a. a \to a$} has precisely 1 inhabitant), and then draw direct lines with the Lambek correspondence. 
}

\frame
{ 
	Second, we will try to understand the Leibniz perspective and how it informs the Curry-Howard correspondence. 
}

\frame
{ 
	Third, we will begin to build the requisite knowledge for understanding the Yoneda perspective, and build some categorical constructs, and an understanding of representation. 
}

\frame
{ 
	Then, we will tie it all together. 
}

\frame
{ 
	Special thanks to Jon Pretty (\href{https://twitter.com/propensive}{@propensive})
}

\section{Some Type Arithmetic}

\subsection{Ground Rules}


\frame
{ 
	We will use the following conventions: 
	
	\begin{itemize}
		\item the type \red{()} with precisely 1 inhabitant (called \blue{Unit}) will be denoted by the numeral  \mred{\one}. 
		\item the type with no inhabitants, \blue{Nothing} or \red{Void} will be denoted \mred{\zero}. 
		\item Function types will be denoted by \red{$a \to b$} or by the notation \red{$b^a$}. 
		\item Universal quantification is given by \red{forall} or \red{$\forall$}.
		\item The notation $|\cdot| : \cat{Type} \to \mathbb{N}$ will denote the function taking a type to its number of type inhabitants
		\item The notation $[\cdot] : \mathbb{N} \to \cat{Type} $ will denote the function taking a natural number $n$ and constructing a type with precisely $n$ inhabitants. 
	\end{itemize}
}

\frame
{
	\begin{itemize}
		\item Our calculus assumes that we have all finite coproducts and will denote them by the plus sign \red{+}. In Scala and Haskell, the binary coproduct is \red{Either}.
		\item Our calculus assumes that we have all finite products, and we will denote they by the times sign \red{*}. In Scala and Haskell, the binary product is \red{(,)} or (\red{(,)} is an alias for \blue{Tuple2} in Scala.
	\end{itemize}
}


\frame
{
	We also assume our types are sufficiently set-like as to be usefully enumerable. 
}

\frame
{
	
	\begin{definition}[Isomorphism]
	
		An \textit{isomorphism} is a pair of functions \mred{to : a \to b} and \mblue{from : b \to a} such that $\red{to} \cdot \blue{from} = \blue{from} \cdot \red{to} = \cat{id}$. 
		
		The existence of an isomorphism between types will be denoted $\red{a}  \sim \blue{b}$. 
		
	\end{definition}
}


\frame
{
	There might be some confusion regarding what exactly we mean by “inhabitants”, e.g. are $1 + 1$ and $2$ different inhabitants of type $\cat{Int}$? For now we will treat two expressions of type \mred{a} to be separate inhabitants of \mred{a} if and only if there is some predicate $f : \red{a} \to \cat{Bool}$ that distinguishes between then. 
}

\frame
{ 
	Proposition: Suppose we were to treat a polymorphic type like your standard high school arithmetic. What would this arithmetic look like? 
}

\subsection{Addition}

\frame
{ 
	Does \mred{1 + 1 = 2}? How can we tell? 
}

\begin{frame}[fragile]
	By simple counting. Axiomatically, \mred{\one} is the type with 1 inhabitant, so
	\begin{minted}[escapeinside=||,mathescape]{haskell}
	
	|\mred{\one}| +  |\mred{\one}|
	~ () + ()
	~ Either () ()
	-- [|Either () ()|]
	~  |\mred{\two}|
	\end{minted}
	
\end{frame}

\frame
{ 
	By inspection, we see that $\cat{Either}$ has precisely two cases - \blue{Left} and \red{Right} containing a single type. Thus, two cases, with one inhabitant in each case. Therefore we have 2 inhabitants! Note also that this is isomorphic to $\cat{Bool}$, since $\cat{Bool}$ has precisely 2 inhabitants. 
}

\frame
{
	Instead of referencing these types by their names, we'll just represent them as numerals $\one, \two, \three, \ldots$. 
}

\frame
{ 
	How about \mred{\cat{Maybe}} containing values of type \mblue{\two}? 
}

\begin{frame}[fragile]

Again, we can apply some natural deduction, nothing that  \mblue{\two} has precisely two inhabitants
	\begin{minted}[escapeinside=||,mathescape]{haskell}
	
	Maybe | \mblue{\two}|
	~ Nothing + Just | \mblue{\two}|
	~ |\mblue{\one}| + | \mblue{\two}|
	~ |\mblue{\three}| 
	\end{minted}
\end{frame}

\frame
{
	Thus, the number of inhabitants of \mred{\cat{Maybe}} can be deduced to be $[1 + |\red{a}|]$
}

\subsection{Multiplication}

\frame
{

	Multiplication operates in the similar way. Using products, we can count \mred{\cat{Bool} * \cat{Bool}}. We have precisely four cases: 
	
	\begin{itemize}	
		\item (\blue{True}, \blue{True})
		\item(\blue{True}, \red{False})
		\item (\red{False}, \blue{True})
		\item (\red{False}, \red{False}) 
	\end{itemize}
}

\frame
{
	This works out as well! How about exponents?
}

\subsection{Exponentiation}

\begin{frame}[fragile]
	Let's consider a function \mred{\cat{Bool} \to \cat{Bool}}. How do we count the number of functions we have? Well, we can list them out: 
	
	\begin{minted}{haskell}
		k1 :: Bool -> Bool
		k1 b 
		  | True = True
		  | False = False 
		
		k2 :: Bool -> Bool 
		k2 b 
		  | True = True
		  | False = True 
		  		
		-- and so on	
	\end{minted}
	
\end{frame}

\begin{frame}[fragile]

	tl;dr there are exactly 4 inabitants. Now, consider the functions
	
	\begin{minted}{haskell}
		f :: Maybe Bool -> Bool
		f ...
	\end{minted}
\end{frame}

\frame
{
	Upon inspection you might find that there are precisely 8 such functions. Inductively, we see that there are \mred{|b|^{|a|}}-many inhabitants of the type \mred{a \to b}. The cardinality of this type behaves like exponentiation in $\mathbb{N}$!
}

\frame
{

As we will see later, \mred{a \to b} is a little bit different from coproducts and products in the way it interacts with \red{forall a} when we have (parametric) type polymorphism. The above formula can be used only if \red{a} and \red{b} are free from any universally quantified variables.

}
\subsection{$\top$ and $\bot$}

\frame
{
	Considering all we have just discussed, there are caveats to this calculus. For example, how many inhabitants are there in the type \mred{\zero \to \one}? How about \mred{\one \to \zero}? \mred{\zero \to \zero}?
}

\subsection{A correspondence Pt. 1}
\frame
{
	The analogy so far: 
	
	\begin{center}
		\begin{tabular}{|c|c|c|c|}
			\hline
			Types & \# of Inhabitants  & Sets & Categories \\
			\hline a       & $|A|$ & ?  & ? \\
			(a, b) &  $|A| \times |B| $ & ? & ? \\
			Either a b & $|A| + |B|$ & ? & ? \\
			$a \to b$ & $|B|^{|A|}$ & ? & ? \\
			() & 1 & ? & ? \\
			Void & 0 & ? & ? \\ \hline
		\end{tabular}
	\end{center}

}

\frame
{ 
	\textbf{Claim}: we can fill in the rest of the table with direct analogies from Set theory and Category theory. 
}


\begin{frame}[fragile]
	What does this look like?
	
	\begin{center}
	\begin{minted}[escapeinside=||,mathescape]{haskell}
	
	leftUnitP  :: (|$\one$| |$\times$| a) = a
	commuteP   :: (a |$\times$| b) = (b |$\times$| a)
	associateP :: ((a |$\times$| b) |$\times$| c) = (a |$\times$| (b |$\times$| c))
	leftUnitC  :: (|$\zero$| + a) = a
	commuteC   :: (a + b) = (b + a)
	associateC :: ((a + b) + c) = (a + (b + c))
	currying   :: |$c^{a \times b}$| = |$(c^b)^a$|
	leftUnitF  :: |$a^{\one}$| = a
	rightUnitF :: |$\one^a$| = |$\one$|
	\end{minted}
	
	\end{center}
\end{frame}

\frame
{ 
	Why do we care in the first place? 
}

\frame
{ 
	Because proving that a type \mblue{T} has inhabitants is equivalent to proving the theorem corresponding with \mblue{T} due to the Curry-Howard-Lambek correspondence.
}



\section{The Leibniz Perspective}

\subsection{When are things equal?}
\frame
{
	When are two things equal? You may have noticed our use of $=$ in the previous slides, but that was a convenient lie.
}

\frame
{
	Are these things equal? 
	
	\begin{itemize}
		\item \blue{1729}
		\item \mblue{12^3 + 1^3}
		\item "The first number expressible by the sum of two cubes in two different ways"
	\end{itemize}
}

\frame
{
	When viewed as expressions, \blue{1729} and \mblue{12^3 + 1^3} are different.
}

\frame
{
	When viewed as integers, they are the same. 
}

\subsection{Isomorphisms}
\frame
{
	Enumeration in this sense is an association of a representative of an equivalence class of \textbf{isomorphisms} of a type with a finite set. 
}


\begin{frame}[fragile]

	\begin{minted}{haskell}
	data Iso a b = Iso 
	    { to   :: a -> b
	    , from :: b -> a
	    }
	    -- fromTo :: (x :: a) -> (from . to) x = x
	    -- toFrom :: (x :: b) -> (to . from) x = x
	\end{minted}
\end{frame}

\frame
{
	We have been suffering from an abuse of notation - what we've really been saying is that two things are equal if we can exhibit an isomorphism between the two.
}

\frame
{ 
	\begin{prop}[Equality Preservation]
		if \red{A} and \blue{B} are isomorphic, and \mred{a_1, a_2 : A}, and \mblue{b_1, b_2 : B}, then \mred{a_1 = a_2} $\Leftrightarrow$ \mblue{b_1 = b_2}.
	\end{prop}
}

\subsection{Identity of Indiscernibles}
\frame
{

	\begin{prop}[Gottfried Wilhelm Leibniz, 1646-1716]
		"For any x and y, if x is identical to y, then x and y have all the same properties. For any x and y, if x and y have all the same properties, then x is identical to y."
	\end{prop}
	
}

\frame
{

	In symbols, $\blue{x} = \red{y} \Leftrightarrow \forall P. P \blue{x} = P \red{y}$ where $P$ is quantified over all properties of \blue{x}.
		
}

\subsection{Putting it to work}
\begin{frame}[fragile]
Let's see some interesting isomorphisms.

\begin{minted}{haskell}
leftUnitP :: Iso ((), a) a
leftUnitP = Iso (\((), a) -> a)
                (\a -> ((), a))
commuteP :: Iso (a, b) (b, a)
commuteP = Iso (\(a, b) -> (b, a))
               (\(b, a) -> (a, b))
associateP :: Iso ((a, b), c) (a, (b, c))
associateP = Iso (\((a, b), c) -> (a, (b, c)))
                 (\(a, (b, c)) -> ((a, b), c))
\end{minted}
\end{frame}
\begin{frame}[fragile]
What does this remind you of?
\begin{minted}{haskell}
rightUnitP  :: Iso (a, ()) a
leftUnitP   :: Iso ((), a) a
associateP  :: Iso ((a, b), c) (a, (b, c))
\end{minted}
\end{frame}
\begin{frame}[fragile]
\begin{minted}{haskell}
leftUnitC :: Iso (Either Void a) a
leftUnitC = ...
commuteC :: Iso (Either a b) (Either b a)
commuteC = ...
associateC :: Iso (Either (Either a b) c)
                  (Either a (Either b c))
associateC =
  Iso (\case Left (Left a)  -> Left a;
             Left (Right b) -> Right (Left b);
             Right c        -> Right (Right c))
      (\case Left a          -> Left (Left a);
             Right (Left b)  -> Left (Right b);
             Right (Right c) -> Right c)
\end{minted}
\end{frame}

\frame
{ 
	So what do our arithmetic rules \textit{really} say about our types?
}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
leftUnitP  :: (|$\one$| |$\times$| a) |$\cong$| a
commuteP   :: (a |$\times$| b) |$\cong$| (b |$\times$| a)
associateP :: ((a |$\times$| b) |$\times$| c) |$\cong$| (a |$\times$| (b |$\times$| c))
leftUnitC  :: (|$\zero$| + a) |$\cong$| a
commuteC   :: (a + b) |$\cong$| (b + a)
associateC :: ((a + b) + c) |$\cong$| (a + (b + c))
currying   :: |$c^{a \times b}$| |$\cong$| |$(c^b)^a$|
leftUnitF  :: |$a^{\one}$| |$\cong$| a
rightUnitF :: |$\one^a$| |$\cong$| |$\one$|
\end{minted}
\end{frame}

\subsection{The million dollar question}

\frame
{ 
	By inspection, we can show that there is a correspondence between sets and types by looking at their cardinalities and inhabitants respectively. 
}

\frame
{
	What are the sets with cardinality $\red{a} \times \blue{b}$, $\red{a} + \blue{b}$, $1$, $0$, and $\blue{b}^{\red{a}}$-many inhabitants? 
}

\frame
{
	We continue to build the picture.
}

\begin{frame}
There is a correspondence between types, sets, natural numbers.
\begin{center}
\begin{tabular}{|c|c|c|c|}
\hline
Types & Sets & \# of Inhabitants & Categories \\
\hline
a       & $A$ & $|A|$  & ? \\
(a, b) & $A \times B$ & $|A| \times |B|$ & ? \\
Either a b & $A \sqcup B$ & $|A| + |B|$ & ? \\
$a \to b$ &  set functions & $|B|^{|A|}$ & ? \\
() & $\{*\}$ & 1 & ? \\
Void & $\emptyset$ & 0 & ? \\ \hline
\end{tabular}
\end{center}
\end{frame}

\section{Some Category Theory}


\subsection{The Basics}

\frame
{
	\textbf{Claim}: the same correspondence can be made within the language of a bicartesian-closed category. 
}

\frame
{
	Lets elaborate on what that means. But first, some definitions.
}

\frame
{
	\begin{definition}[Category]
		A \textbf{category} $\cc$ consists of the following data: 
		
		\begin{itemize}
			\item a collection of \textbf{objects} \mred{x, y, z,...}
			\item a collection of \textbf{morphisms} \mred{f,g,h,...}
		\end{itemize}
		
		Such that 
		
		\begin{itemize}
			\item each morphism has specified \textbf{domain} and \textbf{codomain} objects so that the notation \mred{f : x \to y} signifies a morphism with domain \mred{x} and codomain \mred{y}. 
			\item each object has an associated \textbf{identity} morphism \mblue{1_x : x \to x} which acts as a two-sided unital element for composition.
			\item to each pair of morphisms \mred{f : x \to y}, \mblue{g : y \to z}, there exists a \textbf{composite} arrow $h : \red{x} \to \blue{z}$ where $h :\equiv \blue{g}\red{f}$. 
		\end{itemize}
	\end{definition}
}

\frame
{
	For every category we may speak of its dual notion, $\opc$, the \textbf{opposite} category of $\cc$, consisting of the same object data, but with the domain and codomain of each morphism reversed.
}

\frame
{
	This data is subject to some axioms. 
	
	\begin{itemize}
	
		\item For any $f : \blue{x} \to \red{y}$, $f1_{\blue{x}} = f =  1_{\red{y}} f$. 
		\item For any composable triple $f,g,h$, $h(gf) = (hg)f$, and will simply be denoted $hgf$.
		\item Between any two objects $\blue{x}, \red{y}$ in a category $\cc$, there exists an object $\cc(\red{x},\red{y})$ consisting of all morphisms with domain $\blue{x}$ and codomain $\red{y}$. This is usually called $Hom_{\cc}(\blue{x}, \red{y})$.
	\end{itemize}
}


\frame
{

	Indeed, we are familiar with morphisms, identities, and composition already. In haskell, these translate into types \mred{a \to b}, the identity function \mred{id}, and composition \mred{(.)}. 
	
	In scala, these are roughly the same, modulo naming conventions - \mblue{A \Rightarrow B}, \mblue{identity}, \mblue{compose}.  
}

\frame
{ 
	Isomorphisms in this context become a pair of morphisms \mred{ f : c \to d} and \mblue{g : d \to c} such that $\blue{g}\red{f} = 1_c$ and $\red{f}\blue{g} = 1_d$.
	
	 If \mred{x} and \mblue{y} are isomorphic, we will denote this by $\red{x} \cong \blue{y}$.
}

\frame
{
	We can also speak of the "size" of a category in a precise sense
}

\frame
{
	\begin{definition}[Size matters]
		A category $\cc$ is said to be...
		\begin{itemize}
			\item \textbf{small} if there are at most a set's worth of morphisms and objects in the category
			\item \textbf{locally small} if for all $\blue{c}, \red{d}$, $\cc(\blue{c}, \red{d})$ is a set
			\item \textbf{large} if it is not small
		\end{itemize}
	\end{definition}
}

\frame
{
	For our purposes, everything will be small (set-sized)
}

\frame
{
	
	\begin{definition}[Functor]
		A functor $F : \cc \to \dd$ between categories consists of the following data: 
		
		\begin{itemize}
			\item an object $F\blue{c}$ in $\dd$ for every object \mblue{c} of $\cc$
			\item a morphism $Ff : F\blue{c} \to F\red{d}$ in $\dd$ for each morphism $f : \blue{c} \to \red{d}$ of $\cc$.
		\end{itemize}
		
		Additionally, we require that $Fg \cdot Ff = F(gf)$ when $g$ and $f$ are a composable pair, and that for every object \mblue{c} in $\cc$, $F1_{\blue{c}} = 1_{F\blue{c}}$.
	\end{definition}
}

\begin{frame}[fragile]

In Haskell, we represent this data as a typeclass

	\begin{minted}{haskell}
	
	class Functor f where
	  fmap :: (a -> b) -> f a -> f b
	  -- fmap id fa = fa 
	  -- fmap g . fmap f = fmap (g . f)
	\end{minted}
	
\end{frame}

\frame
{
	Functors that act uniformly on arrows are called \textbf{covariant}. However, if a functor is mapping to or from an opposite category to a normal category, then one calls these functors \textbf{contravariant}.
	
	 Operationally, this can be seen as "flipping the direction of arrows" in the target category. 
}

\frame
{
	Saying "$F$ is a contravariant functor from $\cc$ to $\dd$" is saying that one has a covariant functor $F : \opc \to \dd$. When it matters, I'll just tell you which one that is.

}

\frame
{
	Example: what do we mean by cardinality?
}

\frame
{
	Recall that I mentioned this was an association of an isomorphism class of types with a finite set. 
}

\frame
{
	Enumeration defines a cardinality functor $|\cdot|: \cat{Fin_{Iso}} \to \cat{Set}$.  
}

\frame
{
	As an important example, for any object \mblue{c} of $\cc$, we have the \textbf{covariant represented functor of \blue{c}}, $\cc(\blue{c}, -)$, which is a functor $\cc \to \cat{Set}$.
	
}

\frame
{

 LIkewise, we have the \textbf{contravariant functor represented by \red{c}}: $\cc(-, \red{c}) : \opc \to \cat{Set}$.

}

\frame
{
	We know these well! They're our old friends \textbf{Reader} and \textbf{Coreader}.
}

\begin{frame}[fragile]

	\begin{minted}{haskell}
	newtype Reader t a = Reader (t -> a)
	instance Functor (Reader t) where
	  -- fmap :: (a -> b) -> Reader t a -> Reader t b
	  fmap f (Reader t) = Reader (f . t)
	  
	newtype Coreader t a = Coreader (a -> t)
	instance Contravariant (Coreader t) where
	  contramap f (Coreader k) = Coreader (k . f)
	\end{minted}
\end{frame}

\frame
{
	To each functor $F : \cc \to \dd$ is associated data - a family of maps from each object $c$ of $\cc$ to objects $Fc$ of $\dd$ and likewise between morphisms. But this begs the question - how can we translate the data of one functor into the data of another?  
}

\frame
{
	For one, this entails we have two functors $F, G : \cc \to \dd$ with the same domain and codomain. Second, we need additional data such that to each $c$ of $\cc$ and $Fc$ of $\dd$, we can translate $Fc$ to $Gc$ in a natural way. 
}


\begin{frame}[fragile]

	\begin{definition}[Natural Transformation]
		Let $F,G : \cc \to \dd$ be functors. A \textbf{natural transformation} $\alpha$ consists of the following data: to each $c$ of $\cc$, a \textbf{component} map $\alpha_c : Fc \Rightarrow Gc$ such that the following square commutes for any $f : c \to d$ of $\cc$: 
		
		\begin{center}
			\begin{tikzcd}
			Fc \ar[r, "\alpha_c"] \ar[d, "Ff", swap] & Gc \ar[d, "Gf"]
			\\ Fd \ar[r, "\alpha_d", swap] & Gd
			\end{tikzcd}
		\end{center}
	\end{definition}
\end{frame}

\frame
{
	I.e., $\alpha_d \cdot Ff = Gf \cdot \alpha_c$.
}

\begin{frame}[fragile]

	In haskell, this is rather simple to implement: 
	
	\begin{minted}{haskell}
	type f ~> g = forall a. f a -> g a
	-- given f : a -> b, natural transf. t,
	-- t . fmap f = fmap f . t 
	\end{minted}
\end{frame}

\frame
{
	A \textbf{natural isomorphism} is a natural transformation where each component map is an isomorphism. We will denote this $\alpha : F \cong G$. 
	
}

\frame
{
	One form of category that we will look at later is that of a \textbf{functor category}, denoted $[\cc, \dd]$, whose objects are functors $\cc \to \dd$, and whose morphisms are natural transformations between these functors. 
}

\subsection{Initial and Terminal Objects}

\frame
{
	"Special" objects are determined by how morphisms to or from them act in relation to other objects. 
}

\frame
{
	\begin{definition}[Terminal and Initial objects]
		An object $c$ of $\cc$ is called \textbf{terminal} if there is exactly 1 unique morphism from any other object in $\cc$ to $c$. 
		
		Dually,  an object $c$ of $\cc$ is \textbf{initial} if there is exactly 1 unique morphism to any other object in $\cc$. 
	\end{definition}
}

\frame
{
	We have seen two such objects that act like terminal and initial objects already: \mred{()} and \mblue{Void}
}

\frame
{
	Indeed for every type $a$, the types \mred{a \to ()} and \mblue{Void \to a} has precisely one inhabitant . 
}

\begin{frame}[fragile]

Namely, we have the following functions: 

	\begin{minted}[escapeinside=||,mathescape]{haskell}
	-- a -> ()
	k :: a -> ()
	k = const ()
	
	-- |$\bot$| -> a
	t :: Void -> a
	t = absurd
	\end{minted}
\end{frame}

\subsection{Products and Coproducts}

\frame
{

	In the same way that we have terminal and initial objects, constructions for products and coproducts in category theory follow suit.
}

\frame
{
	\begin{definition}[Product]
	
		A \textbf{product} in a category $\cc$ is an object $P$ together with morphisms $p_c : P \to c$ and $p_d : P \to d$ for $c,d$ in $\cc$ such that for any other object $N$ with morphisms $f_c : N \to c$ and $f_d : N \to d$, then each $f_{(-)}$ can be factored through a unique function $f : N \to P$ such that $f_c = p_cf$ and $f_d = p_df$. 
	\end{definition}
}

\begin{frame}[fragile]
	This is diagram gives this data succinctly: 
	
	\begin{center}
	\begin{tikzcd}
	& & c
	\\ N \ar[r, "f" description, dotted] \ar[urr, "f_c", bend left] \ar[drr, "f_d", bend right, swap] & P \ar[ur, "p_c"] \ar[dr, "p_d", swap]
	\\ & & d
	\end{tikzcd}
	\end{center}
\end{frame}

\begin{frame}[fragile]
	We are all familar with these: in Haskell and Scala, we have the type \mred{(a, b)}. Its defined by having two operators: 
	
	\begin{minted}{haskell}
	fst :: (a,b) -> a
	fst (a,_) = a
	
	snd :: (a,b) -> b
	snd (_,b) = b
	\end{minted}
\end{frame}

\frame
{ 
	\begin{definition}[Coproduct]
	
		A \textbf{coproduct} in a category $\cc$ is an object $P$ together with morphisms $i_c : c \to C $ and $i_d : C \to d$ for $c,d$ in $\cc$ such that for any other object $N$ with morphisms $f_c : c \to N$ and $f_d : d \to N$, then each $f_{(-)}$ can be factored through a unique function $f : C \to N$ such that $f_c = fi_c$ and $f_d = fi_d$. 
	\end{definition}
	
}

\begin{frame}[fragile]
	This is diagram gives this data succinctly: 
	
	\begin{center}
	\begin{tikzcd}
	c \ar[dr, "i_c", swap] \ar[drr, "f_c", bend left]
	\\ & C \ar[r, "f" description, dotted] & N
	\\ d \ar[ur, "i_d"] \ar[urr, "f_d", bend right, swap]
	\end{tikzcd}
	\end{center}
\end{frame}

\begin{frame}[fragile]
	We are all familar with these: in Haskell and Scala, we have the type \blue{Either} \blue{a} \blue{b}. Its defined by having two operators: 
	
	\begin{minted}{haskell}
	inl :: a -> Either a b
	inl = Left
	
	inr :: b -> Either a b
	inr = Right
	\end{minted}
\end{frame}

\subsection{Universal Properties}
\frame
{
	The diagrams for products and coproducts define their \textbf{universal properties}. In an imprecise sense, this means that these constructions are initial themselves in the appropriate category. 
}

\frame
{
	Let's now consider morphisms to and from products and coproducts, beginning with products first. 
}

\frame
{
	Consider $f \in \cc(\red{a \times b}, \blue{c})$. What data is necessary to produce \mblue{c}? 
}

\frame
{
	$f$ specifies an element $f \red{(a,b)}$ of $\cc$. Therefore, we require that $f$ have the additional data that when partially applied to \mred{b}, $f \red{(-,b)}$ specifies a function $\phi : \red{a} \to \blue{c}$. 
}

\frame
{
	Thus, to specify a function $\cc(\red{a \times b}, \blue{c})$ is to specify an equivalent function $\cc(\red{b}, \blue{c}^{\red{a}})$ - hence, an isomorphism. 
}

\begin{frame}[fragile]

	We are familiar with this function! 
	
	\begin{minted}{haskell}
	curry :: ((a,b) -> c) -> a -> b -> c
	curry k a b = k (a,b)
	
	uncurry :: (a -> b -> c) -> (a,b) -> c
	uncurry k (a,b) = k a b  
	\end{minted}
\end{frame}

\frame
{
	The same deduction can be applied to coproducts. What data can we glean from $f \in \cc(\blue{a + b}, \red{c})$? 
}

\frame
{
	When \mblue{a + b} is introduced, we have either the left or the right hand side.
	
	Therefore, the data equivalent to $f$ consists of a pair of function $\blue{a} \to \red{c}$ and $\blue{b} \to \red{c}$ - one for each side. 
}

\frame
{
	In symbols, $\cc(\blue{a + b}, \red{c}) \cong \cc(\blue{a}, \red{c}) \times \cc(\blue{b}, \red{c})$
}

\begin{frame}[fragile]
	\begin{minted}{haskell}
	either 
	  :: Either a b -> (a -> c) -> (b -> c) -> c
	either (Left a) f _ = f a
	either (Right b) _ g = g b
	
	pair :: (a -> c, b -> c) -> Either a b -> c
	pair (f,g) (Left a) = f a
	pair (f,g) (Right b) = g b
	\end{minted}
\end{frame}

\frame
{
	Similarly, how would you deduce that $(\red{a \times b})^{\blue{c}} \cong \red{a}^{\blue{c}} \times \red{b}^{\blue{c}}$?
}

\section{The Yoneda Perspective}


\begin{frame}
	We've filled in the rest of our table! 	
	
	\begin{center}
		\begin{tabular}{|c|c|c|c|}
		\hline
		Types & Sets & \# of Inhabitants & Categories \\
		\hline
			a       & $A$ & $|A|$  & objects of $\cc$ \\
			(a, b) & $A \times B$ & $|A| \times |B|$ & $c \times d$ \\
			Either a b & $A \sqcup B$ & $|A| + |B|$ & $c + d$ \\
			$a \to b$ &  set functions & $|B|^{|A|}$ & morphisms in $\cc$ \\
			() & $\{*\}$ & 1 & terminal objects \\
			Void & $\emptyset$ & 0 & initial objects \\ \hline
		\end{tabular}
	\end{center}
\end{frame}

\frame
{
	Let's start from code and build some intuition, seeing if we can derive a category theoretic Leibniz perspective. 
}

\frame
{
	What would such a perspective look like? 
}

\frame
{
	To remind everyone, Leibniz' rule is $ \red{a} = \blue{b} \Leftrightarrow \forall P. P \red{a} = P \blue{b}$. 
}

\frame
{
	Propositions, as we have seen, correspond with morphisms to or from an object in a category. 
	
	Likewise, equality (in this context) is represented as an isomorphism. 
}

\frame
{
	\textbf{Candidate}: $\red{a} \cong \blue{b} \Leftrightarrow \forall x. \cc(\red{a}, x) \cong \cc(\blue{b}, x)$
}

\frame
{
	\begin{definition}[Yoneda Embedding (corollary)]
		\mred{a} is isomorphic to \mblue{b} if and only if $\cc(\red{a}, -)$ is naturally isomorphic to  $\cc(\blue{b}, -)$
	\end{definition}
	
}

\begin{frame}[fragile]

	\begin{proof}[Proof of $(\Leftarrow)$]
		Suppose $\cc(\red{a}, x) \cong \cc(\blue{b}, x)$ for all objects x. Taking x to be \red{a} and \blue{b} successively, then, we have bijections: 
		\[
		\begin{aligned}
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
  ]
				\cc(\red{a}, \red{a}) \ar[r, isomorphic] & \cc(\blue{b}, \red{a}) 
			\end{tikzcd}
			\qquad
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
  ]
				\cc(\red{a}, \blue{b}) \ar[r, isomorphic] & \cc(\blue{b}, \blue{b})
			\end{tikzcd}
		\end{aligned}
		\]
		
	\end{proof}
\end{frame}

\begin{frame}[fragile]

	\begin{proof}[Proof of $(\Leftarrow)$]
		Suppose $\cc(\red{a}, x) \cong \cc(\blue{b}, x)$ for all objects x. Taking x to be \red{a} and \blue{b} successively, then, we have bijections: 
		\[
		\begin{aligned}
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
  inhabits/.style = {ar symbol={\in}}
  ]
				\cc(\red{a}, \red{a}) \ar[r, isomorphic] & \cc(\blue{b}, \red{a}) 
				\\ 1_{\red{a}}  \ar[u, inhabits]
			\end{tikzcd}
			\qquad
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
    inhabits/.style = {ar symbol={\in}}
  ]
				\cc(\red{a}, \blue{b}) \ar[r, isomorphic] & \cc(\blue{b}, \blue{b})
				\\ & 1_{\blue{b}} \ar[u, inhabits]
			\end{tikzcd}
		\end{aligned}
		\]
		
	\end{proof}
\end{frame}

\begin{frame}[fragile]

	\begin{proof}[Proof of $(\Leftarrow)$]
		Suppose $\cc(\red{a}, x) \cong \cc(\blue{b}, x)$ for all objects x. Taking x to be \red{a} and \blue{b} successively, then, we use bijections: 
		\[
		\begin{aligned}
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
  inhabits/.style = {ar symbol={\in}}
  ]
				\cc(\red{a}, \red{a}) \ar[r, isomorphic] & \cc(\blue{b}, \red{a}) 
				\\ 1_{\red{a}}  \ar[u, inhabits] \ar[r] & \psi \ar[u, inhabits]
			\end{tikzcd}
			\qquad
			\begin{tikzcd}[
  ar symbol/.style = {draw=none,"\textstyle#1" description,sloped},
  isomorphic/.style = {ar symbol={\cong}},
    inhabits/.style = {ar symbol={\in}}
  ]
				\cc(\red{a}, \blue{b}) \ar[r, isomorphic] & \cc(\blue{b}, \blue{b})
				\\  \phi \ar[u, inhabits] & 1_{\blue{b}} \ar[u, inhabits]  \ar[l]
			\end{tikzcd}
		\end{aligned}
		\]
		
	To define functions $\phi$ and $\psi$. In fact, these functions are inverses!
	\end{proof}
\end{frame}


\frame
{
	\begin{proof}[Proof of $(\Rightarrow)$]
		Functors preserve isomorphisms (this is a simple check).
	\end{proof}
}

\subsection{Representable Functors}

\frame
{
	In previous slides we mentioned a functor "represented" by an object.
}


\frame
{
	Indeed, we have a notion of a functor which relates an object to perspectives of that object i.e. morphisms to or from the object to all others. 
}

\frame
{
	"Objects exist in relation to all other objects" 
}

\frame
{
	"Everything in category theory can be proven with a combination of the Yoneda Lemma and some facts about the category of Sets" 
}

\frame
{
	This is the Yoneda perspective. Two objects are isomorphic if and only if the functors represented by them are naturally isomorphic.	
}

\frame
{
	\begin{definition}[Representable Functor]
		A \textbf{representable} functor is a functor $F : \cc \to \cat{Set}$ along with the following data: 
		
		\begin{itemize}
			\item an object \mblue{c} that is said to \textbf{represent} $F$
			\item a natural isomorphism $\Phi : F \cong \cc(\blue{c}, -)$
		\end{itemize}
		
		This data together is called a \textbf{representation} of $F$. 
	\end{definition}
}

\begin{frame}[fragile]

	\begin{minted}{haskell}
	class Representable f c | f -> c where
	  tabulate :: f x -> (c -> x)
	  index :: (c -> x) -> f x
	\end{minted}
\end{frame}

\frame
{
	\begin{definition}[The Yoneda lemma]
		Let $F : \cc \to \cat{Set}$ be a functor where $\cc$ is a locally small category (every collection of morphisms $\cc(\blue{c}, \red{d})$ between any two objects forms a set). Then, $F\blue{c} \cong [\cc, \cat{Set}](\cc(\blue{c}, -), F)$. This bijection associates a natural transformation $\alpha : \cc(\blue{c}, -) \Rightarrow F$ with the element $\alpha_{\blue{c}}(1_{\blue{c}})$ in $F\blue{c}$. 
	\end{definition}
}

\frame
{
	Furthermore, this correspondence is natural in \blue{c} and in $F$.
}

\frame
{
\begin{definition}[Different Yoneda lemmas in Haskell]
\begin{tabular}{rc}

Covariant functor: & $(\forall x. (\blue{a} \to x) \to f~x) \cong f~\blue{a}$. \\
Contravariant functor:     & $(\forall x. (x \to \red{b}) \to f~x) \cong f~\red{b}$. 
\end{tabular}
\end{definition}
}

\frame
{
	\begin{definition}[Covariant Yoneda facts]
		\begin{itemize}
			\item Lemma: $[\cc, \cat{Set}](\cc(\blue{c}, -), F) \cong F\blue{c}$
			\item Embedding: $\blue{c} \cong \red{d} \Leftrightarrow \cc(\blue{c}, -) \cong \cc(\red{d}, -)$
			\item Code: $ (\forall x. (\blue{a} \to x) \to f~x) \cong f~\blue{a}$
		\end{itemize}
	\end{definition}
}

\frame
{
	\begin{definition}[Contravariant Yoneda facts]
		\begin{itemize}
			\item Lemma: $[\cc, \cat{Set}](\cc(-, \red{d}), F) \cong F\red{d}$
			\item Embedding: $\blue{c} \cong \red{d} \Leftrightarrow \cc(-, \blue{c}) \cong \cc(-, \red{d})$
			\item Code: $(\forall x. (x \to \red{b}) \to f~x) \cong f~\red{b}$. 
		\end{itemize}
	\end{definition}
}

\frame
{
	\begin{proof}[Proof of Distribution: $(\red{a} + \blue{b}) \times c \cong (\red{a} \times c) + (\blue{b} \times c)$]
		\[
		\begin{aligned}
			(\red{a} + \blue{b}) \times c &\cong \cc((\red{a} + \blue{b}) \times c, x) &(\text{yoneda embedding}) \\
			& \cong \cc(\red{a}  + \blue{b}, \cc(c, x)) &(curry) \\
			& \cong \cc(\red{a} , \cc(c, x)) \times \cc(\blue{b}, \cc(c, x)) &(pairing) \\
			& \cong \cc(\red{a}  \times c, x) + \cc(\blue{b} \times c, x)) &(uncurry) \\
			& \cong \cc(\red{a}  \times c) + (\blue{b} \times c) &(un-yoneda)
		\end{aligned}
		\]
	\end{proof}
}


\begin{frame}[fragile]
Expressed in Haskell these look like this:
\begin{minted}[escapeinside=||,mathescape]{haskell}
covariant :: Functor f =>
             Iso (forall x. (a -> x) -> f x) (f a)
covariant = Iso (\f -> f identity)
                (\fa -> \f -> fmap f fa)
contravariant :: Contravariant f =>
                 Iso (forall x. (x -> a) -> f x) (f a)
contravariant = Iso (\f -> f identity)
                    (\fa -> \f -> contramap f fa)
\end{minted}
\end{frame}

\begin{frame}[fragile]
	\begin{minted}{haskell}
	to :: (forall x. (a -> x) -> f x) -> f a
	to f = f id
	
	from :: f a -> (forall x. (a -> x) -> f x)
	from fa = \f -> fmap f fa
	\end{minted}
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
fromTo :: Functor f => (forall x. (a -> x) -> f x) ->
                       (forall x. (a -> x) -> f x)
fromTo = from . to
fromTo = (\fa -> \g -> fmap g fa) .
         (\f -> f id)
fromTo = \f -> \g -> fmap g (f id)
-- Using parametricity
fromTo = \f -> \g -> f (g . id)
-- Function composition
fromTo = \f -> \g -> f g
-- Eta reduction
fromTo = \f -> f
fromTo = id
\end{minted}
\end{frame}
\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
toFrom :: Functor f => f a -> f a
toFrom = to . from
toFrom = (\f -> f id) . (\fa -> \g -> fmap g fa)
toFrom = \fa -> (\g -> fmap g fa) id
toFrom = \fa -> fa
toFrom = id
\end{minted}
\end{frame}

\section{Bringing it all back home}


\frame
{
	How many inhabitants does \mred{\forall a. a \to a} have? 
}

\begin{frame}[fragile]

\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a. a -> a
  |$\cong$| |$\forall$| a. (|$\one$| -> a) -> a
  -- newtype Id a = a
  |$\cong$| |$\forall$| a. (|$\one$| -> a) -> Id a
  |$\cong$| Id |$\one$|
  |$\cong$| |$\one$|
\end{minted}
Since () has only one inhabitant, we conclude that $\forall a. a \to a$ has only one inhabitant as well.
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a x. (a, x) -> a
    -- uncurrying
    |$\cong$| |$\forall$| a x. x -> a -> a
    -- |$\one$|-> x $\cong$ x
    |$\cong$| |$\forall$| a x. (|$\one$| -> x) -> a -> a
    -- Yoneda with newtype F a x = a -> a
    |$\cong$| |$\forall$| a. F a |$\one$|
    |$\cong$| |$\forall$| a. a -> a
    -- reusing the proof above
    |$\cong$| |$\one$|
\end{minted}
\end{frame}


\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a. (a, a) -> a
    |$\cong$| |$\forall$| a. (|$\one$| -> a, |$\one$| -> a) -> a
    -- unpairing 
    |$\cong$| |$\forall$| a. (|$\two$| -> a) -> a
    -- Yoneda with newtype F x = x
    |$\cong$| |$\two$|
\end{minted}
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a b c. (a -> c) -> b -> a -> c
    -- newtype F a b x = b -> a -> x
    |$\cong$| |$\forall$| a b. F a b a
    |$\cong$| |$\forall$| a b. b -> a -> a
    -- reusing one of the above theorems
    |$\cong$| |$\one$|
\end{minted}
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a b c. (a -> b) -> (b -> c) -> (a -> c)
    -- reorder the arguments
    |$\cong$| |$\forall$| a b c. (b -> c) -> (a -> b) -> a -> c
    -- Yoneda with newtype F a b x = (a -> b) -> a -> x
    |$\cong$| |$\forall$| a b. F a b b
    |$\cong$| |$\forall$| a b. (a -> b) -> a -> b
    -- Yoneda with newtype G a x = a -> x
    |$\cong$| |$\forall$| a. G a a
    |$\cong$| |$\forall$| a. a -> a
    -- reusing the above theorems
    |$\cong$| |$\one$|
\end{minted}
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a. (a -> |$\zero$|, a -> |$\zero$|) -> (a -> |$\zero$|)
    |$\cong$| |$\forall$| a. a -> (a -> |$\zero$|, a -> |$\zero$|) -> |$\zero$|
    |$\cong$| |$\forall$| a. (|$\one$| -> a) -> (a -> |$\zero$|, a -> |$\zero$|) -> |$\zero$|
    |$\cong$| (|$\one$| -> |$\zero$|, |$\one$| -> |$\zero$|) -> |$\zero$|
    |$\cong$| (|$\zero$|, |$\zero$|) -> |$\zero$|
    |$\cong$| |$\zero$| -> |$\zero$|
    |$\cong$| |$\one$|
\end{minted}
\end{frame}

\frame
{
\begin{definition}[Yoneda (Propositional Equality)]
    $f~\red{a} \cong \forall~x. (\red{a} = x) \to f~x$ with no restrictions on $f$!
\end{definition}
}

\begin{frame}[fragile]

\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| f z. f z -> f z
    -- newtype F z x = (x = z)
    |$\cong$| |$\forall$| z f. (|$\one$| -> f z) -> f z
    |$\cong$| |$\forall$| z f. (|$\forall$| x. F z x -> f x) -> f z
    |$\cong$| |$\forall$| z. F z z
    |$\cong$| |$\forall$| z. z = z
    |$\cong$| |$\one$|
\end{minted}
\end{frame}

\frame
{
	What about types that have \mred{a} occurring in positive and negative focus like $\forall a. (a \to a) \to (a \to a)$?
}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a. (a -> a) -> a -> a
    -- (a -> a, a) |$\cong$| (|$\one$| + a) -> a
    |$\cong$| |$\forall$| a. ((|$\one$| + a) -> a) -> a
    -- define f x = |$\one$| + x
    |$\cong$| |$\forall$| a. (f a -> a) -> a
    |$\cong$| |$\mu$| x. f x
    |$\cong$| |$\mu$| x. |$\one$| + x
\end{minted}
\end{frame}

\frame
{
	And this can even be generalized to containers!
}

\begin{frame}[fragile]
Functors of the shape, $f x \cong \Sigma_i k_i \to x$, are called {\em containers}. Almost every type constructor with a functor instance is a container:
\begin{minted}[escapeinside=||,mathescape]{haskell}
Maybe x       |$\cong$| (|$\zero$| -> x) + (|$\one$| -> x)
(Bool, x)     |$\cong$| (|$\one$| -> x) + (|$\one$| -> x)
Const Bool x  |$\cong$| (|$\zero$| -> x) + (|$\zero$| -> x)
Either Bool x |$\cong$| (|$\zero$| -> x) + (|$\zero$| -> x) + (|$\one$| -> x)
[x] |$\cong$| (|$\zero$| -> x) + (|$\one$| -> x) + (|$\two$| -> x) + ... |$\cong$| |$\Sigma_i$| |$x^i$|
\end{minted}

The only exceptions I know of is $(x \to 0) \to 0$ and similar constructions.
\end{frame}

\begin{frame}[fragile]
Take a closer look at:
\begin{minted}[escapeinside=||,mathescape]{haskell}
[x] |$\cong$| (|$\zero$| -> x) + (|$\one$| -> x) + (|$\two$| -> x) + ... |$\cong$| |$\Sigma_i$| |$x^i$|
\end{minted}
What does this remind you of?
\end{frame}

\begin{frame}[fragile]
Consider some function $f$ that has the same signature as $map$ on lists:
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a b. (a -> b) -> [a] -> [b]
    -- Yoneda with f x = [a] -> [x]
    |$\cong$| |$\forall$| a. [a] -> [a]
    -- using the container formula
    |$\cong$| |$\forall$| a. (|$\Sigma_i$| |$a^i$|) -> [a]
    |$\cong$| |$\Pi_i$| [i]
    -- expressing it using dependent types and renaming i to n
    |$\cong$| (n : Nat) -> [Fin n]
\end{minted}
\end{frame}

\begin{frame}[fragile]
\begin{minted}[escapeinside=||,mathescape]{haskell}
|$\forall$| a b. (a -> b) -> [a] -> [b]
    |$\cong$| (n : Nat) -> [Fin n]
\end{minted}
\end{frame}


\frame
{
	For more exercises, see a joint talk I did with @alexknvl on Isomorphic reasoning, which is the 6 hour version of this talk (slides at cohomolo.gy). 
}

\end{document}