`{Univalence} X (f : X <~> X) (n : Int) (x : X) : transport (Circle_rec Type X (path_universe f)) (equiv_loopCircle_int^-1 n) x = int_iter f n x. Proof. refine (_ @ loopexp_path_universe _ _ _). refine (transport_compose idmap _ _ _ @ _). refine (ap (fun p => transport idmap p x) _). unfold equiv_loopCircle_int; cbn. unfold Circle_decode; simpl. rewrite ap_loopexp. refine (ap (fun p => loopexp p n) _). apply Circle_rec_beta_loop. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.Loops Pointed.pEquiv. Require Import HSet. Require Import Spaces.Int. Require Import Colimits.Coeq. Require Import Truncations.Core Truncations.Connectedness.