Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed WildCat.
Require Import Algebra.Groups.
Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
Require Import Homotopy.Suspension.
Require Import Homotopy.ClassifyingSpace.
Require Import Homotopy.HomotopyGroup.

Local Open Scope trunc_scope.
Local Open Scope pointed_scope.
Import ClassifyingSpaceNotation.

(** In this file we show that the fundamental group of a bouquet of circles indexed by a type S is the free group on that type S. We begin by defining S-indexed wedges of circles as the suspension of the pointification of S. *)

Section AssumeUnivalence.

  Context `{Univalence}.

  (** An S-indexed wedge of circles a.k.a a bouquet can be defined as the suspension of the pointification of S. *)
  Definition Bouquet (S : Type) : pType := psusp (pointify S).

  #[export] Instance isconnected_bouquet (S : Type)
    : IsConnected 0 (Bouquet S).
H: Univalence
S: Type
IsConnected (Tr 0) (Bouquet S)
  Proof.
H: Univalence
S: Type
IsConnected (Tr 0) (Bouquet S)
    exact isconnected_susp.
  Defined.

  (** We can directly prove that it satisfies the desired equivalence together with naturality in the second argument. *)
  Lemma natequiv_pi1bouquet_rec (S : Type)
    : NatEquiv
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type).
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S)))
  (opyon S o group_type)
  Proof.
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S)))
  (opyon S o group_type)
    (** Pointify *)
    nrefine (natequiv_compose _ _).
H: Univalence
S: Type
NatEquiv ?Goal (fun x : Group => opyon S x)
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S))) ?Goal
    1: exact (natequiv_prewhisker (natequiv_pointify_r S) ptype_group).
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S)))
  (fun x : Group => opyon (pointify S) x)
    (** Post-compose with [pequiv_loops_bg_g] *)
    nrefine (natequiv_compose _ _).
H: Univalence
S: Type
NatEquiv ?Goal (fun x : Group => opyon (pointify S) x)
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S))) ?Goal
    1: exact (natequiv_postwhisker _ (natequiv_inverse natequiv_g_loops_bg)).
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S)))
  (fun x : Group =>
   opyon (pointify S)
     ((fun x0 : Group => loops (B x0)) x))
    (** Loop space-suspension adjunction *)
    nrefine (natequiv_compose _ _).
H: Univalence
S: Type
NatEquiv ?Goal
  (fun x : Group => opyon (pointify S) (loops (B x)))
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S))) ?Goal
    1: exact (natequiv_prewhisker
      (natequiv_loop_susp_adjoint_r (pointify S)) B).
H: Univalence
S: Type
NatEquiv (opyon (Pi 1 (Bouquet S)))
  (fun x : Group => opyon (psusp (pointify S)) (B x))
    (** Pi1-BG adjunction *)
    rapply natequiv_bg_pi1_adjoint.
  Defined.

  (** For the rest of this file, we don't need to unfold this. *)
  Local Opaque natequiv_pi1bouquet_rec.

  Theorem equiv_pi1bouquet_rec (S : Type) (G : Group)
    : (Pi 1 (Bouquet S) $-> G) <~> (S -> G).
H: Univalence
S: Type
G: Group
(Pi 1 (Bouquet S) $-> G) <~> (S -> G)
  Proof.
H: Univalence
S: Type
G: Group
(Pi 1 (Bouquet S) $-> G) <~> (S -> G)
    apply natequiv_pi1bouquet_rec.
  Defined.

  #[export] Instance is1natural_equiv_pi1bouquet_rec (S : Type)
    : Is1Natural
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type)
        (fun G => equiv_pi1bouquet_rec S G).
H: Univalence
S: Type
Is1Natural (opyon (Pi 1 (Bouquet S)))
  (opyon S o group_type)
  (fun G : HomotopyGroup_type 1 =>
   equiv_pi1bouquet_rec S G)
  Proof.
H: Univalence
S: Type
Is1Natural (opyon (Pi 1 (Bouquet S)))
  (opyon S o group_type)
  (fun G : HomotopyGroup_type 1 =>
   equiv_pi1bouquet_rec S G)
    exact (is1natural_natequiv (natequiv_pi1bouquet_rec _)).
  Defined.

  (** We can define the inclusion map by using the previous equivalence on the identity group homomorphism. *)
  Definition pi1bouquet_incl (S : Type)
    : S -> Pi 1 (Bouquet S).
H: Univalence
S: Type
S -> Pi 1 (Bouquet S)
  Proof.
H: Univalence
S: Type
S -> Pi 1 (Bouquet S)
    rapply equiv_pi1bouquet_rec.
H: Univalence
S: Type
Pi 1 (Bouquet S) $-> Pi 1 (Bouquet S)
    exact grp_homo_id.
  Defined.

  (** The fundamental group of an S-bouquet is the free group on S. *)
  #[export] Instance isfreegroupon_pi1bouquet (S : Type)
    : IsFreeGroupOn S (Pi 1 (Bouquet S)) (pi1bouquet_incl S).
H: Univalence
S: Type
IsFreeGroupOn S (Pi 1 (Bouquet S)) (pi1bouquet_incl S)
  Proof.
H: Univalence
S: Type
IsFreeGroupOn S (Pi 1 (Bouquet S)) (pi1bouquet_incl S)
    apply equiv_isfreegroupon_isequiv_precomp.
H: Univalence
S: Type
forall G : Group,
IsEquiv
  (fun (f : Pi 1 (Bouquet S) $-> G) (x : S) =>
   f (pi1bouquet_incl S x))
    intro G.
H: Univalence
S: Type
G: Group
IsEquiv
  (fun (f : Pi 1 (Bouquet S) $-> G) (x : S) =>
   f (pi1bouquet_incl S x))
    snapply isequiv_homotopic'.
H: Univalence
S: Type
G: Group
(Pi 1 (Bouquet S) $-> G) <~> (S -> G)
H: Univalence
S: Type
G: Group
?f ==
(fun (f : Pi 1 (Bouquet S) $-> G) (x : S) =>
 f (pi1bouquet_incl S x))
    1: apply equiv_pi1bouquet_rec.
H: Univalence
S: Type
G: Group
equiv_pi1bouquet_rec S G ==
(fun (f : Pi 1 (Bouquet S) $-> G) (x : S) =>
 f (pi1bouquet_incl S x))
    intros f.
H: Univalence
S: Type
G: Group
f: Pi 1 (Bouquet S) $-> G
equiv_pi1bouquet_rec S G f =
(fun x : S => f (pi1bouquet_incl S x))
    refine (_ @ @is1natural_equiv_pi1bouquet_rec S _ _ f grp_homo_id).
H: Univalence
S: Type
G: Group
f: Pi 1 (Bouquet S) $-> G
equiv_pi1bouquet_rec S G f =
(equiv_pi1bouquet_rec S G $o
 fmap (opyon (Pi 1 (Bouquet S))) f) grp_homo_id
    simpl; f_ap; symmetry.
H: Univalence
S: Type
G: Group
f: Pi 1 (Bouquet S) $-> G
grp_homo_compose f grp_homo_id = f
    exact (cat_idr_strong f).
  Defined.

End AssumeUnivalence.