proposition: Lemma is_section_op2 (s t : section U) : is_section (λ p, s p * t p).
proof: Proof. intros p. induction s as [s Hs]. induction t as [t Ht]. use (hinhuniv _ (Hs p)); intro H1. use (hinhuniv _ (Ht p)); intro H2. induction H1 as [V1 H1]. induction H1 as [Hp1 H1]. induction H1 as [HU1 H1]. induction H2 as [V2 H2]. induction H2 as [Hp2 H2]. induction H2 as [HU2 H2]. use (hinhuniv _ H1); intro Hfg1. use (hinhuniv _ H2); intro Hfg2. induction Hfg1 as [f1 Hfg1]. induction Hfg1 as [g1 Hq1]. induction Hfg2 as [f2 Hfg2]. induction Hfg2 as [g2 Hq2]. apply hinhpr. exists (V1 ∩ V2). use make_dirprod. + exact (make_dirprod Hp1 Hp2). + use make_dirprod. * intros x Hx. apply (HU1 x), (dirprod_pr1 Hx). * apply hinhpr. exists (f1 * f2), (g1 * g2). intros q HVq. use (hinhuniv _ (Hq1 q (dirprod_pr1 HVq))); intro Hg1. use (hinhuniv _ (Hq2 q (dirprod_pr2 HVq))); intro Hg2. induction Hg1 as [Hg1 Heq1]. induction Hg2 as [Hg2 Heq2]. set (Hg := prime_ideal_ax1_contraposition (pr1 q) _ _ Hg1 Hg2). apply hinhpr. exists Hg. exact (map_on_two_paths op2 Heq1 Heq2 @ 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