A proof that univalence implies function extensionality

4 files changed, 377 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..138884c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,9 @@
+*.agdai*.aux
+*.log
+*.toc
+*.out
+*.aux
+*.agdai
+*.synctex.gz
+.#*
+auto/*
diff --git a/Univalence-to-funext.agda b/Univalence-to-funext.agda
new file mode 100644
index 0000000..c2935b2
--- /dev/null
+++ b/Univalence-to-funext.agda
@@ -0,0 +1,239 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+module Univalence-to-funext where
+
+open import lib.Base
+open import lib.Equivalence
+open import lib.Function
+open import lib.PathGroupoid
+open import lib.PathFunctor
+open import lib.NType
+
+--============================================================================--
+--                      Generic paths in Σ types
+
+module _ {i j} {A : Type i} {B : A → Type j} where
+  Σ-path-pair : (v w : Σ A B) → Type (lmax i j)
+  Σ-path-pair v w = Σ (fst v == fst w)
+                      (λ p → transport B p (snd v) == snd w)
+
+  pair→Σ= : {v w : Σ A B} → Σ-path-pair v w → v == w
+  pair→Σ= (idp , idp) = idp
+
+  Σ=→pair : {v w : Σ A B} → v == w → Σ-path-pair v w
+  Σ=→pair idp = (idp , idp)
+
+  Σ=→pair→Σ= : {v w : Σ A B} (p : v == w) → pair→Σ= (Σ=→pair p) == p
+  Σ=→pair→Σ= idp = idp
+
+  pair→Σ=→pair : {v w : Σ A B} (z : Σ-path-pair v w) →
+                 Σ=→pair (pair→Σ= z) == z
+  pair→Σ=→pair (idp , idp) = idp
+
+  Σ=≃pair : {v w : Σ A B} → (v == w) ≃ (Σ-path-pair v w)
+  Σ=≃pair = equiv Σ=→pair pair→Σ= pair→Σ=→pair Σ=→pair→Σ=
+
+               
+--============================================================================--
+--                           Univalence
+
+idtoeqv : ∀ {i} {A B : Type i} → (A == B) → (A ≃ B)
+idtoeqv {A = A} idp = ide A
+
+postulate
+  ua : ∀ {i} {A B : Type i} → (A ≃ B) → (A == B)
+  idtoeqv-ua-β : ∀ {i} {A B : Type i} (e : A ≃ B) → idtoeqv (ua e) == e
+
+eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) → 
+            fst (idtoeqv (ap (λ T → (C → T)) p)) == _∘_ (fst (idtoeqv p))
+eqv-post∘ idp = idp
+
+--============================================================================--
+--                         Happly and lemmas
+
+module _ {i j} {A : Type i} {B : A → Type j} {f g : Π A B} where
+  idh : f ∼ f
+  idh a = idp
+
+  happly : f == g → f ∼ g
+  happly p a = ap (λ k → k a) p
+
+  tr-happly-lemma : (p : f == g) →
+                    transport (λ k → f ∼ k) p (idh) == happly p
+  tr-happly-lemma idp = idp
+
+  fib-happly-lemma : (h : f ∼ g) → ((f , idh) == (g , h)) ≃ hfiber happly h
+  fib-happly-lemma h = (equiv from to α β) ∘e Σ=≃pair
+    where
+      to : hfiber happly h → Σ-path-pair (f , idh) (g , h)
+      to (p , q) = (p , tr-happly-lemma p ∙ q)
+
+      from :  Σ-path-pair (f , idh) (g , h) → hfiber happly h
+      from (p , q) = (p , ! (tr-happly-lemma p) ∙ q)
+
+      β : (b : Σ-path-pair (f , idh) (g , h)) → to (from b) == b
+      β (p , q) = pair→Σ= (idp , ! (∙-assoc (tr-happly-lemma p)
+                                            (! (tr-happly-lemma p)) q) ∙
+                                 !-inv-r (tr-happly-lemma p) ∙2 idp)
+
+      α : (a : hfiber happly h) → from (to a) == a
+      α (p , q) = pair→Σ= (idp ,
+                           ! (∙-assoc (! (tr-happly-lemma p))
+                             (tr-happly-lemma p) q) ∙
+                           !-inv-l (tr-happly-lemma p) ∙2 idp)
+
+--============================================================================--
+--                     Equivalences and contractibility
+
+contr-retract : ∀ {i} {A B : Type i}
+                (r : A → B) (s : B → A) →
+                (r ∘ s ∼ (idf B)) →
+                is-contr A → is-contr B
+contr-retract r s h p = has-level-in
+                      ((r (fst c)) , λ y → ap r (snd c (s y)) ∙ h y)
+                      where c = has-level-apply p
+                      
+module _ {i j} {A : Type i} {B : Type j} where
+  is-contr-map : (f : A → B) → Type (lmax i j)
+  is-contr-map f = (y : B) → is-contr (hfiber f y)
+
+  tr-ap-lemma : (f : A → B) {a' a : A} {b : B}
+                (p : a' == a) (q : f a' == b) →
+                transport (λ x → f x == b) p q == ! (ap f p) ∙ q
+  tr-ap-lemma f idp idp = idp
+
+  nat-lemma : {k l : B → B} {a b : B} (p : a == b )(h : k ∼ l) →
+              ap k p ∙ h b == h a ∙ ap l p
+  nat-lemma {a = a} idp h = ! (∙-unit-r (h a))
+
+  contr-map-is-equiv : {f : A → B} → (is-contr-map f → is-equiv f)
+  contr-map-is-equiv {f = f} c = snd (equiv f g α β)
+    where
+      g : B → A
+      g b = fst (fst (has-level-apply (c b)))
+
+      α : f ∘ g ∼ (idf B)
+      α b = snd (fst (has-level-apply (c b)))
+
+      β : g ∘ f ∼ (idf A)
+      β a = fst (Σ=→pair (snd (has-level-apply (c (f a))) (a , idp)))
+
+      
+
+  equiv-is-contr-map : {f : A → B} → (is-equiv f → is-contr-map f)
+  equiv-is-contr-map {f = f} e b =
+                        has-level-in (hf , λ y → pair→Σ= (fc y , sc y))
+    where
+      g : B → A
+      g = is-equiv.g e
+
+      α : g ∘ f ∼ (idf A)
+      α = is-equiv.g-f e
+
+      β : f ∘ g ∼ (idf B)
+      β = is-equiv.f-g e
+      
+      hf : hfiber f b
+      hf = ((g b) , (β b))
+
+      fc : (y : hfiber f b) → (g b) == fst y
+      fc (a , p) = ap (g) (! p) ∙ α a
+
+      sc : (y : hfiber f b) →
+           transport (λ x → f x == b) (fc (fst y , snd y)) (β b) == snd y
+      sc (a , p) =
+        transport (λ x → f x == b) (fc (a , p)) (β b)
+          =⟨ tr-ap-lemma f (fc (a , p)) (β b) ⟩
+        ! (ap f  (fc (a , p))) ∙ (β b)
+          =⟨ ap ! (ap-∙ f (ap g (! p)) (α a)) ∙2 idp ⟩
+        ! (ap f (ap g (! p)) ∙ ap f (α a)) ∙ (β b)
+          =⟨ ap ! (idp ∙2 is-equiv.adj e a) ∙2 idp {a = β b}⟩
+        ! (ap f (ap g (! p)) ∙ (β (f a))) ∙ (β b)
+          =⟨ ap ! (∘-ap f g (! p) ∙2 idp) ∙2 idp ⟩
+        ! (ap (f ∘ g) (! p) ∙ (β (f a))) ∙ (β b)
+          =⟨ !-∙ (ap (f ∘ g) (! p)) (β (f a)) ∙2 idp ⟩
+        (! (β (f a)) ∙ ! (ap (λ x → f (g x)) (! p))) ∙ (β b)
+          =⟨ (idp ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b}⟩
+        (! (β (f a)) ∙ (ap (f ∘ g) (! (! p)))) ∙ (β b)
+          =⟨ (idp ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2 idp {a = β b} ⟩
+        (! (β (f a)) ∙ (ap (f ∘ g) p)) ∙ (β b)
+          =⟨ ∙-assoc (! (β (f a))) (ap (f ∘ g) p) (β b) ⟩
+        ! (β (f a)) ∙ (ap (f ∘ g) p ∙ (β b))
+          =⟨ idp {a = ! (β (f a))} ∙2 (nat-lemma p β ∙ (idp ∙2 ap-idf p)) ⟩
+        ! (β (f a)) ∙ (β (f a) ∙ p)
+          =⟨ ! (∙-assoc (! (β (f a))) (β (f a)) p) ⟩
+        (! (β (f a)) ∙ β (f a)) ∙ p
+          =⟨ !-inv-l (β (f a)) ∙2 idp ⟩
+        p
+          =∎
+
+      
+
+--============================================================================--
+--                        Univalence implies funext
+
+module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
+  image : A → Type i
+  image a = Σ (B a) (λ b → f a == b)
+
+  graphType : Type i
+  graphType = Σ A image
+  
+  prA : graphType → A
+  prA = fst
+
+  prA-is-equiv : graphType ≃ A
+  prA-is-equiv = equiv prA (λ x → (x , f x , idp)) (λ b → idp) β
+    where
+      tr-post-concat : ∀ {i} {X : Type i} {x y z : X} {p : x == y}
+                 (q : z == x) → transport (_==_ z) p q == q ∙ p
+      tr-post-concat {p = idp} idp = idp
+
+      β : (a : graphType) → (fst a , f (fst a), idp) == a
+      β (a , b , p) = pair→Σ= (idp , (pair→Σ= (p , (tr-post-concat idp))))
+                
+  fibreOverId : Type i
+  fibreOverId = hfiber (_∘_ prA) (idf A)
+
+  fibreOverId-is-contr : is-contr fibreOverId
+  fibreOverId-is-contr = prA∘-is-equiv (idf A)
+       where
+        p : graphType == A
+        p = ua prA-is-equiv
+
+        pβ : fst (idtoeqv p) == prA
+        pβ = ap fst (idtoeqv-ua-β prA-is-equiv)
+        
+        prA∘-is-equiv : is-contr-map (λ g → prA ∘ g)
+        prA∘-is-equiv = transport is-contr-map
+                         (eqv-post∘ p ∙ ap (λ x → _∘_ x) pβ)
+                         (equiv-is-contr-map
+                           (snd (idtoeqv (ap (λ T → (A → T)) p))))
+
+  homotopyType : Type i
+  homotopyType = Σ (Π A B) (λ g → f ∼ g)
+
+  -- We crucially make use of the η-rule for functions here
+  s : homotopyType → fibreOverId
+  s (g , h) = ((λ a → (a , g a , h a)) , idp)
+
+  r : fibreOverId → homotopyType
+  r (func , p) = fst ∘ img , snd ∘ img
+               where
+                 img : (a : A) → image a
+                 img a = transport image (happly p a) (snd (func a))
+
+  -- and here
+  var-funext : is-prop homotopyType
+  var-funext = contr-is-prop (contr-retract r s (λ _ → idp)
+                              fibreOverId-is-contr)
+
+module _ {i} {A : Type i} {B : A → Type i} {f g : Π A B} where
+  pre-funext : (h : f ∼ g) → is-contr ((f , idh {g = g}) == (g , h))
+  pre-funext h = has-level-apply var-funext (f , idh {g = g}) (g , h)
+
+  funext : is-equiv (happly {f = f}{g = g})
+  funext = contr-map-is-equiv
+             λ h → equiv-preserves-level
+                     (fib-happly-lemma h)
+                     ⦃ pre-funext h ⦄
diff --git a/univalence-to-funext.pdf b/univalence-to-funext.pdf
new file mode 100644
index 0000000..3d078ca
--- /dev/null
+++ b/univalence-to-funext.pdf
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: