{A : Type} (p : A = A) (z : BinInt) (a : A) : equiv_path A A (loopexp p z) a = binint_iter (equiv_path A A p) z a. Proof. destruct z as [n| |n]; trivial. all: induction n as [|n IH] using pos_peano_ind; try reflexivity; cbn in *. all: unfold loopexp_pos; rewrite pos_peano_ind_beta_pos_succ. all: unfold pos_iter; rewrite pos_peano_rec_beta_pos_succ. all: refine (transport_pp _ _ _ _ @ _); cbn; apply ap, IH. 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.