From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.Universe.
Require Import Spaces.Pos.
Require Import Spaces.BinInt.Core.
Require Import Spaces.BinInt.Spec.
Require Import Spaces.BinInt.Equiv.

Local Open Scope positive_scope.
Local Open Scope binint_scope.

(** ** Exponentiation of loops *)

Definition loopexp_pos {A : Type} {x : A} (p : x = x) (n : Pos) : (x = x).
A: Type
x: A
p: x = x
n: Pos
x = x
Proof.
A: Type
x: A
p: x = x
n: Pos
x = x
  revert n.
A: Type
x: A
p: x = x
Pos -> x = x
  srapply pos_peano_ind.
A: Type
x: A
p: x = x
(fun _ : Pos => x = x) 1%pos
A: Type
x: A
p: x = x
forall p0 : Pos,
(fun _ : Pos => x = x) p0 -> (fun _ : Pos => x = x) (pos_succ p0)
  +
A: Type
x: A
p: x = x
(fun _ : Pos => x = x) 1%pos exact p.
  +
A: Type
x: A
p: x = x
forall p0 : Pos,
(fun _ : Pos => x = x) p0 -> (fun _ : Pos => x = x) (pos_succ p0) intros n q.
A: Type
x: A
p: x = x
n: Pos
q: (fun _ : Pos => x = x) n
(fun _ : Pos => x = x) (pos_succ n)
    exact (q @ p).
Defined.

Definition loopexp {A : Type} {x : A} (p : x = x) (z : BinInt) : (x = x)
  := match z with
       | neg n => loopexp_pos p^ n
       | zero => 1
       | pos n => loopexp_pos p n
     end.

(** TODO: One can also define [loopexp] as [int_iter (equiv_concat_r p x) z idpath].  This has slightly different computational behaviour, e.g., it sends [1 : int] to [1 @ p] rather than [p].  But with this definition, some of the results below become special cases of results in BinInt.Equiv, and others could be generalized to results belonging in BinInt.Equiv.  It's probably worth investigating this. *)

Lemma loopexp_pos_inv {A : Type} {x : A} (p : x = x) (n : Pos)
  : loopexp_pos p^ n = (loopexp_pos p n)^.
A: Type
x: A
p: x = x
n: Pos
loopexp_pos p^ n = (loopexp_pos p n)^
Proof.
A: Type
x: A
p: x = x
n: Pos
loopexp_pos p^ n = (loopexp_pos p n)^
  revert n.
A: Type
x: A
p: x = x
forall n : Pos, loopexp_pos p^ n = (loopexp_pos p n)^
  srapply pos_peano_ind; cbn; trivial.
A: Type
x: A
p: x = x
forall p0 : Pos,
loopexp_pos p^ p0 = (loopexp_pos p p0)^ ->
loopexp_pos p^ (pos_succ p0) = (loopexp_pos p (pos_succ p0))^
  unfold loopexp_pos.
A: Type
x: A
p: x = x
forall p0 : Pos,
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  p0 =
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   p0)^ ->
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  (pos_succ p0) =
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   (pos_succ p0))^
  intros n q.
A: Type
x: A
p: x = x
n: Pos
q: pos_peano_ind (fun _ : Pos => x = x) p^
  (fun (_ : Pos) (q0 : x = x) => q0 @ p^) n =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^
pos_peano_ind (fun _ : Pos => x = x) p^
  (fun (_ : Pos) (q0 : x = x) => q0 @ p^) (pos_succ n) =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) (pos_succ n))^
  rewrite 2 pos_peano_ind_beta_pos_succ, q.
A: Type
x: A
p: x = x
n: Pos
q: pos_peano_ind (fun _ : Pos => x = x) p^
  (fun (_ : Pos) (q0 : x = x) => q0 @ p^) n =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^ @
p^ =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n @
 p)^
  refine ((inv_pp _ _)^ @ _).
A: Type
x: A
p: x = x
n: Pos
q: pos_peano_ind (fun _ : Pos => x = x) p^
  (fun (_ : Pos) (q0 : x = x) => q0 @ p^) n =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^
(p @
 pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^ =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n @
 p)^
  apply ap.
A: Type
x: A
p: x = x
n: Pos
q: pos_peano_ind (fun _ : Pos => x = x) p^
  (fun (_ : Pos) (q0 : x = x) => q0 @ p^) n =
(pos_peano_ind (fun _ : Pos => x = x) p
   (fun (_ : Pos) (q0 : x = x) => q0 @ p) n)^
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  n =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  n @
p
  clear q.
A: Type
x: A
p: x = x
n: Pos
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) n =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) n @
p
  revert n.
A: Type
x: A
p: x = x
forall n : Pos,
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) n =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) n @
p
  srapply pos_peano_ind; cbn; trivial.
A: Type
x: A
p: x = x
forall p0 : Pos,
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  p0 =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  p0 @
p ->
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ p0) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ p0) @
p
  intros n q.
A: Type
x: A
p: x = x
n: Pos
q: p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  n =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  n @
p
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  (pos_succ n) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q0 : x = x) => q0 @ p)
  (pos_succ n) @
p
  by rewrite pos_peano_ind_beta_pos_succ, concat_p_pp, q.
Qed.

Definition ap_loopexp_pos {A B} (f : A -> B) {x : A} (p : x = x) (n : Pos)
  : ap f (loopexp_pos p n) = loopexp_pos (ap f p) n.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp_pos p n) = loopexp_pos (ap f p) n
Proof.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp_pos p n) = loopexp_pos (ap f p) n
  revert n.
A, B: Type
f: A -> B
x: A
p: x = x
forall n : Pos, ap f (loopexp_pos p n) = loopexp_pos (ap f p) n
  srapply pos_peano_ind; cbn; trivial.
A, B: Type
f: A -> B
x: A
p: x = x
forall p0 : Pos,
ap f (loopexp_pos p p0) = loopexp_pos (ap f p) p0 ->
ap f (loopexp_pos p (pos_succ p0)) = loopexp_pos (ap f p) (pos_succ p0)
  unfold loopexp_pos.
A, B: Type
f: A -> B
x: A
p: x = x
forall p0 : Pos,
ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q : x = x) => q @ p) p0) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q : f x = f x) => q @ ap f p) p0 ->
ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q : x = x) => q @ p) (pos_succ p0)) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q : f x = f x) => q @ ap f p) (pos_succ p0)
  intros n q.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
q: ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q0 : x = x) => q0 @ p) n) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q0 : f x = f x) => q0 @ ap f p) n
ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q0 : x = x) => q0 @ p) (pos_succ n)) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q0 : f x = f x) => q0 @ ap f p) 
  (pos_succ n)
  rewrite 2 pos_peano_ind_beta_pos_succ.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
q: ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q0 : x = x) => q0 @ p) n) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q0 : f x = f x) => q0 @ ap f p) n
ap f
  (pos_peano_ind (fun _ : Pos => x = x) p
     (fun (_ : Pos) (q0 : x = x) => q0 @ p) n @
   p) =
pos_peano_ind (fun _ : Pos => f x = f x) (ap f p)
  (fun (_ : Pos) (q0 : f x = f x) => q0 @ ap f p) n @
ap f p
  by rewrite ap_pp, q.
Qed.

Definition ap_loopexp {A B} (f : A -> B) {x : A} (p : x = x) (z : BinInt)
: ap f (loopexp p z) = loopexp (ap f p) z.
A, B: Type
f: A -> B
x: A
p: x = x
z: BinInt
ap f (loopexp p z) = loopexp (ap f p) z
Proof.
A, B: Type
f: A -> B
x: A
p: x = x
z: BinInt
ap f (loopexp p z) = loopexp (ap f p) z
  destruct z as [n| |n]; trivial.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp p (neg n)) = loopexp (ap f p) (neg n)
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp p (pos n)) = loopexp (ap f p) (pos n)
  +
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp p (neg n)) = loopexp (ap f p) (neg n) cbn.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp_pos p^ n) = loopexp_pos (ap f p)^ n
    rewrite loopexp_pos_inv, ap_V, loopexp_pos_inv.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
(ap f (loopexp_pos p n))^ = (loopexp_pos (ap f p) n)^
    apply ap.
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp_pos p n) = loopexp_pos (ap f p) n
    apply ap_loopexp_pos.
  +
A, B: Type
f: A -> B
x: A
p: x = x
n: Pos
ap f (loopexp p (pos n)) = loopexp (ap f p) (pos n) apply ap_loopexp_pos.
Qed.

Lemma loopexp_pos_concat {A : Type} {x : A} (p : x = x) (a : Pos)
  : loopexp_pos p a @ p = p @ loopexp_pos p a.
A: Type
x: A
p: x = x
a: Pos
loopexp_pos p a @ p = p @ loopexp_pos p a
Proof.
A: Type
x: A
p: x = x
a: Pos
loopexp_pos p a @ p = p @ loopexp_pos p a
  induction a as [|a aH] using pos_peano_ind; trivial.
A: Type
x: A
p: x = x
a: Pos
aH: loopexp_pos p a @ p = p @ loopexp_pos p a
loopexp_pos p (pos_succ a) @ p = p @ loopexp_pos p (pos_succ a)
  unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: loopexp_pos p a @ p = p @ loopexp_pos p a
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) @
p =
p @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a)
  rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: loopexp_pos p a @ p = p @ loopexp_pos p a
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) @
p =
p @
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p)
  change ((loopexp_pos p a @ p) @ p = p @ (loopexp_pos p a @ p)).
A: Type
x: A
p: x = x
a: Pos
aH: loopexp_pos p a @ p = p @ loopexp_pos p a
(loopexp_pos p a @ p) @ p = p @ (loopexp_pos p a @ p)
  by rewrite concat_p_pp, aH.
Qed.

Lemma loopexp_pos_add {A : Type} {x : A} (p : x = x) (a b : Pos)
  : loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b.
A: Type
x: A
p: x = x
a, b: Pos
loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
Proof.
A: Type
x: A
p: x = x
a, b: Pos
loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
  revert a b.
A: Type
x: A
p: x = x
forall a b : Pos,
loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
  induction a as [|a aH] using pos_peano_ind;
  induction b as [|b bH] using pos_peano_ind;
  trivial.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (1 + b)%pos = loopexp_pos p 1%pos @ loopexp_pos p b
loopexp_pos p (1 + pos_succ b)%pos =
loopexp_pos p 1%pos @ loopexp_pos p (pos_succ b)
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos, loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
loopexp_pos p (pos_succ a + 1)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p 1%pos
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
loopexp_pos p (pos_succ a + pos_succ b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p (pos_succ b)
  +
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (1 + b)%pos = loopexp_pos p 1%pos @ loopexp_pos p b
loopexp_pos p (1 + pos_succ b)%pos =
loopexp_pos p 1%pos @ loopexp_pos p (pos_succ b) rewrite pos_add_1_l in *.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (pos_succ b) = loopexp_pos p 1%pos @ loopexp_pos p b
loopexp_pos p (pos_succ (pos_succ b)) =
loopexp_pos p 1%pos @ loopexp_pos p (pos_succ b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (pos_succ b) = loopexp_pos p 1%pos @ loopexp_pos p b
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ (pos_succ b)) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  1%pos @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ b)
    rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (pos_succ b) = loopexp_pos p 1%pos @ loopexp_pos p b
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ b) @
p =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  1%pos @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ b)
    change (loopexp_pos p (pos_succ b) @ p
      = p @ loopexp_pos p (pos_succ b)).
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (pos_succ b) = loopexp_pos p 1%pos @ loopexp_pos p b
loopexp_pos p (pos_succ b) @ p = p @ loopexp_pos p (pos_succ b)
    rewrite bH; cbn.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p (pos_succ b) = loopexp_pos p 1%pos @ loopexp_pos p b
(p @ loopexp_pos p b) @ p = p @ (p @ loopexp_pos p b)
    by rewrite concat_pp_p, loopexp_pos_concat.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos, loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
loopexp_pos p (pos_succ a + 1)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p 1%pos rewrite pos_add_1_r in *.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos, loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
loopexp_pos p (pos_succ (pos_succ a)) =
loopexp_pos p (pos_succ a) @ loopexp_pos p 1%pos
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos, loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ (pos_succ a)) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  1%pos
    by rewrite pos_peano_ind_beta_pos_succ.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
loopexp_pos p (pos_succ a + pos_succ b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p (pos_succ b) rewrite pos_add_succ_l.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
loopexp_pos p (pos_succ (a + pos_succ b)%pos) =
loopexp_pos p (pos_succ a) @ loopexp_pos p (pos_succ b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ (a + pos_succ b)%pos) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ b)
    rewrite 2 pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (a + pos_succ b)%pos @
p =
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ b)
    change (loopexp_pos p (a + pos_succ b)%pos @ p
      = (loopexp_pos p a @ p) @ loopexp_pos p (pos_succ b)).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p (a + b0)%pos = loopexp_pos p a @ loopexp_pos p b0
b: Pos
bH: loopexp_pos p (pos_succ a + b)%pos =
loopexp_pos p (pos_succ a) @ loopexp_pos p b
loopexp_pos p (a + pos_succ b)%pos @ p =
(loopexp_pos p a @ p) @ loopexp_pos p (pos_succ b)
    by rewrite aH, 2 concat_pp_p, loopexp_pos_concat.
Qed.


Lemma loopexp_binint_pos_sub_l {A : Type} {x : A} (p : x = x) (a b : Pos)
  : loopexp p (binint_pos_sub a b) = loopexp_pos p^ b @ loopexp_pos p a.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p^ b @ loopexp_pos p a
Proof.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p^ b @ loopexp_pos p a
  symmetry.
A: Type
x: A
p: x = x
a, b: Pos
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
  revert a b.
A: Type
x: A
p: x = x
forall a b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
  induction a as [|a aH] using pos_peano_ind;
  induction b as [|b bH] using pos_peano_ind.
A: Type
x: A
p: x = x
loopexp_pos p^ 1%pos @ loopexp_pos p 1%pos =
loopexp p (binint_pos_sub 1%pos 1%pos)
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p 1%pos = loopexp p (binint_pos_sub 1%pos b)
loopexp_pos p^ (pos_succ b) @ loopexp_pos p 1%pos =
loopexp p (binint_pos_sub 1%pos (pos_succ b))
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
loopexp_pos p^ 1%pos @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) 1%pos)
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p^ (pos_succ b) @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) (pos_succ b))
  +
A: Type
x: A
p: x = x
loopexp_pos p^ 1%pos @ loopexp_pos p 1%pos =
loopexp p (binint_pos_sub 1%pos 1%pos) apply concat_Vp.
  +
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p 1%pos = loopexp p (binint_pos_sub 1%pos b)
loopexp_pos p^ (pos_succ b) @ loopexp_pos p 1%pos =
loopexp p (binint_pos_sub 1%pos (pos_succ b)) cbn; rewrite binint_pos_sub_succ_r.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p 1%pos = loopexp p (binint_pos_sub 1%pos b)
loopexp_pos p^ (pos_succ b) @ p = loopexp p (neg b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p 1%pos = loopexp p (binint_pos_sub 1%pos b)
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  (pos_succ b) @
p = loopexp p (neg b)
    rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p 1%pos = loopexp p (binint_pos_sub 1%pos b)
(pos_peano_ind (fun _ : Pos => x = x) p^
   (fun (_ : Pos) (q : x = x) => q @ p^) b @
 p^) @
p = loopexp p (neg b)
    by rewrite concat_pp_p, concat_Vp, concat_p1.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
loopexp_pos p^ 1%pos @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) 1%pos) rewrite binint_pos_sub_succ_l; cbn.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
p^ @ loopexp_pos p (pos_succ a) = loopexp_pos p a
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
p^ @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) a
    rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
p^ @
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) a
    rewrite loopexp_pos_concat.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
p^ @ (p @ loopexp_pos p a) =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) a
    by rewrite concat_p_pp, concat_Vp, concat_1p.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p^ (pos_succ b) @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) (pos_succ b)) rewrite binint_pos_sub_succ_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p^ (pos_succ b) @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub a b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  (pos_succ b) @
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) =
loopexp p (binint_pos_sub a b)
    rewrite 2 pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
(pos_peano_ind (fun _ : Pos => x = x) p^
   (fun (_ : Pos) (q : x = x) => q @ p^) b @
 p^) @
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) =
loopexp p (binint_pos_sub a b)
    change ((loopexp_pos p^ b @ p^) @ (loopexp_pos p a @ p)
      = loopexp p (binint_pos_sub a b)).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
(loopexp_pos p^ b @ p^) @ (loopexp_pos p a @ p) =
loopexp p (binint_pos_sub a b)
    rewrite (loopexp_pos_concat p).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
(loopexp_pos p^ b @ p^) @ (p @ loopexp_pos p a) =
loopexp p (binint_pos_sub a b)
    rewrite concat_pp_p, (concat_p_pp p^ p).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p^ b @ ((p^ @ p) @ loopexp_pos p a) =
loopexp p (binint_pos_sub a b)
    rewrite concat_Vp, concat_1p.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p^ b0 @ loopexp_pos p a = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p^ b @ loopexp_pos p (pos_succ a) =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p^ b @ loopexp_pos p a = loopexp p (binint_pos_sub a b)
    apply aH.
Qed.

Lemma loopexp_binint_pos_sub_r {A : Type} {x : A} (p : x = x) (a b : Pos)
  : loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
Proof.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
  symmetry.
A: Type
x: A
p: x = x
a, b: Pos
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
  revert a b.
A: Type
x: A
p: x = x
forall a b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
  induction a as [|a aH] using pos_peano_ind;
  induction b as [|b bH] using pos_peano_ind.
A: Type
x: A
p: x = x
loopexp_pos p 1%pos @ loopexp_pos p^ 1%pos =
loopexp p (binint_pos_sub 1%pos 1%pos)
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
loopexp_pos p 1%pos @ loopexp_pos p^ (pos_succ b) =
loopexp p (binint_pos_sub 1%pos (pos_succ b))
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
loopexp_pos p (pos_succ a) @ loopexp_pos p^ 1%pos =
loopexp p (binint_pos_sub (pos_succ a) 1%pos)
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p (pos_succ a) @ loopexp_pos p^ (pos_succ b) =
loopexp p (binint_pos_sub (pos_succ a) (pos_succ b))
  +
A: Type
x: A
p: x = x
loopexp_pos p 1%pos @ loopexp_pos p^ 1%pos =
loopexp p (binint_pos_sub 1%pos 1%pos) apply concat_pV.
  +
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
loopexp_pos p 1%pos @ loopexp_pos p^ (pos_succ b) =
loopexp p (binint_pos_sub 1%pos (pos_succ b)) cbn; rewrite binint_pos_sub_succ_r.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
p @ loopexp_pos p^ (pos_succ b) = loopexp p (neg b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
p @
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  (pos_succ b) =
loopexp p (neg b)
    rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
p @
(pos_peano_ind (fun _ : Pos => x = x) p^
   (fun (_ : Pos) (q : x = x) => q @ p^) b @
 p^) =
loopexp p (neg b)
    change (p @ (loopexp_pos p^ b @ p^) = loopexp p (neg b)).
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
p @ (loopexp_pos p^ b @ p^) = loopexp p (neg b)
    rewrite loopexp_pos_concat.
A: Type
x: A
p: x = x
b: Pos
bH: loopexp_pos p 1%pos @ loopexp_pos p^ b = loopexp p (binint_pos_sub 1%pos b)
p @ (p^ @ loopexp_pos p^ b) = loopexp p (neg b)
    by rewrite concat_p_pp, concat_pV, concat_1p.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
loopexp_pos p (pos_succ a) @ loopexp_pos p^ 1%pos =
loopexp p (binint_pos_sub (pos_succ a) 1%pos) rewrite binint_pos_sub_succ_l; cbn.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
loopexp_pos p (pos_succ a) @ p^ = loopexp_pos p a
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) @
p^ =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) a
    rewrite pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) @
p^ =
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p) a
    change ((loopexp_pos p a @ p) @ p^ = loopexp_pos p a).
A: Type
x: A
p: x = x
a: Pos
aH: forall b : Pos,
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
(loopexp_pos p a @ p) @ p^ = loopexp_pos p a
    by rewrite concat_pp_p, concat_pV, concat_p1.
  +
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p (pos_succ a) @ loopexp_pos p^ (pos_succ b) =
loopexp p (binint_pos_sub (pos_succ a) (pos_succ b)) rewrite binint_pos_sub_succ_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p (pos_succ a) @ loopexp_pos p^ (pos_succ b) =
loopexp p (binint_pos_sub a b)
    unfold loopexp_pos.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
  (pos_succ a) @
pos_peano_ind (fun _ : Pos => x = x) p^ (fun (_ : Pos) (q : x = x) => q @ p^)
  (pos_succ b) =
loopexp p (binint_pos_sub a b)
    rewrite 2 pos_peano_ind_beta_pos_succ.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
(pos_peano_ind (fun _ : Pos => x = x) p (fun (_ : Pos) (q : x = x) => q @ p)
   a @
 p) @
(pos_peano_ind (fun _ : Pos => x = x) p^
   (fun (_ : Pos) (q : x = x) => q @ p^) b @
 p^) =
loopexp p (binint_pos_sub a b)
    change ((loopexp_pos p a @ p) @ (loopexp_pos p^ b @ p^)
      = loopexp p (binint_pos_sub a b)).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
(loopexp_pos p a @ p) @ (loopexp_pos p^ b @ p^) =
loopexp p (binint_pos_sub a b)
    rewrite (loopexp_pos_concat p^).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
(loopexp_pos p a @ p) @ (p^ @ loopexp_pos p^ b) =
loopexp p (binint_pos_sub a b)
    rewrite concat_pp_p, (concat_p_pp p p^).
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p a @ ((p @ p^) @ loopexp_pos p^ b) =
loopexp p (binint_pos_sub a b)
    rewrite concat_pV, concat_1p.
A: Type
x: A
p: x = x
a: Pos
aH: forall b0 : Pos,
loopexp_pos p a @ loopexp_pos p^ b0 = loopexp p (binint_pos_sub a b0)
b: Pos
bH: loopexp_pos p (pos_succ a) @ loopexp_pos p^ b =
loopexp p (binint_pos_sub (pos_succ a) b)
loopexp_pos p a @ loopexp_pos p^ b = loopexp p (binint_pos_sub a b)
    apply aH.
Qed.

Lemma loopexp_add {A : Type} {x : A} (p : x = x) a b
  : loopexp p (a + b) = loopexp p a @ loopexp p b.
A: Type
x: A
p: x = x
a, b: BinInt
loopexp p (a + b) = loopexp p a @ loopexp p b
Proof.
A: Type
x: A
p: x = x
a, b: BinInt
loopexp p (a + b) = loopexp p a @ loopexp p b
  destruct a as [a| |a], b as [b| |b]; trivial;
  try apply loopexp_pos_add; cbn.
A: Type
x: A
p: x = x
a: Pos
loopexp_pos p^ a = loopexp_pos p^ a @ 1
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub b a) = loopexp_pos p^ a @ loopexp_pos p b
A: Type
x: A
p: x = x
b: Pos
loopexp_pos p^ b = 1 @ loopexp_pos p^ b
A: Type
x: A
p: x = x
b: Pos
loopexp_pos p b = 1 @ loopexp_pos p b
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
A: Type
x: A
p: x = x
a: Pos
loopexp_pos p a = loopexp_pos p a @ 1
  1,6: symmetry; apply concat_p1.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub b a) = loopexp_pos p^ a @ loopexp_pos p b
A: Type
x: A
p: x = x
b: Pos
loopexp_pos p^ b = 1 @ loopexp_pos p^ b
A: Type
x: A
p: x = x
b: Pos
loopexp_pos p b = 1 @ loopexp_pos p b
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
  2,3: symmetry; apply concat_1p.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub b a) = loopexp_pos p^ a @ loopexp_pos p b
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
  1: apply loopexp_binint_pos_sub_l.
A: Type
x: A
p: x = x
a, b: Pos
loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b
  apply loopexp_binint_pos_sub_r.
Qed.

(** Under univalence, exponentiation of loops corresponds to iteration of auto-equivalences. *)

Definition equiv_path_loopexp
           {A : Type} (p : A = A) (z : BinInt) (a : A)
  : equiv_path A A (loopexp p z) a = binint_iter (equiv_path A A p) z a.
A: Type
p: A = A
z: BinInt
a: A
equiv_path A A (loopexp p z) a = binint_iter (equiv_path A A p) z a
Proof.
A: Type
p: A = A
z: BinInt
a: A
equiv_path A A (loopexp p z) a = binint_iter (equiv_path A A p) z a
  destruct z as [n| |n]; trivial.
A: Type
p: A = A
n: Pos
a: A
equiv_path A A (loopexp p (neg n)) a =
binint_iter (equiv_path A A p) (neg n) a
A: Type
p: A = A
n: Pos
a: A
equiv_path A A (loopexp p (pos n)) a =
binint_iter (equiv_path A A p) (pos n) a
  all: induction n as [|n IH]
    using pos_peano_ind; try reflexivity; cbn in *.
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p^ n) a = pos_iter (transport idmap p^) n a
transport idmap (loopexp_pos p^ (pos_succ n)) a =
pos_iter (transport idmap p^) (pos_succ n) a
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p n) a = pos_iter (transport idmap p) n a
transport idmap (loopexp_pos p (pos_succ n)) a =
pos_iter (transport idmap p) (pos_succ n) a
  all: unfold loopexp_pos; rewrite pos_peano_ind_beta_pos_succ.
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p^ n) a = pos_iter (transport idmap p^) n a
transport idmap
  (pos_peano_ind (fun _ : Pos => A = A) p^
     (fun (_ : Pos) (q : A = A) => q @ p^) n @
   p^)
  a =
pos_iter (transport idmap p^) (pos_succ n) a
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p n) a = pos_iter (transport idmap p) n a
transport idmap
  (pos_peano_ind (fun _ : Pos => A = A) p
     (fun (_ : Pos) (q : A = A) => q @ p) n @
   p)
  a =
pos_iter (transport idmap p) (pos_succ n) a
  all: unfold pos_iter; rewrite pos_peano_rec_beta_pos_succ.
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p^ n) a = pos_iter (transport idmap p^) n a
transport idmap
  (pos_peano_ind (fun _ : Pos => A = A) p^
     (fun (_ : Pos) (q : A = A) => q @ p^) n @
   p^)
  a =
transport idmap p^
  (pos_peano_rec (A -> A) (transport idmap p^)
     (fun (_ : Pos) (g : A -> A) (x : A) => transport idmap p^ (g x)) n a)
A: Type
p: A = A
n: Pos
a: A
IH: transport idmap (loopexp_pos p n) a = pos_iter (transport idmap p) n a
transport idmap
  (pos_peano_ind (fun _ : Pos => A = A) p
     (fun (_ : Pos) (q : A = A) => q @ p) n @
   p)
  a =
transport idmap p
  (pos_peano_rec (A -> A) (transport idmap p)
     (fun (_ : Pos) (g : A -> A) (x : A) => transport idmap p (g x)) n a)
  all: refine (transport_pp _ _ _ _ @ _); cbn; apply ap, IH.
Defined.

Definition loopexp_path_universe `{Univalence}
           {A : Type} (f : A <~> A) (z : BinInt) (a : A)
  : transport idmap (loopexp (path_universe f) z) a
  = binint_iter f z a.
H: Univalence
A: Type
f: A <~> A
z: BinInt
a: A
transport idmap (loopexp (path_universe f) z) a = binint_iter f z a
Proof.
H: Univalence
A: Type
f: A <~> A
z: BinInt
a: A
transport idmap (loopexp (path_universe f) z) a = binint_iter f z a
  revert f.
H: Univalence
A: Type
z: BinInt
a: A
forall f : A <~> A,
transport idmap (loopexp (path_universe f) z) a = binint_iter f z a equiv_intro (equiv_path A A) p.
H: Univalence
A: Type
z: BinInt
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
binint_iter (equiv_path A A p) z a
  refine (_ @ equiv_path_loopexp p z a).
H: Univalence
A: Type
z: BinInt
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
equiv_path A A (loopexp p z) a
  refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
H: Univalence
A: Type
z: BinInt
a: A
p: A = A
path_universe (equiv_path A A p) = p
  apply eissect.
Defined.