proposition: Lemma is_section_restriction_section_map (s : section U) : is_section (restriction_section_map s).
proof: Proof. intro p. induction p as [p HVp]. induction s as [s Hs]. use (hinhuniv _ (Hs (p ,, (H _ HVp)))); intro HW. induction HW as [W HW]. induction HW as [HWp HW]. induction HW as [HUW Hfg]. use (hinhfun _ Hfg); intro Hq. induction Hq as [f Hq]. induction Hq as [g Hq]. exists (V ∩ W). use make_dirprod. - exact (make_dirprod HVp HWp). - use make_dirprod. + intros x Hx. exact (dirprod_pr1 Hx). + apply hinhpr. exists f, g. intros q H0. induction q as [q HVq]. use (hinhfun _ (Hq (q ,, H _ HVq) (dirprod_pr2 H0))); intro Hg. induction Hg as [Hg Heq]. exists Hg. exact Heq. 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