(P : Type) (b : P) (l : b = b) : Circle -> P := Circle_ind (fun _ => P) b (transport_const _ _ @ l).
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.