G / R. Global Instance congquot_sgop : SgOp . Proof. srapply Quotient_rec2. - intros x y. exact (class_of _ (x * y)). - intros x x' y p. apply qglue. by apply iscong. - intros x y y' q. apply qglue. by apply iscong. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import HSet. Require Import Spaces.Finite.Finite. Require Import WildCat. Require Import Modalities.Modality.