rename

agda · Sep 9, 2022 · 4b72d6e · 4b72d6e
1 parent 284e82f
commit 4b72d6e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/...lgebra/FreeCommAlgebra/CommCoproduct.agda → ...mAlgebra/FreeCommAlgebra/OnCoproduct.agda b/...lgebra/FreeCommAlgebra/CommCoproduct.agda → ...mAlgebra/FreeCommAlgebra/OnCoproduct.agda
@@ -7,7 +7,7 @@
 
   where '⊎' is the disjoint sum.
 -}
-module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.CommCoproduct where
+module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv