(R : Ring) : Group. Proof. snrapply Build_Group. - exact {x : R & IsInvertible R x}. - intros [x p] [y q]. exists (x * y). exact _. - exists 1. exact _. - intros [x p]. exists (inverse_elem x). exact _. - repeat split. 1: exact _. 1-5: hnf; intros; apply path_sigma_hprop. + rapply simple_associativity. + rapply left_identity. + rapply right_identity. + apply rng_inv_l. + apply rng_inv_r. 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.