{R : Ring} (S : R -> Type) : _ <~> IsSubring S := ltac:(issig). Global Instance ishprop_issubring `{Funext} {R : Ring} (S : R -> Type) : IsHProp (IsSubring S). Proof. exact (istrunc_equiv_istrunc _ ( S)). Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.