493 lines
11 KiB
TeX
493 lines
11 KiB
TeX
\documentclass[a4paper]{beamer}
|
||
%% \documentclass[a4paper,handout]{beamer}
|
||
%% \usecolortheme[named=seagull]{structure}
|
||
|
||
\input{packages.tex}
|
||
|
||
\input{macros.tex}
|
||
|
||
\title{Univalent Categories}
|
||
\subtitle{A formalization of category theory in Cubical Agda}
|
||
|
||
\newcommand{\myname}{Frederik Hangh{\o}j Iversen}
|
||
\author[\myname]{
|
||
\myname\\
|
||
\footnotesize Supervisors: Thierry Coquand, Andrea Vezzosi\\
|
||
Examiner: Andreas Abel
|
||
}
|
||
\institute{Chalmers University of Technology}
|
||
|
||
\begin{document}
|
||
|
||
\frame{\titlepage}
|
||
|
||
\begin{frame}
|
||
\frametitle{Introduction}
|
||
Category Theory: The study of abstract functions. Slogan: ``It's the
|
||
arrows that matter''\pause
|
||
|
||
Objects are equal ``up to isomorphism''. Univalence makes this notion
|
||
precise.\pause
|
||
|
||
Agda does not permit proofs of univalence. Cubical Agda admits
|
||
this.\pause
|
||
|
||
Goal: Construct a category whose terminal objects are (equivalent to)
|
||
products. Use this to conclude that products are propositions, not a
|
||
structure on a category.
|
||
\end{frame}
|
||
|
||
\begin{frame}
|
||
\frametitle{Outline}
|
||
The path type
|
||
|
||
Definition of a (pre-) category
|
||
|
||
1-categories
|
||
|
||
Univalent (proper) categories
|
||
|
||
The category of spans
|
||
\end{frame}
|
||
|
||
\section{Paths}
|
||
\begin{frame}
|
||
\frametitle{Paths}
|
||
\framesubtitle{Definition}
|
||
Heterogeneous paths
|
||
\begin{equation*}
|
||
\Path \tp (P \tp \I → \MCU) → P\ 0 → P\ 1 → \MCU
|
||
\end{equation*}
|
||
\pause
|
||
For $P \tp \I → \MCU$ and $a_0 \tp P\ 0$, $a_1 \tp P\ 1$
|
||
inhabitants of $\Path\ P\ a_0\ a_1$ are like functions
|
||
%
|
||
$$
|
||
p \tp ∏_{i \tp \I} P\ i
|
||
$$
|
||
%
|
||
Which satisfy $p\ 0 & = a_0$ and $p\ 1 & = a_1$
|
||
\pause
|
||
|
||
Homogenous paths
|
||
$$
|
||
a_0 ≡ a_1 ≜ \Path\ (\var{const}\ A)\ a_0\ a_1
|
||
$$
|
||
\end{frame}
|
||
|
||
\begin{frame}
|
||
\frametitle{Pre categories}
|
||
\framesubtitle{Definition}
|
||
Data:
|
||
\begin{align*}
|
||
\Object & \tp \Type \\
|
||
\Arrow & \tp \Object → \Object → \Type \\
|
||
\identity & \tp \Arrow\ A\ A \\
|
||
\llll & \tp \Arrow\ B\ C → \Arrow\ A\ B → \Arrow\ A\ C
|
||
\end{align*}
|
||
%
|
||
\pause
|
||
Laws:
|
||
%
|
||
\begin{align*}
|
||
\var{isAssociative} & \tp
|
||
h \llll (g \llll f) ≡ (h \llll g) \llll f \\
|
||
\var{isIdentity} & \tp
|
||
(\identity \llll f ≡ f)
|
||
×
|
||
(f \llll \identity ≡ f)
|
||
\end{align*}
|
||
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Pre categories}
|
||
\framesubtitle{1-categories}
|
||
Cubical Agda does not admit \emph{Uniqueness of Identity Proofs}
|
||
(UIP). Rather there is a hierarchy of \emph{Homotopy Types}:
|
||
Contractible types, mere propositions, sets, groupoids, \dots
|
||
|
||
\pause
|
||
1-categories:
|
||
$$
|
||
\isSet\ (\Arrow\ A\ B)
|
||
$$
|
||
\pause
|
||
\begin{align*}
|
||
\isSet & \tp \MCU → \MCU \\
|
||
\isSet\ A & ≜ ∏_{a_0, a_1 \tp A} \isProp\ (a_0 ≡ a_1)
|
||
\end{align*}
|
||
\end{frame}
|
||
|
||
\begin{frame}
|
||
\frametitle{Outline}
|
||
The path type \ensuremath{\checkmark}
|
||
|
||
Definition of a (pre-) category \ensuremath{\checkmark}
|
||
|
||
1-categories \ensuremath{\checkmark}
|
||
|
||
Univalent (proper) categories
|
||
|
||
The category of spans
|
||
\end{frame}
|
||
|
||
\begin{frame}
|
||
\frametitle{Categories}
|
||
\framesubtitle{Univalence}
|
||
Let $\approxeq$ denote isomorphism of objects. We can then construct
|
||
the identity isomorphism in any category:
|
||
$$
|
||
(\identity , \identity , \var{isIdentity}) \tp A \approxeq A
|
||
$$
|
||
\pause
|
||
Likewise since paths are substitutive we can promote a path to an isomorphism:
|
||
$$
|
||
\idToIso \tp A ≡ B → A ≊ B
|
||
$$
|
||
\pause
|
||
For a category to be univalent we require this to be an equivalence:
|
||
%
|
||
$$
|
||
\isEquiv\ (A ≡ B)\ (A \approxeq B)\ \idToIso
|
||
$$
|
||
%
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Categories}
|
||
\framesubtitle{Univalence, cont'd}
|
||
$$\isEquiv\ (A ≡ B)\ (A \approxeq B)\ \idToIso$$
|
||
\pause%
|
||
$$(A ≡ B) ≃ (A \approxeq B)$$
|
||
\pause%
|
||
$$(A ≡ B) ≅ (A \approxeq B)$$
|
||
\pause%
|
||
Name the inverse of $\idToIso$:
|
||
$$\isoToId \tp (A \approxeq B) → (A ≡ B)$$
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Propositionality of products}
|
||
Construct a category for which it is the case that the terminal
|
||
objects are equivalent to products:
|
||
\begin{align*}
|
||
\var{Terminal} ≃ \var{Product}\ ℂ\ 𝒜\ ℬ
|
||
\end{align*}
|
||
|
||
\pause
|
||
And since equivalences preserve homotopy levels we get:
|
||
%
|
||
$$
|
||
\isProp\ \left(\var{Product}\ \bC\ 𝒜\ ℬ\right)
|
||
$$
|
||
\end{frame}
|
||
|
||
\begin{frame}
|
||
\frametitle{Categories}
|
||
\framesubtitle{A theorem}
|
||
%
|
||
Let the isomorphism $(ι, \inv{ι}, \var{inv}) \tp A \approxeq B$.
|
||
%
|
||
\pause
|
||
%
|
||
The isomorphism induces the path
|
||
%
|
||
$$
|
||
p ≜ \isoToId\ (\iota, \inv{\iota}, \var{inv}) \tp A ≡ B
|
||
$$
|
||
%
|
||
\pause
|
||
and consequently a path on arrows:
|
||
%
|
||
$$
|
||
p_{\var{dom}} ≜ \congruence\ (λ x → \Arrow\ x\ X)\ p
|
||
\tp
|
||
\Arrow\ A\ X ≡ \Arrow\ B\ X
|
||
$$
|
||
%
|
||
\pause
|
||
The proposition is:
|
||
%
|
||
\begin{align}
|
||
\label{eq:coeDom}
|
||
\tag{$\var{coeDom}$}
|
||
∏_{f \tp A → X}
|
||
\var{coe}\ p_{\var{dom}}\ f ≡ f \llll \inv{\iota}
|
||
\end{align}
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Categories}
|
||
\framesubtitle{A theorem, proof}
|
||
\begin{align*}
|
||
\var{coe}\ p_{\var{dom}}\ f
|
||
& ≡ f \llll (\idToIso\ p)_1 && \text{By path-induction} \\
|
||
& ≡ f \llll \inv{\iota}
|
||
&& \text{$\idToIso$ and $\isoToId$ are inverses}\\
|
||
\end{align*}
|
||
\pause
|
||
%
|
||
Induction will be based at $A$. Let $\widetilde{B}$ and $\widetilde{p}
|
||
\tp A ≡ \widetilde{B}$ be given.
|
||
%
|
||
\pause
|
||
%
|
||
Define the family:
|
||
%
|
||
$$
|
||
D\ \widetilde{B}\ \widetilde{p} ≜
|
||
\var{coe}\ \widetilde{p}_{\var{dom}}\ f
|
||
≡
|
||
f \llll \inv{(\idToIso\ \widetilde{p})}
|
||
$$
|
||
\pause
|
||
%
|
||
The base-case becomes:
|
||
$$
|
||
d \tp D\ A\ \refl =
|
||
\left(\var{coe}\ \refl_{\var{dom}}\ f ≡ f \llll \inv{(\idToIso\ \refl)}\right)
|
||
$$
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Categories}
|
||
\framesubtitle{A theorem, proof, cont'd}
|
||
$$
|
||
d \tp
|
||
\var{coe}\ \refl_{\var{dom}}\ f ≡ f \llll \inv{(\idToIso\ \refl)}
|
||
$$
|
||
\pause
|
||
\begin{align*}
|
||
\var{coe}\ \refl_{\var{dom}}\ f
|
||
& =
|
||
\var{coe}\ \refl\ f \\
|
||
& ≡ f
|
||
&& \text{neutral element for $\var{coe}$}\\
|
||
& ≡ f \llll \identity \\
|
||
& ≡ f \llll \var{subst}\ \refl\ \identity
|
||
&& \text{neutral element for $\var{subst}$}\\
|
||
& ≡ f \llll \inv{(\idToIso\ \refl)}
|
||
&& \text{By definition of $\idToIso$}\\
|
||
\end{align*}
|
||
\pause
|
||
In conclusion, the theorem is inhabited by:
|
||
$$
|
||
\var{pathInd}\ D\ d\ B\ p
|
||
$$
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Span category} \framesubtitle{Definition} Given a base
|
||
category $\bC$ and two objects in this category $\pairA$ and $\pairB$
|
||
we can construct the \nomenindex{span category}:
|
||
%
|
||
\pause
|
||
Objects:
|
||
$$
|
||
∑_{X \tp Object} (\Arrow\ X\ \pairA) × (\Arrow\ X\ \pairB)
|
||
$$
|
||
\pause
|
||
%
|
||
Arrows between objects $(A , a_{\pairA} , a_{\pairB})$ and
|
||
$(B , b_{\pairA} , b_{\pairB})$:
|
||
%
|
||
$$
|
||
∑_{f \tp \Arrow\ A\ B}
|
||
(b_{\pairA} \llll f ≡ a_{\pairA}) ×
|
||
(b_{\pairB} \llll f ≡ a_{\pairB})
|
||
$$
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Span category}
|
||
\framesubtitle{Univalence}
|
||
\begin{align*}
|
||
(X , x_{𝒜} , x_{ℬ}) ≡ (Y , y_{𝒜} , y_{ℬ})
|
||
\end{align*}
|
||
\begin{align*}
|
||
\begin{split}
|
||
p \tp & X ≡ Y \\
|
||
& \Path\ (λ i → \Arrow\ (p\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\
|
||
& \Path\ (λ i → \Arrow\ (p\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ}
|
||
\end{split}
|
||
\end{align*}
|
||
\begin{align*}
|
||
\begin{split}
|
||
\var{iso} \tp & X \approxeq Y \\
|
||
& \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\
|
||
& \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ}
|
||
\end{split}
|
||
\end{align*}
|
||
\begin{align*}
|
||
(X , x_{𝒜} , x_{ℬ}) ≊ (Y , y_{𝒜} , y_{ℬ})
|
||
\end{align*}
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Span category}
|
||
\framesubtitle{Univalence, proof}
|
||
%
|
||
\begin{align*}
|
||
%% (f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})
|
||
%% \tp
|
||
(X, x_{𝒜}, x_{ℬ}) \approxeq (Y, y_{𝒜}, y_{ℬ})
|
||
\to
|
||
\begin{split}
|
||
\var{iso} \tp & X \approxeq Y \\
|
||
& \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ 𝒜)\ x_{𝒜}\ y_{𝒜} \\
|
||
& \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ ℬ)\ x_{ℬ}\ y_{ℬ}
|
||
\end{split}
|
||
\end{align*}
|
||
\pause
|
||
%
|
||
Let $(f, \inv{f}, \var{inv}_f, \var{inv}_{\inv{f}})$ be an inhabitant
|
||
of the antecedent.\pause
|
||
|
||
Projecting out the first component gives us the isomorphism
|
||
%
|
||
$$
|
||
(\fst\ f, \fst\ \inv{f}
|
||
, \congruence\ \fst\ \var{inv}_f
|
||
, \congruence\ \fst\ \var{inv}_{\inv{f}}
|
||
)
|
||
\tp X \approxeq Y
|
||
$$
|
||
\pause
|
||
%
|
||
This gives rise to the following paths:
|
||
%
|
||
\begin{align*}
|
||
\begin{split}
|
||
\widetilde{p} & \tp X ≡ Y \\
|
||
\widetilde{p}_{𝒜} & \tp \Arrow\ X\ 𝒜 ≡ \Arrow\ Y\ 𝒜 \\
|
||
\end{split}
|
||
\end{align*}
|
||
%
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Span category}
|
||
\framesubtitle{Univalence, proof, cont'd}
|
||
It remains to construct:
|
||
%
|
||
\begin{align*}
|
||
\begin{split}
|
||
& \Path\ (λ i → \widetilde{p}_{𝒜}\ i)\ x_{𝒜}\ y_{𝒜}
|
||
\end{split}
|
||
\end{align*}
|
||
\pause
|
||
%
|
||
This is achieved with the following lemma:
|
||
%
|
||
\begin{align*}
|
||
∏_{q \tp A ≡ B} \var{coe}\ q\ x_{𝒜} ≡ y_{𝒜}
|
||
→
|
||
\Path\ (λ i → q\ i)\ x_{𝒜}\ y_{𝒜}
|
||
\end{align*}
|
||
%
|
||
Which is used without proof.\pause
|
||
|
||
So the construction reduces to:
|
||
%
|
||
\begin{align*}
|
||
\var{coe}\ \widetilde{p}_{𝒜}\ x_{𝒜} ≡ y_{𝒜}
|
||
\end{align*}%
|
||
\pause%
|
||
This is proven with:
|
||
%
|
||
\begin{align*}
|
||
\var{coe}\ \widetilde{p}_{𝒜}\ x_{𝒜}
|
||
& ≡ x_{𝒜} \llll \fst\ \inv{f} && \text{\ref{eq:coeDom}} \\
|
||
& ≡ y_{𝒜} && \text{Property of span category}
|
||
\end{align*}
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Propositionality of products}
|
||
We have
|
||
%
|
||
$$
|
||
\isProp\ \var{Terminal}
|
||
$$\pause
|
||
%
|
||
We can show:
|
||
\begin{align*}
|
||
\var{Terminal} ≃ \var{Product}\ ℂ\ 𝒜\ ℬ
|
||
\end{align*}
|
||
\pause
|
||
And since equivalences preserve homotopy levels we get:
|
||
%
|
||
$$
|
||
\isProp\ \left(\var{Product}\ \bC\ 𝒜\ ℬ\right)
|
||
$$
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Monads}
|
||
\framesubtitle{Monoidal form}
|
||
%
|
||
\begin{align*}
|
||
\EndoR & \tp \Functor\ ℂ\ ℂ \\
|
||
\pureNT
|
||
& \tp \NT{\widehat{\identity}}{\EndoR} \\
|
||
\joinNT
|
||
& \tp \NT{(\EndoR \oplus \EndoR)}{\EndoR}
|
||
\end{align*}
|
||
\pause
|
||
%
|
||
Let $\fmap$ be the map on arrows of $\EndoR$.
|
||
%
|
||
\begin{align*}
|
||
\join \llll \fmap\ \join
|
||
& ≡ \join \llll \join \\
|
||
\join \llll \pure\ & ≡ \identity \\
|
||
\join \llll \fmap\ \pure & ≡ \identity
|
||
\end{align*}
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Monads}
|
||
\framesubtitle{Kleisli form}
|
||
%
|
||
\begin{align*}
|
||
\omapR & \tp \Object → \Object \\
|
||
\pure & \tp % ∏_{X \tp Object}
|
||
\Arrow\ X\ (\omapR\ X) \\
|
||
\bind & \tp
|
||
\Arrow\ X\ (\omapR\ Y)
|
||
\to
|
||
\Arrow\ (\omapR\ X)\ (\omapR\ Y)
|
||
\end{align*}\pause
|
||
%
|
||
\begin{align*}
|
||
\fish & \tp
|
||
\Arrow\ A\ (\omapR\ B)
|
||
→
|
||
\Arrow\ B\ (\omapR\ C)
|
||
→
|
||
\Arrow\ A\ (\omapR\ C) \\
|
||
f \fish g & ≜ f \rrrr (\bind\ g)
|
||
\end{align*}
|
||
\pause
|
||
%
|
||
\begin{align*}
|
||
\bind\ \pure & ≡ \identity_{\omapR\ X} \\
|
||
\pure \fish f & ≡ f \\
|
||
(\bind\ f) \rrrr (\bind\ g) & ≡ \bind\ (f \fish g)
|
||
\end{align*}
|
||
\end{frame}
|
||
\begin{frame}
|
||
\frametitle{Monads}
|
||
\framesubtitle{Equivalence}
|
||
In the monoidal formulation we can define $\bind$:
|
||
%
|
||
$$
|
||
\bind\ f ≜ \join \llll \fmap\ f
|
||
$$
|
||
\pause
|
||
%
|
||
And likewise in the Kleisli formulation we can define $\join$:
|
||
%
|
||
$$
|
||
\join ≜ \bind\ \identity
|
||
$$
|
||
\pause
|
||
The laws are logically equivalent. Since logical equivalence is
|
||
enough for as an equivalence of types for propositions we get:
|
||
%
|
||
$$
|
||
\var{Monoidal} ≃ \var{Kleisli}
|
||
$$
|
||
%
|
||
\end{frame}
|
||
\end{document}
|