{A B} (f : A -> B) {x : A} (p : x = x) (n : Pos) : ap f (loopexp_pos p n) = loopexp_pos (ap f p) n. Proof. revert n. srapply pos_peano_ind; cbn; trivial. unfold loopexp_pos. intros n q. rewrite 2 pos_peano_ind_beta_pos_succ. by rewrite ap_pp, q. Qed.
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.