proposition: Lemma intersection_submonoid : forall {X : monoid} {I : UU} (S : I -> hsubtype X) (each_is_submonoid : ∏ i : I, issubmonoid (S i)), issubmonoid (subtype_intersection S).
proof: Proof. intros. use make_issubmonoid. + intros g h i. pose (is_subgr := pr1 (each_is_submonoid i)). exact (is_subgr (pr1 g,, (pr2 g) i) (pr1 h,, (pr2 h) i)). + exact (λ i, pr2 (each_is_submonoid i)). Qed.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders