1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
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:
|
