HoTT/book

Subversion checkout URL

You can clone with HTTPS or Subversion.

Update univalence proof to use our standard macros

commit 18e160858ae1b1d5d90149e415e2b8ae605723d4 1 parent a1b20a3
mikeshulman authored
Showing with 179 additions and 190 deletions.
1. +1 −0  macros.tex
2. +0 −17 pa-macros.tex
3. +44 −44 ua-append.tex
4. +68 −66 ua-fe.tex
5. +66 −63 ua.tex
1  macros.tex
 @@ -77,6 +77,7 @@ \defthm{rmk}{Remark} \defthm{eg}{Example} \defthm{egs}{Examples} +\defthm{notes}{Notes} % Number exercises within chapters, with their own counter. \newtheorem{ex}{Exercise}[chapter] \def\exautorefname{Exercise}
17 pa-macros.tex
 @@ -1,21 +1,4 @@ \newcommand{\comment}[1]{} %%%to comment out blocks of text -\newcommand{\be}{\begin} -\newcommand{\en}{\end} - -%\newtheorem{thm}{Theorem:}[section] -%\newtheorem{cor}[thm]{Corollary:} -\newtheorem{propp}[thm]{Proposition:} -%\newtheorem{lem}[thm]{Lemma:} -\newtheorem{deff}[thm]{Definition:} -\newtheorem{exe}[thm]{Exercise:} -\newtheorem{cla}[thm]{Claim:} -\newtheorem{rem}[thm]{Remark:} -\newtheorem{examples}[thm]{Examples:} -\newtheorem{dfn}[thm]{Definition:} -\newtheorem{rmr}[thm]{Remark:} -\newtheorem{pro}[thm]{Proposition:} -\newtheorem{conj}[thm]{Conjecture:} -\newtheorem{notes}[thm]{Notes:} \newcommand{\ra}{\rightarrow}
88 ua-append.tex
 @@ -8,52 +8,52 @@ \subsection{Adjoint Isomorphisms} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% In order to define the notion of an adjoint isomorphism we need the following definition. -\be{deff} $\;$ +\begin{defn} $\;$ If $f:A\ra B$ define, by Id-induction, $fz:fx=fx'$ for $x,x':A, z:x=x'$ such that $f\refl{x} = \refl{fx}$ for $x:A$. -\en{deff} +\end{defn} -\be{deff} A function $f:A\ra B$ is an {\em adjoint isomorphism} if there are $g:B\ra A$, $\eta:\forall_{x:A}\; [x=g(fx)]$ and $\epsilon:\forall_{y:B}\; [f(gy)=y]$ such that +\begin{defn} A function $f:A\ra B$ is an {\em adjoint isomorphism} if there are $g:B\ra A$, $\eta:\forall_{x:A}\; [x=g(fx)]$ and $\epsilon:\forall_{y:B}\; [f(gy)=y]$ such that $\forall_{x:A}\;[(f(\eta x)\; @\;\epsilon(fx))=1_{fx}].$ -\en{deff} -\be{prop}\label{prop:6.3} The following are logically equivalent for $f:A\ra B$. -\be{enumerate} +\end{defn} +\begin{prop}\label{prop:6.3} The following are logically equivalent for $f:A\ra B$. +\begin{enumerate} \item $f$ is an equivalence. \item $f$ is an isomorphism \item $f$ is an adjoint isomorphism -\en{enumerate} -\en{prop} -\proof $1\ra 2$ is Proposition~\ref{prop:3.4}. The other logical implications might best be left to another chapter. -\qed +\end{enumerate} +\end{prop} +\begin{proof} $1\ra 2$ is \autoref{prop:3.4}. The other logical implications might best be left to another chapter. +\end{proof} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{The Main Lemma - version 2} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Let $\bbU$ be a universe. In the following, when we write $Z:X=X'$ it will be implicit that $X,X':\bbU$. We use transport to define, for $Z:X=X'$, $Z_0$ and also $Z_B$, for each type $B$. -\be{deff} $\;$\label{def:6.4} -\be{enumerate} +\begin{defn} $\;$\label{def:6.4} +\begin{enumerate} \item For $Z:X=X'$ let $Z_0:= Z^*_{P_0}$ where $P_0[X]:=X$ for $X:\bbU$. So $Z_0:X\ra X'$ is an equivalence for $Z:X=X'$. \item Let $B$ be a type. For $Z:X=X'$ let $Z_B:=(Z^{-1})^*_{P_B}$ where $P_B[X]:=(X\ra B)$ for $X:\bbU$. So $Z_B: (X'\ra B)\ra(X\ra B)$ is an equivalence for $Z:X=X'$. -\en{enumerate} -\en{deff} +\end{enumerate} +\end{defn} -\be{lem} $\;$\label{lem:6.5} -\be{enumerate} +\begin{lem} $\;$\label{lem:6.5} +\begin{enumerate} \item For $Z:X=X'$ $Z_Bg = g\circ Z_0 \mbox{ for g:X'\ra B}.$ \item For $Z:X=X'$ $Z_0 = \pi_{X,X'}(E_{X,X'}Z),$ where $\pi_{X,X'}:(X\simeq X')\ra (X\ra X')$ is defined by $\pi_{X,X'}(f,q):=f\mbox{ for } f:X\ra X', q:EQ(f).$ -\en{enumerate} -\en{lem} -\proof -\be{enumerate} +\end{enumerate} +\end{lem} +\begin{proof} +\begin{enumerate} \item By Id-induction on $Z:X=X'$, for $X,X':\bbU$, it suffices to show that, for $X:\bbU$ and $g:X\ra B$, $(\refl{X})_Bg = g\circ(\refl{X})_0.$ But - $\be{array}{ll} + \[\begin{array}{ll} (\refl{X})_Bg &= (\refl{X}^{-1})_{P_B}^*g\\ &= (\refl{X})_{P_B}^*g\\ @@ -62,58 +62,58 @@ \subsection{The Main Lemma - version 2} &= \lambda_{x:X}gx\\ &= g\circ 1_X\\ &= g\circ (\refl{X})_0 -\en{array}$ +\end{array}\] \item Observe that $(\refl{X})_0=1_X=\pi_{X,X}(1_X,s_X)=\pi_{X,X}(E_{X,X}\refl{X})$ for $X:\bbU$, where $s_X:EQ(1_X)$. So, by Id-induction on $Z:X=X'$, for $X,X':\bbU$, $Z_0 = \pi_{X,X'}(E_{X,X'}Z).$ -\en{enumerate} -\qed +\end{enumerate} +\end{proof} -\be{lem}[Main Lemma - version 2]\label{fe:lem-main2}\label{lem:6.6} +\begin{lem}[Main Lemma - version 2]\label{fe:lem-main2}\label{lem:6.6} Let $A,A'$ be types in a univalent universe. For each type $C$ and each $f:A\ra A'$ define $G_f := (-)\circ f:(A'\ra C)\ra (A\ra C)$; i.e. $G_f := \lambda_{g:A'\ra C}\; g\circ f$ If $f$ is an equivalence then so is $G_f$. -\en{lem} +\end{lem} %\pagebreak -\proof Let $\bbU$ be a univalent universe and let $f:A\ra A'$ be an +\begin{proof} Let $\bbU$ be a univalent universe and let $f:A\ra A'$ be an equivalence, where $A,A':\bbU$. We want to show that $G_f$ is an equivalence. -By Corollary~\ref{cor:3.5} $E_{A,A'}:(A=A')\ra (A\simeq A')$ is surjective. +By \autoref{cor:3.5} $E_{A,A'}:(A=A')\ra (A\simeq A')$ is surjective. As $f$ is an equivalence there is $q:EQ(f)$ so that $(f,q):A\simeq A'$. Let $u:=(f,q):(A\simeq A')$. So there is $Z_f:(A=A')$ such that $E_{A,A'}Z_f = u$. -\be{description} +\begin{description} \item[Proof that $G_f$ is an equivalence:] -By part 2 of Definition~\ref{def:6.4} +By part 2 of \autoref{def:6.4} $(Z_f)_B^*:(A'\ra B)\ra (A\ra B)$ -is an equivalence. So, by Lemma~\ref{lem:6.5} +is an equivalence. So, by \autoref{lem:6.5} $(Z_f)_B^*g = g\circ (Z_f)_0\mbox{ for } g:A'\ra B.$ -By Proposition~\ref{prop:4.5}, as $EQ((Z_f)_B^*)$, $EQ(G_{(Z_f)_0})$; i.e. $G_{(Z_f)_0}$ is an equivalence. +By \autoref{prop:4.5}, as $EQ((Z_f)_B^*)$, $EQ(G_{(Z_f)_0})$; i.e. $G_{(Z_f)_0}$ is an equivalence. As $u:=(f,q):A\simeq A'$ $(Z_f)_0 = \pi_{A,A'}(E_{A,A'}(Z_f)) =\pi_{A,A'}u = f.$ So $G_f$ is an equivalence. -\en{description} -\qed +\end{description} +\end{proof} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Proof of the Theorem - version 2: } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We use the following lemma. -\be{lem}\label{fe:lem-projs}\label{lem:6.7} +\begin{lem}\label{fe:lem-projs}\label{lem:6.7} If $B$ is a type in a univalent universe then $\pi^1_B = \pi^2_B$. -\en{lem} -\proof By part 3 of Lemma~\ref{lem:4.9} $\delta_B$ is an isomorphism and hence an equivalence, by $2\ra 1$ of Proposition~\ref{prop:6.3}. So, by part 1 of the Main Lemma, if $B$ is in a univalent universe then +\end{lem} +\begin{proof} By part 3 of \autoref{lem:4.9} $\delta_B$ is an isomorphism and hence an equivalence, by $2\ra 1$ of \autoref{prop:6.3}. So, by part 1 of the Main Lemma, if $B$ is in a univalent universe then $(-)\circ\delta_B : (Id(B)\ra B)\ra (B\ra B)$ -is an equivalence and hence is injective. By part 1 of Lemma~\ref{lem:4.9}, +is an equivalence and hence is injective. By part 1 of \autoref{lem:4.9}, $\pi^1_B\circ\delta_B = \pi^2_B\circ\delta_B$ so that $\pi^1_B=\pi^2_B$. -\qed +\end{proof} Let $f_1,f_2:A\ra B$, where $B$ is a type in a univalent universe, and let @@ -122,17 +122,17 @@ \subsection{Proof of the Theorem - version 2: } $f := \lambda_{x:A}(f_1x,f_2x,qx).$ For $i=1,2$, if $x:A$ then - $\be{array}{lll} + \[\begin{array}{lll} \pi^i_B(fx)&=_{def}&\pi^i_B(f_1x,f_2x,qx)\\ &=_{def}& f_ix - \en{array}$ + \end{array}\] so that - $\be{array}{lll} + \[\begin{array}{lll} \pi^i_B\circ f&=_{def}& \lambda_{x:A}\pi^i_B(fx)\\ &=_{def}& \lambda_{x:A}f_ix,\mbox{by } {\bf (FE_{def}})_{A\ra B}\\ &=& f_i,\mbox{by }{(\eta_{\sf prop})}. - \en{array}$ -By Lemma~\ref{lem:6.7} $\pi^1_B\circ f = \pi^2_B\circ f$ so that $f_1=f_2$. + \end{array}\] +By \autoref{lem:6.7} $\pi^1_B\circ f = \pi^2_B\circ f$ so that $f_1=f_2$. \qed % Local Variables:
134 ua-fe.tex
 @@ -3,106 +3,108 @@ \section{Function Extensionality in a Univalent Universe} \subsection{Function Extensionality} -\be{deff} +\begin{defn} Given types $A,B$ we are concerned with the {\bf Function Extensionality} principle for functions $A\ra B$. -\be{center} +\begin{center} {\bf $({\bf FE_{\sf prop}})_{A\ra B}:\;\;$} $\forall_{f_1,f_2:A\ra B}[\forall_{x:A}(f_1x=f_2x)\ra (f_1=f_2)]$ -\en{center} -\en{deff} +\end{center} +\end{defn} We aim to prove the following result. -\be{thm}\label{fe:thm}\label{thm:4.2} For types $A,B$, with $B$ in a univalent universe, +\begin{thm}\label{fe:thm}\label{thm:4.2} For types $A,B$, with $B$ in a univalent universe, $({\bf FE_{\sf prop}})_{A\ra B}$. -\en{thm} +\end{thm} We will need to assume the following principle as part of our type theory. -\be{center} +\begin{center} {\bf $({\eta_{\sf prop}})_{A\ra B}:\;\;$} $\forall_{f:A\ra B}[\lambda_{x:A}fx = f]$. -\en{center} +\end{center} In order to carry through the proof of the theorem we use the following rule of our basic type theory concerning definitional equality. For $f_1,f_2:A\ra B$, -\be{center} +\begin{center} $({\bf FE_{\sf def}})_{A\ra B}$: From $f_1x=_{def}f_2x$ for $x:A$ infer $\lambda_{x:A}f_1x =_{def} \lambda_{x:A}f_2x$. -\en{center} +\end{center} When the definitional equality, $=_{def}$, used in this rule is replaced by propositional equality, $=$, then the rule is not a correct rule of the basic type theory, but when combined with $({\eta_{\sf prop}})_{A\ra B}$ is equivalent to $({\bf FE_{\sf prop}})_{A\ra B}$. I suspect that once Function Extensionality is assumed there will no longer be much need to refer to definitional equality in our informal development. \subsection{Extensional Properties of Maps} -\be{deff} +\begin{defn} If $P[f]$ is a type for $f:A\ra B$ we define $P[f]$ to be {\em extensional in $f$} if, for all $f_1,f_2:A\ra B$ $\forall_{x:A}(f_1x=f_2x)\;\ra\; (P[f_1]\ra P[f_2]).$ -\en{deff} -\be{deff} For a function $f:A\ra B$ let $EQ(f)$ be the type -\be{center} +\end{defn} +\begin{defn} For a function $f:A\ra B$ let $EQ(f)$ be the type +\begin{center} {\em $(f\mbox{ is an equivalence})$}. -\en{center} -\en{deff} -\be{propp}\label{prop:4.5} +\end{center} +\end{defn} +\begin{thm}\label{prop:4.5} For types $A,B$ the type $EQ(f)$ is extensional in $f:A\ra B$. -\en{propp} -\proof By examining the formal definition of $EQ(f)$ it is evident that $f$ only occurs when applied to an argument. -\qed +\end{thm} +\begin{proof} By examining the formal definition of $EQ(f)$ it is evident that $f$ only occurs when applied to an argument. +\end{proof} -\be{cor} \label{cor:4.6} +\begin{cor} \label{cor:4.6} For types $A,B$ the function $\lambda:(A\ra B)\ra(A\ra B)$ is an equivalence, where $\lambda f := \lambda_{x:A} fx\mbox{ for } f:A\ra B.$ -\en{cor} -\proof By $(\eta_{\sf prop})$ +\end{cor} +\begin{proof} By $(\eta_{\sf prop})$ $\lambda f = f = 1_{A\ra B}f\mbox{ for } f:A\ra B$ so that $\forall_{f:A\ra B}\; \lambda f=1_{A\ra B}f$. -As $1_{A\ra B}$ is an equivalence, by Lemma~\ref{lem:2.3}, and $EQ(f)$ is extensional in $f$, by Proposition~\ref{prop:4.5} it follows that $\lambda$ is an equivalence. -\qed +As $1_{A\ra B}$ is an equivalence, by \autoref{lem:2.3}, and $EQ(f)$ is extensional in $f$, by \autoref{prop:4.5} it follows that $\lambda$ is an equivalence. +\end{proof} %%%%%%%%%%%%%%%%% \subsection{The type $Id(B)$} %%%%%%%%%%%%%%%%% -\be{deff} Let $B$ be a type. -\be{enumerate} +\begin{defn} Let $B$ be a type. +\begin{enumerate} \item Define the type $Id(B):=\Sigma_{y,y':B}(y=y')$. \item Define the function $\delta_B:B\ra Id(B)$ by $\delta_B:=\lambda_{y:B}(y,y,\refl{y})$. \item For $i=1,2$, define the function $\pi^i_B:Id(B)\ra B$ by $\pi^i_B(y_1,y_2,z):= y_i\;\;\mbox{ for }y_1,y_2:Id(B), z:(y_1=y_2).$ -\en{enumerate} -\en{deff} -\be{propp} +\end{enumerate} +\end{defn} +\begin{thm} $\forall_{u:Id(B)}(\pi^1_Bu = \pi^2_Bu)$. -\en{propp} -\proof +\end{thm} +\begin{proof} For $y_1,y_2:Id(B), z:(y_1=y_2)$ - $\be{array}{lll} + \[\begin{array}{lll} \pi^1_B(y_1,y_2,z)&=_{def}& y_1\\ &=&y_2, \mbox{by } z\\ &=_{def}&\pi^2_B(y_1,y_2,z) - \en{array}$ + \end{array}\] So, by Id-induction on $u:Id(B)$, $\pi^1_Bu = \pi^2_Bu$. -\qed +\end{proof} It follows that if we could assume the theorem then we would get a proof that - $(*)\;\;\;\pi^1_B = \pi^2_B\mbox{ for B in a univalent universe.}$ -Instead in our second proof of the theorem we will use $(*)$ -and give another proof of (*) in Lemma~\ref{lem:6.7}. +\begin{equation} + \pi^1_B = \pi^2_B\mbox{ for $B$ in a univalent universe.}\label{eq:pi=pi} +\end{equation} +Instead in our second proof of the theorem we will use~\eqref{eq:pi=pi} +and give another proof of~\eqref{eq:pi=pi} in \autoref{lem:6.7}. -\be{lem}\label{fe:lem-delta-equiv} \label{lem:4.9} +\begin{lem}\label{fe:lem-delta-equiv} \label{lem:4.9} For $i=1,2$, -\be{enumerate} +\begin{enumerate} \item $\pi^i_B\circ\delta_B =_{def} 1_B$ and hence $(\pi^i_B\circ\delta_B)y =_{def} y$ for $y:B$. \item $(\delta_B\circ\pi^i_B)u = u$ for $u:Id(B)$ \item $\delta_B$ is an isomorphism. -\en{enumerate} -\en{lem} -\proof Routine -\qed +\end{enumerate} +\end{lem} +\begin{proof} Routine +\end{proof} -\be{lem}\label{lem:4.10} +\begin{lem}\label{lem:4.10} For $i=1,2$, $\pi^i_B$ is an equivalence. -\en{lem} -\proof For $y:B$ we must show that the type $Dy$ is contractible, where +\end{lem} +\begin{proof} For $y:B$ we must show that the type $Dy$ is contractible, where $Dy := \Sigma_{u:Id(B)}\; \pi^i_Bu=y.$ Let $dy:=(\delta_By,\refl{y}):Dy$. We show that $\forall_{v:Dy}\; v=dy$. By $\Sigma$-folding it suffices to show that @@ -116,7 +118,7 @@ \subsection{The type $Id(B)$} By another Id-induction, this time \{a} la Christine Pauline, it suffices to observe that $(\delta_By,\refl{y})=dy$ by the definition of $dy$. -\qed +\end{proof} \section{First Proof of the theorem} @@ -126,36 +128,36 @@ \subsection{ The Main Lemma - version 1} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We now state and prove version 1 of the main lemma needed to prove the theorem. -\be{lem}[Main Lemma]\label{fe:lem-main1}\label{lem:5.1} +\begin{lem}[Main Lemma]\label{fe:lem-main1}\label{lem:5.1} Let $A,A'$ be types in a univalent universe. For each type $C$ and each $f:A\ra A'$ define $H_f := f\circ(-): (C\ra A)\ra (C\ra A')$; i.e. $H_f := \lambda_{g:C\ra A}\; f\circ g.$ If $f$ is an equivalence then so is $H_f$. -\en{lem} -\proof Let $\bbU$ be a univalent universe and let $f:A\ra A'$ be an equivalence, where $A,A':\bbU$. We want to show that $H_f$ is an equivalence. +\end{lem} +\begin{proof} Let $\bbU$ be a univalent universe and let $f:A\ra A'$ be an equivalence, where $A,A':\bbU$. We want to show that $H_f$ is an equivalence. -By Corollary~\ref{cor:3.5} $E_{A,A'}:(A=A')\ra (A\simeq A')$ is surjective. +By \autoref{cor:3.5} $E_{A,A'}:(A=A')\ra (A\simeq A')$ is surjective. As $f$ is an equivalence there is $q:EQ(f)$ so that $(f,q):A\simeq A'$. Let $u:=(f,q):(A\simeq A')$. So there is $Z_f:(A=A')$ such that $E_{A,A'}Z_f = u$. -\be{description} +\begin{description} \item[Proof that $H_f$ is an equivalence:] For $X,X':\bbU$, $Z:X=X'$ let $\tau X X' Z:= \pi_{X,X'}( E_{X,X'}Z)$ where $\pi_{X,X'}:(X\simeq X')\ra (X\ra X')$ is defined by $\pi_{X,X'}(f,q):= f\mbox{ for f:X\ra X',q:EQ(f)}.$ - \be{quote} + \begin{quote} {\bf Claim:} $H_{\tau A A' Z}$ is an equivalence for $Z:A=A'$.\\ -\proof By Id-induction it suffices to show that $H_{\tau X X \refl{X}}$ is an equivalence for $X:\bbU$. As $\tau X X\refl{X}=1_X$, +\begin{proof} By Id-induction it suffices to show that $H_{\tau X X \refl{X}}$ is an equivalence for $X:\bbU$. As $\tau X X\refl{X}=1_X$, $H_{\tau X X\refl{X}} = H_{1_X}=1_{B\ra X}$ -is an equivalence, by Corollary~\ref{cor:4.6}, so that +is an equivalence, by \autoref{cor:4.6}, so that $H_{\tau X X \refl{X}}$ is an equivalence. -\qed -\en{quote} +\end{proof} +\end{quote} Observe that $f = \pi_{A,A'}(f,q)=\pi_{A,A'}(E_{A,A'}Z_f)=\tau A A' Z_f$ so that, by the claim, $H_f$ is an equivalence. -\en{description} -\qed +\end{description} +\end{proof} %\pagebreak %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -170,17 +172,17 @@ \subsection{Proof of the Theorem - version 1: } Define $d:A\ra Id(B)$ by $d:=\delta_B\circ f_1$ Then - $\be{array}{ll} + \[\begin{array}{ll} \pi^1_B\circ d &=\lambda_{x:A}\;\pi^1_B(\delta_B(f_1x))\\ - &=\lambda_{x:A}\; f_1x, \mbox{by part 1 of Lemma~\ref{lem:4.9}}\\ + &=\lambda_{x:A}\; f_1x, \mbox{by part 1 of \autoref{lem:4.9}}\\ &=\pi^1_B\circ f. - \en{array}$ -As, by Lemma~\ref{lem:4.10}, - $\pi^1_B$ is an equivalence, by part 2 of the Main Lemma, so is $H_{\pi^1_B}$ so that, by Proposition~\ref{prop:3.4}, + \end{array}\] +As, by \autoref{lem:4.10}, + $\pi^1_B$ is an equivalence, by part 2 of the Main Lemma, so is $H_{\pi^1_B}$ so that, by \autoref{prop:3.4}, $H_{\pi^1_B}$ is injective. It follows that $d=f$ and so $\pi^2_B\circ d =\pi^2_B\circ f$; i.e. $\lambda_{x:A}f_1x =\lambda_{x:A}f_2x$. So $f_1=f_2$ by $(\eta_{\sf prop})$. -\qed +\qed
129 ua.tex
 @@ -4,8 +4,8 @@ \section{Introduction} {\it This is an informal presentation of a proof of function extensionality in a univalent universe. It is fairly self-contained for those readers who are familiar with the propositions as types treatment of logic in Per Martin-L\"{o}f's intensional' dependent type theory. In fact I give two proofs of function extensionality, the second one is in an appendix and I believe is essentially a presentation of the original Coq proof by Vladimir Voevodsky. The first proof seems to me to be a simpler proof and is essentially a proof I found in a note of Carlo Angiuli. I do not know where it originated. In each proof there is a main lemma concerning composition of functions that comes in two versions, one for each proof of the theorem. Because I have tried to give a self-contained presentation there is a lot of preliminary material that might be better placed in separate chapter(s). There is one key result, needed for the second proof, that I do not prove. -This is $2\ra 1$ of Proposition~\ref{prop:6.3}; i.e. every isomorphism is an -equivalence, which is used in the proof of Lemma~\ref{lem:6.7}. +This is $2\ra 1$ of \autoref{prop:6.3}; i.e. every isomorphism is an +equivalence, which is used in the proof of \autoref{lem:6.7}. I have chosen to give a low-level presentation, where the reason for most inference steps is explicitly given. So there should be little doubt in the readers mind that the mathematics is rigorous. Also it should be fairly routine to implement the informal mathematics in Coq. With more experience of informal HoTT it should be possible to present rigorous HoTT at a higher level that would require more work from the reader. @@ -14,42 +14,44 @@ \section{Introduction} } \section{The Notion of a Univalent Universe} -\be{deff} A type $A$ is {\em contractible} if there is $a:A$, called the {\em center of contraction} such that $a=x$ for all $x:A$. -\en{deff} -\be{deff} A map $f:A\ra B$ is an {\em equivalence} +\begin{defn} A type $A$ is {\em contractible} if there is $a:A$, called the {\em center of contraction} such that $a=x$ for all $x:A$. +\end{defn} +\begin{defn} A map $f:A\ra B$ is an {\em equivalence} if, for $y:B$, its {\em fiber}, $\{x:A\mid fx = y\}$, is contractible. We write $A\simeq B$ if there is an equivalence $A\ra B$. -\en{deff} +\end{defn} -\be{lem}\label{lem:2.3} For each type $A$, the identity map +\begin{lem}\label{lem:2.3} For each type $A$, the identity map $1_A:= \lambda_{x:A}x :A\ra A$ is an equivalence. -\en{lem} -\proof Let $a:A$ and let $\{ a\}_A:= \{ x:A\mid x=a\}$ be its fiber with respect to $1_A$. We show that $\{ a\}_A$ is contractible. Then, discharging $a:A$ we get that $\forall_{x:A}(\{ x\}_A$ is contractible); i.e. $1_A$ is an equivalence. +\end{lem} +\begin{proof} Let $a:A$ and let $\{ a\}_A:= \{ x:A\mid x=a\}$ be its fiber with respect to $1_A$. We show that $\{ a\}_A$ is contractible. Then, discharging $a:A$ we get that $\forall_{x:A}(\{ x\}_A$ is contractible); i.e. $1_A$ is an equivalence. Let $\oa =(a,\refl{a}):\{ a\}_A$. As $(a,\refl{a}) = \oa$ we can use Id-induction \`{a} la Christine-Paulin to get $\forall_{x:A}\forall_{z:(x=a)}\; (x,z)=\oa.$ Hence, by $\Sigma$-folding, $\forall_{u:\{ a\}_A}\; u=\oa$ so that $\{ a\}_A$ is contractible, as desired. -\qed +\end{proof} -\be{cor} +\begin{cor}\label{ua:idtoeqv} If $\bbU$ is a type universe then - $(*)\;\;\; \forall_{X,Y:\bbU}\; [X=Y\;\ra\; X\simeq Y].$ -\en{cor} -\proof -By the lemma, $\forall_{X:\bbU}\; X\simeq X$. Hence $(*)$, by Id-induction on $\bbU$. -\qed - -\be{deff} +\begin{equation}\label{eq:idtoeqv} + \forall_{X,Y:\bbU}\; [X=Y\;\ra\; X\simeq Y]. +\end{equation} +\end{cor} +\begin{proof} +By the lemma, $\forall_{X:\bbU}\; X\simeq X$. Hence~\eqref{eq:idtoeqv}, by Id-induction on $\bbU$. +\end{proof} + +\begin{defn} A type universe $\bbU$ is {\em univalent} if the function $E:\forall_{X,Y:\bbU}\; [X=Y\;\ra\; X\simeq Y],$ -constructed in the proof of (*), is an equivalence. -\en{deff} +constructed in the proof of~\eqref{eq:idtoeqv}, is such that $E_{X,Y}$ is an an equivalence for all $X,Y:\bbU$. +\end{defn} %\pagebreak -\be{notes}[Identity] +\begin{notes}[Identity] We use the Propositions-as-Types (PaT) interpretation of logic. So each proposition is a type and the standard logical operations on propositions are the corresonding type forming operations. In particular we have the following, where we assume that $A$ is a type in some (implicit) context. -\be{enumerate} +\begin{enumerate} \item For $a,a':A$ the proposition $a=a'$ is the identity type $Id_A(a,a')$. It has the introduction rule @@ -61,13 +63,13 @@ \section{The Notion of a Univalent Universe} \item If $P[x,y,z]$ is a proposition for $x,y:A,z:(x=y)$ then proof by Id-induction on $x,y:A,z:(x=y)$ is given by the following rule. -\be{quote} +\begin{quote} From $\forall_{x:A}\; P[x,x,\refl{a}x]$ infer $\forall_{x,y:A}\forall_{z:(x=y)}P[x,y,z]$. -\en{quote} +\end{quote} This is the standard rule. Sometimes the following version due to Christine Paulin is useful when $a:A$ and $P[x,z]$ is a proposition for $x:A,z:(x=a)$. -\be{quote} +\begin{quote} From $P[a,\refl{a}]$ infer $\forall_{x:A}\forall_{z:(x=a)}P[x,z]$. -\en{quote} +\end{quote} \item The following {\em transport rule} is an easy exercise. If $P[x]$ is a type for $x:A$ then there is $z^*_P:P[x]\ra P[x']$ for $z:x=x'$ such that @@ -75,20 +77,20 @@ \section{The Notion of a Univalent Universe} for $x:A$. Moreover $z^*_P$ is an equivalence for $z:x=x'$. Note that we have left implicit $x,x':A$ as, when writing $z:x=x'$, the type of $x$ and $x'$ can usually be recovered when needed. -\en{enumerate} -\en{notes} +\end{enumerate} +\end{notes} %\pagebreak -\be{notes}[ $\Sigma$ types, Contractible types and Equivalences] +\begin{notes}[ $\Sigma$ types, Contractible types and Equivalences] $\;$ -\be{enumerate} +\begin{enumerate} \item Let $B[x]$ be a type for $x:A$ and let $C:=\Sigma_{x:A}B[x]$. $C$ is the type of pairs $(x,y)$ such that $x:A$ and $y:B[x]$. Note that we use $(x,y)$ rather than ${\sf pair}(x,y)$. If $P[u]$ is a proposition for $u: C$ then $\Sigma$-folding is the following rule, with a similar rule for the existential quantifier. -\be{quote} +\begin{quote} From $\forall_{x:A}\forall_{y:B[x]}\; P[{(x,y)}]$ infer $\forall_{u\in C[u]}P[u]$. -\en{quote} +\end{quote} Note that $\Sigma$-unfolding is the converses of the rules for the two quantifiers. \item For $y:A$, $\{ y\}_A$ is the type $\Sigma_{x:A}(x=y)$. @@ -103,8 +105,8 @@ \section{The Notion of a Univalent Universe} -\en{enumerate} -\en{notes} +\end{enumerate} +\end{notes} %\pagebreak %%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -117,40 +119,40 @@ \section{Two more Equivalence Relations between Types} \subsection{Bijections and Isomorphisms} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\be{deff} +\begin{defn} Let $f:A\ra B$. -\be{enumerate} +\begin{enumerate} \item $f$ is a {\em bijection} if it is both injective and surjective, where -\be{itemize} +\begin{itemize} \item $f$ is {\em injective} if $\forall_{x,x':A}\; \; fx=fx'\;\ra\; x=x'$, \item $f$ is {\em surjective} if $\forall_{y:B}\exists_{x:A}\;\; fx=y$, -\en{itemize} +\end{itemize} \item $f$ is {\em an isomorphism} if there is $g:B\ra A$ such that $\forall_{x:A}\; g(fx)=x\;\;\wedge\;\;\forall_{y:B}\; f(gy)=y.$ -\en{enumerate} -\en{deff} +\end{enumerate} +\end{defn} -\be{propp} $\;$ -\be{enumerate} +\begin{thm} $\;$ +\begin{enumerate} \item $1_A:A\ra A$ is an isomorphism. \item If $f:A\ra B$ and $g:B\ra C$ are isomorphisms then so is $g\circ f:A\ra C$. -\en{enumerate} -\en{propp} -\proof Routine -\qed -\be{propp}\label{prop:3.3} +\end{enumerate} +\end{thm} +\begin{proof} Routine +\end{proof} +\begin{thm}\label{prop:3.3} The following are logically equivalent for $f:A\ra B$. -\be{enumerate} +\begin{enumerate} \item $f$ is a bijection. \item $\forall_{y:B}\exists_{x:A}\;\; (fx=y\;\wedge \forall_{x':A}\;\; (fx'=y\;\ra\; x=x'))$. \item $f$ is an isomorphism. -\en{enumerate} -\en{propp} -\proof +\end{enumerate} +\end{thm} +\begin{proof} The proof of this proposition in type theory can be done by proving the implications $1\ra 2\ra 3\ra 1$. $1\ra 2$ and $3\ra 1$ are the same as in set theory. The proof that $2\ra 3$ requires, given $2$, the proof of the existence of a function $g$ inverse to $f$. In set theory this uses the fact that functions are defined to be total single-valued relations. Instead, in type theory the proof of the existence of $g$ uses the non-dependent version of the type theoretic axiom of choice. This axiom holds in the propositions as types interpretation of logic because of the strong form of the existential quantifier. -\qed -\be{quote} +\end{proof} +\begin{quote} {\bf \large The type theoretic axiom of choice: } We first state the general dependent form of the axiom. Let $B[x]$ be a type for $x:A$ and let $C[x,y]$ be a proposition for $x:A,y:B[x]$. Then $\forall_{x:A}\exists_{y:B[x]}\; C[x,y]\;\;\ra\;\; \exists_{f:\Pi_{x:A}B[x]}\forall_{x:A}\; C[x,fx].$ @@ -158,12 +160,12 @@ \subsection{Bijections and Isomorphisms} If $C[x,y]$ is a proposition for $x:A, y:B$, where $A,B$ are types then $\forall_{x:A}\exists_{y:B}\; C[x,y]\;\;\ra\;\; \exists_{f:A\ra B}\forall_{x:A}\; C[x,fx].$ -\en{quote} +\end{quote} -\be{propp}\label{prop:3.4} +\begin{thm}\label{prop:3.4} Each equivalence is an isomorphism. -\en{propp} -\proof Let $f:A\ra B$ be an equivalence. So each type $Cy$ is contractible, where for $y:B$, $Cy := \Sigma_{x:A}\; fx=y$. This means that +\end{thm} +\begin{proof} Let $f:A\ra B$ be an equivalence. So each type $Cy$ is contractible, where for $y:B$, $Cy := \Sigma_{x:A}\; fx=y$. This means that $\forall_{y:B}\exists_{u:Cy}\forall_{u':Cy}\; u'=u.$ By $\Sigma$-unfolding we get $\forall_{y:B}\exists_{x:A}\exists_{z:(fx=y)} @@ -172,15 +174,16 @@ \subsection{Bijections and Isomorphisms} It follows that \[ \forall_{y:B}\exists_{x:A}[fx=y\wedge\forall_{x':A}(fx'=y\ra x=x')].$ -Hence, by $2\ra 3$ of Proposition~\ref{prop:3.3} , $f$ is an isomorphism. -\qed +Hence, by $2\ra 3$ of \autoref{prop:3.3} , $f$ is an isomorphism. +\end{proof} -\be{cor}\label{cor:3.5} +\begin{cor}\label{cor:3.5} If $A,A'$ are elements of a univalent universe and $E_{A,A'}$ is the equivalence $EAA':(A=A')\ra (A\simeq A')$ then $E_{A,A'}$ is a a surjection. -\en{cor} -\proof By the Proposition $E_{A,A'}$ is an isomorphism and hence is surjective. -\qed +\end{cor} +\begin{proof} + By \autoref{prop:3.4}, $E_{A,A'}$ is an isomorphism and hence is surjective. +\end{proof}