Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed Cubical WildCat.
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_scope.
Local Open Scope trunc_scope.
Local Open Scope mc_mult_scope.

(** * 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.

    Global Instance istrunc_ClassifyingSpace
      : IsTrunc 1 (ClassifyingSpace G).
G: Group
IsTrunc 1 (ClassifyingSpace G)
    Proof.
G: Group
IsTrunc 1 (ClassifyingSpace G) Admitted.

  End ClassifyingSpace.

  (** 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
    rewrite <- 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
    unfold ClassifyingSpace_rec.
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_ind
        (fun _ : ClassifyingSpace G => P) bbase'
        (fun x : G => dp_const (bloop' x))
        (fun x y : G =>
         ds_const'
           (sq_GGcc
              (eissect dp_const (bloop' (x * y)))^
              ((eissect dp_const (bloop' x @ bloop' y))^ @
               ap dp_const^-1
                 (dp_const_pp (bloop' x) (bloop' y)))
              (sq_G1 (bloop_pp' x y))))) (bloop x)) =
bloop' x
    rewrite ClassifyingSpace_ind_beta_bloop.
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 (dp_const (bloop' x)) = bloop' x
    apply eissect.
  Qed.

  (** 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.
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. *)
Global 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. *)
Global 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%path
Proof.
G: Group
bloop (mon_unit : G) = 1%path
  symmetry.
G: Group
1%path = bloop (mon_unit : G)
  apply (cancelL (bloop mon_unit)).
G: Group
bloop mon_unit @ 1 = bloop mon_unit @ bloop mon_unit
  refine (_ @ bloop_pp _ _).
G: Group
bloop mon_unit @ 1 = bloop (mon_unit * mon_unit)
  refine (_ @ ap _ (left_identity _)^).
G: Group
bloop mon_unit @ 1 = bloop mon_unit
  apply concat_p1.
Defined.

(** [bloop] "preserves inverses" by taking inverses in [G] to inverses of paths in [BG]. *)
Definition bloop_inv {G : Group} : forall x : G, bloop (-x) = (bloop x)^.
G: Group
forall x : G, bloop (- x) = (bloop x)^
Proof.
G: Group
forall x : G, bloop (- x) = (bloop x)^
  intro x.
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%path
  refine (_ @ bloop_id).
G: Group
x: G
bloop x @ bloop (- x) = bloop mon_unit
  refine ((bloop_pp _ _)^ @ _).
G: Group
x: G
bloop (x * - x) = bloop mon_unit
  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
?Goal pt = pt
  1: exact bloop.
G: Group
bloop pt = pt
  apply 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 (B G) P (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 srapply (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
    rewrite transport_idmap_ap.
H: Univalence
G: Group
x, y: G
transport idmap
  (ap (fun x : B G => codes x) (bloop x)) y = y * x
    rewrite ap_compose.
H: Univalence
G: Group
x, y: G
transport idmap
  (ap trunctype_type (ap codes (bloop x))) y = y * x
    rewrite ClassifyingSpace_rec_beta_bloop.
H: Univalence
G: Group
x, y: G
transport idmap
  (ap trunctype_type
     (path_trunctype
        {|
          equiv_fun := fun t : G => t * x;
          equiv_isequiv := isequiv_group_right_op G x
        |})) y = y * x
    rewrite ap_trunctype.
H: Univalence
G: Group
x, y: G
transport idmap
  (path_universe_uncurried
     {|
       equiv_fun := fun t : G => t * x;
       equiv_isequiv := isequiv_group_right_op G x
     |}) y = y * x
    by rewrite transport_path_universe_uncurried.
  Qed.

  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%path
    apply bloop_id.
  Defined.

  Global 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))
    snrapply 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))
    snrapply (transitive_groupisomorphism _ _ _ grp_iso_g_loopgroup_bg).
H: Univalence
G: Group
GroupIsomorphism (LoopGroup (B G)) (Pi1 (B G))
    snrapply 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]
    snrapply 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
?Goal 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]
      snrapply 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 ?f
      +
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) nrapply fmap_loops_pp.
    -
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
(fun f : X ->** Y =>
 Build_GroupHomomorphism (fmap loops f)) pt = pt cbn beta.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
Build_GroupHomomorphism (fmap loops pt) = pt
      apply equiv_path_grouphomomorphism.
H: Univalence
G: Group
X, Y: pType
IsTrunc0: IsTrunc 1 X
IsTrunc1: IsTrunc 1 Y
Build_GroupHomomorphism (fmap loops 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
    snrapply 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
      snrapply 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%path 1%path
      intros x.
G: AbGroup
x: G
DPath
  (fun b : ClassifyingSpace G => b = bg_mul bbase b)
  (bloop x) 1%path 1%path
      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
      nrapply 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%path
     (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%path
     (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%path
     (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%path
     (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%path
     (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%path =>
             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%path =>
                 fun (px2 : bbase = bbase)
                   (e : 1%path = 1 @ px2) =>
                 match
                   e @ concat_1p px2 in (_ = p)
                   return
                     (1%path = 1 @ p ->
                      PathSquare 1 p 1 1)
                 with
                 | 1%path =>
                     fun _ : 1%path = 1%path =>
                     1%square
                 end e
             end px1
         end 1%path
           ((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%path
  (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%path =>
          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%path =>
              fun (px2 : bbase = bbase)
                (e : 1%path = 1 @ px2) =>
              match
                e @ concat_1p px2 in (_ = p)
                return
                  (1%path = 1 @ p ->
                   PathSquare 1 p 1 1)
              with
              | 1%path =>
                  fun _ : 1%path = 1%path => 1%square
              end e
          end px1
      end 1%path
        ((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
    snrapply 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%path
         (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%path =>
                 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%path =>
                     fun (px2 : bbase = bbase)
                       (e : 1%path = 1 @ px2) =>
                     match ... in ... return ... with
                     | 1%path => fun ... => 1%square
                     end e
                 end px1
             end 1%path
               ((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%path
      (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%path =>
              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%path =>
                  fun (px2 : bbase = bbase)
                    (e : 1%path = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return (... -> ...)
                  with
                  | 1%path =>
                      fun _ : 1%path = 1%path =>
                      1%square
                  end e
              end px1
          end 1%path
            ((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%path
      (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%path =>
              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%path =>
                  fun (px2 : bbase = bbase)
                    (e : 1%path = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return
                      (1%path = ... ->
                       PathSquare 1 p 1 1)
                  with
                  | 1%path =>
                      fun _ : 1%path = 1%path =>
                      1%square
                  end e
              end px1
          end 1%path
            ((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%path
   (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%path =>
           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%path =>
               fun (px2 : bbase = bbase)
                 (e : 1%path = 1 @ px2) =>
               match
                 e @ concat_1p px2 in (_ = p)
                 return
                   (1%path = 1 @ p ->
                    PathSquare 1 p 1 1)
               with
               | 1%path =>
                   fun _ : 1%path = 1%path => 1%square
               end e
           end px1
       end 1%path
         ((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%path
      (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%path =>
              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%path =>
                  fun (px2 : bbase = bbase)
                    (e : 1%path = 1 @ px2) =>
                  match
                    e @ concat_1p px2 in (_ = p)
                    return
                      (1%path = ... ->
                       PathSquare 1 p 1 1)
                  with
                  | 1%path =>
                      fun _ : 1%path = 1%path =>
                      1%square
                  end e
              end px1
          end 1%path
            ((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%path
   (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%path =>
           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%path =>
               fun (px2 : bbase = bbase)
                 (e : 1%path = 1 @ px2) =>
               match
                 e @ concat_1p px2 in (_ = p)
                 return
                   (1%path = 1 @ p ->
                    PathSquare 1 p 1 1)
               with
               | 1%path =>
                   fun _ : 1%path = 1%path => 1%square
               end e
           end px1
       end 1%path
         ((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%path = 1%path
    nrapply (transport_paths_FFlr' (g := idmap)).
G: AbGroup
y: G
ap idmap (ap (bg_mul bbase) (bloop y)) @ 1 =
1 @ bloop y
    apply equiv_p1_1q.
G: AbGroup
y: G
ap idmap (ap (bg_mul bbase) (bloop y)) = bloop y
    lhs nrapply ap_idmap.
G: AbGroup
y: G
ap (bg_mul bbase) (bloop y) = bloop y
    nrapply 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.

  Global Instance ishspace_bg : IsHSpace (B G)
    := Build_IsHSpace _
          bg_mul
          bg_mul_left_id
          bg_mul_right_id.

End HSpace_bg.

(** Functoriality of B(-) *)

Global 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
  snrapply 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
  nrapply 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)
  snrapply 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; rapply 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)
  intros X Y f.
H: Univalence
X, Y: Group
f: X $-> Y
pequiv_g_loops_bg $o fmap ptype_group f $==
fmap (loops o B) f $o pequiv_g_loops_bg
  symmetry.
H: Univalence
X, Y: Group
f: X $-> Y
fmap (loops o B) f $o pequiv_g_loops_bg $==
pequiv_g_loops_bg $o fmap ptype_group f
  apply pbloop_natural.
Defined.

Global 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
    snrapply 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 snrapply 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%path 1%path
      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%path 1%path
      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%path
  (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)
    snrapply 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) snrapply 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%path
  1%path
      intro x.
G: Group
x: G
DPath
  (fun b : ClassifyingSpace G =>
   fmap B (Id G) b = Id (B G) b) (bloop x) 1%path
  1%path
      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%path
  (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
    snrapply 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 snrapply 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%path 1%path
      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%path 1%path
      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
           (grp_homo_op (grp_homo_compose f g) 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
        (grp_homo_op (grp_homo_compose f g) 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
        (grp_homo_op (grp_homo_compose f g) 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
        (grp_homo_op (grp_homo_compose f g) 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: nrapply 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%path
  (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
              (grp_homo_op (grp_homo_compose f g) 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%path)
      :
      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 *)
Global 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)
  snrapply 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: rapply 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
    snrapply 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 snrapply 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%path
                    (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)
  nrapply 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)
  snrapply 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.

Global 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)
  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 snrapply 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%path) x) y): B (Pi1 X) ->* X
B (Pi1 X) <~>* X
  snrapply (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%path) 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%path) x) y): B (Pi1 X) ->* X
IsEquiv (fmap loops f)
  snrapply (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%path) 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%path) 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%path) 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%path) x) y): B (Pi1 X) ->* X
(fun x : Pi1 X => fmap loops f (bloop x)) == ?Goal
  nrapply 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))
  snrapply 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)
  rapply is1natural_prewhisker.
Defined.

(** The classifying space functor and the fundamental group functor form an adjunction (pType needs to be restricted to the subcategory of 0-connected pTypes). 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.