proposition: Lemma intersection_subgr : forall {X : gr} {I : UU} (S : I -> hsubtype X) (each_is_subgr : ∏ i : I, issubgr (S i)), issubgr (subtype_intersection S).
proof: Proof. intros. use make_issubgr. - exact (intersection_submonoid S (λ i, (pr1 (each_is_subgr i)))). - exact (λ x x_in_S i, pr2 (each_is_subgr i) x (x_in_S i)). Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids