cat/doc/presentation.tex

654 lines
15 KiB
TeX
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

\documentclass[a4paper,handout]{beamer}
\usetheme{metropolis}
\beamertemplatenavigationsymbolsempty
%% \usecolortheme[named=seagull]{structure}
\input{packages.tex}
\input{macros.tex}
\title[Univalent Categories]{Univalent Categories\\ \footnotesize 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{Motivating example}
\framesubtitle{Functional extensionality}
Consider the functions
\begin{align*}
\var{zeroLeft} &\lambda (n \tp \bN) \mto (0 + n \tp \bN) \\
\var{zeroRight} &\lambda (n \tp \bN) \mto (n + 0 \tp \bN)
\end{align*}
\pause
We have
%
$$
_{n \tp \bN} \var{zeroLeft}\ n ≡ \var{zeroRight}\ n
$$
%
\pause
But not
%
$$
\var{zeroLeft}\var{zeroRight}
$$
%
\pause
We need
%
$$
\funExt \tp_{a \tp A} f\ a ≡ g\ a → f ≡ g
$$
\end{frame}
\begin{frame}
\frametitle{Motivating example}
\framesubtitle{Univalence}
Consider the set
$\{x \mid \phi\ x \land \psi\ x\}$
\pause
If we show $∀ x . \psi\ x ≡ \top$
then we want to conclude
$\{x \mid \phi\ x \land \psi\ x\}\{x \mid \phi\ x\}$
\pause
We need univalence:
$$(A ≃ B)(A ≡ B)$$
\pause
%
We will return to $$, but for now think of it as an
isomorphism, so it induces maps:
\begin{align*}
\var{toPath} & \tp (A ≃ B) → (A ≡ B) \\
\var{toEquiv} & \tp (A ≡ B) → (A ≃ B)
\end{align*}
\end{frame}
\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$, $A \tp \MCU$ and $a_0, a_1 \tp A$
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{Paths}
\framesubtitle{Functional extenstionality}
$$
\funExt & \tp_{a \tp A} f\ a ≡ g\ a → f ≡ g
$$
\pause
$$
\funExt\ p ≜ λ i\ a → p\ a\ i
$$
\pause
$$
\funExt\ (\var{const}\ \refl)
\tp
\var{zeroLeft}\var{zeroRight}
$$
\end{frame}
\begin{frame}
\frametitle{Paths}
\framesubtitle{Homotopy levels}
\begin{align*}
& \isContr && \tp \MCU\MCU \\
& \isContr\ A && ≜ ∑_{c \tp A}_{a \tp A} a ≡ c
\end{align*}
\pause
\begin{align*}
& \isProp && \tp \MCU\MCU \\
& \isProp\ A && ≜ ∏_{a_0, a_1 \tp A} a_0 ≡ a_1
\end{align*}
\pause
\begin{align*}
& \isSet && \tp \MCU\MCU \\
& \isSet\ A && ≜ ∏_{a_0, a_1 \tp A} \isProp\ (a_0 ≡ a_1)
\end{align*}
\begin{align*}
& \isGroupoid && \tp \MCU\MCU \\
& \isGroupoid\ A && ≜ ∏_{a_0, a_1 \tp A} \isSet\ (a_0 ≡ a_1)
\end{align*}
\end{frame}
\begin{frame}
\frametitle{Paths}
\framesubtitle{A few lemmas}
Let $D$ be a type-family:
$$
D \tp_{b \tp A}_{p \tp a ≡ b} \MCU
$$
%
\pause
And $d$ and in inhabitant of $D$ at $\refl$:
%
$$
d \tp D\ a\ \refl
$$
%
\pause
We then have the function:
%
$$
\pathJ\ D\ d \tp_{b \tp A}_{p \tp a ≡ b} D\ b\ p
$$
\end{frame}
\begin{frame}
\frametitle{Paths}
\framesubtitle{A few lemmas}
Given
\begin{align*}
A & \tp \MCU \\
P & \tp A → \MCU \\
\var{propP} & \tp_{x \tp A} \isProp\ (P\ x) \\
p & \tp a_0 ≡ a_1 \\
p_0 & \tp P\ a_0 \\
p_1 & \tp P\ a_1
\end{align*}
%
We have
$$
\lemPropF\ \var{propP}\ p
\tp
\Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1
$$
%
\end{frame}
\begin{frame}
\frametitle{Paths}
\framesubtitle{A few lemmas}
$$ preserves $\isProp$:
$$
\mathit{propPi}
\tp
\left(_{a \tp A} \isProp\ (P\ a)\right)
\isProp\ \left(_{a \tp A} P\ a\right)
$$
\pause
$$ preserves $\isProp$:
$$
\mathit{propSig} \tp \isProp\ A → \left(_{a \tp A} \isProp\ (P\ a)\right)\isProp\ \left(_{a \tp A} P\ a\right)
$$
\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 \\
\lll & \tp \Arrow\ B\ C → \Arrow\ A\ B → \Arrow\ A\ C
\end{align*}
%
\pause
Laws:
%
$$
h \lll (g \lll f)(h \lll g) \lll f
$$
$$
(\identity \lll f ≡ f)
×
(f \lll \identity ≡ f)
$$
\pause
1-categories:
$$
\isSet\ (\Arrow\ A\ B)
$$
\end{frame}
\begin{frame}
\frametitle{Pre categories}
\framesubtitle{Propositionality}
$$
\isProp\ \left( (\identity \comp f ≡ f) × (f \comp \identity ≡ f) \right)
$$
\pause
\begin{align*}
\isProp\ \IsPreCategory
\end{align*}
\pause
\begin{align*}
\var{isAssociative} & \tp \var{IsAssociative}\\
\isIdentity & \tp \var{IsIdentity}\\
\var{arrowsAreSets} & \tp \var{ArrowsAreSets}
\end{align*}
\pause
\begin{align*}
& \var{propIsAssociative} && a.\var{isAssociative}\
&& b.\var{isAssociative} && i \\
& \propIsIdentity && a.\isIdentity\
&& b.\isIdentity && i \\
& \var{propArrowsAreSets} && a.\var{arrowsAreSets}\
&& b.\var{arrowsAreSets} && i
\end{align*}
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{Univalence}
\begin{align*}
\var{IsIdentity} &
_{A\ B \tp \Object}_{f \tp \Arrow\ A\ B} \phi\ f
%% \\
%% & \mathrel{\ } \identity \lll f ≡ f × f \lll \identity ≡ f
\end{align*}
where
$$
\phi\ f ≜ \identity
( \lll f ≡ f )
×
( f \lll \identity ≡ f)
$$
\pause
Let $\approxeq$ denote ismorphism 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 above maps:
$$\idToIso \tp A ≡ B → A ≊ B$$
%
$$\isoToId \tp (A \approxeq B)(A ≡ B)$$
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{Propositionality}
$$
\isProp\ \IsCategory =_{a, b \tp \IsCategory} a ≡ b
$$
\pause
So, for
$$
a\ b \tp \IsCategory
$$
the proof obligation is the pair:
%
\begin{align*}
p & \tp a.\isPreCategory ≡ b.\isPreCategory \\
& \mathrel{\ } \Path\ (\lambda\; i → (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory
\end{align*}
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{Propositionality, cont'd}
First path given by:
$$
p
\var{propIsPreCategory}\ a\ b
\tp
a.\isPreCategory ≡ b.\isPreCategory
$$
\pause
Use $\lemPropF$ for the latter.
\pause
%
Univalence is indexed by an identity proof. So $A ≜
IsIdentity\ identity$ and $B ≜ \var{Univalent}$.
\pause
%
$$
\lemPropF\ \var{propUnivalent}\ p
$$
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{A theorem}
%
Let the isomorphism $(ι, \inv{ι}) \tp A \approxeq B$.
%
\pause
%
The isomorphism induces the path
%
$$
p ≜ \idToIso\ (\iota, \inv{\iota}) \tp A ≡ B
$$
%
\pause
and consequently an arrow:
%
$$
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 \lll \inv{\iota}
\end{align}
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{A theorem, proof}
\begin{align*}
\var{coe}\ p_{\var{dom}}\ f
& ≡ f \lll \inv{(\idToIso\ p)} && \text{By path-induction} \\
& ≡ f \lll \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 \lll \inv{(\idToIso\ \widetilde{p})}
$$
\pause
%
The base-case becomes:
$$
d \tp D\ A\ \refl =
\var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ \refl)}
$$
\end{frame}
\begin{frame}
\frametitle{Categories}
\framesubtitle{A theorem, proof, cont'd}
$$
d \tp
\var{coe}\ \refl_{\var{dom}}\ f ≡ f \lll \inv{(\idToIso\ \refl)}
$$
\pause
\begin{align*}
\var{coe}\ \refl^*\ f
& ≡ f
&& \text{$\refl$ is a neutral element for $\var{coe}$}\\
& ≡ f \lll \identity \\
& ≡ f \lll \var{subst}\ \refl\ \identity
&& \text{$\refl$ is a neutral element for $\var{subst}$}\\
& ≡ f \lll \inv{(\idToIso\ \refl)}
&& \text{By definition of $\idToIso$}\\
\end{align*}
\pause
In conclusion, the theorem is inhabited by:
$$
\label{eq:pathJ-example}
\pathJ\ 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} \lll f ≡ a_{\pairA} ×
b_{\pairB} \lll f ≡ a_{\pairB}
$$
\end{frame}
\begin{frame}
\frametitle{Span category}
\framesubtitle{Univalence}
\begin{align*}
\label{eq:univ-0}
(X , x_{𝒜} , x_{}) ≡ (Y , y_{𝒜} , y_{})
\end{align*}
\begin{align*}
\label{eq:univ-1}
\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}
\label{eq:product-paths}
& \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_{𝒜} \lll \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 \Endo \\
\pureNT
& \tp \NT{\EndoR^0}{\EndoR} \\
\joinNT
& \tp \NT{\EndoR^2}{\EndoR}
\end{align*}
\pause
%
Let $\fmap$ be the map on arrows of $\EndoR$. Likewise
$\pure$ and $\join$ are the maps of the natural transformations
$\pureNT$ and $\joinNT$ respectively.
%
\begin{align*}
\join \lll \fmap\ \join
&\join \lll \join \\
\join \lll \pure\ &\identity \\
\join \lll \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 \rrr (\bind\ g)
\end{align*}
\pause
%
\begin{align*}
\label{eq:monad-kleisli-laws-0}
\bind\ \pure &\identity_{\omapR\ X} \\
\label{eq:monad-kleisli-laws-1}
\pure \fish f & ≡ f \\
\label{eq:monad-kleisli-laws-2}
(\bind\ f) \rrr (\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 \lll \fmap\ f
$$
\pause
%
And likewise in the Kleisli formulation we can define $\join$:
%
$$
\join\bind\ \identity
$$
\pause
The laws are logically equivalent. So we get:
%
$$
\var{Monoidal}\var{Kleisli}
$$
%
\end{frame}
\end{document}