# HoTT/book

mods in hlevels

 @@ -8,7 +8,7 @@ \newcommand{\comp}[2]{\ensuremath{{#2} \circ {#1}}} -% +% % % Type-theoretic: \newcommand{\contr}{\ensuremath{\mathsf{contr}}} \newcommand{\iscontr}{\ensuremath{\mathsf{iscontr}}} @@ -40,24 +40,21 @@ \chapter{H--Levels} -\section{Introduction} - - -\section{Definition \& First Properties of H--Levels} +\section{Definition and First Properties} \begin{defn} - The h--level of a type $X$ is defined recursively as follows: + The {\em h-level} of a type $X$ is defined recursively as follows: \begin{itemize} \item $X$ is of h-level $0$, if it is contractible. \item $X$ is of h-level $n+1$, if for all $x, y : X$ the type $(x =_X y)$ is of h-level $n$. \end{itemize} - This defines a predicate $\isofhlevel \ n \ X$. + This defines a predicate $\isofhlevel(n)(X)$. \end{defn} -The h-levels are therefore an axiomatization of finite homotopy types. -More precisely, types (in type theory) of h-level $n$ should be thought of exactly as homotopy $(n\mbox{-}2)$-types. -Similarly, as in homotopy theory a type does not have to be of any finite h-level; -in the section on higher inductive types we shall see that one can describe the types (such as, for example, the $2$-sphere) +The h-levels are therefore an axiomatization of finite homotopy types. +More precisely, types (in type theory) of h-level $n$ should be thought of exactly as homotopy $(n\mbox{-}2)$-types. +Similarly, as in homotopy theory a type does not have to be of any finite h-level; +in the section on higher inductive types we shall see that one can describe the types (such as, for example, the $2$-sphere) that are of no finite h-level. We start by showing the preservation of h-levels under certain operations and various logical constructors. @@ -74,21 +71,21 @@ \section{Definition \& First Properties of H--Levels} \begin{enumerate} \item \label{enum:section_paths_1} If $e : s(y) = x$ in $X$, then we have $e' : y = p(x)$ in $Y$ - by the composition - $e' \defeq y \stackrel{\opp{\epsilon_y}}{=} p(s(y)) \stackrel{\map{p}{e}}{=} p(x) \enspace .$ - + by the composition + $e' \defeq y \stackrel{\opp{\epsilon_y}}{=} p(s(y)) \stackrel{\map{p}{e}}{=} p(x) .$ + \item \label{enum:section_paths_2} Given $e : s(y) = s(y')$, we have $\vec e : y = y$. \begin{proof} By \ref{enum:section_paths_1} we obtain $e' : y = p(s(y'))$. - Postcomposing with $\epsilon_{y'}$ we get - $\overrightarrow{e} : y \stackrel{e'}{=} p(s(y)) \stackrel{\epsilon_{y'}}{=} y' \enspace .$ + Postcomposing with $\epsilon_{y'}$ we get + $\overrightarrow{e} : y \stackrel{e'}{=} p(s(y)) \stackrel{\epsilon_{y'}}{=} y' .$ \end{proof} - + \item \label{enum:section_paths_3} If in \ref{enum:section_paths_2} we consider $e = \refl{s(y)}$, then $e' \ct \epsilon_{y}$ is homotopic to the identity path, that is, - $\overrightarrow{\refl{s(y)}} = \refl{y} \enspace .$ + $\overrightarrow{\refl{s(y)}} = \refl{y} .$ \item Given $e : y = y'$ in $Y$, we have $\overrightarrow{\map{s}{e}} = e$. \begin{proof} @@ -100,69 +97,57 @@ \section{Definition \& First Properties of H--Levels} \end{lem} -\begin{proof}[Proof of Theorem \ref{thm:h-level-retracts}] +\begin{proof}[Proof of Theorem \autoref{thm:h-level-retracts}] We proceed by induction on $n$. -\begin{itemize} - \item In case $n=0$, we know that $X$ is contractible and let $x_0 : X$ be the center of contraction. - We claim that $y_0 \defeq p(x_0) : Y$ is the center of contraction for $Y$. - Let $y : Y$, we need a path $y = y_0$. We have $\epsilon_y : p(s(y)) = y$ and $\contr_{s(y)} : s(y) = x_0$. - By composing we obtain a path - $y \stackrel{\opp{\epsilon_y}}{=} p(s(y)) \stackrel{\map{p}{\contr_{s(y)}}}{=} p(x_0) \equiv y_0 \enspace .$ - \item For the inductive step, let $y, y' : Y$. We show that $\idtype {y}{y'}$ is of h--level $n$. - By assumption we know that $\idtype{s(y)}{s(y')}$ is of h--level $n$. - We have two maps - \begin{equation*} - \begin{xy} - \xymatrix@C=2pc{ - **[l] \idtype {y}{y'} \ar@/^/@<1ex>[r]^{\map{s}{\_}} & - **[r] \idtype{s(y)}{s(y')} \ar@/^/@<1ex>[l]^{\overrightarrow{(\_)}} -} - \end{xy} \enspace . -\end{equation*} - By \autoref{lem:path_retract} we have $\comp{\map{s}{\_}}{\overrightarrow{(\_)}} = 1$, + For $n=0$, we know that $X$ is contractible and let $x_0 : X$ be the center of contraction. + We claim that $y_0 \defeq p(x_0) : Y$ is the center of contraction for $Y$. + Let $y : Y$, we need a path $y = y_0$. We have $\epsilon_y : p(s(y)) = y$ and $\contr_{s(y)} : s(y) = x_0$. + By composing we obtain a path + $y \stackrel{\opp{\epsilon_y}}{=} p(s(y)) \stackrel{\map{p}{\contr_{s(y)}}}{=} p(x_0) \equiv y_0 .$ + For the inductive step, let $y, y' : Y$. We show that $\idtype {y}{y'}$ is of h-level $n$. + By assumption we know that $\idtype{s(y)}{s(y')}$ is of h-level $n$. + We have two maps + $\xymatrix{\idtype{y}{y'} \ar@<1.5ex>[rr]^{\map{s}{\_}} & & \idtype{s(y)}{s(y')} \ar@<1.2ex>[ll]^{\overrightarrow{(\_)}}}$ + By \autoref{lem:path_retract} we have $\comp{\map{s}{\_}}{\overrightarrow{(\_)}} = 1$, that is, $\idtype {y}{y'}$ is a retract of $\idtype{s(y)}{s(y')}$. - By induction hypothesis, $\idtype {y}{y'}$ thus has - h--level $n$, as was to be shown. - \end{itemize} + By induction hypothesis, $\idtype {y}{y'}$ thus has + h-level $n$, as was to be shown. \end{proof} As an immediate corollary we obtain the stability of h-levels under weak equivalence: \begin{cor}\label{cor:preservation_hlevels_weq} - If $X \simeq Y$ and $X$ is of h-level $n$, then so is $Y$. + If $\eqv{X}{Y}$ and $X$ is of h-level $n$, then so is $Y$. \end{cor} \begin{thm}\label{thm:hlevel_cumulative} - The hierarchy of h-levels is cumulative in the following sense: + The hierarchy of h-levels is cumulative in the following sense: given a natural number $n$, if $X$ is of h-level $n$, then it is also of h-level $n+1$. \end{thm} \begin{proof} - We proceed by induction on $n$: -\begin{itemize} - \item For $n = 0$, we need to prove that a contractible type, say, $A$, has contractible path spaces. + We proceed by induction on $n$. + + For $n = 0$, we need to show that a contractible type, say, $A$, has contractible path spaces. Let $a_0: A$ be the center of contraction of $A$, and let $x, y : A$. We show that $\idtype[A]{x}{y}$ is contractible. By contractibility of $A$ we have a path $\contr_x \ct \opp{\contr_y} : x = y$, which we choose as the center of contraction for $\idtype{x}{y}$. - Given any $p : x = y$, we need to show $p = \contr_x \ct \opp{\contr_y}$. + Given any $p : x = y$, we need to show $p = \contr_x \ct \opp{\contr_y}$. By identity elimination, it suffices to show that $\refl{x} = \contr_x \ct \opp{\contr_x}$, which is trivial. - \item For the inductive step, we need to show that $\idtype[X]{x}{y}$ is of h--level $n+1$, provided - that $X$ is of h--level $n+1$. Applying the induction hypothesis to $\idtype[X]{x}{y}$ + For the inductive step, we need to show that $\idtype[X]{x}{y}$ is of h-level $n+1$, provided + that $X$ is of h-level $n+1$. Applying the induction hypothesis to $\idtype[X]{x}{y}$ yields the desired result. -\end{itemize} - \end{proof} - -An equivalent criterion for being h-level $n$ can be expressed using loop--spaces: +An equivalent criterion for being of h-level $n$ can be expressed using loop--spaces: \begin{thm}\label{thm:hlevel_loops} - Let $X : \Type$ be a type, and let $n\geq 1$ be a natural number. - If for all $x : X$, the type $\Omega(X, x) := \idtype[X]{x}{x}$ is of h-level $n$, + Let $X : \type$ be a type, and let $n\geq 1$ be a natural number. + If for all $x : X$, the type $\Omega(X, x) := \idtype[X]{x}{x}$ is of h-level $n$, then $X$ is of h-level $n+1$. \end{thm} @@ -171,157 +156,157 @@ \section{Definition \& First Properties of H--Levels} Before proving the theorem, we prove an auxiliary lemma: \begin{lem}\label{lem:hlevel_if_inhab_hlevel} - Given $n \geq 1$ and a type $X : \Type$, $X$ is of h--level $n$ if, given any inhabitant of $X$ it follows that $X$ is - of h--level $n$. + Given $n \geq 1$ and $X : \type$, $X$ is of h-level $n$ if, given any inhabitant of $X$ it follows that $X$ is + of h-level $n$. \end{lem} -\begin{proof}[Proof of \autoref{lem:hlevel_if_inhab_hlevel}] - Let $f : X \to \isofhlevel(n)(X)$ be the given map. For any $x, x' : X$ we need to show that - $\idtype{x}{x'}$ is of h--level $n - 1$. But this is precisely given by +\begin{proof} + Let $f \colon X \to \isofhlevel(n)(X)$ be the given map. For any $x, x' : X$ we need to show that + $\idtype{x}{x'}$ is of h-level $n - 1$. But this is precisely given by $f(x)(x)(x') : \isofhlevel(n-1)(\idtype{x}{x'})$. \end{proof} \begin{proof}[Proof of \autoref{thm:hlevel_loops}] - In order to show that $X$ is of h--level $n+1$, we need to show that for any given $x, x' : X$, - the type $\idtype{x}{x'}$ is of h--level $n$. + In order to show that $X$ is of h-level $n+1$, we need to show that for any given $x, x' : X$, + the type $\idtype{x}{x'}$ is of h-level $n$. Following \autoref{lem:hlevel_if_inhab_hlevel} it suffices to give a map - $\idtype{x}{x'} \to \isofhlevel(n)(\idtype{x}{x'}) \enspace .$ - By identity elimination and the assumption on the h--levels on loop spaces we obtain this map. + $\idtype{x}{x'} \to \isofhlevel(n)(\idtype{x}{x'}) .$ + By the elimination rule and the assumption on the h-levels on loop spaces we obtain this map. \end{proof} +\section{Preservation under constructors} + \begin{thm} - Let $n$ be a natural number, and let $A : \Type$ and $B \colon A \to \Type$. + Let $n$ be a natural number, and let $A : \type$ and $B \colon A \to \type$. If $A$ is of h-level $n$ and for all $a : A$, $B(a)$ is of h-level $n$, then so is $\sum\limits_{x : A} B(x)$. \end{thm} \begin{proof} We proceed by induction on $n$. - \begin{itemize} - \item For $n = 0$, we choose the center of contraction for $\sum_{x : A} B(x)$ to be the pair - $(a_0, b_0)$, where $a_0 : A$ is the center of $A$ and $b_0 : B(a_0)$ is the center of $B(a_0)$. - Given any other element $(a,b)$ of $\sum_{x : A} B(x)$, we provide a path $b = (a_0,b_0)$ - by using contractibility of $A$ and $B(a_0)$, respectively. - \item For the inductive step, suppose that $A$ is of h--level $n+1$ and - for any $a : A$, $B(a)$ is of h--level $n + 1$. We show that $\sum_{x : A} B(x)$ is - of h--level $n + 1$: - fix $(a_1, b_1)$ and $(a_2,b_2)$ in $\sum_{x : A} B(x)$, - we show that $\idtype[\sum_{x : A} B(x)]{(a_1, b_1)}{(a_2,b_2)}$ is of h--level $n$. + + For $n = 0$, we choose the center of contraction for $\sum\limits_{x : A} B(x)$ to be the pair + $(a_0, b_0)$, where $a_0 : A$ is the center of contraction of $A$ and $b_0 : B(a_0)$ is the center of contraction of $B(a_0)$. + Given any other element $(a,b)$ of $\sum\limits_{x : A} B(x)$, we provide a path $\id{(a, b)}{(a_0,b_0)}$ + by contractibility of $A$ and $B(a_0)$, respectively. + + For the inductive step, suppose that $A$ is of h-level $n+1$ and + for any $a : A$, $B(a)$ is of h-level $n + 1$. We show that $\sum\limits_{x : A} B(x)$ is + of h-level $n + 1$: + fix $(a_1, b_1)$ and $(a_2,b_2)$ in $\sum\limits_{x : A} B(x)$, + we show that $\idtype[\sum\limits_{x : A} B(x)]{(a_1, b_1)}{(a_2,b_2)}$ is of h-level $n$. By \autoref{lemma_from_another_chapter} we have - $\idtype[\sum_{x : A} B(x)]{(a_1, b_1)}{(a_2,b_2)} \simeq - \sum_{p : \idtype{a_1}{a_2}} \idtype[B(a_2)]{\trans{p}{b_1}}{b_2}$ - \end{itemize} - and by preservation of h--levels under weak equivalences (\autoref{cor:preservation_hlevels_weq}) - it suffices to prove that the latter type is of h--level $n$. This is proved by applying the + $\eqv{\idtype[\sum\limits_{x : A} B(x)]{(a_1, b_1)}{(a_2,b_2)}}{\sum_{p : \idtype{a_1}{a_2}} \idtype[B(a_2)]{\trans{p}{b_1}}{b_2}}$ + and by preservation of h-levels under weak equivalences (\autoref{cor:preservation_hlevels_weq}) + it suffices to prove that the latter type is of h-level $n$. This follows from the induction hypothesis. \end{proof} \begin{thm} - Let $n$ be a natural number, and let $A : \Type$ and $B \colon A \to \Type$. + Let $n$ be a natural number, and let $A : \type$ and $B \colon A \to \type$. If for all $a : A$, $B(a)$ is of h-level $n$, then so is $\prod\limits_{x : A} B(x)$. \end{thm} TODO : link to definition of weak and strong function extensionality, where -weak is defined as -$\forall a, \iscontr (B(a)) \to \iscontr (\prod_A B)$ -and strong fe as -$\isweq (\idtype{f}{g} \to \prod_x \idtype{f(x)}{g(x)}$ -modulo typos +weak Functional Extensionality is defined as +$\prod_{a : A} \iscontr (B(a)) \to \iscontr (\prod_{a : A} B(a)),$ +and strong Functional Extensionality as +$\isweq (\idtype{f}{g} \to \prod_x \idtype{f(x)}{g(x)}.$ \begin{proof} - We proceed by induction on $n$: - \begin{itemize} - \item For $n = 0$ the result follows immediately by (weak) function extensionality --- - it is precisely the statement of weak function extensionality. - \item For the inductive step, let $f, g : \prod_{x:A}B(x)$. We need to show that - $\idtype{f}{g}$ is of h--level $n$. By (strong) function extensionality and closure - under weak equivalences of h--levels it suffices to show that - $\prod_x \idtype{f(x)}{g(x)}$ is of h--level $n$. But this follows from the + We proceed by induction on $n$. For $n = 0$ the result is precisely the statement of weak function extensionality. + + For the inductive step, let $f, g : \prod\limits_{a:A}B(a)$. We need to show that + $\idtype{f}{g}$ is of h-level $n$. By (strong) function extensionality and closure + under weak equivalences of h-levels it suffices to show that + $\prod\limits_{a : A} \idtype[B(a)]{f(a)}{g(a)}$ is of h-level $n$. But this follows from the induction hypothesis. - \end{itemize} - \end{proof} \noindent -As a special case of the above theorem, we obtain that the function space $A \to B$ is of h--level $n$ -provided that the target space $B$ is of h--level $n$. +As a special case of the above theorem, we obtain that the function space $A \to B$ is of h-level $n$ +provided that the target space $B$ is of h-level $n$. + +\section{Propositions and sets} \begin{defn} - A type $A$ is said to be an \emph{h--proposition} (an \emph{h--prop} for short), if it is of h-level $1$. + A type $A$ is said to be an \emph{h-proposition} (an \emph{h-prop} for short), if it is of h-level $1$. Thus we define the predicate - $\ishProp (A) := \isofhlevel(1)(A) \enspace .$ + $\ishProp (A) := \isofhlevel(1)(A) .$ \end{defn} +\begin{egs} + \begin{itemize} + \item Trivially, the empty type $\emptyset$ is an h-prop. + \item For any type $X$, its negation $\neq X := X \to \emptyset$ is an h-prop. This follows from the previous example by the preservation of h-levels under dependent products. + \end{itemize} +\end{egs} + \begin{thm}\label{thm:hprop_inhab_contr} - If a type $A$ is an h--prop and has at least one element, then $A$ is contractible. + If a type $A$ is an h-prop and is inhabited, then $A$ is contractible. \end{thm} \begin{proof} - Let $a_0$ be said element. We choose $a_0$ as center of contraction and thus have to + Let $a_0$ be an inhabitant of $A$. We choose $a_0$ as center of contraction and thus have to prove that for any $a : A$, $a = a_0$. - Since $A$ is an h--proposition, we know that $\idtype[A]{a}{a_0}$ is contractible. + Since $A$ is an h-prop, we know that $\idtype[A]{a}{a_0}$ is contractible. We choose its center of contraction in order to provide the desired equality. \end{proof} \begin{rmk} - The converse of \autoref{thm:hprop_inhab_contr} is also true: - $A$ is an h--proposition if it having at least one element implies it being contractible. - This follows from \autoref{lem:hlevel_if_inhab_hlevel} and cumulativity of h--levels (\autoref{thm:hlevel_cumulative}). + The converse of \autoref{thm:hprop_inhab_contr} is also true; it follows from \autoref{lem:hlevel_if_inhab_hlevel} and cumulativity of h-levels (\autoref{thm:hlevel_cumulative}). \end{rmk} - -We next turn towards giving some examples of h--propositions: +We next turn towards giving some less obvious examples of h-propositions: \begin{thm}\label{thm:isaprop_isofhlevel} For any $n : \Nat$ and any type $X$, the type: $\isofhlevel(n)(X)$ - is an h--proposition. + is an h-proposition. \end{thm} -The proof of the theorem will proceed by induction. Before giving the proof, we -prove an auxiliary lemma, which will be used in the base case of the induction: + +The theorem will be proven by induction. We start with a lemma, which contains the crucial observation needed in the proof of the base case. \begin{lem}\label{lem:contr_contr_is_contr} Let $X$ be a type. If $X$ is contractible, then so is $\iscontr(X)$. \end{lem} -\begin{proof}[Proof of \autoref{lem:contr_contr_is_contr}] +\begin{proof} Let $c : \iscontr(X)$. We claim that $c$ is the center of contraction of $\iscontr (X)$. - Let $c' : \iscontr (X)$, we need to show that - $c = c' : \sum_{x:X}\prod_{x':X}\idtype{x}{x'} \enspace .$ + Given any $c' : \iscontr (X)$, we need to show that + $c = c' : \sum_{x:X}\prod_{x':X}\idtype{x}{x'} .$ We use the equivalence between paths in total spaces and pairs of paths in the base space and the fiber - + TODO : link to appropriate theorem - The path $e : \pi_1(c) = \pi_1 (c')$ in the base space is given by contractibility. - It remains to show that - $\trans{e}{\pi_2(c)} = \pi_2 (c') : \prod_{x' : X} \idtype[A]{\pi_2 (c)} {x'} \enspace .$ - However, $A$ is contractible and thus $\idtype[A]{\pi_2 (c)} {x'}$ is as well. - Since h--levels are preserved under products, $\prod_{x' : X} \idtype[A]{\pi_2 (c)} {x'}$ - is also contractible, which yields above equality. + The path $e : \pi_1(c) = \pi_1 (c')$ in the base space is given by contractibility of $X$. + It remains to show: + $\trans{e}{\pi_2(c)} = \pi_2 (c') : \prod_{x' : X} \idtype[X]{\pi_2 (c)} {x'} .$ + Since $X$ is contractible and thus $\idtype[X]{\pi_2 (c)} {x'}$ is as well. + We know that $\prod_{x' : X} \idtype[X]{\pi_2 (c)} {x'}$ + is also contractible, so by presevation of h-levels under products, we obtain the desired equality. \end{proof} \begin{proof}[Proof of \autoref{thm:isaprop_isofhlevel}] - We proceed by induction: - \begin{itemize} - \item For the base case, we need to show that for any type $X$, the type $\iscontr(X)$ is an - h--proposition. By applying \autoref{lem:hlevel_if_inhab_hlevel}, it suffices to show that - if $X$ is contractible, then $\iscontr(X)$ is an h--proposition. - But since $X$ is contractible, the type $\iscontr(X)$ is contractible by \autoref{lem:contr_contr_is_contr}, - thus in particular it is an h--proposition by cumulativity. - \item For the inductive step, we need to show, by \autoref{lem:hlevel_if_inhab_hlevel}, that if - $X$ is of h--level $n+1$, then the type $\isofhlevel(n+1)(X)$ is contractible. - By the definition of h--levels, we must show that + We proceed by induction with respect to $n$. + + For the base case, we need to show that for any type $X$, the type $\iscontr(X)$ is an + h-proposition. By applying \autoref{lem:hlevel_if_inhab_hlevel}, it suffices to show that + if $X$ is contractible, then $\iscontr(X)$ is an h-proposition. + But since $X$ is contractible, the type $\iscontr(X)$ is contractible by \autoref{lem:contr_contr_is_contr}, + thus in particular it is an h-proposition by cumulativity. + + For the inductive step, we need to show, by \autoref{lem:hlevel_if_inhab_hlevel}, that if + $X$ is of h-level $n+1$, then the type $\isofhlevel(n+1)(X)$ is contractible. + By the definition of h-levels, we must show that $\prod_{x,y:X} \isofhlevel(n)(\idtype{x}{y})$ - is contractible. Using (weak) function extensionality, it suffices to show that for any $x,y : X$, + is contractible. Using (weak) function extensionality, it suffices to show that for any $x,y : X$, the type $\isofhlevel(n)(\idtype{x}{y})$ is contractible, which follows from the induction hypothesis. - - \end{itemize} - - \end{proof} +As an immediate corollary we obtain: \begin{cor} For any function $f \colon A \to B$ between two types, the type $\isweq(f)$ is an h-prop. @@ -331,12 +316,16 @@ \section{Definition \& First Properties of H--Levels} A type $X$ is an h-prop if and only if we have $\prod\limits_{x, y : X} (x =_X y)$. \end{thm} +\begin{proof} + The only if' direction is trivial. Conversely, suppose that $X$ is an h-prop and let $x, y : X$. We need to show that $\idtype{x}{y}$ is contractible. For that it is enough to show that $X$ is contractible. Choosing $x : X$ as the center of contraction and applying the assumption, gives the desired result. +\end{proof} + \begin{defn} - A type $X$ is a {\em set}, if it is of h-level $2$. + A type $X$ is an {\em h-set}, if it is of h-level $2$. \end{defn} \begin{defn} - Let $X : \Type$. We say that $X$ + Let $X : \type$. We say that $X$ \begin{itemize} \item has {\em uniqueness of identity proofs} (UIP, for short), if for all $x, y : X$ and $p, q : x =_X y$ we have $p = q$. \item satisfies {\em Axiom K}, if for all $x : X$ and $p : (x =_A x)$ we have $p = \refl(x)$. @@ -346,78 +335,75 @@ \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 a set. - \item $X$ has UIP. - \item $X$ satisfies Axiom K. + \item\label{enum:set-set} $X$ is an h-set. + \item\label{enum:set-uip} $X$ has UIP. + \item\label{enum:set-k} $X$ satisfies Axiom K. \end{enumerate} \end{thm} +\begin{proof} (\ref{enum:set-set} $\Rightarrow$ \ref{enum:set-uip}) is clear by definition. (\ref{enum:set-uip} $\Rightarrow$ \ref{enum:set-k}) follows by instantiating UIP with $y := x$ and $q := \refl{x}$. +Finally, we need to show that if $X$ satisfies Axiom K, then $X$ is an h-set. Let $x, y : X$. We need to show that for any $p, q : (\id{x}{y})$ we have $\id{p}{q}$. But elimination on $q$ reduces the problem precisely to Axiom K. +\end{proof} + \begin{defn} A type $X$ has {\em decidable equality}, if for all $x, y : X$ we have: $(x =_X y) + \neg (x =_X y).$ \end{defn} \begin{thm} - Let $X : \Type$. If $X$ has decidable equality, then $X$ is a set. + Let $X : \type$. If $X$ has decidable equality, then $X$ is an h-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! + By \autoref{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 a set. + The type $\Nat$ of natural numbers is an h-set. \end{thm} \begin{proof} - We will show that $\Nat$ has decidable equality that is for all $x, y : \Nat$, we have $(x =_X y) + \neg (x =_X y)$. + We will show that $\Nat$ has decidable equality that is for all $x, y : \Nat$, we have $(x =_X y) + \neg (x =_X y)$. We proceed by induction on $x$ and case analysis on $y$. - - If $x = 0$ and $y = 0$, we take $\inl(\refl(0))$. If $x = 0$ and $y = \S(n)$, + + If $x = 0$ and $y = 0$, we take $\inl(\refl(0))$. If $x = 0$ and $y = \S(n)$, then by injectivity of the constructors we get $\neg (0 = \S (n))$. - - For the inductive step let $x = \S (n)$. If $y = 0$, we use injectivity of the constructors again. + + For the inductive step let $x = \S (n)$. If $y = 0$, we use injectivity of the constructors again. If $y = \S (m)$, using the induction hypothesis we may determine whether $(m = n)$ or $\neg(m = n)$ and proceed accordingly. \end{proof} -\section{H--Level of types of h--level $n$} +\section{H-Level of types of h-level $n$} + +In this section we show that the type of types of h-level $n$ is itself of h-level $n+1$. Formally, we may define the type: + $\HLevel(n) := \sum_{X : \type} \ \isofhlevel(n)(X)$ -We fix a type-theoretic universe $\Type$ closed under standard constructors. Define the type: - $\HLevel(n) := \sum_{X : \Type} \ \isofhlevel(n)(X)$ +In particular, we have $\prop = \HLevel(1)$ and $\set = \HLevel(2)$. \begin{thm}\label{thm:hleveln_of_hlevelSn} The type $\HLevel(n)$ is of h-level $n+1$. \end{thm} -\begin{lem}\label{Id_of_Sigma} - Let $P \colon \Type \to \hProp$ and let $(X, p), (X', p') : \sum_{X : \Type} P(X)$. Then: - $\idtype[\sum_{X : \Type} P(X)]{(X, p)}{(X', p')} \simeq \idtype{X}{X'} \enspace .$ +We start with a lemma that can be seen as a version of Univalence for propositions on the universe. + +\begin{lem}\label{lem:sig-id-h-prop} + Let $P : \type \to \prop$ and let $(X, p), (X', p') : \sum\limits_{X : \type} P(X)$. Then: + $\idtype{(X, p)}{(X', p')} \big) \simeq (\eqv{X}{X'})$ \end{lem} \begin{proof} We have: \begin{equation*}\begin{split} - \idtype[\sum_{X : \Type} P(X)]{(X, p)}{(X', p')} & \simeq \sum_{z : \idtype{X}{X'}} \idtype[P(X')]{z_!p}{p'} \\ - & \simeq \idtype{X}{X'} + \idtype{(X, p)}{(X', p')} & \simeq \sum_{z : \idtype{X}{X'}} \idtype{\trans{z}{p}}{p'} \\ + & \simeq \idtype{X}{X'} \\ + & \simeq (\eqv{X}{X'}), \end{split} \end{equation*} + where the first equivalence follows from the fact that a path in a $\sum$-type corresponds to a pair of paths: one in the base type, and one in the fiber; the second is an immediate consequence of $P(X')$ being an h-Prop; and the third is an application of the Univalence Axiom. \end{proof} \begin{proof}[Proof of \autoref{thm:hleveln_of_hlevelSn}] - Let $(X, p), (X', p') : \HLevel(n)$. We need to show that the type: - $\idtype[\sum_{X : \Type} \isofhlevel(n)(X)] {(X, p)}{(X', p')}$ - is of h-level $n$. Since for any natural number $n$ and any type $X$ the type: - $\isofhlevel(n)(X)$ - is an hProp, we may apply Lemma \ref{Id_of_Sigma} with $P := \isofhlevel \ n$. -In order to show that $\idtype{X}{X'}$ is of h-level $n$ we proceed as follows. -By the Univalence Axiom, it suffices to show that that $\eqv{X}{X'}$ is of h-level $n$. We have an inclusion: - $\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} - - -% Local Variables: -% mode: latex -% TeX-master: "main" -% End: + Let $(X, p), (X', p') : \HLevel(n)$. We need to show that the type $\idtype{(X, p)}{(X', p')}$ is of h-level $n$. Since for any natural number $n$ and any type $X$ the type: $\isofhlevel(n)(X)$ is an h-prop, we may apply \autoref{lem:sig-id-h-prop} with $P := \isofhlevel(n)$. Next we observe that it suffices to show that $X \rightarrow X'$ is of h-level $n$ because the projection: + $(\eqv{X}{X'} \hookrightarrow (X \rightarrow X').$ + is an inclusion (i.e. a map of h-level $1$). 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}