# HoTT/book

make those last changes compile

 @@ -122,7 +122,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) \lra (A\cong B).$ + $(A\simeq B) \simeq (A\cong_a B) \simeq (A\cong_w B) \leftrightarrow (A\cong B).$ \end{cor} \begin{proof} ?? @@ -133,36 +133,36 @@ \section{Identity Systems on a Type Universe} Let $\bbU$ be a type universe. \begin{defn} An {\em identity system $(R,\sfr{})$ on $\bbU$} consists of a type $R_{A,B}$ for $A,B:\bbU$, together with $\sfr{A}:R_{A,A}$ for $A:\bbU$, such that the following holds. -\be{quote} +\begin{quote} If $D_{A,B}(e)$ is a type for $A,B:\bbU$ and $e:R_{A,B}$ then there is $J_{A,B}(e):D_{A,B}(e)\mbox{ for } A,B:\bbU \mbox{ and } e:R_{A,B},$ such that $J_{A,A}(\sfr{A})=d_A\mbox{ for } A:\bbU.$ -\en{quote} +\end{quote} \end{defn} \begin{eg} $(Id_\bbU,\refl{\bbU})$ is an identity system on $\bbU$. \end{eg} -\be{thm} +\begin{thm} If $(R,\sfr{})$ is an identity system on $\bbU$ then -\be{enumerate} +\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$ then $g_e\circ f_e =1_A\mbox{ and } f_e\circ g_e = 1_B \mbox{ for } A,B:\bbU \mbox{ and } e:R_{A,B}$ -\en{enumerate} -\en{thm} +\end{enumerate} +\end{thm} \newcommand{\sfequiv}[1]{{\sf reflequiv}^\bbU_{#1}} -\be{rmk} Once we have the notion of a univalent type universe we can get the following result. -\en{rmk} -\be{thm} +\begin{rmk} Once we have the notion of a univalent type universe we can get the following result. +\end{rmk} +\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.$ -\en{thm} +\end{thm} Using the two theorems I believe (from a still mysterious coq proof of Assia and Cyril) that we can get a quick proof of function extensionality on a univalent universe.