`{Univalence} {A : Type} (f : A <~> A) (z : BinInt) (a : A) : transport idmap (loopexp (path_universe f) z) a = binint_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. Require Import Types.Universe. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec. Require Import Spaces.BinInt.Equiv.