% ----------------------------------------------------------------------------
% 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: