Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed WildCat.
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
Require Import Algebra.AbGroups.
Require Import Homotopy.HSpace.Core.
Require Import TruncType.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.WhiteheadsPrinciple.

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.
Local Open Scope path_scope.

(** * Classifying spaces of groups *)

(** We define the classifying space of a group to be the following HIT:

<<
  HIT ClassifyingSpace (G : Group) : 1-Type
   | bbase : ClassifyingSpace
   | bloop : X -> bbase = bbase
   | bloop_pp : forall x y, bloop (x * y) = bloop x @ bloop y.
>>

  We implement this is a private inductive type. *)
Module Export ClassifyingSpace.

  Section ClassifyingSpace.
Trying to mask the absolute name "ClassifyingSpace.ClassifyingSpace"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]

    Private Inductive ClassifyingSpace (G : Group) :=
      | bbase : ClassifyingSpace G.

    Context {G : Group}.

    Axiom bloop : G -> bbase G = bbase G.

    Global Arguments bbase {_}.

    Axiom bloop_pp : forall x y, bloop (x * y) = bloop x @ bloop y.

    #[export] Instance istrunc_ClassifyingSpace
      : IsTrunc 1 (ClassifyingSpace G).
G: Group
IsTrunc 1 (ClassifyingSpace G)
    Proof.
G: Group
IsTrunc 1 (ClassifyingSpace G) Admitted.

  End ClassifyingSpace.

  Arguments bloop {G} _%_mc_mult_scope.

  (** Now we can state the expected dependent elimination principle, and derive other versions of the elimination principle from it. *)
  Section ClassifyingSpace_ind.

    Local Open Scope dpath_scope.

    Context {G : Group}.

    (** Note that since our classifying space is 1-truncated, we can only eliminate into 1-truncated type families. *)
    Definition ClassifyingSpace_ind
      (P : ClassifyingSpace G -> Type)
      `{forall b, IsTrunc 1 (P b)}
      (bbase' : P bbase)
      (bloop' : forall x, DPath P (bloop x) bbase' bbase')
      (bloop_pp' : forall x y,  DPathSquare P (sq_G1 (bloop_pp x y))
        (bloop' (x * y)) ((bloop' x) @Dp (bloop' y)) 1 1)
      (b : ClassifyingSpace G)
      : P b
      := match b with
            bbase => (fun _ _ => bbase')
         end bloop' bloop_pp'.

    (** Here we state the computation rule for [ClassifyingSpace_ind] over [bloop] as an axiom. We don't need one for [bloop_pp] since we have a 1-type. We leave this as admitted since the computation rule is an axiom. **)
    Definition ClassifyingSpace_ind_beta_bloop
      (P : ClassifyingSpace G -> Type)
     `{forall b, IsTrunc 1 (P b)}
      (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase')
      (bloop_pp' : forall x y,  DPathSquare P (sq_G1 (bloop_pp x y))
        (bloop' (x * y)) ((bloop' x) @Dp (bloop' y)) 1 1)
      (x : G)
      : apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsTrunc 1 (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
bloop_pp': forall x y : G,
DPathSquare P (sq_G1 (bloop_pp x y))
  (bloop' (x * y)) (bloop' x @Dp bloop' y)
  1 1
x: G
apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp')
  (bloop x) = bloop' x
    Proof.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsTrunc 1 (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
bloop_pp': forall x y : G,
DPathSquare P (sq_G1 (bloop_pp x y))
  (bloop' (x * y)) (bloop' x @Dp bloop' y)
  1 1
x: G
apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp')
  (bloop x) = bloop' x Admitted.

  End ClassifyingSpace_ind.

End ClassifyingSpace.

(** Other eliminators *)
Section Eliminators.

  Context {G : Group}.

  (** The non-dependent eliminator *)
  Definition ClassifyingSpace_rec
    (P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G -> bbase' = bbase')
    (bloop_pp' : forall x y : G, bloop' (x * y) = bloop' x @ bloop' y)
    : ClassifyingSpace G -> P.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
ClassifyingSpace G -> P
  Proof.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
ClassifyingSpace G -> P
    srefine (ClassifyingSpace_ind (fun _ => P) bbase' _ _).
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
forall x : G,
DPath (fun _ : ClassifyingSpace G => P) (bloop x)
  bbase' bbase'
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
forall x y : G,
DPathSquare (fun _ : ClassifyingSpace G => P)
  (sq_G1 (bloop_pp x y)) 
  (?bloop' (x * y)) (?bloop' x @Dp ?bloop' y)%dpath
  1%dpath 1%dpath
    1: intro x; apply dp_const, bloop', x.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
forall x y : G,
DPathSquare (fun _ : ClassifyingSpace G => P)
  (sq_G1 (bloop_pp x y))
  ((fun x0 : G =>
    let X := equiv_fun dp_const in X (bloop' x0))
     (x * y))
  ((fun x0 : G =>
    let X := equiv_fun dp_const in X (bloop' x0)) x @Dp
   (fun x0 : G =>
    let X := equiv_fun dp_const in X (bloop' x0)) y)%dpath
  1%dpath 1%dpath
    intros x y.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
DPathSquare (fun _ : ClassifyingSpace G => P)
  (sq_G1 (bloop_pp x y))
  ((fun x : G =>
    let X := equiv_fun dp_const in X (bloop' x))
     (x * y))
  ((fun x : G =>
    let X := equiv_fun dp_const in X (bloop' x)) x @Dp
   (fun x : G =>
    let X := equiv_fun dp_const in X (bloop' x)) y)%dpath
  1%dpath 1%dpath
    apply ds_const'.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
PathSquare
  (dp_const^-1
     (let X := equiv_fun dp_const in
      X (bloop' (x * y))))
  (dp_const^-1
     ((let X := equiv_fun dp_const in X (bloop' x)) @Dp
      (let X := equiv_fun dp_const in X (bloop' y)))%dpath)
  (dp_const^-1 1%dpath) (dp_const^-1 1%dpath)
    rapply sq_GGcc.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
?Goal =
dp_const^-1
  (let X := equiv_fun dp_const in X (bloop' (x * y)))
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
?Goal0 =
dp_const^-1
  ((let X := equiv_fun dp_const in X (bloop' x)) @Dp
   (let X := equiv_fun dp_const in X (bloop' y)))%dpath
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
PathSquare ?Goal ?Goal0 
  (dp_const^-1 1%dpath) 
  (dp_const^-1 1%dpath)
    2: refine (_ @ ap _ (dp_const_pp _ _)).
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
?Goal =
dp_const^-1
  (let X := equiv_fun dp_const in X (bloop' (x * y)))
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
?Goal0 = dp_const^-1 (dp_const (bloop' x @ bloop' y))
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
PathSquare ?Goal ?Goal0 
  (dp_const^-1 1%dpath) 
  (dp_const^-1 1%dpath)
    1,2: symmetry; apply eissect.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x, y: G
PathSquare (bloop' (x * y)) (bloop' x @ bloop' y)
  (dp_const^-1 1%dpath) (dp_const^-1 1%dpath)
    by apply sq_G1.
  Defined.

  (** Computation rule for non-dependent eliminator *)
  Definition ClassifyingSpace_rec_beta_bloop
    (P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G -> bbase' = bbase')
    (bloop_pp' : forall x y : G, bloop' (x * y) = bloop' x @ bloop' y) (x : G)
    : ap (ClassifyingSpace_rec P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
ap (ClassifyingSpace_rec P bbase' bloop' bloop_pp')
  (bloop x) = bloop' x
  Proof.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
ap (ClassifyingSpace_rec P bbase' bloop' bloop_pp')
  (bloop x) = bloop' x
    lhs_V napply dp_apD_const'.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
dp_const^-1
  (apD
     (ClassifyingSpace_rec P bbase' bloop' bloop_pp')
     (bloop x)) = bloop' x
    apply moveR_equiv_V.
G: Group
P: Type
IsTrunc0: IsTrunc 1 P
bbase': P
bloop': G -> bbase' = bbase'
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
apD (ClassifyingSpace_rec P bbase' bloop' bloop_pp')
  (bloop x) = dp_const (bloop' x)
    napply ClassifyingSpace_ind_beta_bloop.
  Defined.

  (** Sometimes we want to induct into a set which means we can ignore the bloop_pp arguments. Since this is a routine argument, we turn it into a special case of our induction principle. *)
  Definition ClassifyingSpace_ind_hset
    (P : ClassifyingSpace G -> Type)
    `{forall b, IsTrunc 0 (P b)}
    (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase')
    : forall b, P b.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHSet (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
forall b : ClassifyingSpace G, P b
  Proof.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHSet (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
forall b : ClassifyingSpace G, P b
    refine (ClassifyingSpace_ind P bbase' bloop' _).
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHSet (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
forall x y : G,
DPathSquare P (sq_G1 (bloop_pp x y)) (bloop' (x * y))
  (bloop' x @Dp bloop' y)%dpath 1%dpath 1%dpath
    intros x y.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHSet (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
x, y: G
DPathSquare P (sq_G1 (bloop_pp x y)) (bloop' (x * y))
  (bloop' x @Dp bloop' y)%dpath 1%dpath 1%dpath
    apply ds_G1.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHSet (P b)
bbase': P bbase
bloop': forall x : G, DPath P (bloop x) bbase' bbase'
x, y: G
DPath
  (fun x : bbase = bbase => DPath P x bbase' bbase')
  (bloop_pp x y) (bloop' (x * y))
  (bloop' x @Dp bloop' y)%dpath
    apply path_ishprop.
  Defined.

  Definition ClassifyingSpace_rec_hset
    (P : Type) `{IsTrunc 0 P} (bbase' : P) (bloop' : G -> bbase' = bbase')
    : ClassifyingSpace G -> P.
G: Group
P: Type
IsTrunc0: IsHSet P
bbase': P
bloop': G -> bbase' = bbase'
ClassifyingSpace G -> P
  Proof.
G: Group
P: Type
IsTrunc0: IsHSet P
bbase': P
bloop': G -> bbase' = bbase'
ClassifyingSpace G -> P
    srapply (ClassifyingSpace_rec P bbase' bloop' _).
G: Group
P: Type
IsTrunc0: IsHSet P
bbase': P
bloop': G -> bbase' = bbase'
forall x y : G, bloop' (x * y) = bloop' x @ bloop' y
    intros; apply path_ishprop.
  Defined.

  (** Similarly, when eliminating into an hprop, we only have to handle the basepoint. *)
  Definition ClassifyingSpace_ind_hprop (P : ClassifyingSpace G -> Type)
    `{forall b, IsTrunc (-1) (P b)} (bbase' : P bbase)
    : forall b, P b.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHProp (P b)
bbase': P bbase
forall b : ClassifyingSpace G, P b
  Proof.
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHProp (P b)
bbase': P bbase
forall b : ClassifyingSpace G, P b
    refine (ClassifyingSpace_ind_hset P bbase' _).
G: Group
P: ClassifyingSpace G -> Type
H: forall b : ClassifyingSpace G, IsHProp (P b)
bbase': P bbase
forall x : G, DPath P (bloop x) bbase' bbase'
    intros; rapply dp_ishprop.
  Defined.

End Eliminators.

(** The classifying space is 0-connected. *)
Instance isconnected_classifyingspace {G : Group}
  : IsConnected 0 (ClassifyingSpace G).
G: Group
IsConnected (Tr 0) (ClassifyingSpace G)
Proof.
G: Group
IsConnected (Tr 0) (ClassifyingSpace G)
  apply (Build_Contr _ (tr bbase)).
G: Group
forall y : Trunc 0 (ClassifyingSpace G), tr bbase = y
  srapply Trunc_ind.
G: Group
forall a : ClassifyingSpace G, tr bbase = tr a
  srapply ClassifyingSpace_ind_hprop; reflexivity.
Defined.

(** The classifying space of a group is pointed. *)
Instance ispointed_classifyingspace (G : Group)
  : IsPointed (ClassifyingSpace G)
  := bbase.

Definition pClassifyingSpace (G : Group) := [ClassifyingSpace G, bbase].

(** To use the [B G] notation for [pClassifyingSpace] import this module. *)
Module Import ClassifyingSpaceNotation.
  Definition B G := pClassifyingSpace G.
End ClassifyingSpaceNotation.

(** [bloop] takes the unit of the group to reflexivity. *)
Definition bloop_id {G : Group} : bloop (mon_unit : G) = idpath.
G: Group
bloop (mon_unit : G) = 1
Proof.
G: Group
bloop (mon_unit : G) = 1
  symmetry.
G: Group
1 = bloop (mon_unit : G)
  apply (cancelL (bloop mon_unit)).
G: Group
bloop 1 @ 1 = bloop 1 @ bloop 1
  refine (_ @ bloop_pp _ _).
G: Group
bloop 1 @ 1 = bloop (mon_unit * mon_unit)
  refine (_ @ ap _ (left_identity _)^).
G: Group
bloop 1 @ 1 = bloop 1
  apply concat_p1.
Defined.

(** [bloop] "preserves inverses" by taking inverses in [G] to inverses of paths in [BG]. *)
Definition bloop_inv {G : Group} (x : G) : bloop x^ = (bloop x)^.
G: Group
x: G
bloop x^ = (bloop x)^
Proof.
G: Group
x: G
bloop x^ = (bloop x)^
  refine (_ @ concat_p1 _).
G: Group
x: G
bloop x^ = (bloop x)^ @ 1
  apply moveL_Vp.
G: Group
x: G
bloop x @ bloop x^ = 1
  refine (_ @ bloop_id).
G: Group
x: G
bloop x @ bloop x^ = bloop 1
  refine ((bloop_pp _ _)^ @ _).
G: Group
x: G
bloop (x * inv x) = bloop 1
  apply ap, right_inverse.
Defined.

(** The underlying pointed map of [pequiv_g_loops_bg]. *)
Definition pbloop {G : Group} : G ->* loops (B G).
G: Group
G ->* loops (B G)
Proof.
G: Group
G ->* loops (B G)
  srapply Build_pMap.
G: Group
G -> loops (B G)
G: Group
?f pt = pt
  1: exact bloop.
G: Group
bloop pt = pt
  exact bloop_id.
Defined.

(** This says that [B] is left adjoint to the loop space functor from pointed 1-types to groups. *)
Definition pClassifyingSpace_rec {G : Group} (P : pType) `{IsTrunc 1 P}
           (bloop' : G -> loops P)
           (bloop_pp' : forall x y : G, bloop' (x * y) = bloop' x @ bloop' y)
  : B G ->* P
  := Build_pMap (ClassifyingSpace_rec P (point P) bloop' bloop_pp') idpath.

(** And this is one of the standard facts about adjoint functors: [(R h') o eta = h], where [h : G -> R P], [h' : L G -> P] is the adjunct, and eta ([bloop]) is the unit. *)
Definition pClassifyingSpace_rec_beta_bloop {G : Group} (P : pType)
  `{IsTrunc 1 P} (bloop' : G -> loops P)
  (bloop_pp' : forall x y : G, bloop' (x * y) = bloop' x @ bloop' y)
  : fmap loops (pClassifyingSpace_rec P bloop' bloop_pp') o bloop == bloop'.
G: Group
P: pType
IsTrunc0: IsTrunc 1 P
bloop': G -> loops P
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
fmap loops (pClassifyingSpace_rec P bloop' bloop_pp')
o bloop == bloop'
Proof.
G: Group
P: pType
IsTrunc0: IsTrunc 1 P
bloop': G -> loops P
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
fmap loops (pClassifyingSpace_rec P bloop' bloop_pp')
o bloop == bloop'
  intro x; simpl.
G: Group
P: pType
IsTrunc0: IsTrunc 1 P
bloop': G -> loops P
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
1 @
(ap (ClassifyingSpace_rec P pt bloop' bloop_pp')
   (bloop x) @ 1) = bloop' x
  refine (concat_1p _ @ concat_p1 _ @ _).
G: Group
P: pType
IsTrunc0: IsTrunc 1 P
bloop': G -> loops P
bloop_pp': forall x y : G,
bloop' (x * y) = bloop' x @ bloop' y
x: G
ap (ClassifyingSpace_rec P pt bloop' bloop_pp')
  (bloop x) = bloop' x
  apply ClassifyingSpace_rec_beta_bloop.
Defined.

(** Here we prove that [BG] is a delooping of [G], i.e. that [loops BG <~> G]. *)
Section EncodeDecode.

  Context `{Univalence} {G : Group}.

  Local Definition codes : B G -> HSet.
H: Univalence
G: Group
B G -> HSet
  Proof.
H: Univalence
G: Group
B G -> HSet
    srapply ClassifyingSpace_rec.
H: Univalence
G: Group
HSet
H: Univalence
G: Group
G -> ?bbase' = ?bbase'
H: Univalence
G: Group
forall x y : G,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    +
H: Univalence
G: Group
HSet exact (Build_HSet G).
    +
H: Univalence
G: Group
G -> Build_HSet G = Build_HSet G intro x.
H: Univalence
G: Group
x: G
Build_HSet G = Build_HSet G
      apply path_trunctype.
H: Univalence
G: Group
x: G
Build_HSet G <~> Build_HSet G
      exact (Build_Equiv _ _ (fun t => t * x) _).
    +
H: Univalence
G: Group
forall x y : G,
(fun x0 : G =>
 path_trunctype
   {|
     equiv_fun := fun t : G => t * x0;
     equiv_isequiv := isequiv_group_right_op G x0
   |}) (x * y) =
(fun x0 : G =>
 path_trunctype
   {|
     equiv_fun := fun t : G => t * x0;
     equiv_isequiv := isequiv_group_right_op G x0
   |}) x @
(fun x0 : G =>
 path_trunctype
   {|
     equiv_fun := fun t : G => t * x0;
     equiv_isequiv := isequiv_group_right_op G x0
   |}) y intros x y; cbn beta.
H: Univalence
G: Group
x, y: G
path_trunctype
  {|
    equiv_fun := fun t : G => t * (x * y);
    equiv_isequiv := isequiv_group_right_op G (x * y)
  |} =
path_trunctype
  {|
    equiv_fun := fun t : G => t * x;
    equiv_isequiv := isequiv_group_right_op G x
  |} @
path_trunctype
  {|
    equiv_fun := fun t : G => t * y;
    equiv_isequiv := isequiv_group_right_op G y
  |}
      refine (_ @ path_trunctype_pp _ _).
H: Univalence
G: Group
x, y: G
path_trunctype
  {|
    equiv_fun := fun t : G => t * (x * y);
    equiv_isequiv := isequiv_group_right_op G (x * y)
  |} =
path_trunctype
  ({|
     equiv_fun := fun t : G => t * y;
     equiv_isequiv := isequiv_group_right_op G y
   |}
   oE {|
        equiv_fun := fun t : G => t * x;
        equiv_isequiv := isequiv_group_right_op G x
      |})
      apply ap, path_equiv, path_forall.
H: Univalence
G: Group
x, y: G
{|
  equiv_fun := fun t : G => t * (x * y);
  equiv_isequiv := isequiv_group_right_op G (x * y)
|} ==
{|
  equiv_fun := fun t : G => t * y;
  equiv_isequiv := isequiv_group_right_op G y
|}
oE {|
     equiv_fun := fun t : G => t * x;
     equiv_isequiv := isequiv_group_right_op G x
   |}
      intro; cbn.
H: Univalence
G: Group
x, y: G
x0: Build_HSet G
x0 * (x * y) = x0 * x * y
      apply associativity.
  Defined.

  Local Definition encode : forall b, bbase = b -> codes b.
H: Univalence
G: Group
forall b : ClassifyingSpace G, bbase = b -> codes b
  Proof.
H: Univalence
G: Group
forall b : ClassifyingSpace G, bbase = b -> codes b
    intros b p.
H: Univalence
G: Group
b: ClassifyingSpace G
p: bbase = b
codes b
    exact (transport codes p mon_unit).
  Defined.

  Local Definition codes_transport
    : forall x y : G, transport codes (bloop x) y = y * x.
H: Univalence
G: Group
forall x y : G,
transport (fun x0 : B G => codes x0) (bloop x) y =
y * x
  Proof.
H: Univalence
G: Group
forall x y : G,
transport (fun x0 : B G => codes x0) (bloop x) y =
y * x
    intros x y.
H: Univalence
G: Group
x, y: G
transport (fun x : B G => codes x) (bloop x) y = y * x
    lhs napply (transport_idmap_ap _ (bloop x)).
H: Univalence
G: Group
x, y: G
transport idmap
  (ap (fun x : B G => codes x) (bloop x)) y = y * x
    rhs_V rapply (transport_path_universe (.* x)).
H: Univalence
G: Group
x, y: G
transport idmap
  (ap (fun x : B G => codes x) (bloop x)) y =
transport idmap (path_universe (fun y : G => y * x)) y
    napply (transport2 idmap).
H: Univalence
G: Group
x, y: G
ap (fun x : B G => codes x) (bloop x) =
path_universe (fun y : G => y * x)
    lhs napply (ap_compose _ trunctype_type (bloop x)).
H: Univalence
G: Group
x, y: G
ap trunctype_type (ap codes (bloop x)) =
path_universe (fun y : G => y * x)
    rhs_V napply ap_trunctype; apply ap.
H: Univalence
G: Group
x, y: G
ap codes (bloop x) =
path_trunctype
  {|
    equiv_fun := fun y : G => y * x;
    equiv_isequiv := isequiv_group_right_op G x
  |}
    napply ClassifyingSpace_rec_beta_bloop.
  Defined.

  Local Definition decode : forall (b : B G), codes b -> bbase = b.
H: Univalence
G: Group
forall b : B G, codes b -> bbase = b
  Proof.
H: Univalence
G: Group
forall b : B G, codes b -> bbase = b
    srapply ClassifyingSpace_ind_hset.
H: Univalence
G: Group
(fun b : ClassifyingSpace G => codes b -> bbase = b)
  bbase
H: Univalence
G: Group
forall x : G,
DPath
  (fun b : ClassifyingSpace G => codes b -> bbase = b)
  (bloop x) ?bbase' ?bbase'
    +
H: Univalence
G: Group
(fun b : ClassifyingSpace G => codes b -> bbase = b)
  bbase exact bloop.
    +
H: Univalence
G: Group
forall x : G,
DPath
  (fun b : ClassifyingSpace G => codes b -> bbase = b)
  (bloop x) bloop bloop intro x.
H: Univalence
G: Group
x: G
DPath
  (fun b : ClassifyingSpace G => codes b -> bbase = b)
  (bloop x) bloop bloop
      apply dp_arrow.
H: Univalence
G: Group
x: G
forall x0 : codes bbase,
DPath (paths bbase) (bloop x) (bloop x0)
  (bloop
     (transport
        (fun x : ClassifyingSpace G => codes x)
        (bloop x) x0))
      intro y; cbn in *.
H: Univalence
G: Group
x, y: G
transport (paths bbase) (bloop x) (bloop y) =
bloop
  (transport (fun x : ClassifyingSpace G => codes x)
     (bloop x) y)
      apply dp_paths_r.
H: Univalence
G: Group
x, y: G
bloop y @ bloop x =
bloop
  (transport (fun x : ClassifyingSpace G => codes x)
     (bloop x) y)
      refine ((bloop_pp _ _)^ @ _).
H: Univalence
G: Group
x, y: G
bloop (y * x) =
bloop
  (transport (fun x : ClassifyingSpace G => codes x)
     (bloop x) y)
      symmetry.
H: Univalence
G: Group
x, y: G
bloop
  (transport (fun x : ClassifyingSpace G => codes x)
     (bloop x) y) = bloop (y * x)
      apply ap, codes_transport.
  Defined.

  Local Lemma decode_encode : forall b p, decode b (encode b p) = p.
H: Univalence
G: Group
forall (b : B G) (p : bbase = b),
decode b (encode b p) = p
  Proof.
H: Univalence
G: Group
forall (b : B G) (p : bbase = b),
decode b (encode b p) = p
    intros b p.
H: Univalence
G: Group
b: B G
p: bbase = b
decode b (encode b p) = p
    destruct p.
H: Univalence
G: Group
decode bbase (encode bbase 1) = 1
    exact bloop_id.
  Defined.

  #[export] Instance isequiv_bloop : IsEquiv (@bloop G).
H: Univalence
G: Group
IsEquiv bloop
  Proof.
H: Univalence
G: Group
IsEquiv bloop
    srapply isequiv_adjointify.
H: Univalence
G: Group
bbase = bbase -> G
H: Univalence
G: Group
bloop o ?g == idmap
H: Univalence
G: Group
?g o bloop == idmap
    +
H: Univalence
G: Group
bbase = bbase -> G exact (encode _).
    +
H: Univalence
G: Group
bloop o encode bbase == idmap rapply decode_encode.
    +
H: Univalence
G: Group
encode bbase o bloop == idmap intro x.
H: Univalence
G: Group
x: G
encode bbase (bloop x) = x
      refine (codes_transport _ _ @ _).
H: Univalence
G: Group
x: G
mon_unit * x = x
      apply left_identity.
  Defined.

  (** The defining property of BG. *)
  Definition equiv_g_loops_bg : G <~> loops (B G)
    := Build_Equiv _ _ bloop _.

  (** Pointed version of the defining property. *)
  Definition pequiv_g_loops_bg : G <~>* loops (B G)
    := Build_pEquiv pbloop _.

  Definition pequiv_loops_bg_g := pequiv_g_loops_bg^-1*%equiv.

  (** We also have that the equivalence is a group isomorphism. *)

  (** First we show that the loop space of a pointed 1-type is a group. *)
  Definition LoopGroup (X : pType) `{IsTrunc 1 X} : Group
    := Build_Group (loops X) concat idpath inverse
      (Build_IsGroup _ _ _ _
        (Build_IsMonoid _ _ _
          (Build_IsSemiGroup _ _ _ concat_p_pp) concat_1p concat_p1)
        concat_Vp concat_pV).

  Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
H: Univalence
G: Group
GroupIsomorphism G (LoopGroup (B G))
  Proof.
H: Univalence
G: Group
GroupIsomorphism G (LoopGroup (B G))
    snapply Build_GroupIsomorphism'.
H: Univalence
G: Group
G <~> LoopGroup (B G)
H: Univalence
G: Group
IsSemiGroupPreserving ?f
    1: exact equiv_g_loops_bg.
H: Univalence
G: Group
IsSemiGroupPreserving equiv_g_loops_bg
    intros x y.
H: Univalence
G: Group
x, y: G
equiv_g_loops_bg (x * y) =
equiv_g_loops_bg x * equiv_g_loops_bg y
    apply bloop_pp.
  Defined.

  Definition grp_iso_g_pi1_bg : GroupIsomorphism G (Pi1 (B G)).
H: Univalence
G: Group
GroupIsomorphism G (Pi1 (B G))
  Proof.
H: Univalence
G: Group
GroupIsomorphism G (Pi1 (B G))
    snapply (transitive_groupisomorphism _ _ _ grp_iso_g_loopgroup_bg).
H: Univalence
G: Group
GroupIsomorphism (LoopGroup (B G)) (Pi1 (B G))
    snapply Build_GroupIsomorphism'.
H: Univalence
G: Group
LoopGroup (B G) <~> Pi1 (B G)
H: Univalence
G: Group
IsSemiGroupPreserving ?f
    -
H: Univalence
G: Group
LoopGroup (B G) <~> Pi1 (B G) rapply equiv_tr.
    -
H: Univalence
G: Group
IsSemiGroupPreserving (equiv_tr 0 (LoopGroup (B G))) intros x y; reflexivity.
  Defined.

  (* We also record this fact. *)
  Definition grp_homo_loops {X Y : pType} `{IsTrunc 1 X} `{IsTrunc 1 Y}
    : (X ->** Y) ->* [LoopGroup X $-> LoopGroup Y, grp_homo_const].
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(X ->** Y) ->*
[LoopGroup X $-> LoopGroup Y, grp_homo_const]
  Proof.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(X ->** Y) ->*
[LoopGroup X $-> LoopGroup Y, grp_homo_const]
    snapply Build_pMap.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(X ->** Y) ->
[LoopGroup X $-> LoopGroup Y, grp_homo_const]
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
?f pt = pt
    -
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(X ->** Y) ->
[LoopGroup X $-> LoopGroup Y, grp_homo_const] intro f.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
f: X ->** Y
[LoopGroup X $-> LoopGroup Y, grp_homo_const]
      snapply Build_GroupHomomorphism.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
f: X ->** Y
LoopGroup X -> LoopGroup Y
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
f: X ->** Y
IsSemiGroupPreserving ?grp_homo_map
      +
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
f: X ->** Y
LoopGroup X -> LoopGroup Y exact (fmap loops f).
      +
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
f: X ->** Y
IsSemiGroupPreserving (fmap loops f) napply fmap_loops_pp.
    -
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(fun f : X ->** Y =>
 {|
   grp_homo_map := fmap loops f;
   issemigrouppreserving_grp_homo := fmap_loops_pp f
 |}) pt = pt cbn beta.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
{|
  grp_homo_map := fmap loops pt;
  issemigrouppreserving_grp_homo := fmap_loops_pp pt
|} = pt
      apply equiv_path_grouphomomorphism.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
{|
  grp_homo_map := fmap loops pt;
  issemigrouppreserving_grp_homo := fmap_loops_pp pt
|} == pt
      exact (pointed_htpy fmap_loops_pconst).
  Defined.

End EncodeDecode.

(** When [G] is an abelian group, [BG] is an H-space. *)
Section HSpace_bg.

  Context {G : AbGroup}.

  Definition bg_mul : B G -> B G -> B G.
G: AbGroup
B G -> B G -> B G
  Proof.
G: AbGroup
B G -> B G -> B G
    intro b.
G: AbGroup
b: B G
B G -> B G
    snapply ClassifyingSpace_rec.
G: AbGroup
b: B G
IsTrunc 1 (B G)
G: AbGroup
b: B G
B G
G: AbGroup
b: B G
G -> ?bbase' = ?bbase'
G: AbGroup
b: B G
forall x y : G,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    1: exact _.
G: AbGroup
b: B G
B G
G: AbGroup
b: B G
G -> ?bbase' = ?bbase'
G: AbGroup
b: B G
forall x y : G,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    1: exact b.
G: AbGroup
b: B G
G -> b = b
G: AbGroup
b: B G
forall x y : G,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    {
G: AbGroup
b: B G
G -> b = b intro x.
G: AbGroup
b: B G
x: G
b = b
      revert b.
G: AbGroup
x: G
forall b : B G, b = b
      snapply ClassifyingSpace_ind_hset.
G: AbGroup
x: G
forall b : ClassifyingSpace G,
IsHSet ((fun b0 : ClassifyingSpace G => b0 = b0) b)
G: AbGroup
x: G
(fun b : ClassifyingSpace G => b = b) bbase
G: AbGroup
x: G
forall x0 : G,
DPath (fun b : ClassifyingSpace G => b = b) (bloop x0)
  ?bbase' ?bbase'
      1: exact _.
G: AbGroup
x: G
(fun b : ClassifyingSpace G => b = b) bbase
G: AbGroup
x: G
forall x0 : G,
DPath (fun b : ClassifyingSpace G => b = b) (bloop x0)
  ?bbase' ?bbase'
      1: exact (bloop x).
G: AbGroup
x: G
forall x0 : G,
DPath (fun b : ClassifyingSpace G => b = b) (bloop x0)
  (bloop x) (bloop x)
      cbn; intro y.
G: AbGroup
x, y: G
transport (fun b : ClassifyingSpace G => b = b)
  (bloop y) (bloop x) = bloop x
      apply dp_paths_lr.
G: AbGroup
x, y: G
((bloop y)^ @ bloop x) @ bloop y = bloop x
      refine (concat_pp_p _ _ _ @ _).
G: AbGroup
x, y: G
(bloop y)^ @ (bloop x @ bloop y) = bloop x
      apply moveR_Vp.
G: AbGroup
x, y: G
bloop x @ bloop y = bloop y @ bloop x
      refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _).
G: AbGroup
x, y: G
bloop (x * y) = bloop (y * x)
      apply ap, commutativity. }
G: AbGroup
b: B G
forall x y : G,
(fun x0 : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x0)
   ((fun y0 : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y0) (bloop x0) (bloop x0)
       (concat_pp_p (bloop y0)^ (bloop x0) (bloop y0) @
        moveR_Vp (bloop x0 @ bloop y0) (bloop x0)
          (bloop y0)
          (((bloop_pp x0 y0)^ @
            ap bloop (commutativity x0 y0)) @
           bloop_pp y0 x0)))
    :
    forall x1 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x1) (bloop x0) (bloop x0)) b) (x * y) =
(fun x0 : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x0)
   ((fun y0 : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y0) (bloop x0) (bloop x0)
       (concat_pp_p (bloop y0)^ (bloop x0) (bloop y0) @
        moveR_Vp (bloop x0 @ bloop y0) (bloop x0)
          (bloop y0)
          (((bloop_pp x0 y0)^ @
            ap bloop (commutativity x0 y0)) @
           bloop_pp y0 x0)))
    :
    forall x1 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x1) (bloop x0) (bloop x0)) b) x @
(fun x0 : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x0)
   ((fun y0 : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y0) (bloop x0) (bloop x0)
       (concat_pp_p (bloop y0)^ (bloop x0) (bloop y0) @
        moveR_Vp (bloop x0 @ bloop y0) (bloop x0)
          (bloop y0)
          (((bloop_pp x0 y0)^ @
            ap bloop (commutativity x0 y0)) @
           bloop_pp y0 x0)))
    :
    forall x1 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x1) (bloop x0) (bloop x0)) b) y
    intros x y.
G: AbGroup
b: B G
x, y: G
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x0) (bloop x) (bloop x)) b) (x * y) =
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x0) (bloop x) (bloop x)) b) x @
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b : ClassifyingSpace G => b = b) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b : ClassifyingSpace G => b = b)
      (bloop x0) (bloop x) (bloop x)) b) y
    revert b.
G: AbGroup
x, y: G
forall b : B G,
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b0 : ClassifyingSpace G => b0 = b0)
      (bloop x0) (bloop x) (bloop x)) b) (x * y) =
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b0 : ClassifyingSpace G => b0 = b0)
      (bloop x0) (bloop x) (bloop x)) b) x @
(fun x : G =>
 ClassifyingSpace_ind_hset
   (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
   ((fun y : G =>
     let X :=
       fun p q r : bbase = bbase =>
       equiv_fun (dp_paths_lr p q r) in
     X (bloop y) (bloop x) (bloop x)
       (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
        moveR_Vp (bloop x @ bloop y) (bloop x)
          (bloop y)
          (((bloop_pp x y)^ @
            ap bloop (commutativity x y)) @
           bloop_pp y x)))
    :
    forall x0 : G,
    DPath (fun b0 : ClassifyingSpace G => b0 = b0)
      (bloop x0) (bloop x) (bloop x)) b) y
    srapply ClassifyingSpace_ind_hprop.
G: AbGroup
x, y: G
(fun b : ClassifyingSpace G =>
 (fun x : G =>
  ClassifyingSpace_ind_hset
    (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
    ((fun y : G =>
      let X :=
        fun p q r : bbase = bbase =>
        equiv_fun (dp_paths_lr p q r) in
      X (bloop y) (bloop x) (bloop x)
        (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
         moveR_Vp (bloop x @ bloop y) (bloop x)
           (bloop y)
           (((bloop_pp x y)^ @
             ap bloop (commutativity x y)) @
            bloop_pp y x)))
     :
     forall x0 : G,
     DPath (fun b0 : ClassifyingSpace G => b0 = b0)
       (bloop x0) (bloop x) (bloop x)) b) (x * y) =
 (fun x : G =>
  ClassifyingSpace_ind_hset
    (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
    ((fun y : G =>
      let X :=
        fun p q r : bbase = bbase =>
        equiv_fun (dp_paths_lr p q r) in
      X (bloop y) (bloop x) (bloop x)
        (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
         moveR_Vp (bloop x @ bloop y) (bloop x)
           (bloop y)
           (((bloop_pp x y)^ @
             ap bloop (commutativity x y)) @
            bloop_pp y x)))
     :
     forall x0 : G,
     DPath (fun b0 : ClassifyingSpace G => b0 = b0)
       (bloop x0) (bloop x) (bloop x)) b) x @
 (fun x : G =>
  ClassifyingSpace_ind_hset
    (fun b0 : ClassifyingSpace G => b0 = b0) (bloop x)
    ((fun y : G =>
      let X :=
        fun p q r : bbase = bbase =>
        equiv_fun (dp_paths_lr p q r) in
      X (bloop y) (bloop x) (bloop x)
        (concat_pp_p (bloop y)^ (bloop x) (bloop y) @
         moveR_Vp (bloop x @ bloop y) (bloop x)
           (bloop y)
           (((bloop_pp x y)^ @
             ap bloop (commutativity x y)) @
            bloop_pp y x)))
     :
     forall x0 : G,
     DPath (fun b0 : ClassifyingSpace G => b0 = b0)
       (bloop x0) (bloop x) (bloop x)) b) y) bbase
    exact (bloop_pp x y).
  Defined.

  Definition bg_mul_symm : forall x y, bg_mul x y = bg_mul y x.
G: AbGroup
forall x y : B G, bg_mul x y = bg_mul y x
  Proof.
G: AbGroup
forall x y : B G, bg_mul x y = bg_mul y x
    intros x.
G: AbGroup
x: B G
forall y : B G, bg_mul x y = bg_mul y x
    srapply ClassifyingSpace_ind_hset.
G: AbGroup
x: B G
(fun b : ClassifyingSpace G => bg_mul x b = bg_mul b x)
  bbase
G: AbGroup
x: B G
forall x0 : G,
DPath
  (fun b : ClassifyingSpace G =>
   bg_mul x b = bg_mul b x) (bloop x0) ?bbase' ?bbase'
    {
G: AbGroup
x: B G
(fun b : ClassifyingSpace G => bg_mul x b = bg_mul b x)
  bbase simpl.
G: AbGroup
x: B G
x = bg_mul bbase x
      revert x.
G: AbGroup
forall x : B G, x = bg_mul bbase x
      srapply ClassifyingSpace_ind_hset.
G: AbGroup
(fun b : ClassifyingSpace G => b = bg_mul bbase b)
  bbase
G: AbGroup
forall x : G,
DPath
  (fun b : ClassifyingSpace G => b = bg_mul bbase b)
  (bloop x) ?bbase' ?bbase'
      1: reflexivity.
G: AbGroup
forall x : G,
DPath
  (fun b : ClassifyingSpace G => b = bg_mul bbase b)
  (bloop x) 1 1
      intros x.
G: AbGroup
x: G
DPath
  (fun b : ClassifyingSpace G => b = bg_mul bbase b)
  (bloop x) 1 1
      apply sq_dp^-1, sq_1G.
G: AbGroup
x: G
ap idmap (bloop x) = ap (bg_mul bbase) (bloop x)
      refine (ap_idmap _ @ _^).
G: AbGroup
x: G
ap (bg_mul bbase) (bloop x) = bloop x
      napply ClassifyingSpace_rec_beta_bloop. }
G: AbGroup
x: B G
forall x0 : G,
DPath
  (fun b : ClassifyingSpace G =>
   bg_mul x b = bg_mul b x) (bloop x0)
  (ClassifyingSpace_ind_hset
     (fun b : ClassifyingSpace G => b = bg_mul bbase b)
     1
     (fun x : G =>
      sq_dp^-1
        (let X := equiv_fun sq_1G in
         X
           (ap_idmap (bloop x) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x1 : G =>
                ClassifyingSpace_ind_hset
                  (fun b : ClassifyingSpace G => b = b)
                  (bloop x1)
                  ((fun y : G =>
                    let X0 :=
                      fun p q r : ... =>
                      equiv_fun (...) in
                    X0 (bloop y) (bloop x1) (bloop x1)
                      (concat_pp_p ...^ ... ... @
                       moveR_Vp ... ... ... ...))
                   :
                   forall x2 : G,
                   DPath
                     (fun b : ClassifyingSpace G =>
                      b = b) (bloop x2) (bloop x1)
                     (bloop x1)) bbase)
               (fun x1 y : G =>
                ClassifyingSpace_ind_hprop
                  (fun b : ClassifyingSpace G =>
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset
                      (... => ...) (bloop x2)
                      (... : ...) b) (x1 * y) =
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) x1 @
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) y)
                  (bloop_pp x1 y) bbase) x)^))) x
   :
   (fun b : ClassifyingSpace G =>
    bg_mul x b = bg_mul b x) bbase)
  (ClassifyingSpace_ind_hset
     (fun b : ClassifyingSpace G => b = bg_mul bbase b)
     1
     (fun x : G =>
      sq_dp^-1
        (let X := equiv_fun sq_1G in
         X
           (ap_idmap (bloop x) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x1 : G =>
                ClassifyingSpace_ind_hset
                  (fun b : ClassifyingSpace G => b = b)
                  (bloop x1)
                  ((fun y : G =>
                    let X0 :=
                      fun p q r : ... =>
                      equiv_fun (...) in
                    X0 (bloop y) (bloop x1) (bloop x1)
                      (concat_pp_p ...^ ... ... @
                       moveR_Vp ... ... ... ...))
                   :
                   forall x2 : G,
                   DPath
                     (fun b : ClassifyingSpace G =>
                      b = b) (bloop x2) (bloop x1)
                     (bloop x1)) bbase)
               (fun x1 y : G =>
                ClassifyingSpace_ind_hprop
                  (fun b : ClassifyingSpace G =>
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset
                      (... => ...) (bloop x2)
                      (... : ...) b) (x1 * y) =
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) x1 @
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) y)
                  (bloop_pp x1 y) bbase) x)^))) x
   :
   (fun b : ClassifyingSpace G =>
    bg_mul x b = bg_mul b x) bbase)
    intros y; revert x.
G: AbGroup
y: G
forall x : B G,
DPath
  (fun b : ClassifyingSpace G =>
   bg_mul x b = bg_mul b x) (bloop y)
  (ClassifyingSpace_ind_hset
     (fun b : ClassifyingSpace G => b = bg_mul bbase b)
     1
     (fun x0 : G =>
      sq_dp^-1
        (let X := equiv_fun sq_1G in
         X
           (ap_idmap (bloop x0) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x1 : G =>
                ClassifyingSpace_ind_hset
                  (fun b : ClassifyingSpace G => b = b)
                  (bloop x1)
                  ((fun y : G =>
                    let X0 :=
                      fun p q r : ... =>
                      equiv_fun (...) in
                    X0 (bloop y) (bloop x1) (bloop x1)
                      (concat_pp_p ...^ ... ... @
                       moveR_Vp ... ... ... ...))
                   :
                   forall x2 : G,
                   DPath
                     (fun b : ClassifyingSpace G =>
                      b = b) (bloop x2) (bloop x1)
                     (bloop x1)) bbase)
               (fun x1 y : G =>
                ClassifyingSpace_ind_hprop
                  (fun b : ClassifyingSpace G =>
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset
                      (... => ...) (bloop x2)
                      (... : ...) b) (x1 * y) =
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) x1 @
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) y)
                  (bloop_pp x1 y) bbase) x0)^))) x
   :
   (fun b : ClassifyingSpace G =>
    bg_mul x b = bg_mul b x) bbase)
  (ClassifyingSpace_ind_hset
     (fun b : ClassifyingSpace G => b = bg_mul bbase b)
     1
     (fun x0 : G =>
      sq_dp^-1
        (let X := equiv_fun sq_1G in
         X
           (ap_idmap (bloop x0) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x1 : G =>
                ClassifyingSpace_ind_hset
                  (fun b : ClassifyingSpace G => b = b)
                  (bloop x1)
                  ((fun y : G =>
                    let X0 :=
                      fun p q r : ... =>
                      equiv_fun (...) in
                    X0 (bloop y) (bloop x1) (bloop x1)
                      (concat_pp_p ...^ ... ... @
                       moveR_Vp ... ... ... ...))
                   :
                   forall x2 : G,
                   DPath
                     (fun b : ClassifyingSpace G =>
                      b = b) (bloop x2) (bloop x1)
                     (bloop x1)) bbase)
               (fun x1 y : G =>
                ClassifyingSpace_ind_hprop
                  (fun b : ClassifyingSpace G =>
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset
                      (... => ...) (bloop x2)
                      (... : ...) b) (x1 * y) =
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) x1 @
                   (fun x2 : G =>
                    ClassifyingSpace_ind_hset (...)
                      (...) (...) b) y)
                  (bloop_pp x1 y) bbase) x0)^))) x
   :
   (fun b : ClassifyingSpace G =>
    bg_mul x b = bg_mul b x) bbase)
    simpl.
G: AbGroup
y: G
forall x : ClassifyingSpace G,
transport
  (fun b : ClassifyingSpace G =>
   bg_mul x b = bg_mul b x) (bloop y)
  (ClassifyingSpace_ind_hset
     (fun b : ClassifyingSpace G => b = bg_mul bbase b)
     1
     (fun x0 : G =>
      sq_dp^-1
        (match
           ap idmap (bloop x0) as p in (_ = a)
           return
             (forall px1 : a = bbase,
              1 @ ap (bg_mul bbase) (bloop x0) =
              p @ px1 ->
              PathSquare 1 px1 p
                (ap (bg_mul bbase) (bloop x0)))
         with
         | 1 =>
             fun px1 : bbase = bbase =>
             match
               ap (bg_mul bbase) (bloop x0) as p in
               (_ = a)
               return
                 (forall px2 : bbase = a,
                  1 @ p = 1 @ px2 ->
                  PathSquare 1 px2 1 p)
             with
             | 1 =>
                 fun (px2 : bbase = bbase)
                   (e : 1 = 1 @ px2) =>
                 match
                   e @ concat_1p px2 in (_ = p)
                   return
                     (1 = 1 @ p -> PathSquare 1 p 1 1)
                 with
                 | 1 => fun _ : 1 = 1 => 1%square
                 end e
             end px1
         end 1
           ((concat_1p (ap (bg_mul bbase) (bloop x0)) @
             (ap_idmap (bloop x0) @
              (ClassifyingSpace_rec_beta_bloop
                 (ClassifyingSpace G) bbase
                 (fun x1 : G => bloop x1)
                 (fun x1 y : G => bloop_pp x1 y) x0)^)^) @
            (concat_p1 (ap idmap (bloop x0)))^))) x) =
ClassifyingSpace_ind_hset
  (fun b : ClassifyingSpace G => b = bg_mul bbase b) 1
  (fun x0 : G =>
   sq_dp^-1
     (match
        ap idmap (bloop x0) as p in (_ = a)
        return
          (forall px1 : a = bbase,
           1 @ ap (bg_mul bbase) (bloop x0) = p @ px1 ->
           PathSquare 1 px1 p
             (ap (bg_mul bbase) (bloop x0)))
      with
      | 1 =>
          fun px1 : bbase = bbase =>
          match
            ap (bg_mul bbase) (bloop x0) as p in
            (_ = a)
            return
              (forall px2 : bbase = a,
               1 @ p = 1 @ px2 -> PathSquare 1 px2 1 p)
          with
          | 1 =>
              fun (px2 : bbase = bbase)
                (e : 1 = 1 @ px2) =>
              match
                e @ concat_1p px2 in (_ = p)
                return
                  (1 = 1 @ p -> PathSquare 1 p 1 1)
              with
              | 1 => fun _ : 1 = 1 => 1%square
              end e
          end px1
      end 1
        ((concat_1p (ap (bg_mul bbase) (bloop x0)) @
          (ap_idmap (bloop x0) @
           (ClassifyingSpace_rec_beta_bloop
              (ClassifyingSpace G) bbase
              (fun x1 : G => bloop x1)
              (fun x1 y : G => bloop_pp x1 y) x0)^)^) @
         (concat_p1 (ap idmap (bloop x0)))^))) x
    snapply ClassifyingSpace_ind_hprop.
G: AbGroup
y: G
forall b : ClassifyingSpace G,
IsHProp
  ((fun b0 : ClassifyingSpace G =>
    transport
      (fun b1 : ClassifyingSpace G =>
       bg_mul b0 b1 = bg_mul b1 b0) (bloop y)
      (ClassifyingSpace_ind_hset
         (fun b1 : ClassifyingSpace G =>
          b1 = bg_mul bbase b1) 1
         (fun x : G =>
          sq_dp^-1
            (match
               ap idmap (bloop x) as p in (_ = a)
               return
                 (forall px1 : a = bbase,
                  1 @ ap (bg_mul bbase) (bloop x) =
                  p @ px1 ->
                  PathSquare 1 px1 p
                    (ap (bg_mul bbase) (bloop x)))
             with
             | 1 =>
                 fun px1 : bbase = bbase =>
                 match
                   ap (bg_mul bbase) (bloop x) as p in
                   (_ = a)
                   return
                     (forall px2 : bbase = a,
                      ... = ... ->
                      PathSquare 1 px2 1 p)
                 with
                 | 1 =>
                     fun (px2 : bbase = bbase)
                       (e : 1 = 1 @ px2) =>
                     match ... in ... return ... with
                     | 1 => fun ... => 1%square
                     end e
                 end px1
             end 1
               ((concat_1p
                   (ap (bg_mul bbase) (bloop x)) @
                 (ap_idmap (bloop x) @
                  (ClassifyingSpace_rec_beta_bloop
                     (ClassifyingSpace G) bbase
                     (fun x0 : G => bloop x0)
                     (fun x0 y : G => bloop_pp x0 y) x)^)^) @
                (concat_p1 (ap idmap (bloop x)))^)))
         b0) =
    ClassifyingSpace_ind_hset
      (fun b1 : ClassifyingSpace G =>
       b1 = bg_mul bbase b1) 1
      (fun x : G =>
       sq_dp^-1
         (match
            ap idmap (bloop x) as p in (_ = a)
            return
              (forall px1 : a = bbase,
               1 @ ap (bg_mul bbase) (bloop x) =
               p @ px1 ->
               PathSquare 1 px1 p
                 (ap (bg_mul bbase) (bloop x)))
          with
          | 1 =>
              fun px1 : bbase = bbase =>
              match
                ap (bg_mul bbase) (bloop x) as p in
                (_ = a)
                return
                  (forall px2 : bbase = a,
                   1 @ p = 1 @ px2 ->
                   PathSquare 1 px2 1 p)
              with
              | 1 =>
                  fun (px2 : bbase = bbase)
                    (e : 1 = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return (... -> ...)
                  with
                  | 1 => fun _ : 1 = 1 => 1%square
                  end e
              end px1
          end 1
            ((concat_1p (ap (bg_mul bbase) (bloop x)) @
              (ap_idmap (bloop x) @
               (ClassifyingSpace_rec_beta_bloop
                  (ClassifyingSpace G) bbase
                  (fun x0 : G => bloop x0)
                  (fun x0 y : G => bloop_pp x0 y) x)^)^) @
             (concat_p1 (ap idmap (bloop x)))^))) b0)
     b)
G: AbGroup
y: G
(fun b : ClassifyingSpace G =>
 transport
   (fun b0 : ClassifyingSpace G =>
    bg_mul b b0 = bg_mul b0 b) (bloop y)
   (ClassifyingSpace_ind_hset
      (fun b0 : ClassifyingSpace G =>
       b0 = bg_mul bbase b0) 1
      (fun x : G =>
       sq_dp^-1
         (match
            ap idmap (bloop x) as p in (_ = a)
            return
              (forall px1 : a = bbase,
               1 @ ap (bg_mul bbase) (bloop x) =
               p @ px1 ->
               PathSquare 1 px1 p
                 (ap (bg_mul bbase) (bloop x)))
          with
          | 1 =>
              fun px1 : bbase = bbase =>
              match
                ap (bg_mul bbase) (bloop x) as p in
                (_ = a)
                return
                  (forall px2 : bbase = a,
                   1 @ p = 1 @ px2 ->
                   PathSquare 1 px2 1 p)
              with
              | 1 =>
                  fun (px2 : bbase = bbase)
                    (e : 1 = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return
                      (1 = ... -> PathSquare 1 p 1 1)
                  with
                  | 1 => fun _ : 1 = 1 => 1%square
                  end e
              end px1
          end 1
            ((concat_1p (ap (bg_mul bbase) (bloop x)) @
              (ap_idmap (bloop x) @
               (ClassifyingSpace_rec_beta_bloop
                  (ClassifyingSpace G) bbase
                  (fun x0 : G => bloop x0)
                  (fun x0 y : G => bloop_pp x0 y) x)^)^) @
             (concat_p1 (ap idmap (bloop x)))^))) b) =
 ClassifyingSpace_ind_hset
   (fun b0 : ClassifyingSpace G =>
    b0 = bg_mul bbase b0) 1
   (fun x : G =>
    sq_dp^-1
      (match
         ap idmap (bloop x) as p in (_ = a)
         return
           (forall px1 : a = bbase,
            1 @ ap (bg_mul bbase) (bloop x) = p @ px1 ->
            PathSquare 1 px1 p
              (ap (bg_mul bbase) (bloop x)))
       with
       | 1 =>
           fun px1 : bbase = bbase =>
           match
             ap (bg_mul bbase) (bloop x) as p in
             (_ = a)
             return
               (forall px2 : bbase = a,
                1 @ p = 1 @ px2 ->
                PathSquare 1 px2 1 p)
           with
           | 1 =>
               fun (px2 : bbase = bbase)
                 (e : 1 = 1 @ px2) =>
               match
                 e @ concat_1p px2 in (_ = p)
                 return
                   (1 = 1 @ p -> PathSquare 1 p 1 1)
               with
               | 1 => fun _ : 1 = 1 => 1%square
               end e
           end px1
       end 1
         ((concat_1p (ap (bg_mul bbase) (bloop x)) @
           (ap_idmap (bloop x) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x0 : G => bloop x0)
               (fun x0 y : G => bloop_pp x0 y) x)^)^) @
          (concat_p1 (ap idmap (bloop x)))^))) b)
  bbase
    1: exact _.
G: AbGroup
y: G
(fun b : ClassifyingSpace G =>
 transport
   (fun b0 : ClassifyingSpace G =>
    bg_mul b b0 = bg_mul b0 b) (bloop y)
   (ClassifyingSpace_ind_hset
      (fun b0 : ClassifyingSpace G =>
       b0 = bg_mul bbase b0) 1
      (fun x : G =>
       sq_dp^-1
         (match
            ap idmap (bloop x) as p in (_ = a)
            return
              (forall px1 : a = bbase,
               1 @ ap (bg_mul bbase) (bloop x) =
               p @ px1 ->
               PathSquare 1 px1 p
                 (ap (bg_mul bbase) (bloop x)))
          with
          | 1 =>
              fun px1 : bbase = bbase =>
              match
                ap (bg_mul bbase) (bloop x) as p in
                (_ = a)
                return
                  (forall px2 : bbase = a,
                   1 @ p = 1 @ px2 ->
                   PathSquare 1 px2 1 p)
              with
              | 1 =>
                  fun (px2 : bbase = bbase)
                    (e : 1 = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return
                      (1 = ... -> PathSquare 1 p 1 1)
                  with
                  | 1 => fun _ : 1 = 1 => 1%square
                  end e
              end px1
          end 1
            ((concat_1p (ap (bg_mul bbase) (bloop x)) @
              (ap_idmap (bloop x) @
               (ClassifyingSpace_rec_beta_bloop
                  (ClassifyingSpace G) bbase
                  (fun x0 : G => bloop x0)
                  (fun x0 y : G => bloop_pp x0 y) x)^)^) @
             (concat_p1 (ap idmap (bloop x)))^))) b) =
 ClassifyingSpace_ind_hset
   (fun b0 : ClassifyingSpace G =>
    b0 = bg_mul bbase b0) 1
   (fun x : G =>
    sq_dp^-1
      (match
         ap idmap (bloop x) as p in (_ = a)
         return
           (forall px1 : a = bbase,
            1 @ ap (bg_mul bbase) (bloop x) = p @ px1 ->
            PathSquare 1 px1 p
              (ap (bg_mul bbase) (bloop x)))
       with
       | 1 =>
           fun px1 : bbase = bbase =>
           match
             ap (bg_mul bbase) (bloop x) as p in
             (_ = a)
             return
               (forall px2 : bbase = a,
                1 @ p = 1 @ px2 ->
                PathSquare 1 px2 1 p)
           with
           | 1 =>
               fun (px2 : bbase = bbase)
                 (e : 1 = 1 @ px2) =>
               match
                 e @ concat_1p px2 in (_ = p)
                 return
                   (1 = 1 @ p -> PathSquare 1 p 1 1)
               with
               | 1 => fun _ : 1 = 1 => 1%square
               end e
           end px1
       end 1
         ((concat_1p (ap (bg_mul bbase) (bloop x)) @
           (ap_idmap (bloop x) @
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace G) bbase
               (fun x0 : G => bloop x0)
               (fun x0 y : G => bloop_pp x0 y) x)^)^) @
          (concat_p1 (ap idmap (bloop x)))^))) b)
  bbase
    simpl.
G: AbGroup
y: G
transport
  (fun b : ClassifyingSpace G => bg_mul bbase b = b)
  (bloop y) 1 = 1
    transport_paths Flr.
G: AbGroup
y: G
ap (bg_mul bbase) (bloop y) @ 1 = 1 @ bloop y
    apply equiv_p1_1q.
G: AbGroup
y: G
ap (bg_mul bbase) (bloop y) = bloop y
    napply ClassifyingSpace_rec_beta_bloop.
  Defined.

  Definition bg_mul_left_id
    : forall b : B G, bg_mul bbase b = b.
G: AbGroup
forall b : B G, bg_mul bbase b = b
  Proof.
G: AbGroup
forall b : B G, bg_mul bbase b = b
    apply bg_mul_symm.
  Defined.

  Definition bg_mul_right_id
    : forall b : B G, bg_mul b bbase = b.
G: AbGroup
forall b : B G, bg_mul b bbase = b
  Proof.
G: AbGroup
forall b : B G, bg_mul b bbase = b
    reflexivity.
  Defined.

  #[export] Instance ishspace_bg : IsHSpace (B G)
    := Build_IsHSpace _
          bg_mul
          bg_mul_left_id
          bg_mul_right_id.

End HSpace_bg.

(** Functoriality of B(-) *)

Instance is0functor_pclassifyingspace : Is0Functor B.
Is0Functor B
Proof.
Is0Functor B
  apply Build_Is0Functor.
forall a b : Group, (a $-> b) -> B a $-> B b
  intros G H f.
G, H: Group
f: G $-> H
B G $-> B H
  snapply pClassifyingSpace_rec.
G, H: Group
f: G $-> H
IsTrunc 1 (B H)
G, H: Group
f: G $-> H
G -> loops (B H)
G, H: Group
f: G $-> H
forall x y : G,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
  -
G, H: Group
f: G $-> H
IsTrunc 1 (B H) exact _.
  -
G, H: Group
f: G $-> H
G -> loops (B H) exact (bloop o f).
  -
G, H: Group
f: G $-> H
forall x y : G,
(bloop o f) (x * y) = (bloop o f) x @ (bloop o f) y intros x y.
G, H: Group
f: G $-> H
x, y: G
(bloop o f) (x * y) = (bloop o f) x @ (bloop o f) y
    refine (ap bloop (grp_homo_op f x y) @ _).
G, H: Group
f: G $-> H
x, y: G
bloop (f x * f y) = bloop (f x) @ bloop (f y)
    apply bloop_pp.
Defined.

Definition bloop_natural (G H : Group) (f : G $-> H)
  : fmap loops (fmap B f) o bloop == bloop o f.
G, H: Group
f: G $-> H
fmap loops (fmap B f) o bloop == bloop o f
Proof.
G, H: Group
f: G $-> H
fmap loops (fmap B f) o bloop == bloop o f
  napply pClassifyingSpace_rec_beta_bloop.
Defined.

Lemma pbloop_natural (G K : Group) (f : G $-> K)
  : fmap loops (fmap B f) o* pbloop ==* pbloop o* f.
G, K: Group
f: G $-> K
fmap loops (fmap B f) o* pbloop ==* pbloop o* f
Proof.
G, K: Group
f: G $-> K
fmap loops (fmap B f) o* pbloop ==* pbloop o* f
  srapply phomotopy_homotopy_hset.
G, K: Group
f: G $-> K
fmap loops (fmap B f) o* pbloop == pbloop o* f
  apply bloop_natural.
Defined.

Definition natequiv_g_loops_bg `{Univalence}
  : NatEquiv ptype_group (loops o B).
H: Univalence
NatEquiv ptype_group (loops o B)
Proof.
H: Univalence
NatEquiv ptype_group (loops o B)
  snapply Build_NatEquiv.
H: Univalence
forall a : Group,
a $<~> (fun x : Group => loops (B x)) a
H: Univalence
Is1Natural ptype_group (fun x : Group => loops (B x))
  (fun a : Group => ?e a)
  1: intros G; exact pequiv_g_loops_bg.
H: Univalence
Is1Natural ptype_group (fun x : Group => loops (B x))
  (fun a : Group =>
   (fun G : Group => pequiv_g_loops_bg) a)
  snapply Build_Is1Natural.
H: Univalence
forall (a a' : Group) (f : a $-> a'),
(fun a0 : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a0))
  a' $o fmap ptype_group f $==
fmap (loops o B) f $o
(fun a0 : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a0)) a
  intros X Y f.
H: Univalence
X, Y: Group
f: X $-> Y
(fun a : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a)) Y $o
fmap ptype_group f $==
fmap (loops o B) f $o
(fun a : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a)) X
  symmetry.
H: Univalence
X, Y: Group
f: X $-> Y
fmap (loops o B) f $o
(fun a : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a)) X $==
(fun a : Group =>
 cate_fun ((fun G : Group => pequiv_g_loops_bg) a)) Y $o
fmap ptype_group f
  apply pbloop_natural.
Defined.

Instance is1functor_pclassifyingspace : Is1Functor B.
Is1Functor B
Proof.
Is1Functor B
  apply Build_Is1Functor.
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap B f $== fmap B g
forall a : Group, fmap B (Id a) $== Id (B a)
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap B (g $o f) $== fmap B g $o fmap B f
  (** Action on 2-cells *)
  -
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap B f $== fmap B g intros G H f g p.
G, H: Group
f, g: G $-> H
p: f $== g
fmap B f $== fmap B g
    snapply Build_pHomotopy.
G, H: Group
f, g: G $-> H
p: f $== g
fmap B f == fmap B g
G, H: Group
f, g: G $-> H
p: f $== g
?p pt = dpoint_eq (fmap B f) @ (dpoint_eq (fmap B g))^
    {
G, H: Group
f, g: G $-> H
p: f $== g
fmap B f == fmap B g snapply ClassifyingSpace_ind_hset.
G, H: Group
f, g: G $-> H
p: f $== g
forall b : ClassifyingSpace G,
IsHSet
  ((fun b0 : ClassifyingSpace G =>
    fmap B f b0 = fmap B g b0) b)
G, H: Group
f, g: G $-> H
p: f $== g
(fun b : ClassifyingSpace G => fmap B f b = fmap B g b)
  bbase
G, H: Group
f, g: G $-> H
p: f $== g
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B f b = fmap B g b) (bloop x) ?bbase' ?bbase'
      1: exact _.
G, H: Group
f, g: G $-> H
p: f $== g
(fun b : ClassifyingSpace G => fmap B f b = fmap B g b)
  bbase
G, H: Group
f, g: G $-> H
p: f $== g
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B f b = fmap B g b) (bloop x) ?bbase' ?bbase'
      1: reflexivity.
G, H: Group
f, g: G $-> H
p: f $== g
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B f b = fmap B g b) (bloop x) 1 1
      intro x.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
DPath
  (fun b : ClassifyingSpace G =>
   fmap B f b = fmap B g b) (bloop x) 1 1
      rapply equiv_sq_dp^-1.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
PathSquare 1 1 (ap (fmap B f) (bloop x))
  (ap (fmap B g) (bloop x))
      simpl.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
PathSquare 1 1
  (ap
     (ClassifyingSpace_rec (ClassifyingSpace H) pt
        (fun x : G => bloop (f x))
        (fun x y : G =>
         ap bloop (grp_homo_op f x y) @
         bloop_pp (f x) (f y))) (bloop x))
  (ap
     (ClassifyingSpace_rec (ClassifyingSpace H) pt
        (fun x : G => bloop (g x))
        (fun x y : G =>
         ap bloop (grp_homo_op g x y) @
         bloop_pp (g x) (g y))) (bloop x))
      rewrite 2 ClassifyingSpace_rec_beta_bloop.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
PathSquare 1 1 (bloop (f x)) (bloop (g x))
      apply sq_1G.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
bloop (f x) = bloop (g x)
      apply ap.
G, H: Group
f, g: G $-> H
p: f $== g
x: G
f x = g x
      exact (p x). }
G, H: Group
f, g: G $-> H
p: f $== g
ClassifyingSpace_ind_hset
  (fun b : ClassifyingSpace G =>
   fmap B f b = fmap B g b) 1
  (fun x : G =>
   sq_dp^-1
     (internal_paths_rew_r
        (fun
           p : ClassifyingSpace_rec
                 (ClassifyingSpace H) pt
                 (fun x0 : G => bloop (f x0))
                 (fun x0 y : G =>
                  ap bloop (grp_homo_op f x0 y) @
                  bloop_pp (f x0) (f y)) bbase =
               ClassifyingSpace_rec
                 (ClassifyingSpace H) pt
                 (fun x0 : G => bloop (f x0))
                 (fun x0 y : G =>
                  ap bloop (grp_homo_op f x0 y) @
                  bloop_pp (f x0) (f y)) bbase =>
         PathSquare 1 1 p
           (ap
              (ClassifyingSpace_rec
                 (ClassifyingSpace H) pt
                 (fun x0 : G => bloop (g x0))
                 (fun x0 y : G =>
                  ap bloop (grp_homo_op g x0 y) @
                  bloop_pp (g x0) (g y))) (bloop x)))
        (internal_paths_rew_r
           (fun
              p : ClassifyingSpace_rec
                    (ClassifyingSpace H) pt
                    (fun x0 : G => bloop (g x0))
                    (fun x0 y : G =>
                     ap bloop (grp_homo_op g x0 y) @
                     bloop_pp (g x0) (g y)) bbase =
                  ClassifyingSpace_rec
                    (ClassifyingSpace H) pt
                    (fun x0 : G => bloop (g x0))
                    (fun x0 y : G =>
                     ap bloop (grp_homo_op g x0 y) @
                     bloop_pp (g x0) (g y)) bbase =>
            PathSquare 1 1 (bloop (f x)) p)
           (let X := equiv_fun sq_1G in
            X (ap bloop (p x)))
           (ClassifyingSpace_rec_beta_bloop
              (ClassifyingSpace H) pt
              (fun x0 : G => bloop (g x0))
              (fun x0 y : G =>
               ap bloop (grp_homo_op g x0 y) @
               bloop_pp (g x0) (g y)) x))
        (ClassifyingSpace_rec_beta_bloop
           (ClassifyingSpace H) pt
           (fun x0 : G => bloop (f x0))
           (fun x0 y : G =>
            ap bloop (grp_homo_op f x0 y) @
            bloop_pp (f x0) (f y)) x)
      :
      PathSquare 1 1 (ap (fmap B f) (bloop x))
        (ap (fmap B g) (bloop x)))) pt =
dpoint_eq (fmap B f) @ (dpoint_eq (fmap B g))^
    reflexivity.
  (** Preservation of identity *)
  -
forall a : Group, fmap B (Id a) $== Id (B a) intros G.
G: Group
fmap B (Id G) $== Id (B G)
    snapply Build_pHomotopy.
G: Group
fmap B (Id G) == Id (B G)
G: Group
?p pt =
dpoint_eq (fmap B (Id G)) @ (dpoint_eq (Id (B G)))^
    {
G: Group
fmap B (Id G) == Id (B G) snapply ClassifyingSpace_ind_hset.
G: Group
forall b : ClassifyingSpace G,
IsHSet
  ((fun b0 : ClassifyingSpace G =>
    fmap B (Id G) b0 = Id (B G) b0) b)
G: Group
(fun b : ClassifyingSpace G =>
 fmap B (Id G) b = Id (B G) b) bbase
G: Group
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) (bloop x) ?bbase'
  ?bbase'
      1: exact _.
G: Group
(fun b : ClassifyingSpace G =>
 fmap B (Id G) b = Id (B G) b) bbase
G: Group
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) (bloop x) ?bbase'
  ?bbase'
      1: reflexivity.
G: Group
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) (bloop x) 1 1
      intro x.
G: Group
x: G
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) (bloop x) 1 1
      rapply equiv_sq_dp^-1.
G: Group
x: G
PathSquare 1 1 (ap (fmap B (Id G)) (bloop x))
  (ap (Id (B G)) (bloop x))
      simpl.
G: Group
x: G
PathSquare 1 1
  (ap
     (ClassifyingSpace_rec (ClassifyingSpace G) pt
        (fun x : G => bloop x)
        (fun x y : G => 1 @ bloop_pp x y)) (bloop x))
  (ap idmap (bloop x))
      rewrite ClassifyingSpace_rec_beta_bloop.
G: Group
x: G
PathSquare 1 1 (bloop x) (ap idmap (bloop x))
      apply sq_1G.
G: Group
x: G
bloop x = ap idmap (bloop x)
      symmetry.
G: Group
x: G
ap idmap (bloop x) = bloop x
      apply ap_idmap. }
G: Group
ClassifyingSpace_ind_hset
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) 1
  (fun x : G =>
   sq_dp^-1
     (internal_paths_rew_r
        (fun
           p : ClassifyingSpace_rec
                 (ClassifyingSpace G) pt
                 (fun x0 : G => bloop x0)
                 (fun x0 y : G => 1 @ bloop_pp x0 y)
                 bbase =
               ClassifyingSpace_rec
                 (ClassifyingSpace G) pt
                 (fun x0 : G => bloop x0)
                 (fun x0 y : G => 1 @ bloop_pp x0 y)
                 bbase =>
         PathSquare 1 1 p (ap idmap (bloop x)))
        (let X := equiv_fun sq_1G in
         X (ap_idmap (bloop x))^)
        (ClassifyingSpace_rec_beta_bloop
           (ClassifyingSpace G) pt
           (fun x0 : G => bloop x0)
           (fun x0 y : G => 1 @ bloop_pp x0 y) x)
      :
      PathSquare 1 1 (ap (fmap B (Id G)) (bloop x))
        (ap (Id (B G)) (bloop x)))) pt =
dpoint_eq (fmap B (Id G)) @ (dpoint_eq (Id (B G)))^
    reflexivity.
  (** Preservation of composition *)
  -
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap B (g $o f) $== fmap B g $o fmap B f intros G H K g f.
G, H, K: Group
g: G $-> H
f: H $-> K
fmap B (f $o g) $== fmap B f $o fmap B g
    snapply Build_pHomotopy.
G, H, K: Group
g: G $-> H
f: H $-> K
fmap B (f $o g) == fmap B f $o fmap B g
G, H, K: Group
g: G $-> H
f: H $-> K
?p pt =
dpoint_eq (fmap B (f $o g)) @
(dpoint_eq (fmap B f $o fmap B g))^
    {
G, H, K: Group
g: G $-> H
f: H $-> K
fmap B (f $o g) == fmap B f $o fmap B g snapply ClassifyingSpace_ind_hset.
G, H, K: Group
g: G $-> H
f: H $-> K
forall b : ClassifyingSpace G,
IsHSet
  ((fun b0 : ClassifyingSpace G =>
    fmap B (f $o g) b0 = (fmap B f $o fmap B g) b0) b)
G, H, K: Group
g: G $-> H
f: H $-> K
(fun b : ClassifyingSpace G =>
 fmap B (f $o g) b = (fmap B f $o fmap B g) b) bbase
G, H, K: Group
g: G $-> H
f: H $-> K
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (f $o g) b = (fmap B f $o fmap B g) b)
  (bloop x) ?bbase' ?bbase'
      1: exact _.
G, H, K: Group
g: G $-> H
f: H $-> K
(fun b : ClassifyingSpace G =>
 fmap B (f $o g) b = (fmap B f $o fmap B g) b) bbase
G, H, K: Group
g: G $-> H
f: H $-> K
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (f $o g) b = (fmap B f $o fmap B g) b)
  (bloop x) ?bbase' ?bbase'
      1: reflexivity.
G, H, K: Group
g: G $-> H
f: H $-> K
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (f $o g) b = (fmap B f $o fmap B g) b)
  (bloop x) 1 1
      intro x.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (f $o g) b = (fmap B f $o fmap B g) b)
  (bloop x) 1 1
      rapply equiv_sq_dp^-1.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1 (ap (fmap B (f $o g)) (bloop x))
  (ap (fmap B f $o fmap B g) (bloop x))
      simpl.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1
  (ap
     (ClassifyingSpace_rec (ClassifyingSpace K) pt
        (fun x : G => bloop (f (g x)))
        (fun x y : G =>
         ap bloop
           (abstract_algebra.compose_sg_morphism g f
              (issemigrouppreserving_grp_homo g)
              (issemigrouppreserving_grp_homo f) x y) @
         bloop_pp (f (g x)) (f (g y)))) (bloop x))
  (ap
     (fun x : ClassifyingSpace G =>
      ClassifyingSpace_rec (ClassifyingSpace K) pt
        (fun x0 : H => bloop (f x0))
        (fun x0 y : H =>
         ap bloop (grp_homo_op f x0 y) @
         bloop_pp (f x0) (f y))
        (ClassifyingSpace_rec (ClassifyingSpace H) pt
           (fun x0 : G => bloop (g x0))
           (fun x0 y : G =>
            ap bloop (grp_homo_op g x0 y) @
            bloop_pp (g x0) (g y)) x)) (bloop x))
      rapply sq_ccGG.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
?Goal =
ap
  (ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x : G => bloop (f (g x)))
     (fun x y : G =>
      ap bloop
        (abstract_algebra.compose_sg_morphism g f
           (issemigrouppreserving_grp_homo g)
           (issemigrouppreserving_grp_homo f) x y) @
      bloop_pp (f (g x)) (f (g y)))) (bloop x)
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
?Goal0 =
ap
  (fun x : ClassifyingSpace G =>
   ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x0 : H => bloop (f x0))
     (fun x0 y : H =>
      ap bloop (grp_homo_op f x0 y) @
      bloop_pp (f x0) (f y))
     (ClassifyingSpace_rec (ClassifyingSpace H) pt
        (fun x0 : G => bloop (g x0))
        (fun x0 y : G =>
         ap bloop (grp_homo_op g x0 y) @
         bloop_pp (g x0) (g y)) x)) (bloop x)
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1 ?Goal ?Goal0
      1,2: symmetry.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
ap
  (ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x : G => bloop (f (g x)))
     (fun x y : G =>
      ap bloop
        (abstract_algebra.compose_sg_morphism g f
           (issemigrouppreserving_grp_homo g)
           (issemigrouppreserving_grp_homo f) x y) @
      bloop_pp (f (g x)) (f (g y)))) (bloop x) = ?Goal
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
ap
  (fun x : ClassifyingSpace G =>
   ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x0 : H => bloop (f x0))
     (fun x0 y : H =>
      ap bloop (grp_homo_op f x0 y) @
      bloop_pp (f x0) (f y))
     (ClassifyingSpace_rec (ClassifyingSpace H) pt
        (fun x0 : G => bloop (g x0))
        (fun x0 y : G =>
         ap bloop (grp_homo_op g x0 y) @
         bloop_pp (g x0) (g y)) x)) (bloop x) = ?Goal0
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1 ?Goal ?Goal0
      2: refine (ap_compose (ClassifyingSpace_rec _ _ _ (fun x y =>
        ap bloop (grp_homo_op g x y) @ bloop_pp (g x) (g y))) _ (bloop x)
        @ ap _ _ @ _).
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
ap
  (ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x : G => bloop (f (g x)))
     (fun x y : G =>
      ap bloop
        (abstract_algebra.compose_sg_morphism g f
           (issemigrouppreserving_grp_homo g)
           (issemigrouppreserving_grp_homo f) x y) @
      bloop_pp (f (g x)) (f (g y)))) (bloop x) = ?Goal
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
ap
  (ClassifyingSpace_rec (ClassifyingSpace H) bbase
     (fun x : G => bloop (g x))
     (fun x y : G =>
      ap bloop (grp_homo_op g x y) @
      bloop_pp (g x) (g y))) (bloop x) = ?Goal3
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
ap
  (ClassifyingSpace_rec (ClassifyingSpace K) pt
     (fun x : H => bloop (f x))
     (fun x y : H =>
      ap bloop (grp_homo_op f x y) @
      bloop_pp (f x) (f y))) ?Goal3 = ?Goal0
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1 ?Goal ?Goal0
      1-3: napply ClassifyingSpace_rec_beta_bloop.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
PathSquare 1 1 (bloop (f (g x))) (bloop (f (g x)))
      apply sq_1G.
G, H, K: Group
g: G $-> H
f: H $-> K
x: G
bloop (f (g x)) = bloop (f (g x))
      reflexivity. }
G, H, K: Group
g: G $-> H
f: H $-> K
ClassifyingSpace_ind_hset
  (fun b : ClassifyingSpace G =>
   fmap B (f $o g) b = (fmap B f $o fmap B g) b) 1
  (fun x : G =>
   sq_dp^-1
     (sq_ccGG
        (ClassifyingSpace_rec_beta_bloop
           (ClassifyingSpace K) bbase
           (fun x0 : G => bloop (f (g x0)))
           (fun x0 y : G =>
            ap bloop
              (abstract_algebra.compose_sg_morphism g
                 f (issemigrouppreserving_grp_homo g)
                 (issemigrouppreserving_grp_homo f) x0
                 y) @ bloop_pp (f (g x0)) (f (g y))) x)^
        ((ap_compose
            (ClassifyingSpace_rec (ClassifyingSpace H)
               bbase (fun x0 : G => bloop (g x0))
               (fun x0 y : G =>
                ap bloop (grp_homo_op g x0 y) @
                bloop_pp (g x0) (g y)))
            (ClassifyingSpace_rec (ClassifyingSpace K)
               pt (fun x0 : H => bloop (f x0))
               (fun x0 y : H =>
                ap bloop (grp_homo_op f x0 y) @
                bloop_pp (f x0) (f y))) (bloop x) @
          ap
            (ap
               (ClassifyingSpace_rec
                  (ClassifyingSpace K) pt
                  (fun x0 : H => bloop (f x0))
                  (fun x0 y : H =>
                   ap bloop (grp_homo_op f x0 y) @
                   bloop_pp (f x0) (f y))))
            (ClassifyingSpace_rec_beta_bloop
               (ClassifyingSpace H) bbase
               (fun x0 : G => bloop (g x0))
               (fun x0 y : G =>
                ap bloop (grp_homo_op g x0 y) @
                bloop_pp (g x0) (g y)) x)) @
         ClassifyingSpace_rec_beta_bloop
           (ClassifyingSpace K) pt
           (fun x0 : H => bloop (f x0))
           (fun x0 y : H =>
            ap bloop (grp_homo_op f x0 y) @
            bloop_pp (f x0) (f y)) (g x))^
        (let X := equiv_fun sq_1G in X 1)
      :
      PathSquare 1 1 (ap (fmap B (f $o g)) (bloop x))
        (ap (fmap B f $o fmap B g) (bloop x)))) pt =
dpoint_eq (fmap B (f $o g)) @
(dpoint_eq (fmap B f $o fmap B g))^
    reflexivity.
Defined.

(** Interestingly, [fmap B] is an equivalence *)
Instance isequiv_fmap_pclassifyingspace `{U : Univalence} (G H : Group)
  : IsEquiv (fmap B (a := G) (b := H)).
U: Univalence
G, H: Group
IsEquiv (fmap B)
Proof.
U: Univalence
G, H: Group
IsEquiv (fmap B)
  snapply isequiv_adjointify.
U: Univalence
G, H: Group
(B G $-> B H) -> G $-> H
U: Univalence
G, H: Group
fmap B o ?g == idmap
U: Univalence
G, H: Group
?g o fmap B == idmap
  {
U: Univalence
G, H: Group
(B G $-> B H) -> G $-> H intros f.
U: Univalence
G, H: Group
f: B G $-> B H
G $-> H
    refine (grp_homo_compose (grp_iso_inverse _) (grp_homo_compose _ _)).
U: Univalence
G, H: Group
f: B G $-> B H
GroupIsomorphism H ?Goal
U: Univalence
G, H: Group
f: B G $-> B H
GroupHomomorphism ?Goal1 ?Goal
U: Univalence
G, H: Group
f: B G $-> B H
GroupHomomorphism G ?Goal1
    1,3: exact grp_iso_g_loopgroup_bg.
U: Univalence
G, H: Group
f: B G $-> B H
GroupHomomorphism (LoopGroup (B G)) (LoopGroup (B H))
    exact (grp_homo_loops f). }
U: Univalence
G, H: Group
fmap B
o (fun f : B G $-> B H =>
   grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) == idmap
U: Univalence
G, H: Group
(fun f : B G $-> B H =>
 grp_homo_compose
   (grp_iso_inverse grp_iso_g_loopgroup_bg)
   (grp_homo_compose (grp_homo_loops f)
      grp_iso_g_loopgroup_bg)) o fmap B == idmap
  {
U: Univalence
G, H: Group
fmap B
o (fun f : B G $-> B H =>
   grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) == idmap intros f.
U: Univalence
G, H: Group
f: B G $-> B H
fmap B
  (grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) = f
    rapply equiv_path_pforall.
U: Univalence
G, H: Group
f: B G $-> B H
fmap B
  (grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) ==* f
    snapply Build_pHomotopy.
U: Univalence
G, H: Group
f: B G $-> B H
fmap B
  (grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) == f
U: Univalence
G, H: Group
f: B G $-> B H
?p pt =
dpoint_eq
  (fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg))) @ (dpoint_eq f)^
    {
U: Univalence
G, H: Group
f: B G $-> B H
fmap B
  (grp_homo_compose
     (grp_iso_inverse grp_iso_g_loopgroup_bg)
     (grp_homo_compose (grp_homo_loops f)
        grp_iso_g_loopgroup_bg)) == f snapply ClassifyingSpace_ind_hset.
U: Univalence
G, H: Group
f: B G $-> B H
forall b : ClassifyingSpace G,
IsHSet
  ((fun b0 : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b0 = f b0) b)
U: Univalence
G, H: Group
f: B G $-> B H
(fun b : ClassifyingSpace G =>
 fmap B
   (grp_homo_compose
      (grp_iso_inverse grp_iso_g_loopgroup_bg)
      (grp_homo_compose (grp_homo_loops f)
         grp_iso_g_loopgroup_bg)) b = f b) bbase
U: Univalence
G, H: Group
f: B G $-> B H
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b) (bloop x)
  ?bbase' ?bbase'
      1: exact _.
U: Univalence
G, H: Group
f: B G $-> B H
(fun b : ClassifyingSpace G =>
 fmap B
   (grp_homo_compose
      (grp_iso_inverse grp_iso_g_loopgroup_bg)
      (grp_homo_compose (grp_homo_loops f)
         grp_iso_g_loopgroup_bg)) b = f b) bbase
U: Univalence
G, H: Group
f: B G $-> B H
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b) (bloop x)
  ?bbase' ?bbase'
      {
U: Univalence
G, H: Group
f: B G $-> B H
(fun b : ClassifyingSpace G =>
 fmap B
   (grp_homo_compose
      (grp_iso_inverse grp_iso_g_loopgroup_bg)
      (grp_homo_compose (grp_homo_loops f)
         grp_iso_g_loopgroup_bg)) b = f b) bbase cbn; symmetry.
U: Univalence
G, H: Group
f: B G $-> B H
f bbase = bbase
        rapply (point_eq f). }
U: Univalence
G, H: Group
f: B G $-> B H
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b) (bloop x)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
      {
U: Univalence
G, H: Group
f: B G $-> B H
forall x : G,
DPath
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b) (bloop x)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase) intro g.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
DPath
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b) (bloop g)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
        rapply equiv_sq_dp^-1.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
PathSquare (point_eq f)^ (point_eq f)^
  (ap
     (fmap B
        (grp_homo_compose
           (grp_iso_inverse grp_iso_g_loopgroup_bg)
           (grp_homo_compose (grp_homo_loops f)
              grp_iso_g_loopgroup_bg))) (bloop g))
  (ap f (bloop g))
        rewrite ClassifyingSpace_rec_beta_bloop.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
PathSquare (point_eq f)^ (point_eq f)^
  (bloop
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg) g))
  (ap f (bloop g))
        simpl.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
PathSquare (point_eq f)^ (point_eq f)^
  (bloop
     (encode bbase
        ((point_eq f)^ @ (ap f (bloop g) @ point_eq f))))
  (ap f (bloop g))
        rapply sq_ccGc.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
?Goal =
bloop
  (encode bbase
     ((point_eq f)^ @ (ap f (bloop g) @ point_eq f)))
U: Univalence
G, H: Group
f: B G $-> B H
g: G
PathSquare (point_eq f)^ (point_eq f)^ ?Goal
  (ap f (bloop g))
        1: symmetry; rapply decode_encode.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
PathSquare (point_eq f)^ (point_eq f)^
  ((point_eq f)^ @ (ap f (bloop g) @ point_eq f))
  (ap f (bloop g))
        apply equiv_sq_path.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
(point_eq f)^ @ ap f (bloop g) =
((point_eq f)^ @ (ap f (bloop g) @ point_eq f)) @
(point_eq f)^
        rewrite concat_pp_p.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
(point_eq f)^ @ ap f (bloop g) =
(point_eq f)^ @
((ap f (bloop g) @ point_eq f) @ (point_eq f)^)
        rewrite concat_pp_V.
U: Univalence
G, H: Group
f: B G $-> B H
g: G
(point_eq f)^ @ ap f (bloop g) =
(point_eq f)^ @ ap f (bloop g)
        reflexivity. } }
U: Univalence
G, H: Group
f: B G $-> B H
ClassifyingSpace_ind_hset
  (fun b : ClassifyingSpace G =>
   fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg)) b = f b)
  ((point_eq f)^
   :
   (fun b : ClassifyingSpace G =>
    fmap B
      (grp_homo_compose
         (grp_iso_inverse grp_iso_g_loopgroup_bg)
         (grp_homo_compose (grp_homo_loops f)
            grp_iso_g_loopgroup_bg)) b = f b) bbase)
  (fun g : G =>
   sq_dp^-1
     (internal_paths_rew_r
        (fun
           p : ClassifyingSpace_rec (B H) pt
                 (fun x : G =>
                  bloop
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) x))
                 (fun x y : G =>
                  ap bloop
                    (grp_homo_op
                       (grp_homo_compose
                          (grp_iso_inverse
                             grp_iso_g_loopgroup_bg)
                          (grp_homo_compose
                             (grp_homo_loops f)
                             grp_iso_g_loopgroup_bg))
                       x y) @
                  bloop_pp
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) x)
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) y))
                 bbase =
               ClassifyingSpace_rec (B H) pt
                 (fun x : G =>
                  bloop
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) x))
                 (fun x y : G =>
                  ap bloop
                    (grp_homo_op
                       (grp_homo_compose
                          (grp_iso_inverse
                             grp_iso_g_loopgroup_bg)
                          (grp_homo_compose
                             (grp_homo_loops f)
                             grp_iso_g_loopgroup_bg))
                       x y) @
                  bloop_pp
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) x)
                    (grp_homo_compose
                       (grp_iso_inverse
                          grp_iso_g_loopgroup_bg)
                       (grp_homo_compose
                          (grp_homo_loops f)
                          grp_iso_g_loopgroup_bg) y))
                 bbase =>
         PathSquare (point_eq f)^ (point_eq f)^ p
           (ap f (bloop g)))
        (sq_ccGc
           (decode_encode pt
              ((point_eq f)^ @
               (ap f (bloop g) @ point_eq f)))^
           (let X := equiv_fun sq_path in
            X
              (internal_paths_rew_r
                 (fun p : pt = f bbase =>
                  (point_eq f)^ @ ap f (bloop g) = p)
                 (internal_paths_rew_r
                    (fun p : f pt = f bbase =>
                     (point_eq f)^ @ ap f (bloop g) =
                     (point_eq f)^ @ p) 1
                    (concat_pp_V (ap f (bloop g))
                       (point_eq f)))
                 (concat_pp_p (point_eq f)^
                    (ap f (bloop g) @ point_eq f)
                    (point_eq f)^)))
         :
         PathSquare (point_eq f)^ (point_eq f)^
           (bloop
              (grp_homo_compose
                 (grp_iso_inverse
                    grp_iso_g_loopgroup_bg)
                 (grp_homo_compose (grp_homo_loops f)
                    grp_iso_g_loopgroup_bg) g))
           (ap f (bloop g)))
        (ClassifyingSpace_rec_beta_bloop (B H) pt
           (fun x : G =>
            bloop
              (grp_homo_compose
                 (grp_iso_inverse
                    grp_iso_g_loopgroup_bg)
                 (grp_homo_compose (grp_homo_loops f)
                    grp_iso_g_loopgroup_bg) x))
           (fun x y : G =>
            ap bloop
              (grp_homo_op
                 (grp_homo_compose
                    (grp_iso_inverse
                       grp_iso_g_loopgroup_bg)
                    (grp_homo_compose
                       (grp_homo_loops f)
                       grp_iso_g_loopgroup_bg)) x y) @
            bloop_pp
              (grp_homo_compose
                 (grp_iso_inverse
                    grp_iso_g_loopgroup_bg)
                 (grp_homo_compose (grp_homo_loops f)
                    grp_iso_g_loopgroup_bg) x)
              (grp_homo_compose
                 (grp_iso_inverse
                    grp_iso_g_loopgroup_bg)
                 (grp_homo_compose (grp_homo_loops f)
                    grp_iso_g_loopgroup_bg) y)) g)))
  pt =
dpoint_eq
  (fmap B
     (grp_homo_compose
        (grp_iso_inverse grp_iso_g_loopgroup_bg)
        (grp_homo_compose (grp_homo_loops f)
           grp_iso_g_loopgroup_bg))) @ (dpoint_eq f)^
      symmetry; apply concat_1p. }
U: Univalence
G, H: Group
(fun f : B G $-> B H =>
 grp_homo_compose
   (grp_iso_inverse grp_iso_g_loopgroup_bg)
   (grp_homo_compose (grp_homo_loops f)
      grp_iso_g_loopgroup_bg)) o fmap B == idmap
  intros f.
U: Univalence
G, H: Group
f: G $-> H
grp_homo_compose
  (grp_iso_inverse grp_iso_g_loopgroup_bg)
  (grp_homo_compose (grp_homo_loops (fmap B f))
     grp_iso_g_loopgroup_bg) = f
  rapply equiv_path_grouphomomorphism.
U: Univalence
G, H: Group
f: G $-> H
grp_homo_compose
  (grp_iso_inverse grp_iso_g_loopgroup_bg)
  (grp_homo_compose (grp_homo_loops (fmap B f))
     grp_iso_g_loopgroup_bg) == f
  intro x.
U: Univalence
G, H: Group
f: G $-> H
x: G
grp_homo_compose
  (grp_iso_inverse grp_iso_g_loopgroup_bg)
  (grp_homo_compose (grp_homo_loops (fmap B f))
     grp_iso_g_loopgroup_bg) x = f x
  rapply (moveR_equiv_V' equiv_g_loops_bg).
U: Univalence
G, H: Group
f: G $-> H
x: G
grp_homo_compose (grp_homo_loops (fmap B f))
  grp_iso_g_loopgroup_bg x = equiv_g_loops_bg (f x)
  napply pClassifyingSpace_rec_beta_bloop.
Defined.

(** Hence we have that group homomorphisms are equivalent to pointed maps between their deloopings. *)
Theorem equiv_grp_homo_pmap_bg `{U : Univalence} (G H : Group)
  : (G $-> H) <~> (B G $-> B H).
U: Univalence
G, H: Group
(G $-> H) <~> (B G $-> B H)
Proof.
U: Univalence
G, H: Group
(G $-> H) <~> (B G $-> B H)
  snapply Build_Equiv.
U: Univalence
G, H: Group
(G $-> H) -> B G $-> B H
U: Univalence
G, H: Group
IsEquiv ?equiv_fun
  2: apply isequiv_fmap_pclassifyingspace.
Defined.

Instance is1natural_grp_homo_pmap_bg_r {U : Univalence} (G : Group)
  : Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G).
U: Univalence
G: Group
Is1Natural (opyon G) (opyon (B G) o B)
  (fun H : Group => equiv_grp_homo_pmap_bg G H)
Proof.
U: Univalence
G: Group
Is1Natural (opyon G) (opyon (B G) o B)
  (fun H : Group => equiv_grp_homo_pmap_bg G H)
  snapply Build_Is1Natural.
U: Univalence
G: Group
forall (a a' : Group) (f : a $-> a'),
(fun H : Group =>
 equiv_fun (equiv_grp_homo_pmap_bg G H)) a' $o
fmap (opyon G) f $==
fmap (opyon (B G) o B) f $o
(fun H : Group =>
 equiv_fun (equiv_grp_homo_pmap_bg G H)) a
  intros K H f h.
U: Univalence
G, K, H: Group
f: K $-> H
h: opyon G K
(equiv_grp_homo_pmap_bg G H $o fmap (opyon G) f) h =
(fmap (opyon (B G) o B) f $o
 equiv_grp_homo_pmap_bg G K) h
  apply path_hom.
U: Univalence
G, K, H: Group
f: K $-> H
h: opyon G K
(equiv_grp_homo_pmap_bg G H $o fmap (opyon G) f) h $==
(fmap (opyon (B G) o B) f $o
 equiv_grp_homo_pmap_bg G K) h
  rapply (fmap_comp B h f).
Defined.

Theorem natequiv_grp_homo_pmap_bg `{U : Univalence} (G : Group)
  : NatEquiv (opyon G) (opyon (B G) o B).
U: Univalence
G: Group
NatEquiv (opyon G) (opyon (B G) o B)
Proof.
U: Univalence
G: Group
NatEquiv (opyon G) (opyon (B G) o B)
  rapply Build_NatEquiv.
Defined.

(** [B(Pi 1 X) <~>* X] for a 0-connected 1-truncated [X]. *)
Theorem pequiv_pclassifyingspace_pi1 `{Univalence}
  (X : pType) `{IsConnected 0 X} `{IsTrunc 1 X}
  : B (Pi1 X) <~>* X.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
B (Pi1 X) <~>* X
Proof.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
B (Pi1 X) <~>* X
  (** The pointed map [f] is the adjunct to the inverse of the natural map [loops X -> Pi1 X]. We define it first, to make the later goals easier to read. *)
  transparent assert (f : (B (Pi1 X) ->* X)).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
B (Pi1 X) ->* X
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= ?Goal: B (Pi1 X) ->* X
B (Pi1 X) <~>* X
  {
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
B (Pi1 X) ->* X snapply pClassifyingSpace_rec.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
IsTrunc 1 X
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
Pi1 X -> loops X
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
forall x y : Pi1 X,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    1: exact _.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
Pi1 X -> loops X
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
forall x y : Pi1 X,
?bloop' (x * y) = ?bloop' x @ ?bloop' y
    1: exact (equiv_tr 0 _)^-1%equiv.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
forall x y : Pi1 X,
(equiv_tr 0 (loops X))^-1%equiv (x * y) =
(equiv_tr 0 (loops X))^-1%equiv x @
(equiv_tr 0 (loops X))^-1%equiv y
    intros x y.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
x, y: Pi1 X
(equiv_tr 0 (loops X))^-1%equiv (x * y) =
(equiv_tr 0 (loops X))^-1%equiv x @
(equiv_tr 0 (loops X))^-1%equiv y
    strip_truncations.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
y, x: loops X
(equiv_tr 0 (loops X))^-1%equiv (tr x * tr y) =
(equiv_tr 0 (loops X))^-1%equiv (tr x) @
(equiv_tr 0 (loops X))^-1%equiv (tr y)
    reflexivity. }
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
B (Pi1 X) <~>* X
  snapply (Build_pEquiv f).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
IsEquiv f
  (** [f] is an equivalence since [loops_functor f o bloop == tr^-1], and the other two maps are equivalences. *)
  apply isequiv_is0connected_isequiv_loops.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
IsEquiv (fmap loops f)
  snapply (cancelR_isequiv bloop).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
IsEquiv bloop
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
IsEquiv (fmap loops f o bloop)
  1: exact _.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
IsEquiv (fmap loops f o bloop)
  rapply isequiv_homotopic'; symmetry.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
IsTrunc0: IsTrunc 1 X
f:= pClassifyingSpace_rec X
  (equiv_tr 0 (loops X))^-1%equiv
  (fun x y : Pi1 X =>
   Trunc_ind
     (fun aa : Trunc 0 (loops X) =>
      (equiv_tr 0 (loops X))^-1%equiv (x * aa) =
      (equiv_tr 0 (loops X))^-1%equiv x @
      (equiv_tr 0 (loops X))^-1%equiv aa)
     (fun y0 : loops X =>
      Trunc_ind
        (fun aa : Trunc 0 (loops X) =>
         (equiv_tr 0 (loops X))^-1%equiv
           (aa * tr y0) =
         (equiv_tr 0 (loops X))^-1%equiv aa @
         (equiv_tr 0 (loops X))^-1%equiv (tr y0))
        (fun x0 : loops X => 1) x) y): B (Pi1 X) ->* X
(fun x : Pi1 X => fmap loops f (bloop x)) == ?Goal
  napply pClassifyingSpace_rec_beta_bloop.
Defined.

Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}
  : NatEquiv (opyon (Pi1 X)) (opyon X o B).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (Pi1 X)) (opyon X o B)
Proof.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (Pi1 X)) (opyon X o B)
  nrefine (natequiv_compose (G := opyon (Pi1 (pTr 1 X))) _ _).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (Pi1 (pTr 1 X)))
  (fun x : Group => opyon X (B x))
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (Pi1 X)) (opyon (Pi1 (pTr 1 X)))
  2: exact (natequiv_opyon_equiv (A:=Group) (grp_iso_inverse (grp_iso_pi_Tr 0 X))).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (Pi1 (pTr 1 X)))
  (fun x : Group => opyon X (B x))
  refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv
  (fun x : Group => opyon (B (Pi1 (pTr 1 X))) (B x))
  (fun x : Group => opyon X (B x))
  refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _); revgoals.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv
  (fun x : Group => opyon (B (Pi1 (pTr 1 X))) (B x))
  (fun x : Group => opyon (pTr 1 X) (B x))
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (fun x : Group => opyon (pTr 1 X) (B x))
  (fun x : Group => opyon X (B x))
  {
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv
  (fun x : Group => opyon (B (Pi1 (pTr 1 X))) (B x))
  (fun x : Group => opyon (pTr 1 X) (B x)) refine (natequiv_prewhisker _ _).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (opyon (B (Pi1 (pTr 1 X)))) (opyon (pTr 1 X))
    refine (natequiv_opyon_equiv _^-1$).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
B (Pi1 (pTr 1 X)) $<~> pTr 1 X
    rapply pequiv_pclassifyingspace_pi1. }
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
NatEquiv (fun x : Group => opyon (pTr 1 X) (B x))
  (fun x : Group => opyon X (B x))
  snapply Build_NatEquiv.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
forall a : Group,
(fun x : Group => opyon (pTr 1 X) (B x)) a $<~>
(fun x : Group => opyon X (B x)) a
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
Is1Natural (fun x : Group => opyon (pTr 1 X) (B x))
  (fun x : Group => opyon X (B x))
  (fun a : Group => ?e a)
  1: intro; exact pequiv_ptr_rec.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
Is1Natural (fun x : Group => opyon (pTr 1 X) (B x))
  (fun x : Group => opyon X (B x))
  (fun a : Group =>
   (fun a0 : Group =>
    pointed_equiv_equiv pequiv_ptr_rec) a)
  exact (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)).
Defined.

(** The classifying space functor and the fundamental group functor form an adjunction ([pType] needs to be restricted to the subcategory of 0-connected pointed types). Note that the full adjunction should also be natural in [X], but this was not needed yet. *)
Theorem equiv_bg_pi1_adjoint `{Univalence} (X : pType)
  `{IsConnected 0 X} (G : Group)
  : (Pi 1 X $-> G) <~> (X $-> B G).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
G: Group
(Pi 1 X $-> G) <~> (X $-> B G)
Proof.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
G: Group
(Pi 1 X $-> G) <~> (X $-> B G)
  rapply natequiv_bg_pi1_adjoint.
Defined.

Lemma is1natural_equiv_bg_pi1_adjoint_r `{Univalence}
  (X : pType) `{IsConnected 0 X}
  : Is1Natural (opyon (Pi1 X)) (opyon X o B)
      (equiv_bg_pi1_adjoint X).
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
Is1Natural (opyon (Pi1 X)) (opyon X o B)
  (fun G : Group => equiv_bg_pi1_adjoint X G)
Proof.
H: Univalence
X: pType
H0: IsConnected (Tr 0) X
Is1Natural (opyon (Pi1 X)) (opyon X o B)
  (fun G : Group => equiv_bg_pi1_adjoint X G)
  rapply (is1natural_natequiv (natequiv_bg_pi1_adjoint X)).
  (** Why so slow? Fixed by making this opaque. *)
  Opaque equiv_bg_pi1_adjoint.
Defined.
Transparent equiv_bg_pi1_adjoint.