proposition: Lemma is_section_inv (s : section U) : is_section (λ p, - s p).
proof: Proof. intro p. induction s as [s Hs]. use (hinhuniv _ (Hs p)); intro H. induction H as [V H]. induction H as [HVp H]. induction H as [HV H]. use (hinhuniv _ H); intro Hfg. induction Hfg as [f Hfg]. induction Hfg as [g Hfg]. apply hinhpr. exists V. use make_dirprod. - exact HVp. - use make_dirprod. + exact HV. + apply hinhpr. exists (-1 * f), g. intros q Hq. use (hinhuniv _ (Hfg q Hq)); intros Hg. induction Hg as [Hg Heq]. apply hinhpr. exists Hg. exact (maponpaths ringinv1 Heq @ idpath _). Qed.
imports: UniMath.Algebra.RigsAndRings UniMath.Algebra.RigsAndRings.Ideals UniMath.MoreFoundations.AxiomOfChoice UniMath.MoreFoundations.Subtypes UniMath.Topology.Topology UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.Commring UniMath.AlgebraicGeometry.Topology UniMath.AlgebraicGeometry.SheavesOfRings