SymmetryBook icon indicating copy to clipboard operation
SymmetryBook copied to clipboard

"principle"

Open DanGrayson opened this issue 4 years ago • 0 comments

This looks possibly unintentional:

diff --git a/intro-uf.tex b/intro-uf.tex
index 6a7033a..2966b09 100644
--- a/intro-uf.tex
+++ b/intro-uf.tex
@@ -3052,7 +3052,7 @@ $R : A \to A \to \Prop$,
 we define the \emph{quotient set}\footnote{%
   We may wonder about the universe level of $A/R$,
   assuming $A : \UU$ and $R : A \to A \to \Prop_\UU$.
-  By the Replacement Principle~\cref{pri:replacement},
+  By the Replacement~\cref{pri:replacement},
   $A/R$ is essentially $\UU$-small, since $A\to\Prop_\UU$
   is locally $\UU$-small. Alternatively, we could use
   Propositional Resizing~\cref{pri:prop-resizing} to push

DanGrayson avatar Jun 10 '21 14:06 DanGrayson