{A B} (f : A -> B) {x : A} (p : x = x) (z : Int) : ap f (loopexp p z) = loopexp (ap f p) z. Proof. nrapply int_iter_commute_map. intro q; apply ap_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.