proposition: Lemma is_section_unel1 : is_section (λ p : carrier U, @rigunel1 (localization_at (pr1 p))).
proof: Proof. intro p. apply hinhpr. exists U. use make_dirprod. - exact (pr2 p). - use make_dirprod. + intros x H. exact H. + apply hinhpr. exists 0, 1. intros q Hq. apply hinhpr. exists (prime_ideal_ax2 _). apply 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