f (- mon_unit) = a * c. Proof. unfold f; apply ap. exact (hspace_right_identity c). Defined.
Require Import Classes.interfaces.abstract_algebra. Require Import Cubical.DPath Cubical.PathSquare. Require Import Pointed.Core Pointed.pSusp. Require Import Homotopy.HSpace.Core. Require Import Homotopy.Suspension. Require Import Homotopy.Join.Core.