Require Import HoTT.Basics HoTT.Types.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 auto-equivalence [f] (the action of [1]) whose iterates are all pointwise distinct. *)
  Context (f : R <~> R)
          (f_free : forall (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. *)
  #[export] Instance isset_RmodZ : IsHSet RmodZ.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
IsHSet RmodZ
  Proof.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
IsHSet RmodZ
    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 _.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) <~> RmodZ
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
{z : Circle & Circle_rec Type R (path_universe f) z} <~>
{w : Coeq idmap idmap &
Coeq_rec Type (unit_name R) (unit_name (path_universe f)) w}
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
IsHSet {z : Circle & Circle_rec Type R (path_universe f) z}
    -
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) <~> RmodZ unshelve rapply equiv_adjointify.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) -> RmodZ
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
RmodZ -> Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
(fun x : RmodZ => ?Goal4 (?Goal5 x)) == idmap
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
(fun x : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
 ?Goal5 (?Goal4 x)) ==
idmap
      +
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) -> RmodZ simple refine (Wtil_rec _ _ _).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall a : Unit, unit_name R a -> RmodZ
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (b : Unit) (y : unit_name R (idmap b)),
?cct' (idmap b) y = ?cct' (idmap b) (unit_name f b y)
        *
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall a : Unit, unit_name R a -> RmodZ intros u r; exact (coeq r).
        *
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (b : Unit) (y : unit_name R (idmap b)),
(fun (u : Unit) (r : unit_name R u) => coeq r) (idmap b) y =
(fun (u : Unit) (r : unit_name R u) => coeq r) (idmap b) (unit_name f b y) intros u r; cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
u: Unit
r: unit_name R (idmap u)
coeq r = coeq (f r) exact ((cglue r)^).
      +
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
RmodZ -> Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) simple refine (Coeq_rec _ _ _).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
R -> Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall b : R, ?coeq' (f b) = ?coeq' (idmap b)
        *
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
R -> Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) exact (cct tt).
        *
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall b : R, cct tt (f b) = cct tt (idmap b) intros r; exact ((ppt tt r)^).
      +
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
(fun x : RmodZ =>
 Wtil_rec RmodZ (fun (u : Unit) (r : unit_name R u) => coeq r)
   (fun (u : Unit) (r : unit_name R (idmap u)) =>
    (cglue r)^
    :
    (fun (u0 : Unit) (r0 : unit_name R u0) => coeq r0) (idmap u) r =
    (fun (u0 : Unit) (r0 : unit_name R u0) => coeq r0) 
      (idmap u) (unit_name f u r))
   (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
      (cct tt) (fun r : R => (ppt tt r)^) x)) ==
idmap refine (Coeq_ind _ (fun a => 1) _); cbn; intros b.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
transport
  (fun w : Coeq f idmap =>
   Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
     (unit_name (fun r : R => (cglue r)^))
     (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
        (cct tt) (fun r : R => (ppt tt r)^) w) =
   w)
  (cglue b) 1 =
1
        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
(ap
   (fun x : Coeq f idmap =>
    Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
      (unit_name (fun r : R => (cglue r)^))
      (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
         (cct tt) (fun r : R => (ppt tt r)^) x))
   (cglue b))^ @
cglue b = 1
        apply moveR_Vp; rewrite concat_p1.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
cglue b =
ap
  (fun x : Coeq f idmap =>
   Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
     (unit_name (fun r : R => (cglue r)^))
     (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
        (cct tt) (fun r : R => (ppt tt r)^) x))
  (cglue b)
        rewrite ap_compose.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
cglue b =
ap
  (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
     (unit_name (fun r : R => (cglue r)^)))
  (ap
     (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
        (cct tt) (fun r : R => (ppt tt r)^))
     (cglue b))
        rewrite (Coeq_rec_beta_cglue
                   (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
                   (cct tt) (fun r => (ppt tt r)^) b).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
cglue b =
ap
  (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
     (unit_name (fun r : R => (cglue r)^)))
  (ppt tt b)^
        rewrite ap_V; symmetry.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
b: R
(ap
   (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
      (unit_name (fun r : R => (cglue r)^)))
   (ppt tt b))^ =
cglue b
        exact (inverse2
                  (Wtil_rec_beta_ppt
                     RmodZ (unit_name (fun r => coeq r))
                     (unit_name (fun r => (cglue r)^)) tt b) @ inv_V _).
      +
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
(fun x : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
 Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
   (cct tt) (fun r : R => (ppt tt r)^)
   (Wtil_rec RmodZ (fun (u : Unit) (r : unit_name R u) => coeq r)
      (fun (u : Unit) (r : unit_name R (idmap u)) =>
       (cglue r)^
       :
       (fun (u0 : Unit) (r0 : unit_name R u0) => coeq r0) (idmap u) r =
       (fun (u0 : Unit) (r0 : unit_name R u0) => coeq r0) 
         (idmap u) (unit_name f u r))
      x)) ==
idmap simple refine (Wtil_ind _ _ _); cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (a : Unit) (x : R),
Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
  (cct tt) (fun r : R => (ppt tt r)^) (coeq x) =
cct a x
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (b : Unit) (y : R),
transport
  (fun w : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
   Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r : R => (ppt tt r)^)
     (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
        (unit_name (fun r : R => (cglue r)^)) w) =
   w)
  (ppt b y) (?Goal4 b y) =
?Goal4 b (f y)
        {
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (a : Unit) (x : R),
Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
  (cct tt) (fun r : R => (ppt tt r)^) (coeq x) =
cct a x intros [] ?; reflexivity. }
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
forall (b : Unit) (y : R),
transport
  (fun w : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
   Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r : R => (ppt tt r)^)
     (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
        (unit_name (fun r : R => (cglue r)^)) w) =
   w)
  (ppt b y)
  ((fun a : Unit =>
    match
      a as u
      return
        (forall x : R,
         Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
           (cct tt) (fun r : R => (ppt tt r)^) (coeq x) =
         cct u x)
    with
    | tt => fun x : R => 1
    end) b y) =
(fun a : Unit =>
 match
   a as u
   return
     (forall x : R,
      Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
        (cct tt) (fun r : R => (ppt tt r)^) (coeq x) =
      cct u x)
 with
 | tt => fun x : R => 1
 end) b (f y)
        intros [] r; cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
transport
  (fun w : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
   Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r0 : R => (ppt tt r0)^)
     (Wtil_rec RmodZ (unit_name (fun r0 : R => coeq r0))
        (unit_name (fun r0 : R => (cglue r0)^)) w) =
   w)
  (ppt tt r) 1 =
1
        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
(ap
   (fun x : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
    Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
      (cct tt) (fun r0 : R => (ppt tt r0)^)
      (Wtil_rec RmodZ (unit_name (fun r0 : R => coeq r0))
         (unit_name (fun r0 : R => (cglue r0)^)) x))
   (ppt tt r))^ @
ppt tt r = 1
        apply moveR_Vp; rewrite concat_p1.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
ppt tt r =
ap
  (fun x : Wtil Unit Unit idmap idmap (unit_name R) (unit_name f) =>
   Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r0 : R => (ppt tt r0)^)
     (Wtil_rec RmodZ (unit_name (fun r0 : R => coeq r0))
        (unit_name (fun r0 : R => (cglue r0)^)) x))
  (ppt tt r)
        rewrite ap_compose.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
ppt tt r =
ap
  (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r0 : R => (ppt tt r0)^))
  (ap
     (Wtil_rec RmodZ (unit_name (fun r0 : R => coeq r0))
        (unit_name (fun r0 : R => (cglue r0)^)))
     (ppt tt r))
        refine (_ @ ap (ap _) (Wtil_rec_beta_ppt
                   RmodZ (unit_name (fun r => coeq r))
                   (unit_name (fun r => (cglue r)^)) tt r)^).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
ppt tt r =
ap
  (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) 
     (cct tt) (fun r0 : R => (ppt tt r0)^))
  (cglue r)^
        rewrite ap_V.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
ppt tt r =
(ap
   (Coeq_rec (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
      (cct tt) (fun r0 : R => (ppt tt r0)^))
   (cglue r))^
        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).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
r: R
ppt tt r = ((ppt tt r)^)^
        symmetry; apply inv_V.
    -
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
{z : Circle & Circle_rec Type R (path_universe f) z} <~>
{w : Coeq idmap idmap &
Coeq_rec Type (unit_name R) (unit_name (path_universe f)) w} apply equiv_functor_sigma_id; intros x.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
Circle_rec Type R (path_universe f) x <~>
Coeq_rec Type (unit_name R) (unit_name (path_universe f)) x
      apply equiv_path.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
Circle_rec Type R (path_universe f) x =
Coeq_rec Type (unit_name R) (unit_name (path_universe f)) x
      revert x; refine (Circle_ind _ 1 _); cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
transport
  (fun x : Circle =>
   Circle_rec Type R (path_universe f) x =
   Coeq_rec Type (unit_name R) (unit_name (path_universe f)) x)
  loop 1 =
1
      rewrite transport_paths_FlFr, concat_p1.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
(ap (fun x : Circle => Circle_rec Type R (path_universe f) x) loop)^ @
ap (Coeq_rec Type (unit_name R) (unit_name (path_universe f))) loop = 1
      apply moveR_Vp; rewrite concat_p1.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
ap (Coeq_rec Type (unit_name R) (unit_name (path_universe f))) loop =
ap (fun x : Circle => Circle_rec Type R (path_universe f) x) loop
      rewrite Circle_rec_beta_loop.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
ap (Coeq_rec Type (unit_name R) (unit_name (path_universe f))) loop =
path_universe f
      unfold loop.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
ap (Coeq_rec Type (unit_name R) (unit_name (path_universe f))) (cglue tt) =
path_universe f
      exact (Coeq_rec_beta_cglue _ _ _ _).
    -
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
IsHSet {z : Circle & Circle_rec Type R (path_universe f) z} apply istrunc_S.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
is_mere_relation {z : Circle & Circle_rec Type R (path_universe f) z} paths
      intros xu yv.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
xu, yv: {z : Circle & Circle_rec Type R (path_universe f) z}
IsHProp (xu = yv)
      nrefine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
xu, yv: {z : Circle & Circle_rec Type R (path_universe f) z}
IsHProp
  {p : xu.1 = yv.1 &
  transport (fun z : Circle => Circle_rec Type R (path_universe f) z) p xu.2 =
  yv.2}
      destruct xu as [x u], yv as [y v]; cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
u: Circle_rec Type R (path_universe f) x
y: Circle
v: Circle_rec Type R (path_universe f) y
IsHProp
  {p : x = y &
  transport (fun z : Circle => Circle_rec Type R (path_universe f) z) p u = v}
      apply hprop_allpath.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
u: Circle_rec Type R (path_universe f) x
y: Circle
v: Circle_rec Type R (path_universe f) y
forall
x0
 y0 : {p : x = y &
      transport (fun z : Circle => Circle_rec Type R (path_universe f) z) p u =
      v},
x0 = y0
      intros [p r] [q s].
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
u: Circle_rec Type R (path_universe f) x
y: Circle
v: Circle_rec Type R (path_universe f) y
p: x = y
r: transport (fun z : Circle => Circle_rec Type R (path_universe f) z) p u = v
q: x = y
s: transport (fun z : Circle => Circle_rec Type R (path_universe f) z) q u = v
(p; r) = (q; s)
      set (P := Circle_rec Type R (path_universe f)) in *.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
(p; r) = (q; s)
      assert (forall z, IsHSet (P z)).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
forall z : Circle, IsHSet (P z)
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
X: forall z : Circle, IsHSet (P z)
(p; r) = (q; s)
      {
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
forall z : Circle, IsHSet (P z) simple refine (Circle_ind _ _ _); cbn beta.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
IsHSet (P base)
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
transport (fun x0 : Circle => IsHSet (P x0)) loop ?Goal1 = ?Goal1
        -
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
IsHSet (P base) exact _.
        -
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
transport (fun x0 : Circle => IsHSet (P x0)) loop IsHSet0 = IsHSet0 apply path_ishprop. }
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
X: forall z : Circle, IsHSet (P z)
(p; r) = (q; s)
      apply path_sigma_hprop; cbn.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r0 : R) (n m : Int), int_iter f n r0 = int_iter f m r0 -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p: x = y
r: transport (fun z : Circle => P z) p u = v
q: x = y
s: transport (fun z : Circle => P z) q u = v
X: forall z : Circle, IsHSet (P z)
p = q
      assert (t := r @ s^); clear r s.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p, q: x = y
X: forall z : Circle, IsHSet (P z)
t: transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u
p = q
      assert (xb := merely_path_is0connected Circle base x).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p, q: x = y
X: forall z : Circle, IsHSet (P z)
t: transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u
xb: merely (base = x)
p = q
      assert (yb := merely_path_is0connected Circle base y).
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p, q: x = y
X: forall z : Circle, IsHSet (P z)
t: transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u
xb: merely (base = x)
yb: merely (base = y)
p = q
      strip_truncations.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
x: Circle
P:= Circle_rec Type R (path_universe f): Circle -> Type
u: P x
y: Circle
v: P y
p, q: x = y
X: forall z : Circle, IsHSet (P z)
t: transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u
yb: base = y
xb: base = x
p = q destruct xb, yb.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
P:= Circle_rec Type R (path_universe f): Circle -> Type
u, v: P base
p, q: base = base
X: forall z : Circle, IsHSet (P z)
t: transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u
p = q
      revert p q t.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n m : Int), int_iter f n r = int_iter f m r -> n = m
RmodZ:= Coeq f idmap: Type
P:= Circle_rec Type R (path_universe f): Circle -> Type
u, v: P base
X: forall z : Circle, IsHSet (P z)
forall p q : base = base,
transport (fun z : Circle => P z) p u = transport (fun z : Circle => P z) q u ->
p = q
      equiv_intro (equiv_loopCircle_int^-1) n.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m : Int), int_iter f n0 r = int_iter f m r -> n0 = m
RmodZ:= Coeq f idmap: Type
P:= Circle_rec Type R (path_universe f): Circle -> Type
u, v: P base
X: forall z : Circle, IsHSet (P z)
n: Int
forall q : base = base,
transport (fun z : Circle => P z) (equiv_loopCircle_int^-1 n) u =
transport (fun z : Circle => P z) q u -> equiv_loopCircle_int^-1 n = q
      equiv_intro (equiv_loopCircle_int^-1) m.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m0 : Int), int_iter f n0 r = int_iter f m0 r -> n0 = m0
RmodZ:= Coeq f idmap: Type
P:= Circle_rec Type R (path_universe f): Circle -> Type
u, v: P base
X: forall z : Circle, IsHSet (P z)
n, m: Int
transport (fun z : Circle => P z) (equiv_loopCircle_int^-1 n) u =
transport (fun z : Circle => P z) (equiv_loopCircle_int^-1 m) u ->
equiv_loopCircle_int^-1 n = equiv_loopCircle_int^-1 m
      subst P.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m0 : Int), int_iter f n0 r = int_iter f m0 r -> n0 = m0
RmodZ:= Coeq f idmap: Type
u, v: Circle_rec Type R (path_universe f) base
X: forall z : Circle, IsHSet (Circle_rec Type R (path_universe f) z)
n, m: Int
transport (fun z : Circle => Circle_rec Type R (path_universe f) z)
  (equiv_loopCircle_int^-1 n) u =
transport (fun z : Circle => Circle_rec Type R (path_universe f) z)
  (equiv_loopCircle_int^-1 m) u ->
equiv_loopCircle_int^-1 n = equiv_loopCircle_int^-1 m
      rewrite !Circle_action_is_iter.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m0 : Int), int_iter f n0 r = int_iter f m0 r -> n0 = m0
RmodZ:= Coeq f idmap: Type
u, v: Circle_rec Type R (path_universe f) base
X: forall z : Circle, IsHSet (Circle_rec Type R (path_universe f) z)
n, m: Int
int_iter f n u = int_iter f m u ->
equiv_loopCircle_int^-1 n = equiv_loopCircle_int^-1 m
      intros p.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m0 : Int), int_iter f n0 r = int_iter f m0 r -> n0 = m0
RmodZ:= Coeq f idmap: Type
u, v: Circle_rec Type R (path_universe f) base
X: forall z : Circle, IsHSet (Circle_rec Type R (path_universe f) z)
n, m: Int
p: int_iter f n u = int_iter f m u
equiv_loopCircle_int^-1 n = equiv_loopCircle_int^-1 m apply ap.
H: Univalence
R: Type
IsHSet0: IsHSet R
f: R <~> R
f_free: forall (r : R) (n0 m0 : Int), int_iter f n0 r = int_iter f m0 r -> n0 = m0
RmodZ:= Coeq f idmap: Type
u, v: Circle_rec Type R (path_universe f) base
X: forall z : Circle, IsHSet (Circle_rec Type R (path_universe f) z)
n, m: Int
p: int_iter f n u = int_iter f m u
n = m
      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.