proposition: Lemma Circle_isaprop : isaprop Circle.
proof: Proof. apply (isofhlevelweqb 1 CircleEquiv). apply invproofirrelevance. intros [C [pt [loop I]]] [C' [pt' [loop' I']]]. set (R := CircleInductionToRecursion' I ). set (R' := CircleInductionToRecursion' I'). set (gre := R C' pt' loop'). set (g := pr1 gre). set (r := pr12 gre). set (e := pr22 gre). set (gre' := R' C pt loop ). set (g' := pr1 gre'). set (r' := pr12 gre'). set (e' := pr22 gre'). fold g in r, e; fold g' in r', e'; fold r in e; fold r' in e'. cbn beta in e, e'. set (fib := (pt ,, pathsinv0 r) : hfiber g pt'). transparent assert (v : (pt = g' (g pt))). { refine (r' @ _). apply maponpaths. assumption. } transparent assert (v' : (pt' = g (g' pt'))). { refine (r @ _). apply maponpaths. assumption. } assert (ie : isweq g). { apply (isweq_iso _ g'). { intros x. apply pathsinv0. generalize x; clear x. simple refine (pr1 (I _ _ _)). - simpl. exact v. - set (Q := ! pathOverEquations (f := idfun _) (g := funcomp g g') v v loop). apply (cast Q); clear Q. intermediate_path (v @ maponpaths g' (maponpaths g loop)). + apply (maponpaths (λ k, v @ k)). apply pathsinv0, maponpathscomp. + rewrite maponpathsidfun. unfold v. rewrite <- path_assoc. rewrite <- maponpathscomp0. intermediate_path (r' @ maponpaths g' (loop' @ r)). * apply maponpaths. apply maponpaths. exact e. * rewrite maponpathscomp0. rewrite path_assoc. rewrite e'. rewrite path_assoc. reflexivity. } { intros x. apply pathsinv0. generalize x; clear x. simple refine (pr1 (I' _ _ _)). - simpl. exact v'. - set (Q := ! pathOverEquations (f := idfun _) (g := funcomp g' g) v' v' loop'). apply (cast Q); clear Q. intermediate_path (v' @ maponpaths g (maponpaths g' loop')). + apply (maponpaths (λ k, v' @ k)). apply pathsinv0, maponpathscomp. + rewrite maponpathsidfun. unfold v'. rewrite <- path_assoc. rewrite <- maponpathscomp0. intermediate_path (r @ maponpaths g (loop @ r')). * apply maponpaths. apply maponpaths. exact e'. * rewrite maponpathscomp0. rewrite path_assoc. rewrite e. rewrite path_assoc. reflexivity. } } unfold CircleInduction' in I, I'. Abort. Definition circle := B ℤ. Lemma loops_circle : ℤ ≃ Ω circle. Proof. apply loopsBG. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Equivalences UniMath.MoreFoundations.PathsOver UniMath.Algebra.Monoids UniMath.SyntheticHomotopyTheory.AffineLine UniMath.NumberSystems.Integers UniMath.Algebra.BinaryOperations UniMath.Algebra.GroupAction UniMath.Algebra.Groups