Library HoTT.HIT.FreeIntQuotient
(* -*- mode: coq; mode: visual-line -*- *)
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.
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
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)).
(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.
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.
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.