G -> G -> Type := fun g1 g2 => hfiber incl (g1 @ g2^). Global Instance ishprop_in_coset : is_mere_relation G . Proof. exact _. Defined.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.