{A B : Type} `{SgOp A} `{SgOp B} `{MonUnit A} `{MonUnit B} {f : A -> B} : _ <~> IsMonoidPreserving f := ltac:(issig). Global Instance ishprop_ismonoidpreserving `{Funext} {A B : Type} `{SgOp A} `{SgOp B} `{IsHSet B} `{MonUnit A} `{MonUnit B} (f : A -> B) : IsHProp (IsMonoidPreserving f). Proof. srapply (istrunc_equiv_istrunc _ ). srapply (istrunc_equiv_istrunc _ (equiv_sigma_prod0 _ _)^-1). srapply istrunc_prod. unfold IsUnitPreserving. exact _. Defined.
Require Import Spaces.Nat.Core. Require Import Modalities.ReflectiveSubuniverse.