Fix links to wikidata to the recommended links; add concept tags at e…

…nd of file for testing purposes (#837)
UniMath · Oct 13, 2023 · d8f1320 · d8f1320
1 parent ee1d474
commit d8f1320
Show file tree

Hide file tree

Showing 41 changed files with 46 additions and 41 deletions.
diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md
@@ -64,8 +64,10 @@ is-acyclic-Undirected-Graph l G =
 ## External links
 
 - [Trees](https://ncatlab.org/nlab/show/tree) at nlab
-- [Acyclic graph](https://www.wikidata.org/wiki/Q3115453) at Wikidata
+- [Acyclic graph](https://www.wikidata.org/entity/Q3115453) at Wikidata
 - [Forests](<https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest>) at
   Wikipedia
 - [Acyclic graphs](https://mathworld.wolfram.com/AcyclicGraph.html) at Wolfram
   Mathworld.
+
+<concept id="https://www.wikidata.org/entity/Q3115453" />
diff --git a/src/graph-theory/circuits-undirected-graphs.lagda.md b/src/graph-theory/circuits-undirected-graphs.lagda.md
@@ -44,8 +44,10 @@ module _
 
 ## External links
 
-- [Cycle](https://www.wikidata.org/wiki/Q245595) at Wikidata
+- [Cycle](https://www.wikidata.org/entity/Q245595) at Wikidata
 - [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
   Mathworld
+
+<concept id="https://www.wikidata.org/entity/Q245595" />
diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
@@ -40,7 +40,7 @@ module _
 
 ## External links
 
-- [Cycle](https://www.wikidata.org/wiki/Q245595) at Wikidata
+- [Cycle](https://www.wikidata.org/entity/Q245595) at Wikidata
 - [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram

diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -52,7 +52,8 @@ pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p =
 - [Complete bipartite graph](https://d3gt.com/unit.html?complete-bipartite) at
   D3 Graph Theory
 - [Bipartite graphs](https://ncatlab.org/nlab/show/bipartite+graph) at nlab
-- [Complete bipartite graph](https://www.wikidata.org/wiki/Q913598) at Wikidata
+- [Complete bipartite graph](https://www.wikidata.org/entity/Q913598) at
+  Wikidata
 - [Complete bipartite graph](https://en.wikipedia.org/wiki/Complete_bipartite_graph)
   at Wikipedia
 - [Complete bipartite graphs](https://mathworld.wolfram.com/CompleteBipartiteGraph.html)

diff --git a/src/graph-theory/complete-multipartite-graphs.lagda.md b/src/graph-theory/complete-multipartite-graphs.lagda.md
@@ -47,7 +47,7 @@ pr2 (complete-multipartite-Undirected-Graph-𝔽 X Y) p =
 
 ## External links
 
-- [Multipartite graph](https://www.wikidata.org/wiki/Q1718082) on Wikidata
+- [Multipartite graph](https://www.wikidata.org/entity/Q1718082) on Wikidata
 - [Multipartite graph](https://en.wikipedia.org/wiki/Multipartite_graph) on
   Wikipedia
 - [Complete multipartite graph](https://mathworld.wolfram.com/CompleteMultipartiteGraph.html)

diff --git a/src/graph-theory/complete-undirected-graphs.lagda.md b/src/graph-theory/complete-undirected-graphs.lagda.md
@@ -41,7 +41,7 @@ complete-Undirected-Graph-𝔽 X =
 ## External links
 
 - [Complete graph](https://d3gt.com/unit.html?complete-graph) at D3 Graph theory
-- [Complete graph](https://www.wikidata.org/wiki/Q45715) on Wikidata
+- [Complete graph](https://www.wikidata.org/entity/Q45715) on Wikidata
 - [Complete graph](https://en.wikipedia.org/wiki/Complete_graph) on Wikipedia
 - [Complete graph](https://mathworld.wolfram.com/CompleteGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/connected-undirected-graphs.lagda.md b/src/graph-theory/connected-undirected-graphs.lagda.md
@@ -50,7 +50,7 @@ module _
 ## External links
 
 - [Connected graph](https://ncatlab.org/nlab/show/connected+graph) at nlab
-- [Connected graph](https://www.wikidata.org/wiki/Q230655) on Wikidata
+- [Connected graph](https://www.wikidata.org/entity/Q230655) on Wikidata
 - [Connectivity (graph theory)](<https://en.wikipedia.org/wiki/Connectivity_(graph_theory)>)
   on Wikipedia
 - [Connected graph](https://mathworld.wolfram.com/ConnectedGraph.html) at

diff --git a/src/graph-theory/cycles-undirected-graphs.lagda.md b/src/graph-theory/cycles-undirected-graphs.lagda.md
@@ -40,7 +40,7 @@ module _
 
 ## External links
 
-- [Cycle](https://www.wikidata.org/wiki/Q245595) on Wikidata
+- [Cycle](https://www.wikidata.org/entity/Q245595) on Wikidata
 - [Cycle (graph theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram

diff --git a/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md b/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md
@@ -28,7 +28,7 @@ Directed-Graph-Fin = Σ ℕ (λ V → Fin V → Fin V → ℕ)
 
 - [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
 - [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
-- [Directed graph](https://www.wikidata.org/wiki/Q1137726) on Wikdiata
+- [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikdiata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Directed graph](https://mathworld.wolfram.com/DirectedGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/directed-graphs.lagda.md b/src/graph-theory/directed-graphs.lagda.md
@@ -137,7 +137,7 @@ module equiv {l1 l2 : Level} where
 
 - [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
 - [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
-- [Directed graph](https://www.wikidata.org/wiki/Q1137726) on Wikidata
+- [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikidata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Directed graph](https://mathworld.wolfram.com/DirectedGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/edge-coloured-undirected-graphs.lagda.md b/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
@@ -107,4 +107,4 @@ module _
 - [Edge coloring](https://en.wikipedia.org/wiki/Edge_coloring) at Wikipedia
 - [Edge coloring](https://mathworld.wolfram.com/EdgeColoring.html) at Wolfram
   Mathworld
-- [Graph coloring](https://www.wikidata.org/wiki/Q504843) on Wikidata
+- [Graph coloring](https://www.wikidata.org/entity/Q504843) on Wikidata
diff --git a/src/graph-theory/embeddings-directed-graphs.lagda.md b/src/graph-theory/embeddings-directed-graphs.lagda.md
@@ -73,6 +73,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) on
   Wikipedia
diff --git a/src/graph-theory/embeddings-undirected-graphs.lagda.md b/src/graph-theory/embeddings-undirected-graphs.lagda.md
@@ -130,6 +130,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) on
   Wikipedia
diff --git a/src/graph-theory/enriched-undirected-graphs.lagda.md b/src/graph-theory/enriched-undirected-graphs.lagda.md
@@ -199,7 +199,7 @@ module _
 ## External links
 
 - [Graph](https://ncatlab.org/nlab/show/graph) at nlab
-- [Graph](https://www.wikidata.org/wiki/Q141488) on Wikidata
+- [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
 - [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md
@@ -541,7 +541,7 @@ module _
 
 ## External links
 
-- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomoprhism](https://www.wikidata.org/entity/Q303100) at Wikidata
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at

diff --git a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
@@ -300,7 +300,7 @@ module _
 
 ## External links
 
-- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomoprhism](https://www.wikidata.org/entity/Q303100) at Wikidata
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at

diff --git a/src/graph-theory/equivalences-undirected-graphs.lagda.md b/src/graph-theory/equivalences-undirected-graphs.lagda.md
@@ -300,7 +300,7 @@ module _
 
 ## External links
 
-- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomoprhism](https://www.wikidata.org/entity/Q303100) at Wikidata
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at

diff --git a/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md b/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
@@ -63,7 +63,7 @@ module _
 
 - [Eulerian circuit](https://d3gt.com/unit.html?eulerian-circuit) on D3 Graph
   theory
-- [Eulerian cycle](https://www.wikidata.org/wiki/Q11691793) on Wikidata
+- [Eulerian cycle](https://www.wikidata.org/entity/Q11691793) on Wikidata
 - [Eulerian path](https://en.wikipedia.org/wiki/Eulerian_path) on Wikipedia
 - [Eulerian cycle](https://mathworld.wolfram.com/EulerianCycle.html) on Wolfram
   mathworld
diff --git a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
@@ -121,6 +121,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
   Wikipedia
diff --git a/src/graph-theory/finite-graphs.lagda.md b/src/graph-theory/finite-graphs.lagda.md
@@ -103,7 +103,7 @@ incident-edges-vertex-Undirected-Graph-𝔽 G x =
 ## External links
 
 - [Multigraph](https://ncatlab.org/nlab/show/multigraph) at nlab
-- [Multigraph](https://www.wikidata.org/wiki/Q2642629) on Wikidata
+- [Multigraph](https://www.wikidata.org/entity/Q2642629) on Wikidata
 - [Multigraph](https://en.wikipedia.org/wiki/Multigraph) at Wikipedia
 - [Multigraph](https://mathworld.wolfram.com/Multigraph.html) at Wolfram
   mathworld
diff --git a/src/graph-theory/hypergraphs.lagda.md b/src/graph-theory/hypergraphs.lagda.md
@@ -45,7 +45,7 @@ module _
 ## External links
 
 - [Hypergraph](https://ncatlab.org/nlab/show/hypergraph) at nlab
-- [Hypergraph](https://www.wikidata.org/wiki/Q840247) on Wikidata
+- [Hypergraph](https://www.wikidata.org/entity/Q840247) on Wikidata
 - [Hypergraph](https://en.wikipedia.org/wiki/Hypergraph) at Wikipedia
 - [Hypergraph](https://mathworld.wolfram.com/Hypergraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/matchings.lagda.md b/src/graph-theory/matchings.lagda.md
@@ -65,7 +65,7 @@ module _
 
 ## External links
 
-- [Matching](https://www.wikidata.org/wiki/Q1065144) on Wikidata
+- [Matching](https://www.wikidata.org/entity/Q1065144) on Wikidata
 - [Matching (graph theory)](<https://en.wikipedia.org/wiki/Matching_(graph_theory)>)
   at Wikipedia
 - [Matching](https://mathworld.wolfram.com/Matching.html) at Wolfram Mathworld
diff --git a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
@@ -60,7 +60,7 @@ module _
 
 ## External links
 
-- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomoprhism](https://www.wikidata.org/entity/Q303100) at Wikidata
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at

diff --git a/src/graph-theory/morphisms-directed-graphs.lagda.md b/src/graph-theory/morphisms-directed-graphs.lagda.md
@@ -225,6 +225,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
   Wikipedia
diff --git a/src/graph-theory/morphisms-undirected-graphs.lagda.md b/src/graph-theory/morphisms-undirected-graphs.lagda.md
@@ -198,6 +198,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
   Wikipedia
diff --git a/src/graph-theory/neighbors-undirected-graphs.lagda.md b/src/graph-theory/neighbors-undirected-graphs.lagda.md
@@ -83,7 +83,7 @@ neighbor-id-equiv-Undirected-Graph G x (pair y e) =
 
 ## External links
 
-- [Neighborhood](https://www.wikidata.org/wiki/Q1354987) on Wikidata
+- [Neighborhood](https://www.wikidata.org/entity/Q1354987) on Wikidata
 - [Neighborhood (graph theory)](<https://en.wikipedia.org/wiki/Neighbourhood_(graph_theory)>)
   at Wikipedia
 - [Graph neighborhood](https://mathworld.wolfram.com/GraphNeighborhood.html) at

diff --git a/src/graph-theory/orientations-undirected-graphs.lagda.md b/src/graph-theory/orientations-undirected-graphs.lagda.md
@@ -44,7 +44,7 @@ module _
 
 ## External links
 
-- [Orientation](https://www.wikidata.org/wiki/Q7102401) on Wikidata
+- [Orientation](https://www.wikidata.org/entity/Q7102401) on Wikidata
 - [Orientation (graph theory)](<https://en.wikipedia.org/wiki/Orientation_(graph_theory)>)
   at Wikipedia
 - [Graph orientation](https://mathworld.wolfram.com/GraphOrientation.html) at

diff --git a/src/graph-theory/paths-undirected-graphs.lagda.md b/src/graph-theory/paths-undirected-graphs.lagda.md
@@ -78,7 +78,7 @@ is-path-refl-walk-Undirected-Graph G x =
 
 ## External links
 
-- [Path](https://www.wikidata.org/wiki/Q1415372) on Wikidata
+- [Path](https://www.wikidata.org/entity/Q1415372) on Wikidata
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Graph path](https://mathworld.wolfram.com/GraphPath.html) at Wolfram

diff --git a/src/graph-theory/polygons.lagda.md b/src/graph-theory/polygons.lagda.md
@@ -146,7 +146,7 @@ This remains to be formalized.
 
 ## External links
 
-- [Cycle graph](https://www.wikidata.org/wiki/Q622506) on Wikidata
+- [Cycle graph](https://www.wikidata.org/entity/Q622506) on Wikidata
 - [Cycle graph](https://en.wikipedia.org/wiki/Cycle_graph) at Wikipedia
 - [Cycle graph](https://mathworld.wolfram.com/CycleGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
@@ -42,7 +42,7 @@ module _
 ## External links
 
 - [Reflexive graph](https://ncatlab.org/nlab/show/reflexive+graph) at nlab
-- [Graph](https://www.wikidata.org/wiki/Q141488) on Wikidata
+- [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Reflexive graph](https://mathworld.wolfram.com/ReflexiveGraph.html) at
   Wolfram Mathworld
diff --git a/src/graph-theory/regular-undirected-graphs.lagda.md b/src/graph-theory/regular-undirected-graphs.lagda.md
@@ -51,7 +51,7 @@ is-prop-is-regular-Undirected-Graph X G =
 ## External links
 
 - [Regular graph](https://d3gt.com/unit.html?regular-graph) at D3 Graph Theory
-- [Regular graph](https://www.wikidata.org/wiki/Q826467) on Wikidata
+- [Regular graph](https://www.wikidata.org/entity/Q826467) on Wikidata
 - [Regular graph](https://en.wikipedia.org/wiki/Regular_graph) at Wikipedia
 - [Regular graph](https://mathworld.wolfram.com/RegularGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/simple-undirected-graphs.lagda.md b/src/graph-theory/simple-undirected-graphs.lagda.md
@@ -70,6 +70,6 @@ Simple-Undirected-Graph l1 l2 =
 - [Graph](https://ncatlab.org/nlab/show/graph) at nlab
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
-- [Simple graph](https://www.wikidata.org/wiki/Q15838309) on Wikidata
+- [Simple graph](https://www.wikidata.org/entity/Q15838309) on Wikidata
 - [Simple graph](https://mathworld.wolfram.com/SimpleGraph.html) at Wolfram
   Mathworld
diff --git a/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md b/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md
@@ -55,5 +55,5 @@ module _
 
 ## External links
 
-- [Stereoisomerism](https://www.wikidata.org/wiki/Q47455153) on Wikidata
+- [Stereoisomerism](https://www.wikidata.org/entity/Q47455153) on Wikidata
 - [Stereoisomerism](https://en.wikipedia.org/wiki/Stereoisomerism) at Wikipedia
diff --git a/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md
@@ -84,6 +84,6 @@ module _
 
 ## External links
 
-- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://www.wikidata.org/entity/Q3385162) on Wikidata
 - [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
   Wikipedia
diff --git a/src/graph-theory/trails-directed-graphs.lagda.md b/src/graph-theory/trails-directed-graphs.lagda.md
@@ -52,5 +52,5 @@ module _
 
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
-- [Trail](https://www.wikidata.org/wiki/Q17455228) on Wikidata
+- [Trail](https://www.wikidata.org/entity/Q17455228) on Wikidata
 - [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram Mathworld
diff --git a/src/graph-theory/trails-undirected-graphs.lagda.md b/src/graph-theory/trails-undirected-graphs.lagda.md
@@ -165,5 +165,5 @@ module _
 
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
-- [Trail](https://www.wikidata.org/wiki/Q17455228) on Wikidata
+- [Trail](https://www.wikidata.org/entity/Q17455228) on Wikidata
 - [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram Mathworld
diff --git a/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md b/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md
@@ -28,7 +28,7 @@ Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)
 ## External links
 
 - [Graph](https://ncatlab.org/nlab/show/graph) at nlab
-- [Graph](https://www.wikidata.org/wiki/Q141488) on Wikidata
+- [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
 - [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
@@ -119,7 +119,7 @@ module _
 ## External links
 
 - [Graph](https://ncatlab.org/nlab/show/graph) at nlab
-- [Graph](https://www.wikidata.org/wiki/Q141488) on Wikidata
+- [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
 - [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
diff --git a/src/graph-theory/vertex-covers.lagda.md b/src/graph-theory/vertex-covers.lagda.md
@@ -48,4 +48,4 @@ vertex-cover G =
 - [Vertex cover](https://en.wikipedia.org/wiki/Vertex_cover) at Wikipedia
 - [Vertex cover](https://mathworld.wolfram.com/VertexCover.html) at Wolfram
   Mathworld
-- [Vertex cover problem](https://www.wikidata.org/wiki/Q924362) on Wikidata
+- [Vertex cover problem](https://www.wikidata.org/entity/Q924362) on Wikidata
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -783,7 +783,7 @@ module _
 
 ## External links
 
-- [Path](https://www.wikidata.org/wiki/Q917421) on Wikidata
+- [Path](https://www.wikidata.org/entity/Q917421) on Wikidata
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram Mathworld
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -516,7 +516,7 @@ module _
 
 ## External links
 
-- [Path](https://www.wikidata.org/wiki/Q917421) on Wikidata
+- [Path](https://www.wikidata.org/entity/Q917421) on Wikidata
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram Mathworld