Library HoTT.HIT.FreeIntQuotient

Require Import HoTT.Basics HoTT.Types.
Require Import Spaces.Int Spaces.Circle.
Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.

Local Open Scope path_scope.

Quotients by free actions of Int

We will show that if Int acts freely on a set, then the set-quotient of that action can be defined without a 0-truncation, giving it a universal property for mapping into all types.

Section FreeIntAction.

Context `{Univalence}.
Context (R : Type) `{IsHSet R}.

A free action by Int is the same as a single autoequivalence f (the action of 1) whose iterates are all pointwise distinct.

  Context (f : R <~> R)
          (f_free : ∀ (r : R) (n m : Int ),
                      (int_iter f n r = int_iter f m r ) → (n = m )).

We can then define the quotient to be the coequalizer of f and the identity map. This gives it the desired universal property for all types; it remains to show that this definition gives a set.

Let RmodZ := Coeq f idmap.

Together, R and f define a fibration over Circle. By the flattening lemma, its total space is equivalent to the quotient.

  Global Instance isset_RmodZ : IsHSet RmodZ.
  Proof.
    nrefine (istrunc_equiv_istrunc
              { z : Circle & Circle_rec Type R (path_universe f) z }
              (_ oE (@equiv_flattening _ Unit Unit idmap idmap
                                  (fun _ ⇒ R) (fun _ ⇒ f))^-1
              oE _));
    try exact _.
    - unshelve rapply equiv_adjointify.
      + simple refine (Wtil_rec _ _ _).
        × intros u r; exact (coeq r).
        × intros u r; cbn. exact ((cglue r)^).
      + simple refine (Coeq_rec _ _ _).
        × exact (cct tt).
        × intros r; exact ((ppt tt r)^).
      + refine (Coeq_ind _ (fun a ⇒ 1) _); cbn; intros b.
        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
        apply moveR_Vp; rewrite concat_p1.
        rewrite ap_compose.
        rewrite (Coeq_rec_beta_cglue
                   (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
                   (cct tt) (fun r ⇒ (ppt tt r )^) b).
        rewrite ap_V; symmetry.
        refine (inverse2
                  (Wtil_rec_beta_ppt
                     RmodZ (unit_name (fun r ⇒ coeq r))
                     (unit_name (fun r ⇒ (cglue r )^)) tt b) @ inv_V _).
      + simple refine (Wtil_ind _ _ _); cbn.
        { intros [] ?; reflexivity. }
        intros [] r; cbn.
        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
        apply moveR_Vp; rewrite concat_p1.
        rewrite ap_compose.
        refine (_ @ ap (ap _) (Wtil_rec_beta_ppt
                   RmodZ (unit_name (fun r ⇒ coeq r))
                   (unit_name (fun r ⇒ (cglue r )^)) tt r)^).
        rewrite ap_V.
        rewrite (Coeq_rec_beta_cglue
                   (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
                   (cct tt) (fun r0 : R ⇒ (ppt tt r0 )^) r).
        symmetry; apply inv_V.
    - apply equiv_functor_sigma_id; intros x.
      apply equiv_path.
      revert x; refine (Circle_ind _ 1 _); cbn.
      rewrite transport_paths_FlFr, concat_p1.
      apply moveR_Vp; rewrite concat_p1.
      rewrite Circle_rec_beta_loop.
      unfold loop.
      exact (Coeq_rec_beta_cglue _ _ _ _).
    - apply istrunc_S.
      intros xu yv.
      nrefine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)).
      destruct xu as [x u], yv as [y v]; cbn.
      apply hprop_allpath.
      intros [p r] [q s].
      set (P := Circle_rec Type R (path_universe f)) in ×.
      assert (∀ z , IsHSet (P z)).
      { simple refine (Circle_ind _ _ _); cbn beta.
        - exact _.
        - apply path_ishprop. }
      apply path_sigma_hprop; cbn.
      assert (t := r @ s^); clear r s.
      assert (xb := merely_path_is0connected Circle base x).
      assert (yb := merely_path_is0connected Circle base y).
      strip_truncations. destruct xb, yb.
      revert p q t.
      equiv_intro (equiv_loopCircle_int ^-1) n.
      equiv_intro (equiv_loopCircle_int ^-1) m.
      subst P.
      rewrite !Circle_action_is_iter.
      intros p. apply ap.
      exact (f_free u n m p).
  Qed.

TODO: Prove that this RmodZ is equivalent to the set-quotient of R by a suitably defined equivalence relation.

End FreeIntAction.