{A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A := match n with | negS n => fun x => nat_iter n.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.