From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Universe Equiv NatTrans Yoneda.
Require Import Pointed.
From HoTT.Algebra.Groups Require Import Group FreeGroup.
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.