diff --git a/formalizations/guarded-cubical/Common/Common.agda b/formalizations/guarded-cubical/Common/Common.agda
index 0c422dc4e96a66d285632e77a9d597753e731a7d..7a42434a0944dd2d19cce8a0b77b6d2876d73e8a 100644
--- a/formalizations/guarded-cubical/Common/Common.agda
+++ b/formalizations/guarded-cubical/Common/Common.agda
@@ -15,10 +15,14 @@ open import Cubical.Data.Empty
 open import Cubical.Data.Sigma
 open import Cubical.Data.Unit renaming (Unit to ⊤)
 
+open import Cubical.Algebra.Monoid.Base
+open import Cubical.Algebra.Monoid.FreeCommProduct
+open import Cubical.Algebra.CommMonoid.Base
+
 
 private
   variable
-    â„“ â„“' : Level
+    â„“ â„“' â„“'' : Level
     â„“A â„“B â„“C â„“D : Level
     â„“R â„“S : Level
 
@@ -77,3 +81,17 @@ isPropTwoCell isPropValuedS =
   isPropΠ3 (λ a b aRb -> isPropValuedS _ _)
 
 
+
+
+
+isSplitMono : {â„“A â„“B : Level} {A : Type â„“A} {B : Type â„“B} ->
+  (f : A -> B) -> Type (â„“-max â„“A â„“B)
+isSplitMono {A = A} {B = B} f =
+ Σ[ g ∈ (B -> A) ] (∀ a -> g (f a) ≡ a)
+
+
+InjectiveMonoidHom : {â„“m â„“n : Level} ->
+  (M : Monoid â„“m) (N : Monoid â„“n) -> Type (â„“-max â„“m â„“n)
+InjectiveMonoidHom M N =
+  Σ[ f ∈ MonoidHom M N ] isSplitMono (fst f)
+