Library HoTT.Spaces.Int.Equiv
Require Import Basics.
Require Import Spaces.Pos.
Require Import Spaces.Int.Core.
Require Import Spaces.Int.Spec.
Require Import Spaces.Pos.
Require Import Spaces.Int.Core.
Require Import Spaces.Int.Spec.
Definition int_iter {A} (f : A → A) `{!IsEquiv f} (n : Int) : A → A
:= match n with
| neg n ⇒ fun x ⇒ pos_iter f^-1 n x
| zero ⇒ idmap
| pos n ⇒ fun x ⇒ pos_iter f n x
end.
Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse.
Definition int_iter_succ_l {A} (f : A → A) `{IsEquiv _ _ f}
(n : Int) (a : A)
: int_iter f (int_succ n) a = f (int_iter f n a).
Proof.
destruct n as [n| |n]; trivial.
+ revert n f H a.
srapply pos_peano_ind.
{ intros f H a.
symmetry.
apply eisretr. }
hnf; intros n p f H a.
refine (ap (fun x ⇒ _ x _) _ @ _).
1: rewrite int_neg_pos_succ.
1: exact (eisretr int_succ (neg n)).
apply moveL_equiv_M.
cbn; symmetry.
srapply pos_iter_succ_l.
+ cbn.
rewrite pos_add_1_r.
srapply pos_iter_succ_l.
Qed.
Definition int_iter_succ_r {A} (f : A → A) `{IsEquiv _ _ f}
(n : Int) (a : A) : int_iter f (int_succ n) a = int_iter f n (f a).
Proof.
destruct n as [n| |n]; trivial.
+ revert n f H a.
srapply pos_peano_ind.
{ intros f H a.
symmetry.
apply eissect. }
hnf; intros n p f H a.
rewrite int_neg_pos_succ.
refine (ap (fun x ⇒ _ x _) _ @ _).
1: exact (eisretr int_succ (neg n)).
cbn; rewrite pos_add_1_r.
rewrite pos_iter_succ_r.
rewrite eissect.
reflexivity.
+ cbn.
rewrite pos_add_1_r.
srapply pos_iter_succ_r.
Qed.
Definition iter_int_pred_l {A} (f : A → A) `{IsEquiv _ _ f}
(n : Int) (a : A)
: int_iter f (int_pred n) a = f^-1 (int_iter f n a).
Proof.
destruct n as [n| |n]; trivial.
+ cbn; rewrite pos_add_1_r.
by rewrite pos_iter_succ_l.
+ revert n.
srapply pos_peano_ind.
- cbn; symmetry; apply eissect.
- hnf; intros p q.
rewrite <- pos_add_1_r.
change (int_pred (pos (p + 1)%pos))
with (int_pred (int_succ (pos p))).
rewrite int_pred_succ.
change (pos (p + 1)%pos)
with (int_succ (pos p)).
rewrite int_iter_succ_l.
symmetry.
apply eissect.
Qed.
Definition iter_int_pred_r {A} (f : A → A) `{IsEquiv _ _ f}
(n : Int) (a : A)
: int_iter f (int_pred n) a = int_iter f n (f^-1 a).
Proof.
revert f H n a.
destruct n as [n| |n]; trivial;
induction n as [|n nH] using pos_peano_ind; trivial.
2: hnf; intros; apply symmetry, eisretr.
all: rewrite <- pos_add_1_r.
all: intro a.
1: change (neg (n + 1)%pos) with (int_pred (neg n)).
2: change (pos (n + 1)%pos) with (int_succ (pos n)).
1: rewrite <- 2 int_neg_pos_succ.
1: cbn; apply pos_iter_succ_r.
rewrite int_pred_succ.
rewrite int_iter_succ_r.
rewrite eisretr.
reflexivity.
Qed.