{A : Type} (p : A = A) (z : Int) (a : A) : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a. Proof. refine (int_iter_commute_map _ _ (fun p => equiv_path A A p a) _ _ _). intro q; cbn. nrapply transport_pp. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.