`{Univalence} {A : Type} (f : A <~> A) (z : Int) (a : A) : transport idmap (loopexp (path_universe f) z) a = int_iter f z a. Proof. revert f. equiv_intro (equiv_path A A) p. refine (_ @ equiv_path_loopexp p z a). refine (ap (fun q => equiv_path A A (loopexp q z) a) _). apply eissect. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.