(P : Circle -> Type) (b : P base) (l : loop # b = b) : forall (x : Circle), P x. Proof. refine (Coeq_ind P (fun u => transport P (ap coeq (path_unit tt u)) b) _). intros []; exact l. 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.