(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
Require Import HSet.
Require Import Spaces.Pos Spaces.Int.
Require Import Colimits.Coeq.
Require Import Truncations.Core Truncations.Connectedness.

(** * Theorems about the [Circle]. *)

Local Open Scope pointed_scope.
Local Open Scope path_scope.

Generalizable Variables X A B f g n.

(* ** Definition of the [Circle]. *)

(** We define the circle as the coequalizer of two copies of the identity map of [Unit].  This is easily equivalent to the naive definition

<<
Private Inductive Circle : Type0 :=
| base : Circle
| loop : base = base.
>>

but it allows us to apply the flattening lemma directly rather than having to pass across that equivalence.  *)

(** The circle is defined to be the coequalizer of two copies of the identity map on [Unit]. *)
Definition Circle := @Coeq Unit Unit idmap idmap.

(** It has a basepoint. *)
Definition base : Circle := coeq tt.

(** And a non-trivial path. *)
Definition loop : base = base := cglue tt.

(** Here is a notation for the circle that can be imported. *)
Module CircleNotation.
  Notation S1 := Circle (only parsing).
End CircleNotation.

(** Circle induction *)
Definition Circle_ind (P : Circle -> Type)
  (b : P base) (l : loop # b = b)
  : forall (x : Circle), P x.
P: Circle -> Type
b: P base
l: transport P loop b = b
forall x : Circle, P x
Proof.
P: Circle -> Type
b: P base
l: transport P loop b = b
forall x : Circle, P x
  refine (Coeq_ind P (fun u => transport P (ap coeq (path_unit tt u)) b) _).
P: Circle -> Type
b: P base
l: transport P loop b = b
forall b0 : Unit,
transport P (cglue b0)
  (transport P (ap coeq (path_unit tt b0)) b) =
transport P (ap coeq (path_unit tt b0)) b
  intros []; exact l.
Defined.

(** Computation rule for circle induction. *)
Definition Circle_ind_beta_loop (P : Circle -> Type)
  (b : P base) (l : loop # b = b)
  : apD (Circle_ind P b l) loop = l
  := Coeq_ind_beta_cglue P _ _ tt.

(** We mark [Circle], [base] and [loop] to never be simplified by [simpl] or [cbn] in order to hide how we defined it from the user. *) 
Arguments Circle : simpl never.
Arguments base : simpl never.
Arguments loop : simpl never.
Arguments Circle_ind_beta_loop : simpl never.

(** The recursion princple or non-dependent eliminator. *)
Definition Circle_rec (P : Type) (b : P) (l : b = b)
  : Circle -> P
  := Circle_ind (fun _ => P) b (transport_const _ _ @ l).

(** Computation rule for non-dependent eliminator. *)
Definition Circle_rec_beta_loop (P : Type) (b : P) (l : b = b)
  : ap (Circle_rec P b l) loop = l.
P: Type
b: P
l: b = b
ap (Circle_rec P b l) loop = l
Proof.
P: Type
b: P
l: b = b
ap (Circle_rec P b l) loop = l
  unfold Circle_rec.
P: Type
b: P
l: b = b
ap
  (Circle_ind (fun _ : Circle => P) b
     (transport_const loop b @ l)) loop = l
  refine (cancelL (transport_const loop b) _ _ _).
P: Type
b: P
l: b = b
transport_const loop b @
ap
  (Circle_ind (fun _ : Circle => P) b
     (transport_const loop b @ l)) loop =
transport_const loop b @ l
  refine ((apD_const (Circle_ind (fun _ => P) b _) loop)^ @ _).
P: Type
b: P
l: b = b
apD
  (Circle_ind (fun _ : Circle => P) b
     (transport_const loop b @ l)) loop =
transport_const loop b @ l
  refine (Circle_ind_beta_loop (fun _ => P) _ _).
Defined.

(** The [Circle] is pointed by [base]. *)
Global Instance ispointed_Circle : IsPointed Circle := base.

Definition pCircle : pType := [Circle, base].

(** ** The loop space of the [Circle] is the Integers [Int]

  This is the encode-decode style proof a la Licata-Shulman. *)

Section EncodeDecode.
  (** We assume univalence throughout this section. *)
  Context `{Univalence}.

  (** First we define the type of codes, this is a type family over the circle. This can be thought of as the covering space by the homotopical real numbers. It is defined by mapping loop to the path given by univalence applied to the automorphism of the integers. We will show that the section of this family at [base] is equivalent to the loop space of the circle. Giving us an equivalence [base = base <~> Int]. *)
  Definition Circle_code : Circle -> Type
    := Circle_rec Type Int (path_universe int_succ).

  (** Transporting along [loop] gives us the successor automorphism on [Int]. *)
  Definition transport_Circle_code_loop (z : Int)
    : transport Circle_code loop z = int_succ z.
H: Univalence
z: Int
transport Circle_code loop z = int_succ z
  Proof.
H: Univalence
z: Int
transport Circle_code loop z = int_succ z
    refine (transport_compose idmap Circle_code loop z @ _).
H: Univalence
z: Int
transport idmap (ap Circle_code loop) z = int_succ z
    unfold Circle_code; rewrite Circle_rec_beta_loop.
H: Univalence
z: Int
transport idmap (path_universe int_succ) z =
int_succ z
    apply transport_path_universe.
  Defined.

  (** Transporting along [loop^] gives us the predecessor on [Int]. *)
  Definition transport_Circle_code_loopV (z : Int)
    : transport Circle_code loop^ z = int_pred z.
H: Univalence
z: Int
transport Circle_code loop^ z = int_pred z
  Proof.
H: Univalence
z: Int
transport Circle_code loop^ z = int_pred z
    refine (transport_compose idmap Circle_code loop^ z @ _).
H: Univalence
z: Int
transport idmap (ap Circle_code loop^) z = int_pred z
    rewrite ap_V.
H: Univalence
z: Int
transport idmap (ap Circle_code loop)^ z = int_pred z
    unfold Circle_code; rewrite Circle_rec_beta_loop.
H: Univalence
z: Int
transport idmap (path_universe int_succ)^ z =
int_pred z
    rewrite <- (path_universe_V int_succ).
H: Univalence
z: Int
transport idmap (path_universe int_succ^-1) z =
int_pred z
    apply transport_path_universe.
  Defined.

  (** To turn a path in [Circle] based at [base] into a code we transport along it. We call this encoding. *)
  Definition Circle_encode (x:Circle) : (base = x) -> Circle_code x
    := fun p => p # zero.

  (** TODO: explain this proof in more detail. *)
  (** Turning a code into a path based at [base]. We call this decoding. *)
  Definition Circle_decode (x : Circle) : Circle_code x -> (base = x).
H: Univalence
x: Circle
Circle_code x -> base = x
  Proof.
H: Univalence
x: Circle
Circle_code x -> base = x
    revert x; refine (Circle_ind (fun x => Circle_code x -> base = x) (loopexp loop) _).
H: Univalence
transport
  (fun x : Circle => Circle_code x -> base = x) loop
  (loopexp loop) = loopexp loop
    apply path_forall; intros z; simpl in z.
H: Univalence
z: Int
transport
  (fun x : Circle => Circle_code x -> base = x) loop
  (loopexp loop) z = loopexp loop z
    refine (transport_arrow _ _ _ @ _).
H: Univalence
z: Int
transport (paths base) loop
  (loopexp loop (transport Circle_code loop^ z)) =
loopexp loop z
    refine (transport_paths_r loop _ @ _).
H: Univalence
z: Int
loopexp loop (transport Circle_code loop^ z) @ loop =
loopexp loop z
    rewrite transport_Circle_code_loopV.
H: Univalence
z: Int
loopexp loop (int_pred z) @ loop = loopexp loop z
    destruct z as [n| |n].
H: Univalence
n: Pos
loopexp loop (int_pred (neg n)) @ loop =
loopexp loop (neg n)
H: Univalence
loopexp loop (int_pred 0%int) @ loop =
loopexp loop 0%int
H: Univalence
n: Pos
loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
    2: apply concat_Vp.
H: Univalence
n: Pos
loopexp loop (int_pred (neg n)) @ loop =
loopexp loop (neg n)
H: Univalence
n: Pos
loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
    {
H: Univalence
n: Pos
loopexp loop (int_pred (neg n)) @ loop =
loopexp loop (neg n) rewrite <- int_neg_pos_succ.
H: Univalence
n: Pos
loopexp loop (neg (pos_succ n)) @ loop =
loopexp loop (neg n)
      unfold loopexp, loopexp_pos.
H: Univalence
n: Pos
pos_peano_ind (fun _ : Pos => base = base) loop^
  (fun (_ : Pos) (q : base = base) => q @ loop^)
  (pos_succ n) @ loop =
pos_peano_ind (fun _ : Pos => base = base) loop^
  (fun (_ : Pos) (q : base = base) => q @ loop^) n
      rewrite pos_peano_ind_beta_pos_succ.
H: Univalence
n: Pos
(pos_peano_ind (fun _ : Pos => base = base) loop^
   (fun (_ : Pos) (q : base = base) => q @ loop^) n @
 loop^) @ loop =
pos_peano_ind (fun _ : Pos => base = base) loop^
  (fun (_ : Pos) (q : base = base) => q @ loop^) n
      apply concat_pV_p. }
H: Univalence
n: Pos
loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
    induction n as [|n nH] using pos_peano_ind.
H: Univalence
loopexp loop (int_pred 1%int) @ loop =
loopexp loop 1%int
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp loop (int_pred (pos (pos_succ n))) @ loop =
loopexp loop (pos (pos_succ n))
    1: apply concat_1p.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp loop (int_pred (pos (pos_succ n))) @ loop =
loopexp loop (pos (pos_succ n))
    rewrite <- pos_add_1_r.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp loop (int_pred (pos (n + 1%pos))) @ loop =
loopexp loop (pos (n + 1%pos))
    change (pos (n + 1)%pos)
      with (int_succ (pos n)).
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp loop (int_pred (int_succ (pos n))) @ loop =
loopexp loop (int_succ (pos n))
    rewrite int_pred_succ.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp loop (pos n) @ loop =
loopexp loop (int_succ (pos n))
    cbn; rewrite pos_add_1_r.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
loopexp_pos loop n @ loop =
loopexp_pos loop (pos_succ n)
    unfold loopexp_pos.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
pos_peano_ind (fun _ : Pos => base = base) loop
  (fun (_ : Pos) (q : base = base) => q @ loop) n @
loop =
pos_peano_ind (fun _ : Pos => base = base) loop
  (fun (_ : Pos) (q : base = base) => q @ loop)
  (pos_succ n)
    rewrite pos_peano_ind_beta_pos_succ.
H: Univalence
n: Pos
nH: loopexp loop (int_pred (pos n)) @ loop =
loopexp loop (pos n)
pos_peano_ind (fun _ : Pos => base = base) loop
  (fun (_ : Pos) (q : base = base) => q @ loop) n @
loop =
pos_peano_ind (fun _ : Pos => base = base) loop
  (fun (_ : Pos) (q : base = base) => q @ loop) n @
loop
    reflexivity.
  Defined.

  (** The non-trivial part of the proof that decode and encode are equivalences is showing that decoding followed by encoding is the identity on the fibers over [base]. *)
  Definition Circle_encode_loopexp (z:Int)
    : Circle_encode base (loopexp loop z) = z.
H: Univalence
z: Int
Circle_encode base (loopexp loop z) = z
  Proof.
H: Univalence
z: Int
Circle_encode base (loopexp loop z) = z
    destruct z as [n | | n]; unfold Circle_encode.
H: Univalence
n: Pos
transport Circle_code (loopexp loop (neg n)) 0%int =
neg n
H: Univalence
transport Circle_code (loopexp loop 0%int) 0%int =
0%int
H: Univalence
n: Pos
transport Circle_code (loopexp loop (pos n)) 0%int =
pos n
    -
H: Univalence
n: Pos
transport Circle_code (loopexp loop (neg n)) 0%int =
neg n induction n using pos_peano_ind; simpl in *.
H: Univalence
transport Circle_code (loopexp_pos loop^ 1%pos) 0%int =
(-1)%int
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code (loopexp_pos loop^ (pos_succ n))
  0%int = neg (pos_succ n)
      +
H: Univalence
transport Circle_code (loopexp_pos loop^ 1%pos) 0%int =
(-1)%int refine (moveR_transport_V _ loop _ _ _).
H: Univalence
0%int = transport Circle_code loop (-1)%int
        by symmetry; apply transport_Circle_code_loop.
      +
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code (loopexp_pos loop^ (pos_succ n))
  0%int = neg (pos_succ n) unfold loopexp_pos.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop^
     (fun (_ : Pos) (q : base = base) => q @ loop^)
     (pos_succ n)) 0%int = neg (pos_succ n)
        rewrite pos_peano_ind_beta_pos_succ.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop^
     (fun (_ : Pos) (q : base = base) => q @ loop^) n @
   loop^) 0%int = neg (pos_succ n)
        rewrite transport_pp.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code loop^
  (transport Circle_code
     (pos_peano_ind (fun _ : Pos => base = base) loop^
        (fun (_ : Pos) (q : base = base) => q @ loop^)
        n) 0%int) = neg (pos_succ n)
        refine (moveR_transport_V _ loop _ _ _).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop^
     (fun (_ : Pos) (q : base = base) => q @ loop^) n)
  0%int =
transport Circle_code loop (neg (pos_succ n))
        refine (_ @ (transport_Circle_code_loop _)^).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop^
     (fun (_ : Pos) (q : base = base) => q @ loop^) n)
  0%int = int_succ (neg (pos_succ n))
        refine (IHn @ _^).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
int_succ (neg (pos_succ n)) = neg n
        rewrite int_neg_pos_succ.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop^ n) 0%int = neg n
int_succ (int_pred (neg n)) = neg n
        by rewrite int_succ_pred.
    -
H: Univalence
transport Circle_code (loopexp loop 0%int) 0%int =
0%int reflexivity.
    -
H: Univalence
n: Pos
transport Circle_code (loopexp loop (pos n)) 0%int =
pos n induction n using pos_peano_ind; simpl in *.
H: Univalence
transport Circle_code (loopexp_pos loop 1%pos) 0%int =
1%int
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code (loopexp_pos loop (pos_succ n))
  0%int = pos (pos_succ n)
      +
H: Univalence
transport Circle_code (loopexp_pos loop 1%pos) 0%int =
1%int by apply transport_Circle_code_loop.
      +
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code (loopexp_pos loop (pos_succ n))
  0%int = pos (pos_succ n) unfold loopexp_pos.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop
     (fun (_ : Pos) (q : base = base) => q @ loop)
     (pos_succ n)) 0%int = pos (pos_succ n)
        rewrite pos_peano_ind_beta_pos_succ.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop
     (fun (_ : Pos) (q : base = base) => q @ loop) n @
   loop) 0%int = pos (pos_succ n)
        rewrite transport_pp.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code loop
  (transport Circle_code
     (pos_peano_ind (fun _ : Pos => base = base) loop
        (fun (_ : Pos) (q : base = base) => q @ loop)
        n) 0%int) = pos (pos_succ n)
        refine (moveR_transport_p _ loop _ _ _).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop
     (fun (_ : Pos) (q : base = base) => q @ loop) n)
  0%int =
transport Circle_code loop^ (pos (pos_succ n))
        refine (_ @ (transport_Circle_code_loopV _)^).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
transport Circle_code
  (pos_peano_ind (fun _ : Pos => base = base) loop
     (fun (_ : Pos) (q : base = base) => q @ loop) n)
  0%int = int_pred (pos (pos_succ n))
        refine (IHn @ _^).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
int_pred (pos (pos_succ n)) = pos n
        rewrite <- pos_add_1_r.
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
int_pred (pos (n + 1%pos)) = pos n
        change (int_pred (int_succ (pos n)) = pos n).
H: Univalence
n: Pos
IHn: transport Circle_code (loopexp_pos loop n) 0%int = pos n
int_pred (int_succ (pos n)) = pos n
        apply int_pred_succ.
  Defined.

  (** Now we put it together. *)
  Definition Circle_encode_isequiv (x:Circle) : IsEquiv (Circle_encode x).
H: Univalence
x: Circle
IsEquiv (Circle_encode x)
  Proof.
H: Univalence
x: Circle
IsEquiv (Circle_encode x)
   refine (isequiv_adjointify (Circle_encode x) (Circle_decode x) _ _).
H: Univalence
x: Circle
(fun x0 : Circle_code x =>
 Circle_encode x (Circle_decode x x0)) == idmap
H: Univalence
x: Circle
(fun x0 : base = x =>
 Circle_decode x (Circle_encode x x0)) == idmap
    (* Here we induct on [x:Circle].  We just did the case when [x] is [base]. *)
    -
H: Univalence
x: Circle
(fun x0 : Circle_code x =>
 Circle_encode x (Circle_decode x x0)) == idmap refine (Circle_ind (fun x => (Circle_encode x) o (Circle_decode x) == idmap)
        Circle_encode_loopexp _ _).
H: Univalence
x: Circle
transport
  (fun x : Circle =>
   (fun x0 : Circle_code x =>
    Circle_encode x (Circle_decode x x0)) == idmap)
  loop Circle_encode_loopexp = Circle_encode_loopexp
      (* What remains is easy since [Int] is known to be a set. *)
      by apply path_forall; intros z; apply hset_path2.
    (* The other side is trivial by path induction. *)
    -
H: Univalence
x: Circle
(fun x0 : base = x =>
 Circle_decode x (Circle_encode x x0)) == idmap intros []; reflexivity.
  Defined.

  (** Finally giving us an equivalence between the loop space of the [Circle] and [Int]. *)
  Definition equiv_loopCircle_int : (base = base) <~> Int
    := Build_Equiv _ _ (Circle_encode base) (Circle_encode_isequiv base).

End EncodeDecode.

(** ** Connectedness and truncatedness of the [Circle] *)

(** The circle is 0-connected. *)
Global Instance isconnected_Circle `{Univalence} : IsConnected 0 Circle.
H: Univalence
IsConnected (Tr 0) Circle
Proof.
H: Univalence
IsConnected (Tr 0) Circle
  apply is0connected_merely_allpath.
H: Univalence
merely Circle
H: Univalence
forall x y : Circle, merely (x = y)
  1: exact (tr base).
H: Univalence
forall x y : Circle, merely (x = y)
  srefine (Circle_ind _ _ _).
H: Univalence
(fun x : Circle => forall y : Circle, merely (x = y))
  base
H: Univalence
transport
  (fun x : Circle => forall y : Circle, merely (x = y))
  loop ?b = ?b
  -
H: Univalence
(fun x : Circle => forall y : Circle, merely (x = y))
  base simple refine (Circle_ind _ _ _).
H: Univalence
(fun x : Circle => trunctype_type (merely (base = x)))
  base
H: Univalence
transport (fun x : Circle => merely (base = x)) loop
  ?b = ?b
    +
H: Univalence
(fun x : Circle => trunctype_type (merely (base = x)))
  base exact (tr 1).
    +
H: Univalence
transport (fun x : Circle => merely (base = x)) loop
  (tr 1) = tr 1 apply path_ishprop.
  -
H: Univalence
transport
  (fun x : Circle => forall y : Circle, merely (x = y))
  loop
  (Circle_ind (fun x : Circle => merely (base = x))
     (tr 1)
     (path_ishprop
        (transport
           (fun x : Circle => merely (base = x)) loop
           (tr 1)) (tr 1))) =
Circle_ind (fun x : Circle => merely (base = x))
  (tr 1)
  (path_ishprop
     (transport (fun x : Circle => merely (base = x))
        loop (tr 1)) (tr 1)) apply path_ishprop.
Defined.

(** It follows that the circle is a 1-type. *)
Global Instance istrunc_Circle `{Univalence} : IsTrunc 1 Circle.
H: Univalence
IsTrunc 1 Circle
Proof.
H: Univalence
IsTrunc 1 Circle
  apply istrunc_S.
H: Univalence
forall x y : Circle, IsHSet (x = y)
  intros x y.
H: Univalence
x, y: Circle
IsHSet (x = y)
  assert (p := merely_path_is0connected Circle base x).
H: Univalence
x, y: Circle
p: merely (base = x)
IsHSet (x = y)
  assert (q := merely_path_is0connected Circle base y).
H: Univalence
x, y: Circle
p: merely (base = x)
q: merely (base = y)
IsHSet (x = y)
  strip_truncations.
H: Univalence
x, y: Circle
q: base = y
p: base = x
IsHSet (x = y)
  destruct p, q.
H: Univalence
IsHSet (base = base)
  refine (istrunc_equiv_istrunc (n := 0) Int equiv_loopCircle_int^-1).
Defined.

(** ** Iteration of equivalences *)

(** If [P : Circle -> Type] is defined by a type [X] and an autoequivalence [f], then the image of [n : Int] regarded as in [base = base] is [iter_int f n]. *)
Definition Circle_action_is_iter `{Univalence} X (f : X <~> X) (n : Int) (x : X)
: transport (Circle_rec Type X (path_universe f)) (equiv_loopCircle_int^-1 n) x
  = int_iter f n x.
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
transport (Circle_rec Type X (path_universe f))
  (equiv_loopCircle_int^-1 n) x = int_iter f n x
Proof.
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
transport (Circle_rec Type X (path_universe f))
  (equiv_loopCircle_int^-1 n) x = int_iter f n x
  refine (_ @ loopexp_path_universe _ _ _).
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
transport (Circle_rec Type X (path_universe f))
  (equiv_loopCircle_int^-1 n) x =
transport idmap (loopexp (path_universe f) n) x
  refine (transport_compose idmap _ _ _ @ _).
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
transport idmap
  (ap (Circle_rec Type X (path_universe f))
     (equiv_loopCircle_int^-1 n)) x =
transport idmap (loopexp (path_universe f) n) x
  refine (ap (fun p => transport idmap p x) _).
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
ap (Circle_rec Type X (path_universe f))
  (equiv_loopCircle_int^-1 n) =
loopexp (path_universe f) n
  unfold equiv_loopCircle_int; cbn.
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
ap (Circle_rec Type X (path_universe f))
  (Circle_decode base n) = loopexp (path_universe f) n
  unfold Circle_decode; simpl.
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
ap (Circle_rec Type X (path_universe f))
  (loopexp loop n) = loopexp (path_universe f) n
  rewrite ap_loopexp.
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
loopexp
  (ap (Circle_rec Type X (path_universe f)) loop) n =
loopexp (path_universe f) n
  refine (ap (fun p => loopexp p n) _).
H: Univalence
X: Type
f: X <~> X
n: Int
x: X
ap (Circle_rec Type X (path_universe f)) loop =
path_universe f
  apply Circle_rec_beta_loop.
Defined.

(** The universal property of the circle (Lemma 6.2.9 in the Book).  We could deduce this from [isequiv_Coeq_rec], but it's nice to see a direct proof too. *)
Definition Circle_rec_uncurried (P : Type)
  : {b : P & b = b} -> (Circle -> P)
  := fun x => Circle_rec P (pr1 x) (pr2 x).

Global Instance isequiv_Circle_rec_uncurried `{Funext} (P : Type) : IsEquiv (Circle_rec_uncurried P).
H: Funext
P: Type
IsEquiv (Circle_rec_uncurried P)
Proof.
H: Funext
P: Type
IsEquiv (Circle_rec_uncurried P)
  srapply isequiv_adjointify.
H: Funext
P: Type
(Circle -> P) -> {b : P & b = b}
H: Funext
P: Type
Circle_rec_uncurried P o ?g == idmap
H: Funext
P: Type
?g o Circle_rec_uncurried P == idmap
  -
H: Funext
P: Type
(Circle -> P) -> {b : P & b = b} exact (fun g => (g base ; ap g loop)).
  -
H: Funext
P: Type
Circle_rec_uncurried P
o (fun g : Circle -> P => (g base; ap g loop)) ==
idmap intros g.
H: Funext
P: Type
g: Circle -> P
Circle_rec_uncurried P (g base; ap g loop) = g
    apply path_arrow.
H: Funext
P: Type
g: Circle -> P
Circle_rec_uncurried P (g base; ap g loop) == g
    srapply Circle_ind.
H: Funext
P: Type
g: Circle -> P
(fun x : Circle =>
 Circle_rec_uncurried P (g base; ap g loop) x = g x)
  base
H: Funext
P: Type
g: Circle -> P
transport
  (fun x : Circle =>
   Circle_rec_uncurried P (g base; ap g loop) x = g x)
  loop ?b = ?b
    +
H: Funext
P: Type
g: Circle -> P
(fun x : Circle =>
 Circle_rec_uncurried P (g base; ap g loop) x = g x)
  base reflexivity.
    +
H: Funext
P: Type
g: Circle -> P
transport
  (fun x : Circle =>
   Circle_rec_uncurried P (g base; ap g loop) x = g x)
  loop 1 = 1 unfold Circle_rec_uncurried; cbn.
H: Funext
P: Type
g: Circle -> P
transport
  (fun x : Circle =>
   Circle_rec P (g base) (ap g loop) x = g x) loop 1 =
1
      apply transport_paths_FlFr'.
H: Funext
P: Type
g: Circle -> P
ap (Circle_rec P (g base) (ap g loop)) loop @ 1 =
1 @ ap g loop
      apply equiv_p1_1q.
H: Funext
P: Type
g: Circle -> P
ap (Circle_rec P (g base) (ap g loop)) loop =
ap g loop
      apply Circle_rec_beta_loop.
  -
H: Funext
P: Type
(fun g : Circle -> P => (g base; ap g loop))
o Circle_rec_uncurried P == idmap intros [b p]; apply ap.
H: Funext
P: Type
b: P
p: b = b
ap (Circle_rec_uncurried P (b; p)) loop = p
    apply Circle_rec_beta_loop.
Defined.

Definition equiv_Circle_rec `{Funext} (P : Type)
  : {b : P & b = b} <~> (Circle -> P)
  := Build_Equiv _ _ _ (isequiv_Circle_rec_uncurried P).

(** A pointed version of the universal property of the circle. *)
Definition pmap_from_circle_loops `{Funext} (X : pType)
  : (pCircle ->** X) <~>* loops X.
H: Funext
X: pType
(pCircle ->** X) <~>* loops X
Proof.
H: Funext
X: pType
(pCircle ->** X) <~>* loops X
  snrapply Build_pEquiv'.
H: Funext
X: pType
(pCircle ->** X) <~> loops X
H: Funext
X: pType
?f pt = pt
  -
H: Funext
X: pType
(pCircle ->** X) <~> loops X refine (_ oE (issig_pmap _ _)^-1%equiv).
H: Funext
X: pType
{f : pCircle -> X & f pt = pt} <~> loops X
    equiv_via { xp : { x : X & x = x } & xp.1 = pt }.
H: Funext
X: pType
{f : pCircle -> X & f pt = pt} <~>
{xp : {x : X & x = x} & xp.1 = pt}
H: Funext
X: pType
{xp : {x : X & x = x} & xp.1 = pt} <~> loops X
    2: make_equiv_contr_basedpaths.
H: Funext
X: pType
{f : pCircle -> X & f pt = pt} <~>
{xp : {x : X & x = x} & xp.1 = pt}
    exact ((equiv_functor_sigma_pb (equiv_Circle_rec X)^-1%equiv)).
  -
H: Funext
X: pType
(equiv_composeR'
   (equiv_functor_sigma_pb (equiv_Circle_rec X)^-1)
   (equiv_adjointify
      (fun H0 : {xp : {x : X & x = x} & xp.1 = pt} =>
       (fun H1 : {x : X & x = x} =>
        (fun (H2 : X) (H3 : H2 = H2)
           (H4 : (H2; H3).1 = pt) =>
         paths_ind_r pt
           (fun (y : X) (_ : y = pt) =>
            y = y -> loops X)
           (fun H5 : pt = pt => H5 : loops X) H2 H4 H3)
          H1.1 H1.2) H0.1 H0.2)
      (fun H0 : loops X =>
       ((let H1 := pt in H1;
        H0
        :
        (let H1 := pt in H1) = (let H1 := pt in H1))
        :
        {x : X & x = x};
       1%path
       :
       ((let H1 := pt in H1;
        H0
        :
        (let H1 := pt in H1) = (let H1 := pt in H1))
        :
        {x : X & x = x}).1 = pt)
       :
       {xp : {x : X & x = x} & xp.1 = pt})
      ((fun H0 : loops X => 1%path)
       :
       (fun H0 : {xp : {x : X & x = x} & xp.1 = pt} =>
        (fun H1 : {x : X & x = x} =>
         (fun (H2 : X) (H3 : H2 = H2)
            (H4 : (H2; H3).1 = pt) =>
          paths_ind_r pt
            (fun (y : X) (_ : y = pt) =>
             y = y -> loops X)
            (fun H5 : pt = pt => H5 : loops X) H2 H4
            H3) H1.1 H1.2) H0.1 H0.2)
       o (fun H0 : loops X =>
          ((let H1 := pt in H1;
           H0
           :
           (let H1 := pt in H1) = (let H1 := pt in H1))
           :
           {x : X & x = x};
          1%path
          :
          ((let H1 := pt in H1;
           H0
           :
           (let H1 := pt in H1) = (let H1 := pt in H1))
           :
           {x : X & x = x}).1 = pt)
          :
          {xp : {x : X & x = x} & xp.1 = pt}) == idmap)
      ((fun H0 : {xp : {x : X & x = x} & xp.1 = pt} =>
        (fun H1 : {x : X & x = x} =>
         (fun (H2 : X) (H3 : H2 = H2)
            (H4 : (H2; H3).1 = pt) =>
          paths_ind_r pt
            (fun (y : X) (p : y = pt) =>
             forall H5 : y = y,
             ((let H6 := pt in H6;
              paths_ind_r pt (... => ...) idmap y p H5);
             1%path) = ((y; H5); p))
            (fun H5 : pt = pt => 1%path) H2 H4 H3)
           H1.1 H1.2) H0.1 H0.2)
       :
       (fun H0 : loops X =>
        ((let H1 := pt in H1;
         H0
         :
         (let H1 := pt in H1) = (let H1 := pt in H1))
         :
         {x : X & x = x};
        1%path
        :
        ((let H1 := pt in H1;
         H0
         :
         (let H1 := pt in H1) = (let H1 := pt in H1))
         :
         {x : X & x = x}).1 = pt)
        :
        {xp : {x : X & x = x} & xp.1 = pt})
       o (fun H0 : {xp : {x : X & x = x} & xp.1 = pt}
          =>
          (fun H1 : {x : X & x = x} =>
           (fun (H2 : X) (H3 : H2 = H2)
              (H4 : (H2; H3).1 = pt) =>
            paths_ind_r pt
              (fun (y : X) (_ : y = pt) =>
               y = y -> loops X)
              (fun H5 : pt = pt => H5 : loops X) H2 H4
              H3) H1.1 H1.2) H0.1 H0.2) == idmap))
 oE (issig_pmap pCircle X)^-1) pt = pt simpl.
H: Funext
X: pType
ap (fun _ : Circle => pt) loop = pt  apply ap_const.
Defined.