fields.tex

\chapter{Rings, fields and vector spaces}
\label{ch:fields}

In this chapter we will extend the hierarchy of algebraic structures from 
monoids (\cref{def:monoid}) and 
groups (\cref{def:typegroup}) to
rings (\cref{def:abstractring}),
fields (\cref{def:field}), and
vector spaces (\cref{def:vectorspace}).
Of all these structures there are several varieties, 
satisfying additional properties, such as 
abelian groups (\cref{sec:abelian-groups}),
non-trivial rings (\cref{def:non-trivial-ring}),
commutative rings (\cref{def:commutative-ring}),
....

Quotients; subspaces (= ?). Bases and so. Dual space; orthogonality. (all of this depends on good implementations of subobjects). Eigen-stuff. Characteristic polynomials; Hamilton-Cayley.

\section{Rings, abstract and concrete}\label{sec:rings}

A ring is an algebraic structure that consists of a group and a
monoid that share the same underlying set. The interaction between
the respective operations is governed by laws that are called
the distributivity laws. 
The standard example of a (commutative) ring 
is the ring with set of integers as underlying set, with addition as
group operation and multiplication as monoid operation.
Note that multiplication in a ring need not be commutative.\footnote{%
In contrast, in \cref{xca:ring-group-abelian} you are asked to prove
that the group of a ring is always abelian, as a consequence of the
extra structure and properties.} We start by defining rings abstractly.

\subsection{Abstract rings}\label{sec:abstrings}

We follow the convention that the group data of an abstract group
are denoted by $0,\,+,\,-$ and the monoid data by $1,\,\cdot\,$.

\begin{definition}\label{def:abstractring}
An \emph{abstract ring} $\mathscr R$ consists of an abstract group 
$(R,0,+,-)$ and a monoid $(R,1,\cdot)$ with the
same underlying set $R$. Moreover, the following equations should hold
for all $a,b,c : R$:
    \begin{enumerate}      %[ref=\ref{def:abstractring} (\alph*)]
    \item\label{ring:ldistr-law} $a \cdot (b + c) = a \cdot b + a \cdot c$ (the \emph{left distributive law})
    \item\label{ring:rdistr-law} $(a + b) \cdot  c = a \cdot c + b \cdot c$ (the \emph{right distributive law})
    \end{enumerate}
The latter two properties
are together denoted by $\mathrm{DistrLaws}(R,\cdot,+)$.

The abstract ring $\mathscr R$ is called \emph{non-trivial} if $0\neq 1$
and \emph{commutative} if its multiplication $\cdot$ is commutative, that is,
if $a\cdot b= b\cdot a$ for all $a,b:R$.
\end{definition}

The abstract group $(R,0,+,-)$ is called the \emph{(additive) group}
of $\mathscr R$, and the monoid $(R,1,\cdot)$ the 
\emph{(multiplicative) monoid} of $\mathscr R$.

\begin{definition}\label{def:typering}
The type of abstract rings is defined as\footnote{%
See \cref{not:GroupLaws} for the monoid laws.}
\begin{align*}
\typering\defeq 
\sum_{(R,0,+,-):\Group^{\abstr}} ~ &\sum_{e:R} ~ \sum_{\mu:R\to R\to R} \\
&\mathrm{MonoidLaws}(R,e,\mu)\times\mathrm{DistrLaws}(R,\mu,+).
\end{align*}
The type $\typecommring$ of commutative rings is similar to the type
of rings with the additional property $\prod_{a,b:R}\mu(a,b)=\mu(b,a)$. 
\end{definition}

\begin{xca}\label{xca:ring-group-abelian}
Let $\mathscr R$ be an abstract ring. Show that the additive group 
of $\mathscr R$ is abelian. Hint: elaborate $(a+1)\cdot(b+1)$.
\end{xca}

\begin{definition}\label{def:ringhom}
Let $\mathscr R,\mathscr S : \Ring$ be abstract rings, with
$\mathscr R$ consisting of an abstract group $\agp R$ with underlying set $R$
and a monoid $(R,1_R,\cdot_R)$, and 
$\mathscr S$ consisting of an abstract group $\agp S$ with underlying set $S$
and a monoid $(S,1_S,\cdot_S)$.
An \emph{abstract ring homomorphism} from $\mathscr R$ to $\mathscr S$ is an
abstract homomorphism $f:\absHom(\agp R,\agp S)$ that is a monoid homomorphism
from $(R,1_R,\cdot_R)$ to $(S,1_S,\cdot_S)$.
\end{definition}



\begin{example}\label{exa:ring-Z-polynomials}
We elaborate the abstract ring of polynomials with integer coefficients.
\MB{TBD}
\end{example}

\subsection{Mixed rings}\label{sec:mixring}

Here we explore a definition of a ring that is based
on a concrete group $G$ and left and right multiplications 
that are still half abstract. %Therefore we call them mixed rings.

We first note that, for any abstract ring $\mathscr R$ and elements $a,b:R$,
the left multiplication function $(a\cdot\blank)$ 
and the right multiplication function $(\blank\cdot b)$ are
abstract homomorphisms
of the additive group $(R,0,+,-)$ of $\mathscr R$ to itself.\footnote{%
    These functions provide two ways to write the product $a\cdot b$,
see the coherence law in \cref{def:mixring}\ref{mixring:lr-coherence-law}.}
There are two ways to compose them: $(a\cdot(\blank\cdot b))$
and $((a\cdot\blank)\cdot b)$. Equality of the latter two functions is
an elegant way of expressing associativity.
These observations lead to the following alternative definition of a ring.

\begin{definition}\label{def:mixring}
An \emph{mixed ring} $R$ consists of a group\footnote{%
It will follow as in \cref{xca:ring-group-abelian} that the group $R$
is abelian.} also denoted $R$ together with
a symmetry $1_R : \USymR$ and two maps $\ell,r: \USymR\to\Hom(R,R)$
from the set of symmetries in $R$ to the set of homomorphisms from
$R$ to $R$.\footnote{We call these rings ``mixed'' since they are
based on a concrete group $R$ and data referring to $\abstr(R)$.}
Given $g:\USymR$, we write $\ell_g$ for the homomorphism $\ell(g)$ and 
$r_g$ for $r(g)$.
Moreover, the following equations should hold.
    \begin{enumerate}
    \item\label{mixring:unit-laws} $\ell_{1_R} = \id_G = r_{1_R}$ (the \emph{multiplicative unit laws})
    \item\label{mixring:lr-coherence-law} $(\USym\ell_g)(h) = (\USymr_h)(g)$, 
    for all $g,h : \USymR$ (the \emph{coherence law})
        \item\label{mixring:assoc-law} $\ell\circ r= r\circ\ell$ (the \emph{associativity law})
    \end{enumerate}
%The properties \ref{mixring:unit-laws}-\ref{mixring:assoc-law} 
%are together denoted by $\RingProps(R,1_R,\ell,r)$.
The ring $R$ is called \emph{commutative} if $\ell=r$,
and \emph{non-trivial} if $1_R \neq \refl{R}$.
\end{definition}

The coherence law \ref{mixring:lr-coherence-law} allows us to abbreviate both 
$(\USym\ell_g)(h)$ and $(\USymr_h)(g)$ by $g\cdot h$. We will do this when
no confusion can occur. Then, $\ell=r$ 
amounts to $g\cdot h = h\cdot g$, for all $g,h : \USymG$,
as could be expected from the abstract case.

We proceed by giving the standard example of the integers as a ring
in the sense of \cref{def:mixring}.
\begin{example}
Consider the group $\ZZ$ classified by the circle.
Using the same notation $\ZZ$ also for the ring, take $1_\ZZ \defeq\Sloop$
and $\ell: (\base\eqto\base)\to\Hom(\ZZ,\ZZ)$ defined as follows.
For every $g:\base\eqto\base$, let $\ell_g$ be the homomorphism
classified by the map $\B\ell_g(\base)\defeq\base$, 
$\B\ell_g(\Sloop)\defis g$, and pointed by reflexivity.\footnote{%
The reader may recognize the degree $m$
map from \cref{def:mfoldS1cover} as a special case.}
Take $r\defeq\ell$. Now the unit laws, the coherence law and
the associativity law can easily be verified. It follows that
$(\ZZ,1_\ZZ,\ell,!)$ is a non-trivial commutative ring.
\end{example}

\begin{definition}\label{def:typemixring}
The type of rings is defined as
\[
\typering\defeq\sum_{R:\typegroup}\sum_{1_R:\USymR}\sum_{\ell,r:\USymR\to\Hom(R,R)} \RingProps(R,1_R,\ell,r).
\]
The type $\typecommring$ of commutative rings is similar to the type
of rings but with $\RingProps(R,1_R,\ell,r) \times(\ell=r)$. 
\end{definition}
% end wip

\begin{xca}\label{xca:Rmixring->URabstring}
Let $(R,1_r,\ell,r)$ be an mixed ring. 
Show that $\USymR$ is an abstract ring with
additive group $\abstr(R)$ and multiplicative 
monoid $(\USymR,1_R,\cdot)$. \MB{TBD}
\end{xca}

\subsection{Move to a better place (Ch.\ 11 or 2)}
\begin{marginfigure}
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  \pt_Y\ar[rr,eqr,"f_\pt"]\ar[ddrr,eql,"g_\pt"']
  \& \& f(\pt_X)  \ar[dd,eqr,"k(\pt_X)"]
  \\ \& \mbox{} \& \\
  \pt_Y\ar[uu,"{\jdeq}"']\ar[rr,eql,"g_\pt"']\ar[ddrr,eql,"h_\pt"']    
  \& \mbox{} \& g(\pt_X)\ar[dd,eqr,"k'(\pt_X)"]
  \\\& \mbox{} \& \\
 \&\& h(\pt_X)
  \end{tikzcd}
  \caption{\label{fig:ptd-homotopy-compo}
  Path for $(k'\cdot_{\protect\ptw} k)$.} 
\end{marginfigure}
\begin{definition}\label{def:ptd-homotopy-compo}
Let $X$ and $Y$ be pointed types and
$f,g: X\ptdto Y$ pointed maps from $X$ to $Y$.
Recall from \cref{con:identity-ptd-maps} the equivalence $\ptw_*$ of type 
$(f\eqto g) \equivto H(f,g)$, where 
\[ H(f,g) \defeq \sum_{k:\prod_{x:X}(f_\div(x)\eqto g_\div(x))}
                               ((k(\pt_X)\cdot f_\pt) \eqto g_\pt ).
\]

Assume also $h: X\ptdto Y$ and let $k: H(f,g)$ and 
$k': H(g,h)$. In line with the notation for pointed maps, 
we denote the pair $k$ by $(k_\div,k_\pt)$, an likewise for $k'$. 
Define the \emph{pointwise composition}
$(k'\cdot_{\ptw} k)$ of $k'$ and $k$ by\footnote{%
We use $k_\div$ to denote the first component of $k$,
as we do for non-dependent pointed maps, but we will often drop
this subscript ``$\div$''.
We use the notation ``$\cdot_{\ptw}$'' for pointwise composition
of $k$ and $k'$, as well as of $k_\div$ and $k'_\div$.}
\begin{align*}
\bigl(k'\cdot_{\ptw} k\bigr)&\defeq
\bigl(k'_\div\cdot_{\ptw} k_\div ~,~ 
       k'_\pt\cdot\ap{(k'_\div(\pt_X)\cdot\blank)}(k_\pt)\bigr),
\quad\text{where}\\
(k'_\div\cdot_{\ptw} k_\div) &\defeq (x\mapsto k'_\div(x)\cdot k_\div(x)).
\end{align*}
In \cref{fig:ptd-homotopy-compo}, the upper-right triangle represents
the type of $k_\pt$, the upper-left triangle is a reflexivity triangle,
the lower triangle represents the type of $k'_\pt$,
and the outer diagram represents the type 
$k'(\pt_X)\cdot k(\pt_X)\cdot f_\pt \eqto h_\pt$
of $k'_\pt\cdot\ap{(k'_\div(\pt_X)\cdot\blank)}(k_\pt)$.
Thus we see that $(k'\cdot_{\ptw} k)$ is an element of $H(f,h)$.
\end{definition}

\begin{construction}\label{con:ptd-homotopy-compo}
Let conditions be as in \cref{def:ptd-homotopy-compo}.
Let $p:(f\eqto g)$ and $q:(g\eqto h)$.
Then we have an identification of $\ptw_*(qp)$ with
$\ptw_*(q) \cdot_{\ptw} \ptw_*(p)$.
\end{construction}
\begin{implementation}{con:ptd-homotopy-compo}
By path induction on $q$, it suffices to construct an identification
of $\ptw_*(p)$ and $\ptw_*(\refl{g}) \cdot_{\ptw} \ptw_*(p)$.
Using \cref{con:identity-ptd-maps} and \cref{def:funext} we
can identify $\ptw_*(\refl{g})$ with the pair
$((x\mapsto\refl{g_\div(x)}),\refl{g_\pt)}$. 
For use in \cref{fig:ptd-homotopy-compo} we write the latter
pair as $(k'_\div,k'_\pt)$, noting that $h\jdeq g$ in this case.
Writing also $(k_\div,k_\pt)$ for $\ptw_*(p)$, the goal is to
identify $(k'\cdot_{\ptw} k)$ with $k$.
This identification is easily obtained by using
that $\refl{g(x)}\cdot r$ is definitionally equal to $r$,
for all $x:X$ and $r:f(x)\eqto g(x)$.
\end{implementation}

\begin{definition}\label{def:cst-ptd}
Let $A$ and $B$ be pointed types.
For any $b:B$ and $p:\pt_B\eqto b$, 
define the \emph{pointed constant map} $\cst{\ast}^A(b,p) : A\ptdto B$
\emph{at} $(b,p)$ by setting $\cst{\ast}^A(b,p)\defeq (\cst{b}^A,p)$.\footnote{%
Here $\cst{b}^A$ is from \cref{def:cst-map}.
We may omit superscripts $A$ if $A$ is clear from the context.}
Thus $\cst{\ast}^A$ is a function from $\sum_{x:B}(\pt_B\eqto x)$ to
$A\ptdto B$.\footnote{%
Of course, $\sum_{x:B}(\pt_B\eqto x)$ is contractible.
In \cref{def:O-functor} we will see why $\cst{\ast}^A$ is useful.}
\end{definition}

\begin{remark}\label{rem:loops-at-ptd-cst}
In case $f$ and $g$ in \cref{con:identity-ptd-maps} are both the point of
$X\ptdto Y$, \ie $f\jdeq g\jdeq\pt_{X\ptdto Y}\jdeq(\cst{\pt_Y},\refl{\pt_Y})$,
it is convenient to work with a minor variant of $\ptw_*$ of type 
$\loops({X\ptdto Y}) \equivto (X\ptdto\loops Y)$.
The latter type is obtained by definitional simplifications
and replacing $(h(\pt_X)\cdot \refl{\pt_Y})\eqto \refl{\pt_Y}$
in $H(\pt_{X\ptdto Y},\pt_{X\ptdto Y})$ from \cref{def:ptd-homotopy-compo}
by an equivalent type:\footnote{By laws of symmetry and right unit.}
\[ 
H(\pt_{X\ptdto Y},\pt_{X\ptdto Y}) \equivto 
\Bigl(\sum_{h:X\to\loops Y}(\refl{\pt_Y}\eqto h(\pt_X))\Bigr) \jdeq
(X\ptdto\loops Y).
\]
Abusing notations, we denote this variant also by $\ptw_*$.
\end{remark}


The following construction is useful since it
will allow us to simplify identifying two pointed maps
to identifying their underlying unpointed maps
in some important cases. The construction is based on BCFR which
in turn uses a result by Cavallo.

\begin{construction}\label{con:Id-(B->*A)}
Let $A$ be a pointed type and let $\ev: (\id_A\eqto\id_A)\to(\pt_A\eqto\pt_A)$
be the evaluation map that sends identifications $i:(\id_A\eqto\id_A)$ 
to paths $\ptw(i)(\pt_A) : (\pt_A\eqto\pt_A)$.
Furthermore, let  $s: (\pt_A\eqto\pt_A)\to(\id_A\eqto\id_A)$
be a section of $\ev$, that is, we are given
identifications $\ev(s(p))\eqto p$ for all $p:(\pt_A\eqto\pt_A)$.
Let also $B$ be a pointed type and consider pointed
maps $f,f' : B\ptdto A$ with underlying unpointed maps
$f_\div,f'_\div : B\to A$.

Then we have a map $(f_\div\eqto f'_\div)\to(f\eqto f')$.
\end{construction}

\begin{implementation}{con:Id-(B->*A)}
By path induction on $f_\div\eqto f'_\div$ we may take
$f_\div\jdeq f'_\div$, so that the goal is to identify\footnote{%
Henceforth we simply write $f$ for $f_\div$.}
$(f,f_\pt)$ with $(f,f'_\pt)$, 
for two paths $f_\pt,f'_\pt: (\pt_A\eqto f(\pt_B))$.

Define $r\defeq (f'_\pt\cdot\inv{f}_\pt) : (f(\pt_B)\eqto f(\pt_B))$.
By \cref{con:identity-ptd-maps}, it suffices to give
an element $h: \prod_{b:B}(f(b)\eqto f(b))$ and an identification
of $h(\pt_B)$ with $r$.
By path induction on $f_\pt$ we may take $\pt_A\jdeq f(\pt_B)$,
so that the domain of $s$ is $f(\pt_B)\eqto f(\pt_B)$,
and so $r$ is an element of this domain. 
Now take $h(b)\defeq \ptw(s(r))(f(b))$ for any $b:B$.
Then indeed $h(b):(f(b)\eqto f(b))$, and we can identify
$h(\pt_B)\jdeq \ptw(s(r))(f(\pt_B))\jdeq\ev(s(r))$ with $r$ 
since $s$ is a section of $\ev$.
\end{implementation}

\begin{construction}\label{con:ev-section-loopsA}
Let $A$ be a pointed type and $\loops A$ its pointed loop type.
We use $\pt$ for $\pt_A$ and $\rfl$ for $\refl{\pt_A}$.
Let $\ev: (\id_{\loops A}\eqto\id_{\loops A})\to (\rfl\eqto\rfl)$ 
be the evaluation map that sends $i:(\id_{\loops A}\eqto\id_{\loops A})$
to $\ptw(i)(\rfl)$. 
Then $\ev$ has a section, that is, a 
map $s: (\rfl\eqto\rfl)\to(\id_{\loops A}\eqto\id_{\loops A})$
with identifications $\ev(s(\alpha))\eqto\alpha$ for 
all $\alpha: (\rfl\eqto\rfl)$.
\end{construction}

\begin{implementation}{con:ev-section-loopsA}
Recall from \cref{def:funext} the equivalence $\ptw$ identifying
$\id_{\loops A}\eqto\id_{\loops A}$ with $\prod_{p:\loops A}(p\eqto p)$.
Since $(\rfl\cdot p)$ and $p$ are definitionally equal for any $p:\loops A$,
any $\alpha: (\rfl\eqto\rfl)$ gives a path 
$\ap{\blank\cdot p}(\alpha): (p\eqto p)$.\footnote{%
In a picture:
\[
  \begin{tikzcd}[ampersand replacement=\&,column sep=large]
  \rfl \ar[r,mapsto,"{\blank\cdot p}"]\ar[d,eql,"\alpha"']
  \& (\rfl\cdot p)  \ar[d,eqr,shift right=1em,"{\ap{\blank\cdot p}(\alpha)}"] \jdeq p
\\
  \rfl \ar[r,mapsto,"{\blank\cdot p}"]
  \& (\rfl\cdot p) \jdeq p
  \end{tikzcd}
\]
}
Taking $\rfl$ for $p$, $\ap{\blank\cdot \rfl}(\alpha)$
can be identified with $\alpha$.\footnote{%
As obvious as this may seem, it requires a generalization of
the type of $\alpha$ to enable path induction, and we delegate
this to \cref{xca:ev-section-loopsA}.} 
For any $\alpha: (\rfl\eqto\rfl)$ and $p:\loops A$,
define $s_\alpha$ by $s_\alpha(p)\defeq\ap{\blank\cdot p}(\alpha)$.
Then $\inv{\ptw}(s_\alpha):(\id_{\loops A}\eqto\id_{\loops A})$.
Hence 
\[
s\defeq(\alpha\mapsto\inv{\ptw}(s_\alpha)) : 
(\rfl\eqto\rfl)\to(\id_{\loops A}\eqto\id_{\loops A}),
\]
and we have 
$\ev(s(\alpha)) \jdeq \ptw(\inv{\ptw}(s_\alpha))(\rfl) \eqto \alpha$ 
by \cref{def:funext} and \cref{xca:ev-section-loopsA}.
\end{implementation}

\begin{exercise}\label{xca:ev-section-loopsA}
Given a type $A$ with elements $a,x:A$ and a path $q:a\eqto x$,
define $\rho_{q} : (q\cdot\refl{a}) \eqto q$ by induction on $q$.
For any $p:a\eqto a$ and $\beta:(p\eqto \refl{a})$,
define $i(\beta): \ap{\blank\cdot\refl{a}}(\beta) \eqto
\beta\cdot\rho_{p} $ by induction on $\beta$.
Now, give an identification of $\ap{\blank\cdot\refl{a}}(\alpha)$ and 
$\alpha$ for any $\alpha:(\refl{a}\eqto \refl{a})$.
\end{exercise}

\begin{corollary}\label{cor:Id-(B->*loopsA)}
The combination of \cref{con:Id-(B->*A)} and \cref{con:ev-section-loopsA}
yields a function from $(f_\div\eqto f'_\div)$ to $(f\eqto f')$ for all pointed
maps $f,f' : B\ptdto \loops A$.
\end{corollary}

Recall $\loops$ from \cref{def:looptype} and \cref{def:loops-map},
which together form a wild functor $\UUp\to\UUp$, \cf \cref{sec:naturality}. 
In the following we will define a closely related
wild functor that is sometimes easier to use.

\begin{definition}\label{def:O-functor}
For any pointed type $A$, define $\OO A \defeq (\Sc\ptdto A)$.
Let $A$ and $B$ be pointed types and let $f: A\ptdto B$ be a pointed map.
Define $\OO(f):\OO A\ptdto \OO B$ to be composition with $f$,
that is, for $g:(\Sc\ptdto A)$, $\OO(f)(g)\defeq(f\circ g):(\Sc\ptdto B)$.%
\footnote{Here we mean composition as pointed maps,
so that the pointing path $\OO(f)(g)_\pt$ is defined in 
\cref{def:pointedtypes} as $f(g_\pt)\cdot f_\pt$.}
We point $\OO(f)$ as follows. First, observe that
$\pt_{\OO B}\jdeq\pt_{\Sc\ptdto B}\jdeq(\cst{\pt_B},\refl{\pt_B})$ and
$\OO(\pt_{\OO A})\jdeq f\circ\pt_{\OO A}\jdeq (\cst{f(\pt_A)},f_\pt)$.
So both $\pt_{\OO B}$ and $\OO(\pt_{\OO A})$ are images of
$\cst{\ast}^\Sc$, and we can obtain a path between them 
by applying $\cst{\ast}^\Sc$ to the unique path $(f_\pt,\rho_{f_\pt})$
between $(\pt_B,\refl{\pt_B})$ and $(f(\pt_A),f_\pt)$ 
in the contractible type $\sum_{x:B}(\pt_B\eqto x)$.\footnote{%
Here $\rho_{f_\pt} : f_\pt \cdot \refl{\pt_B} \eqto f_\pt$
is defined by induction on $f_\pt$, 
setting $\rho_{\refl{\pt_B}}\defeq\refl{\refl{\pt_B}}$.
}
The situation is illustrated in the diagram below and we define 
$\OO(f)_\pt\defeq\ap{\cst{\ast}}(f_\pt,\rho_{f_\pt})$.
\end{definition}
\[
\begin{tikzcd}[ampersand replacement=\&,column sep=small]
   (\pt_B,\refl{\pt_B})
    \ar[r,mapsto,"{\cst{\ast}}"]
    \ar[d,eql,"{(f_\pt,\rho_{f_\pt})}"']
  \& (\cst{\pt_B},\refl{\pt_B})\jdeq\pt_{\OO B}
    \ar[d,eqr,"{\ap{\cst{\ast}}(f_\pt,\rho_{f_\pt})}"]
\\
  (f(\pt_A),f_\pt)
    \ar[r,mapsto,"{\cst{\ast}}"] 
  \& (\cst{f(\pt_A)},f_\pt)\jdeq\OO(\pt_{\OO A})
  \end{tikzcd}
\]
Note that $\OO(f)_\pt$ is a reflexivity path if $f_\pt\jdeq\refl{\pt_B}$.
\begin{xca}\label{xca:O-functor}
Complete the structure of $\OO$ as a wild functor, \cf \cref{sec:naturality}.
Identify $\OO(f)_\pt$ with $\inv{\ptw_*}(\cst{f_\pt},\rho_{f_\pt})$.
\end{xca}


\begin{remark}\label{rem:pointing-ev}
Given a pointed type $A$, recall from \cref{cor:circle-loopspace}
the equivalence $\ev_A$ from $\Sc\ptdto A$ to $\loops{A}$.
This equivalence sends $f:\Sc\ptdto A$ to $\loops(f)(\Sloop)\jdeq
\inv{f_\pt}\cdot f(\Sloop)\cdot f_\pt$, and the
inverse $\inv{\ev}_A$ sends $p:\loops{A}$ to the pointed map
$f:\Sc\ptdto A$ defined by  $f(\base)\defeq\pt_A$ and $f(\Sloop)\defis p$,
pointed by reflexivity.\footnote{When $A$ is clear from the context 
we may simply write $\ev$. Similarly for $\varepsilon_A$ defined next.}

The equivalence $\ev_A$ can itself be
pointed as follows. The point of $\Sc\ptdto A$ is the constant map 
$\cst{\pt_A}$, pointed by reflexivity, which is sent by $\ev_A$ 
to $\cst{\pt_A}(\Sloop)\cdot \refl{\pt_A}$.\footnote{%
Recall that reflexivity paths cancel definitionally on the left.} Define 
$\varepsilon_A(p): \refl{\pt_A} \eqto (\cst{\pt_A}(p)\cdot\refl{\pt_A})$,
for any $z:\Sc$, $p:\base\eqto z$, by path induction, setting
$\varepsilon_A(\refl{\base})\defeq \refl{\refl{\pt_A}}$.\footnote{%
Note that $\cst{\pt_A}(p):\loops A$ for any $p$.} 
Now we define $(\ev_A)_\pt \defeq \varepsilon_A(\Sloop)$.
\end{remark}

The following construction shows that $\loops$
corresponds to $\OO$ from \cref{def:O-functor} under the equivalences $\ev$,
as illustrated in \cref{fig:Omega-O}.\footnote{\MB{$\ev_\blank$ is an example
of a wild natural equivalence between the wild functors
$\loops, \Sc\blank : \UUp\ptdto\UUp$, cf.\ \cref{ch:cats}.}}


\begin{marginfigure}
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  \OO A\ar[rr,"\OO(f)"]\ar[dd,equivl,"\ev_A"']
  \& \&\OO B  \ar[dd,equivr,"\ev_B"]
  \\ \& \mbox{} \& \\
  \loops{A}\ar[rr,"\loops(f)"'] \& \& \loops{B}
  \end{tikzcd}
  \caption{\label{fig:Omega-O} $\loops(f)$ and $\protect\OO(f)$ correspond.} 
\end{marginfigure}


\begin{construction}\label{con:Omega-O}
Let $A$ and $B$ be pointed types and 
let $f: A\ptdto B$ be a pointed map.
Then we have an identification of $\loops(f)\circ \ev_A$ 
and ${\ev_B} \circ {\OO(f)}$, as represented by \cref{fig:Omega-O}.
Consequently, we have that $e\defeq(\inv{\ev_B}\circ{{\blank}\circ\ev_A})$
is an equivalence of type 
$(\loops A\ptdto\loops B)\equivto(\OO A\ptdto\OO B)$,
and $\OO \eqto (e\circ \loops)$. 
\end{construction}

\begin{figure}
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  (\Sc\ptdto A)\ar[rr,"\ev_A"]
  \& \& \loops A \ar[rr,"{\loops(f)}"]
  \& \& \loops B 
  \\ 
  (p,p_\pt)\ar[rr,mapsto]
  \& \& \inv{p_\pt}\cdot p(\Sloop)\cdot p_\pt \ar[rr,mapsto]
  \& \& \inv{f_\pt}\cdot f(\inv{p_\pt}\cdot p(\Sloop)\cdot p_\pt)\cdot f_\pt
   \quad (1)
  \\
  (\Sc\ptdto A)\ar[rr,"\OO(f)"]
  \& \& (\Sc\ptdto B) \ar[rr,"{\ev_B}"]
  \& \& \loops B
  \\ 
  (p,p_\pt)\ar[rr,mapsto]
  \& \& (f\circ p,f(p_\pt)\cdot f_\pt) \ar[rr,mapsto]
  \& \& \inv{(f(p_\pt)\cdot f_\pt)}\cdot (f\circ p)(\Sloop)
  \cdot (f(p_\pt)\cdot f_\pt)  \quad (2)
  \end{tikzcd}
  \caption{\label{fig:Omega-O-elab} 
  Elaborating the two composites $(\Sc\ptdto A)\to\loops B$.} 
\end{figure}


\begin{implementation}{con:Omega-O}
We will apply \cref{con:identity-ptd-maps}.
Elaborating the situation in \cref{fig:Omega-O-elab}, we have to identify
$(1)\jdeq \inv{f_\pt}\cdot f(\inv{p_\pt}\cdot p(\Sloop)\cdot p_\pt)\cdot f_\pt$
and $(2)\jdeq \inv{(f(p_\pt)\cdot f_\pt)}\cdot (f\circ p)(\Sloop)
\cdot (f(p_\pt)\cdot f_\pt)$ by a path $i(f,f_\pt)(p,p_\pt)$, 
for all $(p,p_\pt)$.\footnote{We often leave out the ``$\ap{\blank}$'s''.}
Moreover, we must fill the following triangle:
\[
\begin{tikzcd}[ampersand replacement=\&,row sep=tiny]
  \& \&\inv{f_\pt}\cdot f(\cst{\pt_A}(\Sloop)\cdot \refl{\pt_A})\cdot f_\pt  \ar[dddd,eqr,"{i(f,f_\pt)(\cst{\pt_A},\refl{\pt_A})}"]
\\
  \&\inv{f_\pt}\cdot f_\pt
   \ar[ru,eqr,"{\loops(f)((\ev_A)_\pt)}"]
\\
  \refl{\pt_B}
  \ar[rd,eql,"{(\ev_B)_\pt}"'] 
  \ar[ru,eqr,"{\loops(f)_{\pt}}"]
\\
 \&\cst{\pt_B}(\Sloop)\cdot\refl{\pt_B}
    \ar[rd,eql,"{\ev_B(\OO(f)_\pt)}"']  
\\
 \& \&\inv{f_\pt}\cdot \cst{f(\pt_A)}(\Sloop)\cdot f_\pt 
\end{tikzcd}
\]
For defining $i(f)(p,p_\pt)$ we apply path induction on $p_\pt$ and on $f_\pt$,
setting $\pt_A\jdeq p(\base)$ and $p_\pt\jdeq \refl{p(\base)}$,
as well as  $\pt_B\jdeq f(\pt_A)\jdeq f(p(\base))$ and
$f_\pt\jdeq \refl{f(p(\base))}$. Then identifying (1) and (2)
reduces to the task of identifying 
$f(p(\Sloop)\cdot \refl{p(\base)})\cdot \refl{f(p(\base))}$ and 
$(f\circ p)(\Sloop)\cdot \refl{f(p(\base))}$.

The latter identity type stays well typed when we replace
$\Sloop$ by an arbitrary $g:\base\eqto z$, $z:\Sc$. 
By induction on $g$, we define an element
\[
\iota(f,p,g) :
\bigl((f(p(g)\cdot \refl{p(\base)})\cdot \refl{f(p(\base))})
\eqto %_{f(p(\base)) \eqto f(p(z))}
((f\circ p)(g)\cdot \refl{f(p(\base))})\bigr),
\]
setting $\iota(f,p,\refl{\base})\defeq\refl{\refl{f(p(\base))}}$.
We complete the definition of $i(f,f_\pt)(p,p_\pt)$ by setting
$i(f,\refl{f(p(\base))})(p,\refl{p(\base)})\defeq\iota(f,p,\Sloop)$.

Again applying path induction on $f_\pt$, assuming 
that $\pt_B\jdeq f(\pt_A)$ and $f_\pt \jdeq \refl{\pt_B}$, 
the triangle above reduces to the following triangle:
\[
\begin{tikzcd}[ampersand replacement=\&,row sep=tiny]
  \& \&f(\cst{\pt_A}(\Sloop)\cdot \refl{\pt_A})\cdot \refl{\pt_B}  
   \ar[dddd,eqr,"{i(f,\refl{f(\pt_A)})(\cst{\pt_A},\refl{\pt_A})}"]
\\
  \& \refl{\pt_B}
   \ar[ru,eqr,"{\loops(f)((\ev_A)_\pt)}"]
\\
  \refl{\pt_B}
   \ar[rd,eql,"{(\ev_B)_\pt}"'] 
   \ar[ru,eqr,"{\refl{\refl{\pt_B}}}"]
\\
 \&\cst{\pt_B}(\Sloop)\cdot\refl{\pt_B}
    \ar[rd,eql,"{\ev_B(\OO(f)_\pt)}"']  
\\
 \& \&\cst{\pt_B}(\Sloop)\cdot \refl{\pt_B} 
\end{tikzcd}
\]
Note that $i(f,\refl{f(\pt_A)})(\cst{\pt_A},\refl{\pt_A})\jdeq
\iota(f,\cst{\pt_A},\Sloop)$. By \cref{def:O-functor}, as $f_\pt$ is
a reflexivity path, we get that $\OO(f)_\pt$ and $\ev_B(\OO(f)_\pt)$ are
also reflexivity paths. Hence, recalling \cref{rem:pointing-ev} for 
the pointing paths $(\ev_A)_\pt$, $(\ev_B)_\pt$, 
we have to fill the following triangle:
\[
\begin{tikzcd}[ampersand replacement=\&,row sep=small,column sep=large]
  \&f(\cst{\pt_A}(\Sloop)\cdot \refl{\pt_A})\cdot \refl{\pt_B}  
  \ar[dd,eqr,"{\iota(f,\cst{\pt_A},\Sloop)}"]
 \\
\refl{\pt_B}
   \ar[ru,eqr,"{\loops(f)(\varepsilon_A(\Sloop))}"]
   \ar[rd,eql,"{\varepsilon_B(\Sloop)}"'] 
\\
  \&\cst{\pt_B}(\Sloop)\cdot \refl{\pt_B} 
\end{tikzcd}
\]
This last triangle stays well typed when we replace
$\Sloop$ by an arbitrary $g:\base\eqto z$, $z:\Sc$.\footnote{
$\varepsilon_A(g) : \refl{\pt_A}\eqto \cst{\pt_A}(g)\cdot\refl{\pt_A}$,
so $\loops(f)(\varepsilon_A(g))$ is a path from 
$\loops(f)(\refl{\pt_A})\jdeq \refl{\pt_B}$ to 
$\loops(f)(\cst{\pt_A}(g)\cdot\refl{\pt_A}) \jdeq
f(\cst{\pt_A}(g)\cdot \refl{\pt_A})\cdot \refl{\pt_B}$, by the induction
on $f_\pt$. Also, $\iota(f,\cst{\pt_A},g)$ has the right type.} 
Then apply induction on $g$, setting $g\jdeq\refl{\base}$,
which boils down to the same triangle with $\Sloop$ replaced by $\refl{\base}$.
The whole diagram has now become a reflexivity diagram,
as also $\iota(f,\cst{\pt_A},\refl{\base})$ is reflexivity by definition, 
and we are done.
\end{implementation}


Composition with $\OO$, \ie $(\OO\circ\blank)\defeq(q\mapsto \OO\circ q)$,
gives the map\footnote{
This map corresponds to a map of type
$\loops(X\ptdto Y) \to \loops(\loops X\ptdto \loops Y)$.} 
\[
(\OO\circ\blank): (\Sc\ptdto(A\ptdto B))\to
(\Sc\to((\Sc\ptdto A)\ptdto(\Sc\ptdto B)).
\]

\begin{construction}\label{con:swap-ptd-doms}
Let $X$, $Y$ and $Z$ be pointed types. We use $T_\div$ to
denote the underlying type of a pointed type $T$.
Then we have a pointed equivalence 
\[
\swap: (X\ptdto (Y\ptdto Z)) \ptdto (Y\ptdto (X\ptdto Z))
\] 
such that the totally unpointed map $\swap_{\div\div}$, defined by
\begin{align*}
\swap_{\div\div}&\defeq (f\mapsto(y\mapsto (x\mapsto f(x)(y)))) \\
 &:~(X_\div\to (Y_\div\to Z_\div))\to(Y_\div\to (X_\div\to Z_\div))
\end{align*}
can be identified with the map swapping the two arguments of any input map. 
\end{construction}
\begin{implementation}{con:swap-ptd-doms}
\MB{TBD} (Do first the equivalence of $(X\ptdto (Y\ptdto Z))$
with the sum type of totally unpointed maps with additional structure,
including coherence.)
\end{implementation}

\begin{xca}\label{xca:allptd-S1-contractible}
Let $X,Y,Z$ be pointed types and let $X,Y$ be connected
and $Z$ a $1$-type.
Show that $X\ptdto(Y\ptdto Z)$ is contractible.
\end{xca}

\begin{example}\label{exa:allS1*-swap}
In this example we will explore the type $$M\defeq(\Sc\ptdto(\Sc\ptdto\BB\ZZ)),$$
where $\BB\ZZ$ is the simply connected $2$-type $\sum_{X:\UU}\setTrunc{\Sc\eqto X}$
from \cref{sec:abelian-groups}, pointed at 
$\pt\defeq(\Sc,\settrunc{\refl{\Sc}})$. 

There are several ways to see that $\loops(\BB\ZZ) \jdeq (\pt=\pt,\refl{\pt})$
is equivalent to $\B\ZZ \jdeq \Sc$. One is to use
\cref{thm:abelian-groups-weq-sc2types}, as $\ZZ$ is abelian.
Another is to
recall from the proof of
\cref{lemma:universal-cover-simply-connected} the equivalence
between $\pt\eqto\pt$ and the component of $\Sc\eqto\Sc$ at $\id_\Sc$.%
\footnote{We use $\refl{\pt}$ and $\id_\Sc$ interchangeably.}
The latter component is equivalent to $\Sc$ by 
\cref{xca:(S1->S1)_(f)-eqv-S1}. Using $\ev$ from \cref{rem:pointing-ev},
it follows that $M$ is equivalent to $\loops\loops(\BB\ZZ)$ 
and hence to $\zet$.

Via the above equivalence between $\loops(\BB\ZZ)$ and $\Sc$, 
combined with the equivalence $\ptw_*$ from \cref{con:identity-ptd-maps},
we get an equivalence between $\loops(\Sc\ptdto\BB\ZZ)$ and $\Sc\ptdto\Sc$.
This means that we have maps corresponding to the degree $k$ map $\dg{k}$
in $\loops(\Sc\ptdto\BB\ZZ)$, for any $k>0$. We will need such maps for
all $k:\zet$ and define them explicitly in the following paragraph.


For any $k:\zet$, define $\dg{k}': \Sc\ptdto\loops(\BB\ZZ)$ by 
$\dg{k}'(\base)\defeq\id_\Sc$, taking for $\dg{k}'(\Sloop)$
the $k$-loop around $\id_\Sc$ given by function extensionality and
$\Sloop^k:\base\eqto\base$ (the loop case is a true proposition).
We point $\dg{k}'$ by reflexivity.

Now let $k:\zet$ and define $m_k:M$ as follows:
\begin{align*}
m_k(\base) &\defeq\pt_{\Sc\ptdto\BB\ZZ}\jdeq(\cst{\pt},\refl{\pt}) \\
m_k(\Sloop) &\defis\ptw_*^{-1} (\dg{k}') :\loops(\Sc\ptdto\BB\ZZ)\\
(m_k)_\pt &\defeq\refl{\pt_{\Sc\ptdto\BB\ZZ}}
\end{align*}
We see that applying $\ptw_*(m_k(\Sloop))=\dg{k}'$ to $\Sloop^j$ 
gives the $jk$-loop around $\id_\Sc$.
Also, using \cref{con:ptd-homotopy-compo}, 
applying $\ptw_*(m_k(\Sloop^i))$ to $\Sloop^j$ 
gives the $ijk$-loop around $\id_\Sc$.

\MB{TBD1}: clarify the relation between $m_k$ and multiplication of
its arguments by $k$ ($m_1$ is useful for the concrete ring of the integers).

\MB{TBD2}: Find out if $\swap(m_k)$ is equal to $m_k$ or to $m_{-k}$.
\end{example}

\begin{remark}\label{rem:grpHomOK}
\newcommand{\redloops}[1]{\inred{\loops{#1}}}
In \cref{fig:ulrik}, $X$ and $Y$ are pointed types,
and $\ptw_*$ is from \cref{rem:loops-at-ptd-cst}.
%Recall \cref{def:looptype} for $\loops$ applied to types.
The three occurrences of $\loops$ in the labels of the
downward arrows are all instances of \cref{def:loops-map}.
In \cref{fig:ulrik}, we have colored occurrences of 
$\loops$ that come from the $\loops$ in the left upper corner.
Note that $\redloops{}$ shifts position from first to 
second along the arrow labelled $(i\circ\blank)$,
where $i\defeq (q:\loops{}^2 Y \mapsto \inv q)$.

\begin{marginfigure}
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  \redloops(X\ptdto Y)\ar[rr,equivr,"{\ptw_*}"]\ar[dd,"{\redloops{}(\loops)}"']
  \& \& X\ptdto \redloops{} Y  \ar[dd,"{\loops{}}"]
  \\ \& \mbox{} \& \\
  \redloops{}(\loops X\ptdto \loops Y) \ar[dd,equivl,"{\ptw_*}"']   
  \& \mbox{} \& \loops X\ptdto \loops \redloops{} Y
                 \ar[lldd,equivr,"{(i\circ\blank)}"]
  \\ \& \mbox{} \& \\
  \loops X\ptdto \redloops{}\loops Y  
  \end{tikzcd}
  \caption{\label{fig:ulrik}Complete and fill!} 
\end{marginfigure}

In order to formally define $\redloops(\loops)$, we need
to define the pointing path $\loops_\pt$ of $\loops$.
Note that $\pt_{X\ptdto Y} \jdeq (\cst{\pt_Y},\refl{\pt_Y})$,
\ie the point of $X\ptdto Y$ is the constant map 
$x\mapsto\pt_Y$ pointed by reflexivity.
Likewise, the point of $\loops X\ptdto \loops Y$ is the pointed constant 
map $(\cst{\refl{\pt_Y}},\refl{\refl{\pt_Y}})$.
We want a path $\loops_\pt$ of type
$(\cst{\refl{\pt_Y}},\refl{\refl{\pt_Y}}) \eqto 
\loops(\cst{\pt_Y},\refl{\pt_Y})$, where\footnote{%
Recall that $\loops(f)$ is pointed by path algebra
identifying $\refl{\pt_Y}$ with $\inv f_\pt\cdot\refl{\pt_Y}\cdot f_\pt$, by
induction on $f_\pt$.}
\[
\loops(\cst{\pt_Y},\refl{\pt_Y}) \jdeq
(p\mapsto \ap{\cst{\pt_Y}}(p) \cdot \refl{\pt_Y},\refl{\refl{\pt_Y}}).
\]
By induction on $p:(\pt_X\eqto x)$, define
$h(p): \refl{\pt_Y} \eqto (\ap{\cst{\pt_Y}}(p)\cdot \refl{\pt_Y})$
setting $h(\refl{\pt_X})\defeq \refl{\refl{\pt_Y}}$.
Applying $\ptw_*$ we can now define
\[
\loops_\pt \defeq \inv{\ptw}_*(h,\refl{\refl{\refl{\pt_Y}}}):
\bigl((\cst{\refl{\pt_Y}},\refl{\refl{\pt_Y}}) \eqto 
\loops(\cst{\pt_Y},\refl{\pt_Y})\bigr).
\]
Now we can state the definition of $\redloops{}(\loops)$:
\[
\redloops{}(\loops)(q) \jdeq
\inv{\loops{}}_\pt \cdot \ap{\loops}(q) \cdot \loops_\pt
\quad\text{for all $q:\loops(X\ptdto Y)$}.
\]
 
We want to fill the diagram in \cref{fig:ulrik}
in full generality, even though we will only need it
for $X$ a pointed $1$-type and $Y$ a pointed $2$-type.\footnote{%
Then $p=_{\loops X}p'$ and $q=_{{\loops}^2 Y}q'$ are proof-irrelevant.}
\MB{TODO: Elaborate the composites,
and identify their first components, then using \cref{cor:Id-(B->*loopsA)}.}
\end{remark}

\begin{definition}\label{def:O'}
Let $A$ and $B$ be pointed types. Define the map
map $O'_{A,B}: ((A\ptdto B)\ptdto((\Sc\ptdto A)\ptdto(\Sc\ptdto B))$
by $O'_{A,B}\defeq (\OO_{A,B} \circ\inv{\swap}\circ\blank)$.\footnote{%
Again, we often write $O'$ for $O'_{A,B}$.} 
 \end{definition}

\begin{marginfigure}
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  \OO(X\ptdto Y)\ar[rr,equivr,"\swap"] \ar[dd,equivl,"{\ev}"']
  \& \& X\ptdto \OO Y \ar[dd,equivr,"{{\ev}\circ{\blank}}"]
  \\ \& \mbox{} \& \\
  \loops(X\ptdto Y)\ar[rr,equivl,"\ptw_*"'] \& \& X\ptdto \loops Y 
  \end{tikzcd}
  \caption{\label{fig:ptw-swap-ptd-doms} 
  $\swap$ and $\protect\ptw_*$ correspond.} 
\end{marginfigure}

\begin{construction}\label{con:ptw-swap-ptd-doms}
Let $X$ and $Y$ be pointed types and 
consider the equivalences $\ptw_*: \loops(X\ptdto Y) \to (X\ptdto \loops Y)$
from \cref{rem:loops-at-ptd-cst}, $\swap$ from \cref{con:swap-ptd-doms},
and $\ev$ from \cref{rem:pointing-ev}. 
Then we have an identification of $\ev\circ\swap(\blank)$ 
and $(\ptw_*\circ\ev)$, as represented by \cref{fig:ptw-swap-ptd-doms}.
\end{construction}
\begin{implementation}{con:ptw-swap-ptd-doms}
Using function extensionality, it suffices to identify ${\ev}\circ{\swap(f)}$
and $(\ptw_*\circ\ev)(f)$ for every $f:\Sc\ptdto(X\ptdto Y)$. The latter
identification is in the type $X\ptdto\loops Y$, which means that we only 
have to identify the underlying functions, due to \cref{cor:Id-(B->*loopsA)}.
This greatly simplifies our task: given $f:\Sc\ptdto(X\ptdto Y)$,
the pointing path of $\swap(f)$ plays no role in 
the underlying function of $\ev\circ{\swap(f)}$.
In contrast, the pointing path $f_\pt: \pt_{X\ptdto Y} \eqto f(\base)$
is important, but only in so far it applies to the underlying functions
of $\pt_{X\ptdto Y}$ and $f(\base)$. Therefore we abbreviate
$f'_\pt \defeq \ptw(\fst(f_\pt))$, so that 
$f'_\pt(x): (\pt_Y \eqto f(\base)(x))$ for $x:X$.

The underlying function of $\swap(f)$ maps any $x:X$ to the 
function $(z:\Sc)\mapsto f(z)(x)$, pointed by $f'_\pt(x)$.
Evaluating this pointed map at $\Sloop$ gives
$({\ev}\circ{\swap(f)})(x) \jdeq 
\inv{f'_\pt(x)}\cdot f(\Sloop)(x)\cdot f'_\pt(x)$.\footnote{%
Here $f(\Sloop)(x)$ is short for $\ap{z\mapsto\fst(f_\div(z))(x)}(\Sloop)$.}
This is the result of going first right and then down in
\cref{fig:ptw-swap-ptd-doms}, applied to $x:X$.

Now we go first down and then right in \cref{fig:ptw-swap-ptd-doms}.
Evaluating $f$ as above at $\Sloop$ gives
$\ev(f) \jdeq \inv{f}_\pt\cdot f(\Sloop)\cdot f_\pt$.
Applying $\ptw_*$ and taking the underlying function gives
$\ptw(\fst(\inv{f}_\pt\cdot f(\Sloop)\cdot f_\pt))$.
Applying the latter function to $x:X$ gives a result
that is easily identified with 
$\inv{f'_\pt(x)}\cdot \ptw(\fst(f(\Sloop)))(x)\cdot f'_\pt(x)$,
as both $\fst$ and $\ptw$ preserve composition.\footnote{%
Here $\ptw(\fst(f(\Sloop)))(x)$ is in fact 
$\ptw(\fst(\ap{f_\div}(\Sloop)))(x)$.}

Finally, we complete the construction by identifying the results
of the last two paragraphs, for which it suffices to identify
the elements as given in the footnotes. We generalize them from $\Sloop$
to an arbitrary $p:\base\eqto z$, $z:\Sc$, and note that both
$\ap{z\mapsto\fst(f_\div(z))(x)}(p)$ and
$\ptw(\fst(\ap{f_\div}(p)))(x)$ have type
$\fst(f_\div(\base))(x) \eqto \fst(f_\div(z))(x)$,
and are readily identified by induction on $p$. 
\end{implementation}

\def\Scc{\inred{\Sc}}
\begin{figure}[h]
  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
  \USym{\grpHom(H,G)}\ar[dd,equivl,"{\inv{\ev}}"']
  \\ \& \mbox{} \& \\
  \Scc(X\ptdto Y)
    \ar[rr,equivr,"{\swap_{\Scc,X}}"]
    \ar[dd,"{\OO\circ\blank}"']
  \& \& X\ptdto \Scc Y  
    \ar[dd,"{O'}"] \ar[drr,equivl,"{\OO}"']
    %\ar[rr,equivr,"{(\ev\circ\blank)}"]
  %\& \& \BHom(H,G) 
  \\ 
  \&\&\&\& \sum_{f:\Sc X \ptdto \Sc (\Scc Y)} P(f)
    \ar[rr,equivl]
    \ar[d,"{\fst}"]
  \& \& \absHom(\abstr(H),\abstr(G))
  \\
  \Scc(\Sc X\ptdto \Sc Y) 
    \ar[rr,equivl,"{\swap_{\Scc,\Sc X}}"']   
  \& \& \Sc X \ptdto \Scc (\Sc Y) 
    \ar[rr,equivl,"{(\swap\circ\blank)}"']
  \& \& \Sc X \ptdto \Sc (\Scc Y) 
  \end{tikzcd}
  \caption{\label{fig:bjørn}
  Legenda:
  $X\defeq\BH$;
  $Y\defeq\protect\BB G$;
  $\protect\ev$ is from \cref{cor:circle-loopspace};
  $\swap$ is from \cref{con:ptw-swap-ptd-doms};
  $\protect\OO$ is from \cref{def:O-functor};
  $O'$ is from \cref{def:O'};
  $P(f)$ expresses that $\protect\ev\circ f\circ \inv{\protect\ev}$
  classifies a homomorphism.
  Moreover, the colors track
  related occurrences of $\Sc$.
  }
\end{figure}

Recall from \cref{thm:abelian-groups-weq-sc2types} the equivalence
$\BB$ from the type of abelian groups to the type of pointed
simply connected $2$-types. Let $H:\Group$ be a group and let
$G:\AbGroup$ be an abelian group.
Then $\BB G$ and hence also $\BH\ptdto\BB G$ is a $2$-type, 
pointed at the constant map that sends any $w:\BH$ to the 
point $\pt_{\BB G}\defeq (\BG_\div,\settrunc{\id_{\BG_\div}})$ 
of $\BB G$.\footnote{Itself pointed by reflexivity.} In fact,
the type $\BG\ptdto\BB G$ is a $1$-type, since the maps are pointed.

\begin{definition}\label{def:AbHomgroup}
Let $H:\Group$ be a group and let $G:\AbGroup$ be an abelian group. 
Define the group $\grpHom(H,G)$ of homomorphisms from $H$ to $G$ by 
\[
\grpHom(H,G) \defeq \Aut_{\BH\ptdto\BB G}
((w \mapsto \pt_{\BB G}),\refl{\pt_{\BB G}}).\qedhere
\]
\end{definition}

\DELETE{%temporarily
The following lemma identifies the group $\grpHom(H,G)$ as the 
delooping of $\absHom_{\ptw}(\abstr(H),\abstr(G))$, 
the abelian abstract group of abstract homomorphisms with
pointwise operations, as given by
\cref{xca:abs-homgroup} and \cref{xca:abstract-group-of-maps}.
Consequently, $\grpHom(H,G)$ is an abelian group.


\begin{lemma}\label{lem:grpHomOK}
Let conditions be as in \cref{def:AbHomgroup}. %Abbreviate the shape
%$((w\mapsto \pt_{\BB G}),\refl{\pt_{\BB G}})$ of $\grpHom(H,G)$ by $\sh$. 
Consider the diagram in \cref{fig:bjørn}. This diagram commutes and
the composite of the chain of equivalences 
from $\USym\grpHom(H,G)$ to $\absHom(\abstr(H),\abstr(G))$
defines an abstract isomorphism from $\abstr(\grpHom(H,G))$ 
to the abstract group $\absHom_{\ptw}(\abstr(H),\abstr(G))$.
\end{lemma}

\begin{proof}
\begin{enumerate}
\item In the right square, the image of $\OO$ is indeed given by $P$.
\item The right square commutes.
$O'\jdeq \OO_{A,B} \circ(\inv{\swap}\circ\blank)$
\item The left square commutes. First we observe that the totally
unpointed maps commute definitionally ...
\end{enumerate}
\end{proof}
}%end DELETE



\subsection{Concrete rings}\label{sec:concrings}

We will now elaborate an approach to rings that is even more concrete
than mixed rings. For the latter rings we took the
obvious first step to replace the abstract additive group by a 
(concrete) group. Since monoids have no concrete counterpart in our set up,
we replaced in \cref{def:mixring} the multiplicative monoid 
by the half abstract $\ell,r:\USymR\to\Hom(R,R)$.

The use of $\ell,r$ was based on the observation that, 
for any abstract ring $\mathscr R$, left and right multiplication
by a fixed but arbitrary element of $R$ are 
abstract homomorphisms from the additive group $(R,0,+,-)$ of 
$\mathscr R$ to itself. 
Even more so, the map $a\mapsto(a\cdot\blank)$ is an abstract homomorphism
from $(R,0,+,-)$ to the abstract group $\absHom_{\ptw}(R,R)$
of abstract homomorphisms from $(R,0,+,-)$ to itself, with
pointwise operations induced by $(R,0,+,-)$.\footnote{%
$\absHom_{\ptw}(R,R)$ is an abelian abstract group by
\cref{xca:abs-homgroup} and \cref{xca:abstract-group-of-maps}.}

Given that we have replaced $(R,0,+,-)$ by an abelian group $G:\Group$,
the plan is to deloop $\absHom_{\ptw}(\abstr(G),\abstr(G))$. 
Denoting the result of the delooping by $\grpHom(G,G)$,\footnote{%
This notation presupposes that $G$ is abelian and distinguishes 
the \emph{set} of homomorphisms from $G$ to $G$ from the \emph{group}
with this set of homomorphisms as underlying set.}
we can then define the multiplication as a homomorphism
$\mu: \Hom(G,\grpHom(G,G))$.

One way of delooping $\absHom_{\ptw}(\abstr(G),\abstr(G))$ would be
to use the inverse of $\abstr$ in \cref{lem:homomabstrconcr}
which involves torsors.  
We prefer to use $\grpHom(G,G)$ from \cref{def:AbHomgroup},
making direct use of the assumption that $G$ is abelian.


\begin{definition}\label{def:ring}
A \emph{ring} $R$ consists of the following data:
\begin{enumerate}
\item An abelian group also denoted $R$;
\item A homomorphism $1_R:\Hom(\ZZ,R)$;
\item A homomorphism $\mu: \Hom(R,\grpHom(R,R))$, with $\grpHom(R,R)$
the group defined in \cref{def:AbHomgroup}.
\end{enumerate}
Moreover, the following equations should hold:
    \begin{enumerate}
    \item\label{ring:unit-laws}\
    $\ev\circ(\USym(\mu\circ{1_R})(\Sloop)) = \B\id_R \approx \MB{TBD}$ 
    (the \emph{multiplicative unit laws})\footnote{%
\MB{Not great:} $\USym(\mu\circ{1_R})$ is an abstract homomorphism
from $\USym\ZZ$ to $\USym\Hom(R,R)$ and the latter type
is equivalent to $(\BR\ptdto\loops\BB R)$. Finally by postcomposition
with $\ev$, we get equivalence with $(\BR\ptdto\BR)$.
The other unit law is probably worse.}
    \item\label{ring:assoc-law} \MB{TBD} (the \emph{associative law}). %for all $z : \BR$
    \end{enumerate}
The properties \ref{ring:unit-laws}-\ref{ring:assoc-law} 
are together denoted by $\RingProps(R,1_R,\mu)$.
The ring $R$ is called \emph{commutative} if \MB{TBD}, 
and \emph{non-trivial} if $1_R$ is not trivial.\footnote{%
A homomorphism is trivial if it classified by the constant function
at the shape to the target group. Or, equivalently, if it factors
through the trivial group.}
\end{definition}

We proceed by giving the standard example of the integers as a ring
in the sense of \cref{def:ring}.

%\MB{CURSOR}

\begin{example}
We take the group $\ZZ$ of the integers classified by the circle
as the abelian group for the ring of the integers.
We take $1_\ZZ \defeq \id_\ZZ$, the identity homomorphism.
For defining $\mu$ we first elaborate $\Hom(\ZZ,\ZZ)$ as a group.
Unfolding the definition we get (leaving the points implicit)
$\B\Hom(\ZZ,\ZZ) \jdeq(\Sc\ptdto\sum_{X:\UU}\setTrunc{\Sc\eqto X})$.
The shape of $\Hom(\ZZ,\ZZ)$ is the constant map 
that sends any $z:\Sc$ to $(\Sc,\settrunc{\id_{\Sc}})$, pointed by reflexivity.

Recall that $\BB\ZZ \jdeq \sum_{X:\UU}\setTrunc{\Sc\eqto X})$,
pointed at $\sh_{\BB\ZZ}\jdeq (\Sc,\settrunc{\id_\Sc})$.
For $\mu: \Hom(\ZZ,\Hom(\ZZ,\ZZ))$ we take,\footnote{\MB{Exercise material?}
Define $s:\id_\Sc\eqto\id_\Sc$ by function extensionality,
setting $s(\base)\defeq\Sloop$, $s(\Sloop)\defis {!}$.
Now define $e_z: \Sc\eqto\Sc$ by $e_z(\base)\defeq z$,
$e_z(\Sloop) \defis s(z) : (z\eqto z)$. Indeed, $e_\base = \id_\Sc$
and, by path induction $e_p(\base)=p$ for all $p:\base\eqto z$,
so $e_{\Sloop} = s$.}
with $\ve$ from \cref{lem:freeloopspace},
\[
\B\mu \defeq (z:\Sc) \mapsto \ve_{\BB\ZZ}(\sh_{\BB\ZZ},(e_z,!)).
\]
In this succint definition, $\ve_{\BB\ZZ}(\sh_{\BB\ZZ},\settrunc{e_z})$
can be identified as the function from $\Sc$ to $\BB\ZZ$ that sends 
$\base$ to $\Sc$ and $\Sloop$ to $(e_z,!)$ where $e_z:(\Sc\eqto\Sc)$,
$!: \Trunc{e_z\eqto\id_\Sc}$. In the following we focus on first components,
that is, on $\Sc$ and $e_z$, analyzing how $\B\mu$ applies to paths.

For any $z:\Sc$ and $k:\zet$ we have that 
$\B\mu(z,{\Sloop}^k)= e_z^k : (\Sc\eqto\Sc)$.
Hence for any $j:\zet$ we have that 
$\B\mu({\Sloop}^j,{\Sloop}^k )= e_{{\Sloop}^j}^k = s^{jk}: (\id_\Sc\eqto\id_\Sc)$.
\MB{Almost there! Use $\ev$ to get to $\USym\ZZ$?}




%\cref{xca:(S1->S1)_(f)-eqv-S1,xca:S1=S1-components},
%which give an equivalence $e:\Sc\to(\Sc\eqto\Sc)_{\id_\Sc}$
%which maps $\base$ to $\id_\Sc$.%
It follows that
$(\ZZ,1_\ZZ,\mu)$ is a non-trivial commutative ring.
\end{example}

\begin{xca}\label{xca:Rconcring->URabstring}
Let $(R,1_r,\mu)$ be a ring. Show that $\USymR$ is an abstract ring with
additive group $\abstr(R)$ and multiplicative monoid 
$(\USymR,\USym1_R(\Sloop),\USym\mu$. \MB{TBD}
\end{xca}
%Solution: 



\MB{TBD define type of (abstract) rings, prove equivalence, define
ring homomorphisms, delooping etc. No interesting difficulties
expected before we come to fields.}





\begin{definition}
Given a commutative ring $R$, an element $e:R$ is \textbf{invertible} if there exists an element $a:R$ such that $e \cdot a = 1$ and $a \cdot e = 1$:
$$\mathrm{isInvertible}(e) := \left\Vert\sum_{a:R} (e \cdot a = 1) \times (a \cdot e = 1)\right\Vert$$
\end{definition}

\begin{theorem}
In any nontrivial commutative ring $R$, $0$ is always a non-invertible element. 
$$\mathrm{isNonTrivialCRing}(R) \to \neg \mathrm{isInvertible}(0)$$
\end{theorem}

\begin{proof}
Suppose that $0$ is invertible. Then there exists an element $a:R$ such that $a \cdot 0 = 1$. However, due to the absorption properties of $0$ and the fact that $R$ is a set, $a \cdot 0 = 0$. This implies that $0 = 1$, which contradicts the fact that $0 \neq 1$ in a nontrivial commutative ring. Thus, $0$ is a non-invertible element in any nontrivial commutative ring $R$. 
\end{proof}

\begin{definition}
A nontrivial commutative ring $R$ is a \textbf{field} if and only if the type of all non-invertible elements in $R$ is contractible:
$$\mathrm{isField}(R) := \mathrm{isNonTrivialCRing}(R) \times \mathrm{isContr}\left(\sum_{x:R} \neg \mathrm{isInvertible}(x)\right)$$ 
Equivalently, $R$ is a field if and only if every non-invertible element is equal to zero. 
\end{definition}

\begin{remark}
In other parts of the constructive mathematics literature, such as in Peter Johnstone's \textit{Rings, Fields, and Spectra}, this is called a "residue field". However, in this book we shall refrain from using the term "residue field" for our definition, since that contradicts the usage of "residue field" in other parts of mathematics, such as in algebraic geometry. 
\end{remark}

\begin{definition}
A field is \textbf{discrete} if every element is either invertible or equal to zero. 
$$\mathrm{isDiscreteField}(R) := \mathrm{isField}(R) \times \prod_{a:R} \Vert(a = 0) \amalg \mathrm{isInvertible}(a)\Vert$$ 
\end{definition}

\begin{definition}
A nontrivial commutative ring $R$ is a \textbf{local ring} if for every element $a:R$ and $b:R$, if the sum $a + b$ is invertible, then either $a$ is invertible or $b$ is invertible. 
$$\mathrm{isLocalRing}(R) := \mathrm{isNonTrivialCRing}(R) \times \prod_{a:R} \prod_{b:R} \mathrm{isInvertible}(a + b) \to \Vert\mathrm{isInvertible}(a) \amalg \mathrm{isInvertible}(b)\Vert$$ 
\end{definition}

\begin{definition}
A field $R$ is \textbf{Heyting} if it is also a local ring. 
$$\mathrm{isHeytingField}(R) := \mathrm{isField}(R) \times \mathrm{isLocalRing}(R)$$ 
\end{definition}

References used in this section: 
\begin{itemize}
\item Emmy Noether, \textit{Ideal Theory in Rings}, Mathematische Annalen 83 (1921)
\item Henri Lombardi, Claude Quitté, \textit{Commutative algebra: Constructive methods (Finite projective modules)}
\item Peter Johnstone, \textit{Rings, Fields, and Spectra}, Journal of Algebra 49 (1977) 238-260
\end{itemize}

\section{vector spaces}

\begin{definition}
Given a field $K$, a $K$-\textbf{vector space} is an abelian group $V$ with a bilinear function $(-)(-):K \times V \to V$ called \textbf{scalar multiplication} such that $1 v = v$ and for all elements $a:K$, $b:K$, and $v:V$, $(a \cdot b) v = a (b v)$. 
\end{definition}

\begin{definition}
A $K$-\textbf{linear map} between two $K$-vector spaces $V$ and $W$ is a group homomorphism $h:V \to W$ which also preserves scalar multiplication: for all elements $a:K$ and $v:V$, $f(a v) = a f(v)$. 
\end{definition}

\begin{definition}
Given a field $K$ and a set $S$, the \textbf{free $K$-vector space} on $S$ is the homotopy initial $K$-vector space $V$ with a function $i:S \to V$: for every other $K$-vector space $W$ with a function $j:S \to W$, the type of linear maps $h:V \to W$ such that for all elements $s:S$, $h(i(s)) = j(s)$ is contractible. 
\end{definition}

\begin{definition}
Given a field $K$ and a natural number $n$, an \textbf{$n$-dimensional $K$-vector space} is a free $K$-vector space on the finite type $\mathrm{Fin}(n)$. 
\end{definition}

\section{the general linear group as automorphism group}
\section{determinants\titledagger}
\section{examples: rationals, polynomials, adding a root, field extensions}
\section{ordered fields, real-closed fields, pythagorean fields, euclidean fields}
\section{complex fields, quadratically closed fields, algebraically closed fields}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: