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