first draft of discussion about Warn's contruction (end argument is m…

…issing, will complete soon)

group.tex

@@ -3404,11 +3404,59 @@ \subsection{Abelian groups and simply connected $2$-types}
   wanted.
 \end{proof}
 
+The function $\BB$ defined in the previous proof provides a delooping of $\BG$ whenever $G$ is abelian. That is, there is an identification
+$\loops \BB G \eqto \BG$. A systematic way of obtaining deloopings has been developped by David W\"{a}rn in \footcite{Warn-EM}, that can be
+applied here to give an alternative definition of $\BB G$. W\"{a}rn defines, for any pointed type $X$, a type $TX$ of {\em $X$-torsors} as
+follows:
+\begin{displaymath}
+  TX \defequi \sum_{Y : \UU} \Trunc{Y} \times \left( \prod_{y:Y}(Y,y) \ptdweto X \right)
+\end{displaymath}
+In order to compare this construction with our own, note that there is an equivalence of type
+\begin{displaymath}
+  TX \equivto \sum_{Y : \UU} \Trunc{Y} \times \secfun(\ev_{X_\div,Y})
+\end{displaymath}
+where $\ev_{X_\div,Y} : (X_\div \eqto Y) \to Y$ is the evaluation (defined by path-induction, sending $\refl X$ to the distinguished point of
+$X$), and $\secfun(f)$ is the type of sections of any function $f$. Write $\tilde TX$ for the type on the right hand side, whose elements are
+still called (abusively) $X$-torsors. We are interested here in the case $X \jdeq \BG$ for an abelian group $G$. Then, for each type $Y$, we can
+construct a function $f_Y : \Trunc{Y} \times \secfun(\ev_{X_\div,Y}) \to \setTrunc{\BG_\div \eqto Y}$ as follows: an element $(!,s)$ proves that
+$Y$ is connected (being connected is a proposition, so we can assume an actual $y:Y$ and then $s(y) : \BG_\div \eqto Y$ proves that $Y$ is as
+connected as $\BG_\div$ is), and consequently $s$ must send $Y$ into one of the connected component of $\BG_\div \eqto Y$, that we choose as the
+definition of $f_Y(!,s)$. But the fiber at $c : \setTrunc{\BG_\div \eqto Y}$ of $f_Y$ can then be identified with the type of sections $s$ of
+$\ev_{\BG_\div,Y}$ with values in $c$. However, we can show that for any $Z$ and $p: \BG_\div \eqto Z$ the restriction of the evaluation
+$\ev_{\BG_\div,Z}\restriction_p : \conncomp{\BG_\div \eqto Z} p \to Z$ is an equivalence: by induction, we only have to show it for
+$p\jdeq \refl {\BG_\div}$, but then $\ev_{\BG_\div,\BG_\div}\restriction_{\refl {\BG_\div}}$ is exactly $\B\grpcenterinc G$, which is an
+equivalence since $G$ is abelian. So we have shown that every fiber of $f_Y$ is contractible, meaning $f_Y$ is an equivalence
+$\Trunc{Y} \times \secfun(\ev_{X_\div,Y}) \equivto \setTrunc{\BG_\div \eqto Y}$. In particular, this provides an equivalence
+$\tilde T\BG \simeq \univcover \UU {\BG_\div}$ \footnote{Notice that the construction of an equivalence $TX \equivto \univcover \UU {X_\div}$ that
+  we carried for $X\jdeq\BG$ relies only on $X_\div$ being connected and $\ev_{X_\div,X_\div}\restriction_{\refl {X_\div}}$ being an
+  equivalence. Such types $X$ are called {\em central} and are studied in details by~\citeauthor{2301.02636}\footnotemark{}.}.%
+\footcitetext{2301.02636}
+
+Although we have already established an equivalence between W\"arn's type of $\BG$-torsors and our type $\BB G$ when $G$ in abelian, and thus we
+have de facto proven $T\BG$ to be a delooping of $\BG$, it is worth exploring how we can directly prove this latter fact. The clever idea
+developped by W\"arn is that the type of $X$-torsors is a deloopoing of $X$ as soon as the type $\sum_{t : \tilde TX}\fst t$ of {\em pointed
+  $X$-torsors} is contractible. Indeed, for any center of contraction $(t,y)$, by contracting away (\cref{lem:contract-away}) in two different
+ways, we obtained a composition of equivalences:
+\begin{displaymath}
+  (t \eqto t) \equivto \sum_{u : \tilde TX}\fst u \times (t \eqto u) \equivto \fst t 
+\end{displaymath}
+that maps $\refl t$ to $y$. In other words, this equivalence, trivially pointed, presents $(\tilde TX, t)$ as a delooping of $(\fst t ,
+y)$. Moreover, each $X$-torsors $t$, if pointed at $y:\fst t$, comes with an identification $p : X_\div \eqto Y$ and an identification of type
+$\ev_{X_\div \eqto Y}(p) \eqto y $. Through univalence, this amount to a pointed equivalence $X \ptdweto (\fst t,y)$. So in the end, we have an
+equivalence $(\tilde TX, t) \ptdweto X$ whenever we can prove that the type of pointed $X$-torsors is contractible. When $X \jdeq \BG$ for an
+abelian group $G$, we know already a pointed $\BG$-torsor, namely $\BG_\div$ pointed at $\sh_G$ together with the section of
+$\ev_{\BG_\div,\BG_\div}$ provided by the inverse of the isomorphism $\grpcenterinc G$. We write $(t_G,\sh_G)$ for this pointed
+$\BG$-torsors. To conclude that $\tilde T\BG$ is a delooping of $X$, it suffices then to show that $(t_G,\sh_G)$ is a center of
+contraction. However, for any $\BG$-torsors $t$ pointed at $y: \fst t$, and with section $s$ of $\ev_{\BG_\div,\fst t}$, we obtain an
+identification $s(y) : \BG_\div \eqto \fst t$. Moreover, we know from the analysis above that $s$ is fully determined by the connected component
+of $s(y)$. Thus, to provide an identification $(t_G,\sh_G) \eqto (t , y)$, we construct $p : t_G \eqto t$ with first projection $s(y)$ by simply
+noting that {\tt to complete}.
+
 
 \section{$G$-sets vs $\abstr(G)$-sets}
 \label{sec:Gsetsabstrconcr}
 \marginnote{Recall from \cref{def:abstrGtorsors} that the type of $\abstr(G)$-set is
-  $$Set_{\abstr(G)}^\abstr\defequi \sum_{\mathcal X:\Set}\Hom_\abstr({\abstr(G)},\abstr(\Sigma_{\mathcal X})).$$}
+  $$\Set_{\abstr(G)}^\abstr\defequi \sum_{\mathcal X:\Set}\Hom_\abstr({\abstr(G)},\abstr(\Sigma_{\mathcal X})).$$}
 
 Given a group $G$ it should by now come as no surprise that the type of $G$-sets is equivalent to the type of $\abstr(G)$-sets.
 According to \cref{lem:homomabstrconcr}

macros.tex

@@ -520,6 +520,7 @@
 \newcommand*{\apc}{\casop{\constant{ap}{\ct}}}
 \newcommand*{\ns}{\casop{\constant{ns}}}
 \newcommand*{\ev}{\casop{\constant{ev}}}
+\newcommand*{\secfun}{\casop{\constant{sec}}}
 \newcommand*{\pow}[1]{\casop{\constant{pow}}_{#1}} % power bundle/map
 \newcommand*{\ve}{\casop{\constant{ve}}} % cute: the inverse of \ev
 \newcommand*{\out}{\casop{\constant{out}}} % projection from copy

papers.bib

@@ -883,6 +883,12 @@ @Misc{1802.02191
  year = {February, 2018},
  note = {\arxiv{1802.02191}}}
 
+@Misc{2301.02636,
+ title = {{Central H-spaces and banded types}},
+ author = {Buchholtz, Ulrik and Christensen, J. Daniel and Flaten, Jarl G. Taxerås and Rijke, Egbert},
+ year = {February, 2023},
+ note = {\arxiv{2301.02636}}}
+
 @article{Kleiner-group-survey,
     AUTHOR = {Kleiner, Israel},
      TITLE = {The evolution of group theory: a brief survey},
@@ -1504,6 +1510,15 @@ @Misc{            Warn2023
   URL             = {https://dwarn.se/po-paths.pdf}
 }
 
+@Misc{            Warn-EM,
+  Author          = {Wärn, David},
+  Title           = {Eilenberg-MacLane spaces and stabilisation in homotopy type theory},
+  Year            = {2023},
+  EPrint          = {2301.03685},
+  ArchivePrefix   = {arXiv},
+  PrimaryClass    = {math.AT}
+}
+
 @Misc{            Riehl2023,
   Title           = {Could $\infty$-category theory be taught to undergraduates?},
   Author          = {Emily Riehl},