module Algebra.Group.Homotopy.BAut where

# Deloopings of automorphism groupsπ

Recall that any set $X$ generates a group $Sym(X)$ given by the automorphisms $XβX.$ We also have a generic construction of deloopings: special spaces $K(G,1)$ (for a group $G),$ where the fundamental group $Ο_{1}(K(G,1))$ recovers $G.$ For the specific case of deloping automorphism groups, we can give an alternative construction: The type of small types merely equivalent to $X$ has a fundamental group of $Sym(X).$

module _ {β} (T : Type β) where BAut : Type (lsuc β) BAut = Ξ£[ B β Type β ] β₯ T β B β₯ base : BAut base = T , inc (id , id-equiv)

The first thing we note is that `BAut`

is a *connected*
type, meaning that it only has βa single pointβ, or, more precisely,
that all of its interesting information is in its (higher) path
spaces:

connected : (x : BAut) β β₯ x β‘ base β₯ connected = elim! Ξ» b e β inc (p b e) where p : β b e β (b , inc e) β‘ base p _ = EquivJ (Ξ» B e β (B , inc e) β‘ base) refl

We now turn to proving that
$Ο_{1}(B(X))β(XβX).$
We will define a type family
$Code(b),$
where a value
$p:Code(x)$
codes for an identification
$pβ‘base.$
Correspondingly, there are functions to and from these types: The core
of the proof is showing that these functions, `encode`

and `decode`

, are inverses.

Code : BAut β Type β Code b = T β b .fst encode : β b β base β‘ b β Code b encode x p = pathβequiv (ap fst p) decode : β b β Code b β base β‘ b decode (b , eqv) rot = Ξ£-pathp (ua rot) (is-propβpathp (Ξ» _ β squash) _ _)

Recall that
$base$
is the type
$T$
itself, equipped with the identity equivalence. Hence, to code for an
identification
$baseβ‘(X,e),$
it suffices to record
$e$
β which by univalence corresponds to a path
$ua(e):Tβ‘X.$
We can not directly extract the equivalence from a given point
$(X,e):B(X):$
it is βhidden awayβ under a truncation. But, given an identification
$p:bβ‘base,$
we can recover the equivalence by seeing *how*
$p$
identifies
$Xβ‘T.$

decodeβencode : β b (p : base β‘ b) β decode b (encode b p) β‘ p decodeβencode b = J (Ξ» b p β decode b (encode b p) β‘ p) (Ξ£-prop-square (Ξ» _ β squash) sq) where sq : ua (encode base refl) β‘ refl sq = ap ua pathβequiv-refl β ua-id-equiv

`Encode`

and `decode`

are inverses by a direct
application of `univalence`

.

encodeβdecode : β b (p : Code b) β encode b (decode b p) β‘ p encodeβdecode b p = ua.Ξ· _

We now have the core result: Specialising `encode`

and `decode`

to the `basepoint`

, we conclude that loop space
$baseβ‘base$
is equivalent to
$Sym(X).$

Ξ©ΒΉBAut : (base β‘ base) β (T β T) Ξ©ΒΉBAut = IsoβEquiv (encode base , iso (decode base) (encodeβdecode base) (decodeβencode base))

We can also characterise the h-level of these connected components.
Intuitively the h-level should be one more than that of the type weβre
delooping, because `BAut`

βonly has one pointβ (itβs
connected), and as we established right above, the space of loops of
that point is the automorphism group we delooped. The trouble here is
that `BAut`

has many points, and while
we can pick paths between any two of them, we can not do so
*continuously* (otherwise `BAut`

would be a
proposition).

This turns out not to matter! Since βbeing of h-level $n$β is a proposition, our discontinuous (i.e.: truncated) method of picking paths is just excellent. In the case when $T$ is contractible, we can directly get at the underlying equivalences, but for the higher h-levels, we proceed exactly by using connectedness.

BAut-is-hlevel : β n β is-hlevel T n β is-hlevel BAut (1 + n) BAut-is-hlevel zero hl (x , f) (y , g) = Ξ£-prop-path! (sym (ua f') β ua g') where extract : β {X} β is-prop (T β X) extract f g = ext Ξ» x β ap fst $ is-contrβis-prop ((f eβ»ΒΉ) .snd .is-eqv (hl .centre)) (f .fst x , is-contrβis-prop hl _ _) (g .fst x , is-contrβis-prop hl _ _) f' = β₯-β₯-rec extract (Ξ» x β x) f g' = β₯-β₯-rec extract (Ξ» x β x) g BAut-is-hlevel (suc n) hl x y = β₯-β₯-elimβ {P = Ξ» _ _ β is-hlevel (x β‘ y) (1 + n)} (Ξ» _ _ β is-hlevel-is-prop _) (Ξ» p q β transport (apβ (Ξ» a b β is-hlevel (a β‘ b) (1 + n)) (sym p) (sym q)) (Equivβis-hlevel (1 + n) Ξ©ΒΉBAut (β-is-hlevel (1 + n) hl hl))) (connected x) (connected y)