proposition: Lemma lemma3 : g mon_unit = c * b.
proof: Proof. unfold g; apply ap. apply left_identity. Defined.
imports: Classes.interfaces.abstract_algebra Cubical Pointed.Core Pointed.pSusp Homotopy.HSpace.Core Homotopy.Suspension Homotopy.Join.Core