{G H : Group} (g : G) (h : H) : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h). Proof. snrapply path_prod; symmetry. - snrapply grp_unit_r. - snrapply grp_unit_l. Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.