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. 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.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.