SymmetryBook
SymmetryBook copied to clipboard
"principle"
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