(P : Type) (b : P) (l : b = b) : ap (Circle_rec P b l) loop = l. Proof. unfold Circle_rec. refine (cancelL (transport_const loop b) _ _ _). refine ((apD_const (Circle_ind (fun _ => P) b _) loop)^ @ _). refine (Circle_ind_beta_loop (fun _ => P) _ _). 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.