Library HoTT.Homotopy.WhiteheadsPrinciple

Require Import Basics Types.
Require Import Pointed.
Require Import WildCat.Core HFiber.
Require Import Truncations.
Require Import Algebra.Groups.Group.
Require Import Homotopy.HomotopyGroup.

Local Open Scope pointed_scope.
Local Open Scope nat_scope.

8.8.1

Definition isequiv_issurj_tr0_isequiv_ap
           `{Univalence} {A B : Type} (f : A → B)
           {i : IsSurjection (Trunc_functor 0 f)}
           {ii : ∀ x y , IsEquiv (@ap _ _ f x y)}
  : IsEquiv f.
Proof.
  apply (equiv_isequiv_ap_isembedding f)^-1 in ii.
  srapply isequiv_surj_emb.
  srapply BuildIsSurjection.
  cbn; intro b.
  pose proof (@center _ (i (tr b))) as p.
  revert p.
  apply Trunc_functor.
  apply sig_ind.
  srapply Trunc_ind.
  intros a p.
  apply (equiv_path_Tr _ _)^-1 in p.
  strip_truncations.
  ∃ a.
  exact p.
Defined.

8.8.2

Definition isequiv_isbij_tr0_isequiv_loops
           `{Univalence} {A B : Type} (f : A → B)
           {i : IsEquiv (Trunc_functor 0 f)}
           {ii : ∀ x , IsEquiv (fmap loops (pmap_from_point f x)) }
  : IsEquiv f.
Proof.
  srapply (isequiv_issurj_tr0_isequiv_ap f).
  intros x y.
  apply isequiv_inhab_codomain.
  intro p.
  apply (ap (@tr 0 _)) in p.
  apply (@equiv_inj _ _ _ i (tr x) (tr y)) in p.
  apply (equiv_path_Tr _ _)^-1 in p.
  strip_truncations.
  destruct p.
  cbn in ii.
  snrapply (isequiv_homotopic _ (H:=ii x)).
  exact (fun _ ⇒ concat_1p _ @ concat_p1 _).
Defined.

When the types are 0-connected and the map is pointed, just one loops_functor needs to be checked.

Definition isequiv_is0connected_isequiv_loops
           `{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B}
           (f : A ->* B)
           (e : IsEquiv (fmap loops f))
  : IsEquiv f.
Proof.
  apply isequiv_isbij_tr0_isequiv_loops.

The pi_0 condition is trivial because A and B are 0-connected.

1: apply isequiv_contr_contr.

Since A is 0-connected, it's enough to check the loops_functor condition for the basepoint.

rapply conn_point_elim.

The loops_functor condition for pmap_from_point f _ is equivalent to the loops_functor condition for f with its given pointing.

  srapply isequiv_homotopic'.
  - exact (equiv_concat_lr (point_eq f) (point_eq f)^ oE (Build_Equiv _ _ _ e)).
  - intro r.
    simpl.
    hott_simpl.
Defined.

Truncated Whitehead's principle (8.8.3)

Definition whiteheads_principle
           {ua : Univalence} {A B : Type} {f : A → B}
           (n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
           {i : IsEquiv (Trunc_functor 0 f)}
           {ii : ∀ (x : A) (k : nat ), IsEquiv (fmap (Pi k .+1) (pmap_from_point f x)) }
  : IsEquiv f.
Proof.
  revert A B H0 H1 f i ii.
  induction n as [|n IHn].
  1: intros; apply isequiv_contr_contr.
  intros A B H0 H1 f i ii.
  nrefine (@isequiv_isbij_tr0_isequiv_loops ua _ _ f i _).
  intro x.
  nrefine (isequiv_homotopic (@ap _ _ f x x) _).
  2:{intros p; cbn.
     symmetry; exact (concat_1p _ @ concat_p1 _). }
  pose proof (@istrunc_paths _ _ H0 x x) as h0.
  pose proof (@istrunc_paths _ _ H1 (f x) (f x)) as h1.
  nrefine (IHn (x=x) (f x=f x) h0 h1 (@ap _ _ f x x) _ _).
  - pose proof (ii x 0) as h2.
    unfold is0functor_pi in h2; cbn in h2.
    refine (@isequiv_homotopic _ _ _ _ h2 _).
    apply (O_functor_homotopy (Tr 0)); intros p.
    exact (concat_1p _ @ concat_p1 _).
  - intros p k; revert p.
    assert (h3 : ∀ (y:A) (q:x=y ),
               IsEquiv (fmap (Pi k.+1) (pmap_from_point (@ap _ _ f x y) q))).
    2:exact (h3 x).
    intros y q. destruct q.
    snrefine (isequiv_homotopic _ _).
    1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))).
    2:{ rapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
        - intros p; cbn.
          refine (concat_1p _ @ concat_p1 _).
        - reflexivity. }
    nrefine (isequiv_commsq _ _ _ _ (fmap_pi_loops k.+1 (pmap_from_point f x))).
    2-3:refine (equiv_isequiv (pi_loops _ _)).
    exact (ii x k.+1).
Defined.