fact: Definition Circle_ind_beta_loop (P : Circle -> Type) (b : P base) (l : loop # b = b) : apD (Circle_ind P b l) loop = l := Coeq_ind_beta_cglue P _ _ tt.
imports: Basics Types Pointed.Core Pointed.Loops Pointed.pEquiv HSet Spaces.Pos Spaces.Int Colimits.Coeq Truncations.Core Truncations.Connectedness Cubical.DPath