(z : Int) : Circle_encode base (loopexp loop z) = z. Proof. induction z as [|n | n]. - reflexivity. - rewrite loopexp_succ_r. unfold Circle_encode in IHz |- *. rewrite transport_pp. rewrite IHz. apply transport_Circle_code_loop. - rewrite loopexp_pred_r. unfold Circle_encode in IHz |- *. rewrite transport_pp. rewrite IHz. apply transport_Circle_code_loopV. 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.