Merge pull request #1166 from mikeshulman/impred-trunc

fix exercise 3.15, close #1165

Author: mikeshulman

logic.tex

@@ -1217,12 +1217,16 @@ \section{Contractibility}
   Thus, under \LEM{}, the propositional truncation can be defined rather than taken as a separate type former.
 \end{ex}
 
-\begin{ex}\label{ex:impred-brck}
+\begin{ex}\label{ex:impred-brck}\ 
   \index{propositional!resizing}%
-  Show that if we assume propositional resizing as in \cref{subsec:prop-subsets}, then the type
-  \[\prd{P:\prop} \Parens{(A\to P)\to P}\]
-  has the same recursion principle as $\brck A$, \emph{with} the same judgmental computation rule.
-  Thus, we can also define the propositional truncation in this case.
+  \begin{enumerate}
+  \item Show that for any $A : \UU$, the type
+    \[\prd{P:\prop_{\UU}} \Parens{(A\to P)\to P}\]
+    has the same recursion principle as $\brck A$, at least relative to propositions in $\UU$, \emph{with} the same judgmental computation rule.
+  \item The type considered in the previous part does not lie in the same universe $\UU$, and its recursion principle only applies to propositions in $\UU$.
+    Show that if we assume propositional resizing, we can define a type that does lie in the same universe $\UU$ and satisfies the same recursion principle as $\brck A$, albeit with only a propositional computation rule.
+    Thus, we can also define the propositional truncation in this case.
+  \end{enumerate}
 \end{ex}
 
 \begin{ex}\label{ex:lem-impl-dn-commutes}