(z : Int) : transport Circle_code loop^ z = int_pred z. Proof. refine (transport_compose idmap Circle_code loop^ z @ _). rewrite ap_V. unfold Circle_code; rewrite Circle_rec_beta_loop. rewrite <- (path_universe_V int_succ). apply transport_path_universe. 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.