include inverses and ap on id in lem:apcomp

group.tex

@@ -943,7 +943,7 @@ \section{Homomorphisms}
   f (g ^ {-1})     & = (f (g))^{-1}         && \text {for any $g : \USymG$},    \\
   f (g' \cdot g)   & =  f (g') \cdot  f (g) && \text {for any $g, g' : \USymG$}.
 \end{alignat*}
-The first one is true by definition, the second can be proved by induction on $g$, and the third one follows from \cref{lem:apcomp}.
+The first one is true by definition, the others follow from~\cref{lem:apcomp}.
 These three identities assert that the function $\ap k$ \emph{preserves}, in a certain sense, the operations provided by \cref{lem:idtypesgiveabstractgroups} that
 make up the abstract groups $\abstr(G)$ and $\abstr(H)$.
 In the traditional study of abstract groups, these three identities play an important role and entitle one to call the function $f$ a
@@ -3488,7 +3488,7 @@ \section{Semidirect products}
   Applying the definition of the map $\Phi$ in the proof of \cref{lem:isEq-pair=} to our three pairs, we see that it suffices to show that
   $\left( \apap g {\refl x} {q'} \right) \cdot \left( \apap g {\refl x} {q} \right) = \apap g {\refl x} {q' \cdot q}$, with $g$, as there, being the function $ g(x)(y) \defeq (x,y)$.
   By \cref{def:applfun2comp} it suffices to show that $\left( \ap {g(x)} {q'} \right) \cdot \left( \ap {g(x)} {q} \right) = \ap {g(x)} {(q' \cdot q)}$, which follows from
-  compatibility of $\ap {g(x)}$ with composition, as in \cref{lem:apcomp}.
+  compatibility of $\ap {g(x)}$ with composition, as in~\cref{lem:apcomp}.
 \end{proof}
 
 The lemma above will be applied mostly in the case where $x'$ and $x''$ are $x$, but if it had been stated only for that case, we would not have

intro-uf.tex

@@ -759,6 +759,13 @@ \section{Product types}
 \begin{construction}\label{lem:apcomp}
   Given a function $f:X\to Y$, and elements $x,x',x'':X$, and paths $p : x \eqto x'$ and $p' : x' \eqto x''$,
   we have an identification of type $\ap f (p' \cdot p) \eqto  \ap f (p') \cdot  \ap f (p)$.
+
+  Similarly, we have that $\ap f$ is compatible with path inverse
+  in that we have an identification of type
+  $\ap f(p^{-1}) \eqto  (\ap f (p))^{-1}$ for all $p : x \eqto x'$.
+
+  Finally, we have an identification of type $\ap \id (p) \eqto p$ for all
+  $p : x \eqto x'$.
 \end{construction}
 
 \begin{implementation}{lem:apcomp}
@@ -770,16 +777,12 @@ \section{Product types}
   $\ap f ( \refl x ) \cdot  \ap f ( \refl x )$
   are equal to $\refl { f(x) }$ by definition,
   so the identification $\refl {\refl { f(x) }}$ has the desired type.
-\end{implementation}
-
-In a similar way one shows that $\ap f$ is compatible with path inverse,
-by constructing an identification of type
-$\ap f(p^{-1}) \eqto  (\ap f (p))^{-1}$.
-One may also construct an identification of type $\ap \id (p) \eqto p$.
 
+  The other two parts of the construction are also easily done by induction on $p$.
+\end{implementation}
 
 \begin{xca}\label{xca:trp-ap}
-  Let $X$ be a type, and let $T(x)$ be a family of types parametrized by a variable $x:X$. Furthermore, let $A$ be a type, let $f:A\to X$ be a
+  Let $X$ be a type and $T(x)$ a family of types parametrized by a variable $x:X$. Furthermore, let $A$ be a type, let $f:A\to X$ be a
   function, let $a$ and $a'$ be elements of $A$, and let $p: a \eqto a'$ be a path.
   Verify that the two functions $\trp[T \circ f]{p}$ and $\trp[T]{\ap{f}(p)}$ are of type $T(f(a)) \to T(f(a'))$.
   Then construct an identification between them, i.e., construct an element of type $\trp[T \circ f]{p} \eqto \trp[T]{\ap{f}(p)}$.