proposition: Lemma section_intersection (s : section U) (t : section V) : restriction_section (intersection_contained1 U V) s = restriction_section (intersection_contained2 U V) t -> ∏ p (HUp : U p) (HVp : V p), s (p ,, HUp) = t (p ,, HVp).
proof: Proof. intros Heq p HUp HVp. set (Hp := make_dirprod HUp HVp). assert (H : restriction_section (intersection_contained1 U V) s (p ,, Hp) = restriction_section (intersection_contained2 U V) t (p ,, Hp)). { induction Heq. apply idpath. } apply H. 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