# HoTT/book

working on uniformizing notation and terminology

 @@ -2,33 +2,50 @@ \chapter{Equivalences} \label{cha:equivalences} \section{Equivalences and Homotopies} -\begin{defn}\label{defn:contractible} 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$. + +\begin{defn}\label{defn:contractible} + A type $A$ is \textbf{contractible}, or a \textbf{singleton}, if there is $a:A$, called the \textbf{center of contraction}, such that $a=x$ for all $x:A$. \end{defn} -\begin{defn}\label{defn:equivalence} 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$. + +\begin{defn}\label{defn:equivalence} + A map $f:A\ra B$ is an {\em equivalence} if, for $y:B$, its {\em fiber}, $\setof{x:A | fx = y}$, is contractible. + We write $A\eqv B$ for the type of equivalences $A\ra B$. \end{defn} -\begin{lem}\label{lem:id-map} For each type $A$, the identity map -$1_A:= \lambda_{x:A}x :A\ra A$ is an equivalence. +\begin{lem}\label{lem:id-map} + For each type $A$, the identity map $\idfunc[A]\defeq \lambda_{x:A}x :A\ra 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. +\begin{proof} + Let $a:A$ and let $\{a\}_A\defeq \setof{ x:A | x=a }$ be its fiber with respect to $\idfunc[A]$. + We show that $\{ a\}_A$ is contractible. + Then, discharging $a:A$, we get that $\fall{x:A} (\{ x\}_A$ is contractible); i.e.\ $\idfunc[A]$ is an equivalence. + + Let $\oa \defeq (a,\refl{a}):\{ a\}_A$. As $(a,\refl{a}) = \oa$ we can use Id-induction \{a} la Christine-Paulin to get + $\fall{x:A}{z:x=a} ((x,z)=\oa).$ + Hence, by $\Sigma$-folding, $\fall{u:\{ a\}_A} (u=\oa)$. + Thus $\{ a\}_A$ is contractible, as desired. \end{proof} -\begin{defn}\label{defn:homotopy-between-functions} A {\em homotopy, $f\simeq f'$} between maps $f,f':A\ra B$ is a function $h:\prod_{x:A}\; f(x)=f'(x)$. + +\begin{defn}\label{defn:homotopy-between-functions} + A \textbf{homotopy, $f\sim f'$} between maps $f,f':A\ra B$ is a function $h:\prd{x:A} (f(x)=f'(x))$. \end{defn} -\begin{lem}\label{lem:homotopy-props} $\;$ + +\begin{lem}\label{lem:homotopy-props}\ \begin{enumerate} -\item $\simeq$ is an equivalence relation on each function type $A\ra B$. -\item If $f:A\ra B$ then $f\circ 1_A\simeq f\simeq 1_B\circ f$. -\item If $f:A\ra B, g:B\ra C$ and $h:c\ra D$ then $h\circ (g\circ f)\;\simeq\; (h\circ g)\circ f$. +\item $\sim$ is an equivalence relation on each function type $A\ra B$. + That is, we have terms of types + \begin{gather*} + \prd{f:A\to B} (f\sim f)\\ + \prd{f,g:A\to B} (f\sim g) \to (g\sim f)\\ + \prd{f,g,h:A\to B} (f\sim g) \to (g\sim h) \to (f\sim h). + \end{gather*} +\item If $f:A\ra B$ then $f\circ \idfunc[A]\sim f\sim \idfunc[B]\circ f$. +\item If $f:A\ra B, g:B\ra C$ and $h:C\ra D$ then $h\circ (g\circ f)\;\sim\; (h\circ g)\circ f$. \end{enumerate} \end{lem} -\newpage + +%% TODO: This should probably be folded into wherever we discuss function extensionality, so that $(f\sim g)\eqv (f=g)$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -46,11 +63,11 @@ \section{Bijections and Isomorphisms} \item $f$ is {\em an isomorphism} if it has $g:B\ra A$ that is both a left and a right inverse where, \begin{itemize} \item $g:B\ra A$ is a {\em left/right inverse} to $f$ if -$g\circ f\simeq 1_A$/$f\circ g\simeq 1_B$. +$g\circ f\sim \idfunc[A]$/$f\circ g\sim \idfunc[B]$. \end{itemize} \item $f$ is {\em (left/right)-invertible} if it has a (left/right) inverse. \item $f$ is a {\em weak isomorphism} if it is both left invertible and right invertible. -\item We write $A\cong B/A\cong_w B$ if there is a(n) isomorphism/weak isomorphism $A\ra B$. +\item We write $A\cong B$ if there is an) isomorphism $A\ra B$, and $A\cong_w B$ if there is a weak isomorphism $A\to B$. \end{enumerate} \end{defn} @@ -59,7 +76,7 @@ \section{Bijections and Isomorphisms} \begin{enumerate} \item $f:A\ra B$ is a surjection iff it is right-invertible. \item If $f:A\ra B$ is left-invertible then it is injective. -\item $1_A:A\ra A$ is an isomorphism. +\item $\idfunc[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$. \end{enumerate} \end{thm} @@ -91,7 +108,7 @@ \section{Adjoint Isomorphisms} }%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \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}\;[(\map{f}{\eta x}\; \ct\;\epsilon(fx))=1_{fx}].$ + $\forall_{x:A}\;[(\map{f}{\eta x}\; \ct\;\epsilon(fx))=\refl{fx}].$ We write $A\cong_a B$ if there is an adjoint isomorphism $A\ra B$. \end{defn} \begin{thm}\label{thm:equiv-iso-adj} The following are logically equivalent for $f:A\ra B$. @@ -105,7 +122,7 @@ \section{Adjoint Isomorphisms} \begin{description} \item[$(i)\ra (ii)$] -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 +Let $f:A\ra B$ be an equivalence. So each type $Cy$ is contractible, where for $y:B$, $Cy \defeq \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)} @@ -122,7 +139,7 @@ \section{Adjoint Isomorphisms} \begin{cor}\label{cor:equivs-equiv} For types A,B we have the following sequence of two equivalences and a logical equivalence between our four equivalence relations. - \[ (A\simeq B) \simeq (A\cong_a B) \simeq (A\cong_w B) \leftrightarrow (A\cong B).$ + $(\eqv A B) \simeq (A\cong_a B) \simeq (A\cong_w B) \leftrightarrow (A\cong B).$ \end{cor} \begin{proof} ?? @@ -148,9 +165,9 @@ \section{Identity Systems on a Type Universe} \begin{enumerate} \item $R_{A,B}\ra \eqv{A}{B}$ for $A,B:\bbU$ \item If $f_e:A\ra B$ and $g_e:B\ra A$ for $A,B:\bbU$ and $e:R_{A,B}$ such that - $f_{\sfr{A}} = g_{\sfr{A}}=1_A\mbox{ for } A:\bbU$ + $f_{\sfr{A}} = g_{\sfr{A}}=\idfunc[A]\mbox{ for } A:\bbU$ then - $g_e\circ f_e =1_A\mbox{ and } f_e\circ g_e = 1_B + \[ g_e\circ f_e =\idfunc[A]\mbox{ and } f_e\circ g_e = \idfunc[B] \mbox{ for } A,B:\bbU \mbox{ and } e:R_{A,B}$ \end{enumerate} \end{thm} @@ -160,8 +177,8 @@ \section{Identity Systems on a Type Universe} \begin{thm} $\bbU$ is a univalent type universe iff $(Equiv^\bbU,\sfequiv{})$ is an identity system on $\bbU$, where $Equiv^\bbU_{A,B}\defeq (\eqv{A}{B})\mbox{ for } A,B:\bbU$ -and, if $s_A: (1_A\mbox{ is an equivalence }A\ra A)$, - $\sfequiv{A}\defeq (1_A,s_A):\eqv{A}{A}\mbox{ for } A:\bbU.$ +and, if $s_A: (\idfunc[A]\mbox{ is an equivalence }A\ra A)$, + $\sfequiv{A}\defeq (\idfunc[A],s_A):\eqv{A}{A}\mbox{ for } A:\bbU.$ \end{thm}
 @@ -332,7 +332,7 @@ \section{Definition \& First Properties of H--Levels} \end{thm} \begin{defn} - A type $X$ is an {\em h-set}, if it is of h-level $2$. + A type $X$ is a {\em set}, if it is of h-level $2$. \end{defn} \begin{defn} @@ -346,7 +346,7 @@ \section{Definition \& First Properties of H--Levels} \begin{thm}\label{thm:h-set-uip-K} For a type $X$ the following are equivalent: \begin{enumerate} - \item $X$ is an h-set. + \item $X$ is a set. \item $X$ has UIP. \item $X$ satisfies Axiom K. \end{enumerate} @@ -358,15 +358,15 @@ \section{Definition \& First Properties of H--Levels} \end{defn} \begin{thm} - Let $X : \Type$. If $X$ has decidable equality, then $X$ is an h-set. + Let $X : \Type$. If $X$ has decidable equality, then $X$ is a set. \end{thm} \begin{proof} By Theorem \ref{thm:h-set-uip-K} it suffices to show that $X$ satisfies Axiom K. This is so trivial that I can't even write it! \end{proof} \begin{thm}\label{prop:nat-is-set} - The type $\Nat$ of natural numbers is an h-set. + The type $\Nat$ of natural numbers is a set. \end{thm} \begin{proof} @@ -414,4 +414,10 @@ \section{H--Level of types of h--level $n$} $\eqv{X}{X'} \hookrightarrow X \rightarrow X'$ i.e. a map of h-level $1$. Thus it suffices to show that $X \rightarrow X'$ is of h-level $n$. Since h-levels are preserved under $\prod$ and hence under the arrow type, this reduces to an assumption that $X'$ is of h-level $n$. -\end{proof} +\end{proof} + + +% Local Variables: +% mode: latex +% TeX-master: "main" +% End: