xca:map-induces-quotient

intro-uf.tex

@@ -3258,7 +3258,10 @@ \section{Predicates and subtypes}
   A \emph{injection into a type}\index{injection!into a type} $T$
   is a type $S$ together with an injection $f : S \to T$.%
   \glossary(Injinto){$\protect\Inj(T)$}{type of injections into $T$}
-  The type $S$ is called the \emph{underlying type} of the injection into $T$.
+  The type $S$ is called the \emph{underlying type} of the injection into $T$.%
+  \footnote{Instead of using this tedious phrase, we will simply call $S$
+  a `subtype' of $T$, if the injection is clear from the context.
+  The cautioning \cref{ft:caution-subtype} applies here as well.}
   Selecting a universe $\UU$ as a repository for such types $S$ allows
   us to introduce the type of injections into $T$ in $\UU$ as follows.
   \[
@@ -3885,6 +3888,26 @@ \subsection{Set quotients}
   $A \to (A \to \sum_{X:\UU}\mathrm{is}{n}\mathrm{Type})$.}
 \end{remark}
 
+\begin{xca}\label{xca:map-induces-quotient}
+Let $A$ and $B$ be types and $f:A\to B$ a function.
+The \emph{equivalence relation on $A$ induced by} $f$ is
+\index{equivalence relation!induced by map}
+given by 
+\[
+(a\mapsto(a'\mapsto\Trunc{f(a)\eqto f(a')})) : A\to (A\to\Prop).
+\]
+The corresponding \emph{quotient of $A$ induced by} $f$ is denoted by $A/f$.
+\index{quotient!induced by map}
+\glossary[A/f]{$A/f$}{quotient induced by $f:A\to B$}
+Now:
+\begin{enumerate}
+\item\label{it:inj-ind-settrunc-domain}
+If $f$ is injective, give an equivalence from $A/f$ to $\setTrunc{A}$;
+\item\label{it:surj-ind-equiv-codomain}
+If $B$ is a set and $f$ surjective, give an equivalence from $A/f$ to $B$.\qedhere
+\end{enumerate}
+\end{xca}
+
 \section{More on natural numbers}
 \label{sec:more-on-N}