\documentclass[a4paper,handout]{beamer}
\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}  & \defeq \lambda (n \tp \bN) \mto (0 + n \tp \bN) \\
    \var{zeroRight} & \defeq \lambda (n \tp \bN) \mto (n + 0 \tp \bN)
  \end{align*}
  \pause
  We have
  %
  $$
  \prod_{n \tp \bN} \var{zeroLeft}\ n \equiv \var{zeroRight}\ n
  $$
  %
  \pause
  But not
  %
  $$
  \var{zeroLeft} \equiv \var{zeroRight}
  $$
  %
  \pause
  We need
  %
  $$
  \funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
  $$
\end{frame}
\begin{frame}
  \frametitle{Motivating example}
  \framesubtitle{Univalence}
  Consider the set
  $\{x \mid \phi\ x \land \psi\ x\}$
  \pause

  If we show $\forall x . \psi\ x \equiv \top$
  then we want to conclude
  $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid \phi\ x\}$
  \pause

  We need univalence:
  $$(A \simeq B) \simeq (A \equiv B)$$
  \pause
  %
  We will return to $\simeq$, but for now think of it as an
  isomorphism, so it induces maps:
  \begin{align*}
    \var{toPath}  & \tp (A \simeq B) \to (A \equiv B) \\
    \var{toEquiv} & \tp (A \equiv B) \to (A \simeq 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 \to \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$
  inhabitants of $\Path\ P\ a_0\ a_1$ are like functions
  %
  $$
  p \tp \prod_{i \tp I} P\ i
  $$
  %
  Which satisfy $p\ 0 & = a_0$ and $p\ 1 & = a_1$
  \pause

  Homogenous paths
  $$
  a_0 \equiv a_1 \defeq \Path\ (\var{const}\ A)\ a_0\ a_1
  $$
\end{frame}
\begin{frame}
  \frametitle{Paths}
  \framesubtitle{Functional extenstionality}
  $$
  \funExt & \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g
  $$
  \pause
  $$
  \funExt\ p \defeq λ i\ a → p\ a\ i
  $$
  \pause
  $$
  \funExt\ (\var{const}\ \refl)
  \tp
  \var{zeroLeft} \equiv \var{zeroRight}
  $$
\end{frame}
\begin{frame}
  \frametitle{Paths}
  \framesubtitle{Homotopy levels}
  \begin{align*}
    & \isContr    && \tp    \MCU \to \MCU \\
    & \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
  \end{align*}
  \pause
  \begin{align*}
    & \isProp    && \tp \MCU \to \MCU \\
    & \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
  \end{align*}
  \pause
  \begin{align*}
    & \isSet    && \tp \MCU \to \MCU \\
    & \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
  \end{align*}
  \begin{align*}
    & \isGroupoid    && \tp \MCU \to \MCU \\
    & \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
  \end{align*}
\end{frame}
\begin{frame}
  \frametitle{Paths}
  \framesubtitle{A few lemmas}
  Let $D$ be a type-family:
  $$
  D \tp \prod_{b \tp A} \prod_{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 \prod_{b \tp A} \prod_{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 \to \MCU \\
    \var{propP} & \tp \prod_{x \tp A} \isProp\ (P\ x) \\
    p           & \tp a_0 \equiv 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}
  $\prod$ preserves $\isProp$:
  $$
  \mathit{propPi}
  \tp
  \left(\prod_{a \tp A} \isProp\ (P\ a)\right)
  \to \isProp\ \left(\prod_{a \tp A} P\ a\right)
  $$
  \pause
  $\sum$ preserves $\isProp$:
  $$
  \mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right)
  $$
\end{frame}
\begin{frame}
  \frametitle{Pre categories}
  \framesubtitle{Definition}
  Data:
  \begin{align*}
    \Object   & \tp \Type \\
    \Arrow    & \tp \Object \to \Object \to \Type \\
    \identity & \tp \Arrow\ A\ A \\
    \lll      & \tp \Arrow\ B\ C \to \Arrow\ A\ B \to \Arrow\ A\ C
  \end{align*}
  %
  \pause
  Laws:
  %
  $$
  h \lll (g \lll f) ≡ (h \lll g) \lll f
  $$
  $$
  (\identity \lll f ≡ f)
  \x
  (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 \equiv f) \x (f \comp \identity \equiv 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} & \defeq
    \prod_{A\ B \tp \Object} \prod_{f \tp \Arrow\ A\ B} \phi\ f
    %% \\
    %%   & \mathrel{\ } \identity \lll f \equiv f \x f \lll \identity \equiv f
  \end{align*}
  where
  $$
  \phi\ f \defeq \identity \lll f \equiv f \x f \lll \identity \equiv 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 \equiv B)\ (A \approxeq B)\ \idToIso
  $$
  %
\end{frame}
\begin{frame}
  \frametitle{Categories}
  \framesubtitle{Univalence, cont'd}
  $$\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso$$
  \pause%
  $$(A \equiv B) \simeq (A \approxeq B)$$
  \pause%
  $$(A \equiv B) \cong (A \approxeq B)$$
  \pause%
  Name the above maps:
  $$\idToIso \tp A ≡ B → A ≊ B$$
  %
  $$\isoToId \tp (A \approxeq B) \to (A \equiv B)$$
\end{frame}
\begin{frame}
  \frametitle{Categories}
  \framesubtitle{Propositionality}
  $$
  \isProp\ \IsCategory = \prod_{a, b \tp \IsCategory} a \equiv b
  $$
  \pause
  So, for
  $$
  a\ b \tp \IsCategory
  $$
  the proof obligation is the pair:
  %
  \begin{align*}
    p & \tp a.\isPreCategory \equiv b.\isPreCategory \\
    & \mathrel{\ } \Path\ (\lambda\; i \to (p\ i).Univalent)\ a.\isPreCategory\ b.\isPreCategory
  \end{align*}
\end{frame}
\begin{frame}
  \frametitle{Categories}
  \framesubtitle{Propositionality, cont'd}
  First path given by:
  $$
  p
  \defeq
  \var{propIsPreCategory}\ a\ b
  \tp
  a.\isPreCategory \equiv b.\isPreCategory
  $$
  \pause
  Use $\lemPropF$ for the latter.
  \pause
  %
  Univalence is indexed by an identity proof. So $A \defeq
  IsIdentity\ identity$ and $B \defeq \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 \defeq \idToIso\ (\iota, \inv{\iota}) \tp A \equiv B
  $$
  %
  \pause
  and consequently an arrow:
  %
  $$
  p_{\var{dom}} \defeq \congruence\ (λ x → \Arrow\ x\ X)\ p
  \tp
  \Arrow\ A\ X \equiv \Arrow\ B\ X
  $$
  %
  \pause
  The proposition is:
  %
  \begin{align}
    \label{eq:coeDom}
    \tag{$\var{coeDom}$}
    \prod_{f \tp A \to X}
    \var{coe}\ p_{\var{dom}}\ f \equiv f \lll \inv{\iota}
  \end{align}
\end{frame}
\begin{frame}
  \frametitle{Categories}
  \framesubtitle{A theorem, proof}
  \begin{align*}
    \var{coe}\ p_{\var{dom}}\ f
    & \equiv f \lll \inv{(\idToIso\ p)} && \text{By path-induction} \\
    & \equiv 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 \equiv \widetilde{B}$ be given.
  %
  \pause
  %
  Define the family:
  %
  $$
  D\ \widetilde{B}\ \widetilde{p} \defeq
  \var{coe}\ \widetilde{p}_{\var{dom}}\ f
  \equiv
  f \lll \inv{(\idToIso\ \widetilde{p})}
  $$
  \pause
  %
  The base-case becomes:
  $$
  d \tp D\ A\ \refl =
  \var{coe}\ \refl_{\var{dom}}\ f \equiv 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 \equiv f \lll \inv{(\idToIso\ \refl)}
  $$
  \pause
  \begin{align*}
    \var{coe}\ \refl^*\ f
    & \equiv f
    && \text{$\refl$ is a neutral element for $\var{coe}$}\\
    & \equiv f \lll \identity \\
    & \equiv f \lll \var{subst}\ \refl\ \identity
    && \text{$\refl$ is a neutral element for $\var{subst}$}\\
    & \equiv 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:
  $$
  \sum_{X \tp Object} \Arrow\ X\ \pairA × \Arrow\ X\ \pairB
  $$
  \pause
  %
  Arrows between objects $A ,\ a_{\pairA} ,\ a_{\pairB}$ and
  $B ,\ b_{\pairA} ,\ b_{\pairB}$:
  %
  $$
  \sum_{f \tp \Arrow\ A\ B}
  b_{\pairA} \lll f \equiv a_{\pairA} \x
  b_{\pairB} \lll f \equiv a_{\pairB}
  $$
\end{frame}
\begin{frame}
  \frametitle{Span category}
  \framesubtitle{Univalence}
  \begin{align*}
    \label{eq:univ-0}
    (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≡ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
  \end{align*}
  \begin{align*}
    \label{eq:univ-1}
    \begin{split}
      p \tp & X \equiv Y \\
      & \Path\ (λ i → \Arrow\ (p\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
      & \Path\ (λ i → \Arrow\ (p\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
    \end{split}
  \end{align*}
  \begin{align*}
    \begin{split}
      \var{iso} \tp & X \approxeq Y \\
      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
    \end{split}
  \end{align*}
  \begin{align*}
    (X , x_{\mathcal{A}} , x_{\mathcal{B}}) ≊ (Y , y_{\mathcal{A}} , y_{\mathcal{B}})
  \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_{\mathcal{A}}, x_{\mathcal{B}}) \approxeq (Y, y_{\mathcal{A}}, y_{\mathcal{B}})
    \to
    \begin{split}
      \var{iso} \tp & X \approxeq Y \\
      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{A})\ x_{\mathcal{A}}\ y_{\mathcal{A}} \\
      & \Path\ (λ i → \Arrow\ (\widetilde{p}\ i)\ \mathcal{B})\ x_{\mathcal{B}}\ y_{\mathcal{B}}
    \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 \equiv Y \\
      \widetilde{p}_{\mathcal{A}} & \tp \Arrow\ X\ \mathcal{A} \equiv \Arrow\ Y\ \mathcal{A} \\
    \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}_{\mathcal{A}}\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}
    \end{split}
  \end{align*}
  \pause
  %
  This is achieved with the following lemma:
  %
  \begin{align*}
    \prod_{q \tp A \equiv B} \var{coe}\ q\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}
    →
    \Path\ (λ i → q\ i)\ x_{\mathcal{A}}\ y_{\mathcal{A}}
  \end{align*}
  %
  Which is used without proof.\pause

  So the construction reduces to:
  %
  \begin{align*}
    \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}} ≡ y_{\mathcal{A}}
  \end{align*}%
  \pause%
  This is proven with:
  %
  \begin{align*}
    \var{coe}\ \widetilde{p}_{\mathcal{A}}\ x_{\mathcal{A}}
    & ≡ x_{\mathcal{A}} \lll \fst\ \inv{f} && \text{\ref{eq:coeDom}} \\
    & ≡ y_{\mathcal{A}} && \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}\ ℂ\ \mathcal{A}\ \mathcal{B}
  \end{align*}
  \pause
  And since equivalences preserve homotopy levels we get:
  %
  $$
  \isProp\ \left(\var{Product}\ \bC\ \mathcal{A}\ \mathcal{B}\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 % \prod_{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 & \defeq 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 \defeq \join \lll \fmap\ f
  $$
  \pause
  %
  And likewise in the Kleisli formulation we can define $\join$:
  %
  $$
  \join \defeq \bind\ \identity
  $$
  \pause
  The laws are logically equivalent. So we get:
  %
  $$
  \var{Monoidal} \simeq \var{Kleisli}
  $$
  %
\end{frame}
\end{document}