fill Agda field

UniMath · Nov 28, 2023 · bea8068 · bea8068
1 parent 876b325
commit bea8068
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/graph-theory/cycles-undirected-graphs.lagda.md b/src/graph-theory/cycles-undirected-graphs.lagda.md
@@ -22,7 +22,7 @@ open import graph-theory.undirected-graphs
 ## Idea
 
 A
-{{#concept "cycle" Agda= Disambiguation="undirected graph" WD="Cycle" WDID=Q245595}}
+{{#concept "cycle" Agda=cycle-Undirected-Graph Disambiguation="undirected graph" WD="Cycle" WDID=Q245595}}
 in an [undirected graph](graph-theory.undirected-graphs.md) `G` consists of a
 [`k`-gon](graph-theory.polygons.md) `H` equipped with an
 [embedding of graphs](graph-theory.embeddings-undirected-graphs.md) from `H`