A proof that univalence implies function extensionality

1 files changed, 129 insertions, 0 deletions

diff --git a/univalence-to-funext.tex b/univalence-to-funext.tex
new file mode 100644
index 0000000..ffadf28
--- /dev/null
+++ b/univalence-to-funext.tex
@@ -0,0 +1,129 @@
+% ----------------------------------------------------------------------------
+% Document aesthetics
+\documentclass[a4paper,12pt]{article}
+\usepackage[oldstylemath,fulloldstylenums]{kpfonts}
+\usepackage[UKenglish,nodayofweek]{datetime}
+\usepackage{a4wide, fullpage, textcomp, cite, multicol}
+\usepackage[bf,big,center]{titlesec}
+
+\titleformat{\section}[hang]{\bfseries\Large\filcenter}{\arabic{section}.}{0.5em}{}
+\titleformat{\subsection}[hang]{\bfseries\large\filcenter}{\arabic{section}.\arabic{subsection}.}{0.5em}{}
+\titleformat{\subsubsection}[hang]{\bfseries\filcenter}{}{0.5em}{}
+
+% ----------------------------------------------------------------------------
+% Theorems, props, links, etc
+\usepackage[hidelinks]{hyperref}
+\usepackage{amsmath, amssymb, amsfonts}
+\usepackage[centercolon=true]{mathtools}
+\usepackage{amsthm}
+                
+% ----------------------------------------------------------------------------
+% Types
+\newcommand{\trm}[1]{{\textbf{\fontfamily{cmss}\selectfont\text{#1}}}}
+\newcommand{\uni}[1]{\ensuremath{\mathcal{U}_{{#1}}}}
+\usepackage{scalerel}
+\newcommand{\sq}{\mathbin{\scalerel*{\strut\rule{2ex}{2ex}}{\circ}}}
+\newcommand{\bigpi}{\mathop{\scalerel*{\Pi}{\textstyle\int}}}
+\newcommand{\bigsig}{\mathop{\scalerel*{\Sigma}{\textstyle\int}}}
+\newcommand{\Prod}[1]{\mathchoice{\underset{\left(\,{#1}\,\right)}{\bigpi}}
+  {\Pi({#1}),}
+  {\Pi({#1}),}
+  {\Pi({#1}),}}
+\newcommand{\Sum}[1]{\mathchoice{\underset{\left(\,{#1}\,\right)}{\bigsig}}
+  {\Sigma({#1}),}
+  {\Sigma({#1}),}
+  {\Sigma({#1}),}}
+
+\newcommand{\eqv}{\mathrel{\simeq}}
+\newcommand{\col}{\mathop{:}}
+\newcommand{\dfn}{\mathrel{:\equiv}}
+\newcommand{\je}{\mathrel{\equiv}}
+
+\DeclareMathOperator{\refl}{\trm{refl}}
+\DeclareMathOperator{\tr}{\trm{tr}}
+\DeclareMathOperator{\id}{\trm{id}}
+\DeclareMathOperator{\ite}{\trm{idtoqev}}
+\DeclareMathOperator{\hap}{\trm{happly}}
+\DeclareMathOperator{\pr}{\trm{pr}}
+\DeclareMathOperator{\ie}{\trm{is-eqv}}
+\DeclareMathOperator{\ic}{\trm{is-contr}}
+\DeclareMathOperator{\is}{\trm{is-set}}
+\DeclareMathOperator{\fib}{\trm{fib}}
+\DeclareMathOperator{\him}{\trm{himg}}
+\DeclareMathOperator{\hgr}{\trm{hgraph}}
+
+% ----------------------------------------------------------------------------
+% Document
+
+\title{Univalence implies Function Extensionality}
+\author{tslil clingman}
+
+\begin{document}
+\maketitle
+\abstract{ Assume a judgemental $\eta$-rule for functions and
+  univalence. Given $f\col\Prod{a\col A}B$, let:
+  $\him_{f}(a)\dfn(\Sum{b\col Ba}fa=b)$ for $a\col A$,
+  $\hgr(f)\dfn(\Sum{a\col A}\him_{f}(a))$, and
+  $\pr_{A}\col\hgr(f)\rightarrow A$ be the canonical projection. Note
+  that $\pr_{A}$ is an equivalence ($f$ gives the data). Construct a
+  retract
+  $r\col\fib_{\pr_{A}\circ(-)}(\id_{A})\rightarrow
+  (\Sum{g\col\Prod{a\col A}B}f\sim g)$ as
+  $r(k,p)\dfn(\trm{fst}\circ\trm{im},\, \trm{snd}\circ\trm{im})$ where
+  $\trm{im}\dfn\lambda a.\tr_{A,\him}(pa,\, \trm{snd}(ka))$, as
+  witnessed by $s(g,h)\dfn(\lambda a.(a,(ga,ha)),\,\refl_{\id_{A}})$.
+  Using univalence, deduce that the function
+  $\pr_{A}\circ(-)\col(A\rightarrow\hgr(f))\rightarrow(A\rightarrow A)$
+  is an equivalence so that $\Sum{g\col\Prod{a\col A}B}f\sim g$ is
+  contractible and a set. Observe
+  $\tr_{\Prod{a\col A}B,\,f\sim}(f,g,p,\lambda a.\refl_{fa})=\hap(p)$,
+   and conclude that
+  $\fib_{\hap}(h)\je(\Sum{p\col f=g}\hap(p)=h)\eqv((f,\lambda
+  a.\refl_{fa})=(g,h))$ is contractible.\hfill$\blacksquare$ }
+
+ 
+\section{Why this proof?}
+
+Given a function $f\col\Prod{a\col A}B$ and $a\col A$, we know that
+the homotopy image of $a$, defined as
+$\him_{f}(a)\dfn\Sum{b\col Ba}fa=b$, is contractible. Should we define
+the corresponding homotopy graph of $f$ as
+$\hgr(f)\dfn\Sum{a\col A} \him_{f}(a)$, the previous observation
+allows us to prove that $\trm{pr}_{A}\col \hgr(f) \rightarrow A$ is an
+equivalence.
+
+While not interesting on its own, we may note that functions
+$g\col\Prod{a\col A}B$ which are homotopic to $f$ are \emph{nearly}
+the same things as functions $A\rightarrow \hgr(f)$. Nearly
+only so because that type has things which are `wild', they may map a
+term $a$ to a term $b^{\prime}\col B(a^{\prime})$ in a fibre not
+necessarily related to $B(a)$ and so may not be readily
+rectified into functions. Some meditation on this reveals that terms
+$\overline{g}\col A\rightarrow \hgr(f)$ corresponding to
+functions $g\col\Prod{a\col A}B$ and witnesses $f\sim g$ are precisely
+those for which we have a proof
+$\trm{pr}_{A}\circ \overline{g}\sim \id_{A}$.
+
+Thus we see that the data carried by the type
+$\Sum{g\col\Prod{a\col A}B}f\sim g$ may be equivalently found in some
+sub-type of $A\rightarrow \hgr(f)$. Were we able to show that
+this sub-type was contractible, we would in particular show that if
+$f\sim g$ then $f=g$. Unfortunately, in the absence of function
+extensionality, there does not appear to be an easy way to pin-down
+this sub-type of functions in such a way that contractibility is
+easily shown.
+
+Instead, we restrict our attention to an \emph{a priori} `larger'
+sub-type of $A\rightarrow \hgr(f)$, viz., those terms
+$\overline{g}$ for which we have a proof
+$p:\trm{pr}_{A}\circ g=\id_{A}$. As the existence of such a term $p$
+certainly entails the existence of a term
+$\hap(p)\col\trm{pr}_{A}\circ g\sim\id_{A}$ we expect (and may prove)
+that this sub-type retracts onto $\Sum{g\col\Prod{a\col A}B}f\sim g$.
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: