(P : Circle -> Type) (b : P base) (l : loop # b = b) : apD (Circle_ind P b l) loop = l := Coeq_ind_beta_cglue P _ _ tt.
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.