proposition: Lemma iscontr_Q (X: Torsor ℤ) : iscontr_hProp (Q X).
proof: Proof. use (hinhuniv _ (torsor_nonempty X)). intros x. use (iscontrweqb (Y := ∑ a', PathOver (s x) a a')). 2 : { apply PathOverUniqueness. } apply weqfibtototal; intros a'. exact (ℤTorsorRecursion_weq (λ x, weqcomp (composePathOver_weq a' (s x) p) (cp (ε x))) x). Qed.
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