fixes of \Sub and subtype in Ch3

Author: marcbezem

circle.tex

@@ -18,7 +18,7 @@ \chapter{The universal symmetry: the circle}
   The type $\Prop$ of propositions has the property that
 given any type $A$ a function $A\to\Prop$ provides exactly
 the same information as picking a subtype of $A$,
-see \cref{lem:Prop-Set-pointed-families}\ref{lem:Prop-families}.
+see \cref{def:subtype} and \cref{lem:Sub(T)=Inj(T)}.
 \end{enumerate}
 We are interested in symmetries, and so we should search for a type $X$
 which is so that given \emph{any} type $A$ the type of functions
@@ -648,15 +648,16 @@ \section{\Coverings}
 \cref{rem:diagram}.
 
 \begin{remark}\label{rem:subtype-diagram}
-Consider the left diagram below, where $i_1, i_2$
-are injections constituting $S$ as a subtype of $X$ and
-$T$ as a subtype of $Y$, respectively (see \cref{def:subtype}).\footnote{%
+Consider the left diagram below, where $i_1, i_2$ are injections 
+constituting $S$ as a subtype of $X$ and $T$ as a subtype of $Y$, respectively, in the sense of \cref{def:injtype}.\footnote{%
 To stress that a function is an injection we may decorate
-the $\to$ in its type with a hook: $\hookrightarrow$.}
+the $\to$ in its type with a hook: $\mono$.}
 This diagram represents the identity type $f\circ i_1 \eqto i_2\circ g$.
 Since $i_2$ is an injection, the type
-$\sum_{g:S\to T} (f\circ i_1 \eqto i_2\circ g)$ is a proposition.\footnote{%
-Use \cref{xca:prod-of-fibs} to see this.}
+$\sum_{g:S\to T} (f\circ i_1 \eqto i_2\circ g)$ is a proposition,\footnote{%
+Consider $\inv i_2(f(i_1(s)))$ for all $s:S$, 
+and then use \cref{xca:AC-in-TT}.}
+which may or may not be true. So, when is it true?
 \[
 \begin{tikzcd}
   X \ar[r,"f"]  & Y &&
@@ -667,8 +668,8 @@ \section{\Coverings}
 \]
 In the right diagram we depict the case
 in which $S$ is given by a predicate $P: X\to\Prop$
-and $T$ is given by a predicate $Q: Y\to\Prop$,
-with the injections being first projections of the right type.
+and $T$ by a predicate $Q: Y\to\Prop$,
+with the injections being first projections.
 We can now apply the universal property of subtypes
 \cref{xca:subtype-univ-prop} to $Y_Q$ with
 $(f\circ\fst) : X_P \to Y$ and get that the three propositions