From 719cd0c77adbe6f0c8d55d3707ec678a99c74670 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 22 Aug 2023 20:08:30 -0400
Subject: [PATCH] Additions to Common.agda

---
 .../guarded-cubical/Common/Common.agda        | 20 ++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/formalizations/guarded-cubical/Common/Common.agda b/formalizations/guarded-cubical/Common/Common.agda
index 0c422dc..7a42434 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)
+
-- 
GitLab