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