refactor: rename commutative graphs to marked graphs

the1lab · Sep 21, 2024 · 3ca644c · 3ca644c
1 parent a71f4a3
commit 3ca644c
Show file tree

Hide file tree

Showing 3 changed files with 188 additions and 181 deletions.
diff --git a/src/Borceux.lagda.md b/src/Borceux.lagda.md
@@ -47,7 +47,7 @@ open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Limit.Finite
 open import Cat.Functor.Conservative
 open import Cat.Functor.Hom.Coyoneda
-open import Cat.Instances.CommGraphs
+open import Cat.Instances.MarkedGraphs
 open import Cat.Diagram.Coequaliser
 open import Cat.Functor.Adjoint.Hom
 open import Cat.Functor.Adjoint.Kan
@@ -893,18 +893,18 @@ _ = Graph-hom
 _ = Path-in
 _ = Path-category
 _ = Free-category
-_ = Comm-graph
-_ = Comm-graphs
-_ = Comm-free-category
+_ = Marked-graph
+_ = Marked-graphs
+_ = Marked-free-category
 ```
 -->
 
 * Definition 5.1.1: `Graph`{.Agda}
 * Definition 5.1.2: `Graph-hom`{.Agda}
 * Definition 5.1.3: `Path-in`{.Agda}
 * Proposition 5.1.4: `Path-category`{.Agda}, `Free-category`{.Agda}
-* Definition 5.1.5: `Comm-graph`{.Agda}, `Comm-graphs`{.Agda}
-* Proposition 5.1.6: `Comm-free-category`{.Agda}
+* Definition 5.1.5: `Marked-graph`{.Agda}, `Marked-graphs`{.Agda}
+* Proposition 5.1.6: `Marked-free-category`{.Agda}
 
 ### 5.2 Calculus of fractions