FreeIntQuotient.v

(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 : 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. *)
  Global 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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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
        refine (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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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 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 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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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 r : R => (ppt tt r)^)
      (Wtil_rec RmodZ
         (unit_name (fun r : R => coeq r))
         (unit_name (fun r : R => (cglue r)^)) 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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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 r : R => (ppt tt r)^)
     (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
        (unit_name (fun r : R => (cglue r)^)) x))
  (ppt tt r)
        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
r: R
ppt tt r =
ap
  (Coeq_rec
     (Wtil Unit Unit idmap idmap (unit_name R)
        (unit_name f)) (cct tt)
     (fun r : R => (ppt tt r)^))
  (ap
     (Wtil_rec RmodZ (unit_name (fun r : R => coeq r))
        (unit_name (fun r : R => (cglue r)^)))
     (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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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 r : R => (ppt tt r)^)) (cglue r)^
        rewrite ap_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
r: R
ppt tt r =
(ap
   (Coeq_rec
      (Wtil Unit Unit idmap idmap (unit_name R)
         (unit_name f)) (cct tt)
      (fun r : R => (ppt tt r)^)) (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 (r : R) (n m : Int),
int_iter f n r = int_iter f m r -> 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 (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
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 (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: 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 (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: 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 (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: 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 (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: 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 (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: 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 (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: 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 x : Circle => IsHSet (P x)) loop ?Goal1 =
?Goal1
        -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: 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 (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: 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 x : Circle => IsHSet (P x)) loop
  IsHSet0 = IsHSet0 apply path_ishprop. }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: 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 (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: 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) (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)
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) (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)
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) (n m : Int),
int_iter f n r = int_iter f m r -> n = m
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) (n m : Int),
int_iter f n r = int_iter f m r -> n = m
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) (n m : Int),
int_iter f n r = int_iter f m r -> n = m
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) (n m : Int),
int_iter f n r = int_iter f m r -> n = m
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.