Typeset nlab as $n$Lab (#911)

UniMath · Nov 9, 2023 · f0bafbe · f0bafbe
1 parent 85f9582
commit f0bafbe
Show file tree

Hide file tree

Showing 55 changed files with 61 additions and 60 deletions.
diff --git a/src/category-theory/conservative-functors-precategories.lagda.md b/src/category-theory/conservative-functors-precategories.lagda.md
@@ -113,6 +113,6 @@ module _
 - [Conservative Functors](https://1lab.dev/Cat.Functor.Conservative.html) at
   1lab
 - [conservative functor](https://ncatlab.org/nlab/show/conservative+functor) at
-  nlab
+  $n$Lab
 - [Conservative functor](https://en.wikipedia.org/wiki/Conservative_functor) at
   Wikipedia
diff --git a/src/category-theory/copresheaf-categories.lagda.md b/src/category-theory/copresheaf-categories.lagda.md
@@ -165,5 +165,5 @@ module _
 - [Presheaf precategories](https://1lab.dev/Cat.Functor.Base.html#presheaf-precategories)
   at 1lab
 - [category of presheaves](https://ncatlab.org/nlab/show/category+of+presheaves)
-  at nlab
-- [copresheaf](https://ncatlab.org/nlab/show/copresheaf) at nlab
+  at $n$Lab
+- [copresheaf](https://ncatlab.org/nlab/show/copresheaf) at $n$Lab
diff --git a/src/category-theory/cores-categories.lagda.md b/src/category-theory/cores-categories.lagda.md
@@ -139,4 +139,4 @@ module _
 ## External links
 
 - [The core of a category](https://1lab.dev/Cat.Instances.Core.html) at 1lab
-- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at nlab
+- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at $n$Lab
diff --git a/src/category-theory/cores-precategories.lagda.md b/src/category-theory/cores-precategories.lagda.md
@@ -207,4 +207,4 @@ module _
 ## External links
 
 - [The core of a category](https://1lab.dev/Cat.Instances.Core.html) at 1lab
-- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at nlab
+- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at $n$Lab
diff --git a/src/category-theory/essential-fibers-of-functors-precategories.lagda.md b/src/category-theory/essential-fibers-of-functors-precategories.lagda.md
@@ -55,4 +55,4 @@ module _
 
 - [Essential Fibres](https://1lab.dev/Cat.Functor.Properties.html#essential-fibres)
   at 1lab
-- [essential fiber](https://ncatlab.org/nlab/show/essential+fiber) at nlab
+- [essential fiber](https://ncatlab.org/nlab/show/essential+fiber) at $n$Lab
diff --git a/src/category-theory/essentially-injective-functors-precategories.lagda.md b/src/category-theory/essentially-injective-functors-precategories.lagda.md
@@ -94,4 +94,4 @@ module _
 ## External links
 
 - [essentially injective functor](https://ncatlab.org/nlab/show/essentially+injective+functor)
-  at nlab
+  at $n$Lab
diff --git a/src/category-theory/essentially-surjective-functors-precategories.lagda.md b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
@@ -124,7 +124,7 @@ Rezk completion_.
 - [Essential Fibres](https://1lab.dev/Cat.Functor.Properties.html#essential-fibres)
   at 1lab
 - [essentially surjective functor](https://ncatlab.org/nlab/show/essentially+surjective+functor)
-  at nlab
+  at $n$Lab
 - [Fully Faithful and Essentially Surjective Functors](https://kerodon.net/tag/01JG)
   at Kerodon
 - [Essentially surjective functor](https://en.wikipedia.org/wiki/Essentially_surjective_functor)

diff --git a/src/category-theory/full-subprecategories.lagda.md b/src/category-theory/full-subprecategories.lagda.md
@@ -305,4 +305,4 @@ module _
 
 - [Full subcategories](https://1lab.dev/Cat.Functor.FullSubcategory.html) at
   1lab
-- [full subcategory](https://ncatlab.org/nlab/show/full+subcategory) at nlab
+- [full subcategory](https://ncatlab.org/nlab/show/full+subcategory) at $n$Lab
diff --git a/src/category-theory/fully-faithful-functors-precategories.lagda.md b/src/category-theory/fully-faithful-functors-precategories.lagda.md
@@ -414,7 +414,7 @@ module _
 - [Fully Faithful Functors](https://1lab.dev/Cat.Functor.Properties.html#fully-faithful-functors)
   at 1lab
 - [full and faithful functor](https://ncatlab.org/nlab/show/full+and+faithful+functor)
-  at nlab
+  at $n$Lab
 - [Full and faithful functors](https://en.wikipedia.org/wiki/Full_and_faithful_functors)
   at Wikipedia
 - [fully faithful functor](https://wikidata.org/wiki/Q120721906) at Wikidata
diff --git a/src/category-theory/functors-nonunital-precategories.lagda.md b/src/category-theory/functors-nonunital-precategories.lagda.md
@@ -335,4 +335,4 @@ module _
 
 ## External links
 
-- [semifunctor](https://ncatlab.org/nlab/show/semifunctor) at nlab
+- [semifunctor](https://ncatlab.org/nlab/show/semifunctor) at $n$Lab
diff --git a/src/category-theory/gaunt-categories.lagda.md b/src/category-theory/gaunt-categories.lagda.md
@@ -356,4 +356,4 @@ module _
 
 - [Gaunt (pre)categories](https://1lab.dev/Cat.Gaunt.html) at 1lab
 - [gaunt category](https://ncatlab.org/nlab/show/gaunt+category#in_type_theory)
-  at nlab
+  at $n$Lab
diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md
@@ -222,4 +222,5 @@ module _
 
 ## External links
 
-- [univalent groupoid](https://ncatlab.org/nlab/show/univalent+groupoid) at nlab
+- [univalent groupoid](https://ncatlab.org/nlab/show/univalent+groupoid) at
+  $n$Lab
diff --git a/src/category-theory/nonunital-precategories.lagda.md b/src/category-theory/nonunital-precategories.lagda.md
@@ -205,7 +205,7 @@ module _
 ## Comments
 
 As discussed in [Semicategories](https://ncatlab.org/nlab/show/semicategory) at
-nlab, it seems that a nonunital precategory should be the underlying nonunital
+$n$Lab, it seems that a nonunital precategory should be the underlying nonunital
 precategory of a [category](category-theory.categories.md) if and only if the
 projection map
 
@@ -220,6 +220,6 @@ equivalences of hom-[sets](foundation-core.sets.md) by pre- and postcomposition.
 
 ## External links
 
-- [Semicategories](https://ncatlab.org/nlab/show/semicategory) at nlab
+- [Semicategories](https://ncatlab.org/nlab/show/semicategory) at $n$Lab
 - [Semigroupoid](https://en.wikipedia.org/wiki/Semigroupoid) at Wikipedia
 - [semigroupoid](https://www.wikidata.org/wiki/Q4164581) at Wikidata
diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
@@ -265,4 +265,4 @@ module _
 ## External links
 
 - [Precategories](https://1lab.dev/Cat.Base.html) at 1lab
-- [precategory](https://ncatlab.org/nlab/show/precategory) at nlab
+- [precategory](https://ncatlab.org/nlab/show/precategory) at $n$Lab
diff --git a/src/category-theory/pregroupoids.lagda.md b/src/category-theory/pregroupoids.lagda.md
@@ -141,4 +141,4 @@ module _
 ## External links
 
 - [Groupoids](https://1lab.dev/Cat.Groupoid.html) at 1lab
-- [pregroupoid](https://ncatlab.org/nlab/show/pregroupoid) at nlab
+- [pregroupoid](https://ncatlab.org/nlab/show/pregroupoid) at $n$Lab
diff --git a/src/category-theory/presheaf-categories.lagda.md b/src/category-theory/presheaf-categories.lagda.md
@@ -156,5 +156,5 @@ module _
 - [Presheaf precategories](https://1lab.dev/Cat.Functor.Base.html#presheaf-precategories)
   at 1lab
 - [category of presheaves](https://ncatlab.org/nlab/show/category+of+presheaves)
-  at nlab
-- [presheaf](https://ncatlab.org/nlab/show/presheaf) at nlab
+  at $n$Lab
+- [presheaf](https://ncatlab.org/nlab/show/presheaf) at $n$Lab
diff --git a/src/category-theory/pseudomonic-functors-precategories.lagda.md b/src/category-theory/pseudomonic-functors-precategories.lagda.md
@@ -298,6 +298,6 @@ module _
 - [Pseudomonic Functors](https://1lab.dev/Cat.Functor.Properties.html#pseudomonic-functors)
   at 1lab
 - [pseudomonic functor](https://ncatlab.org/nlab/show/pseudomonic+functor) at
-  nlab
+  $n$Lab
 
 A wikidata identifier was not available for this concept.
diff --git a/src/category-theory/replete-subprecategories.lagda.md b/src/category-theory/replete-subprecategories.lagda.md
@@ -325,7 +325,7 @@ This remains to be formalized.
 ## External links
 
 - [replete subcategory](https://ncatlab.org/nlab/show/replete+replete-subprecategory)
-  at nlab
+  at $n$Lab
 - [Isomorphism-closed subcategory](https://en.wikipedia.org/wiki/Isomorphism-closed_subcategory)
   at Wikipedia
 - [isomorphism-closed subcategory](https://www.wikidata.org/wiki/Q6086096) at

diff --git a/src/category-theory/representing-arrow-category.lagda.md b/src/category-theory/representing-arrow-category.lagda.md
@@ -164,4 +164,4 @@ This is a consequence of the
 
 - [Interval category](https://1lab.dev/Cat.Instances.Shape.Interval.html#interval-category)
   at 1lab
-- [interval category](https://ncatlab.org/nlab/show/interval+category) at nlab
+- [interval category](https://ncatlab.org/nlab/show/interval+category) at $n$Lab
diff --git a/src/category-theory/restrictions-functors-cores-precategories.lagda.md b/src/category-theory/restrictions-functors-cores-precategories.lagda.md
@@ -184,4 +184,4 @@ module _
 ## External links
 
 - [The core of a category](https://1lab.dev/Cat.Instances.Core.html) at 1lab
-- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at nlab
+- [core groupoid](https://ncatlab.org/nlab/show/core+groupoid) at $n$Lab
diff --git a/src/category-theory/rigid-objects-categories.lagda.md b/src/category-theory/rigid-objects-categories.lagda.md
@@ -71,4 +71,4 @@ module _
 
 ## External links
 
-- [rigid object](https://ncatlab.org/nlab/show/rigid+object) at nlab
+- [rigid object](https://ncatlab.org/nlab/show/rigid+object) at $n$Lab
diff --git a/src/category-theory/rigid-objects-precategories.lagda.md b/src/category-theory/rigid-objects-precategories.lagda.md
@@ -65,4 +65,4 @@ module _
 
 ## External links
 
-- [rigid object](https://ncatlab.org/nlab/show/rigid+object) at nlab
+- [rigid object](https://ncatlab.org/nlab/show/rigid+object) at $n$Lab
diff --git a/src/category-theory/set-magmoids.lagda.md b/src/category-theory/set-magmoids.lagda.md
@@ -229,6 +229,6 @@ module _
 
 ## External links
 
-- [magmoid](https://ncatlab.org/nlab/show/magmoid) at nlab
+- [magmoid](https://ncatlab.org/nlab/show/magmoid) at $n$Lab
 
 A wikidata identifier was not available for this concept.
diff --git a/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md b/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
@@ -184,6 +184,6 @@ Rezk completion_.
 - [Essential Fibres](https://1lab.dev/Cat.Functor.Properties.html#essential-fibres)
   at 1lab
 - [split essentially surjective functor](https://ncatlab.org/nlab/show/split+essentially+surjective+functor)
-  at nlab
+  at $n$Lab
 
 A wikidata identifier was not available for this concept.
diff --git a/src/category-theory/strict-categories.lagda.md b/src/category-theory/strict-categories.lagda.md
@@ -277,6 +277,6 @@ postcomp-hom-Strict-Category C =
 
 - [Strict Precategories](https://1lab.dev/Cat.Strict.html#strict-precategories)
   at 1lab
-- [strict category](https://ncatlab.org/nlab/show/strict+category) at nlab
+- [strict category](https://ncatlab.org/nlab/show/strict+category) at $n$Lab
 - [Category (mathematics)](<https://en.wikipedia.org/wiki/Category_(mathematics)>)
   at Wikipedia
diff --git a/src/category-theory/subprecategories.lagda.md b/src/category-theory/subprecategories.lagda.md
@@ -528,7 +528,7 @@ module _
 
 ## External links
 
-- [subcategory](https://ncatlab.org/nlab/show/subcategory) at nlab
+- [subcategory](https://ncatlab.org/nlab/show/subcategory) at $n$Lab
 - [Subcategory](https://en.wikipedia.org/wiki/Subcategory) at Wikipedia
 - [Subcategory](https://mathworld.wolfram.com/Subcategory.html) at Wolfram
   MathWorld
diff --git a/src/category-theory/wide-subcategories.lagda.md b/src/category-theory/wide-subcategories.lagda.md
@@ -471,4 +471,4 @@ This remains to be formalized. This is a consequence of repeleteness.
 
 - [Wide subcategories](https://1lab.dev/Cat.Functor.WideSubcategory.html) at
   1lab
-- [wide subcategory](https://ncatlab.org/nlab/show/wide+subcategory) at nlab
+- [wide subcategory](https://ncatlab.org/nlab/show/wide+subcategory) at $n$Lab
diff --git a/src/category-theory/wide-subprecategories.lagda.md b/src/category-theory/wide-subprecategories.lagda.md
@@ -454,4 +454,4 @@ module _
 
 - [Wide subcategories](https://1lab.dev/Cat.Functor.WideSubcategory.html) at
   1lab
-- [wide subcategory](https://ncatlab.org/nlab/show/wide+subcategory) at nlab
+- [wide subcategory](https://ncatlab.org/nlab/show/wide+subcategory) at $n$Lab
diff --git a/src/category-theory/yoneda-lemma-categories.lagda.md b/src/category-theory/yoneda-lemma-categories.lagda.md
@@ -107,7 +107,7 @@ The inverse to the Yoneda map:
 
 - [The Yoneda embedding](https://1lab.dev/Cat.Functor.Hom.html#the-yoneda-embedding)
   at 1lab
-- [Yoneda lemma](https://ncatlab.org/nlab/show/Yoneda+lemma) at nlab
+- [Yoneda lemma](https://ncatlab.org/nlab/show/Yoneda+lemma) at $n$Lab
 - [The Yoneda lemma](https://www.math3ma.com/blog/the-yoneda-lemma) at Math3ma
 - [Yoneda lemma](https://en.wikipedia.org/wiki/Yoneda_lemma) at Wikipedia
 - [Yoneda lemma](https://www.wikidata.org/wiki/Q320577) at Wikidata
diff --git a/src/category-theory/yoneda-lemma-precategories.lagda.md b/src/category-theory/yoneda-lemma-precategories.lagda.md
@@ -166,7 +166,7 @@ The inverse is an inverse:
 
 - [The Yoneda embedding](https://1lab.dev/Cat.Functor.Hom.html#the-yoneda-embedding)
   at 1lab
-- [Yoneda lemma](https://ncatlab.org/nlab/show/Yoneda+lemma) at nlab
+- [Yoneda lemma](https://ncatlab.org/nlab/show/Yoneda+lemma) at $n$Lab
 - [The Yoneda lemma](https://www.math3ma.com/blog/the-yoneda-lemma) at Math3ma
 - [Yoneda lemma](https://en.wikipedia.org/wiki/Yoneda_lemma) at Wikipedia
 - [Yoneda lemma](https://www.wikidata.org/wiki/Q320577) at Wikidata
diff --git a/src/elementary-number-theory/peano-arithmetic.lagda.md b/src/elementary-number-theory/peano-arithmetic.lagda.md
@@ -155,7 +155,7 @@ peano-9-ℕ P = ind-ℕ {P = type-Prop ∘ P}
 
 ## External links
 
-- [Peano arithmetic](https://ncatlab.org/nlab/show/Peano+arithmetic) at nlab
+- [Peano arithmetic](https://ncatlab.org/nlab/show/Peano+arithmetic) at $n$Lab
 - [Peano axioms](https://www.wikidata.org/wiki/Q842755) at Wikidata
 - [Peano axioms](https://www.britannica.com/science/Peano-axioms) at Britannica
 - [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms) at Wikipedia

diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md
@@ -111,6 +111,6 @@ homotopy precategory of types.
 
 ## External links
 
-- [Set](https://ncatlab.org/nlab/show/Set) at nlab
+- [Set](https://ncatlab.org/nlab/show/Set) at $n$Lab
 - [Category of sets](https://en.wikipedia.org/wiki/Category_of_sets) at
   Wikipedia
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
@@ -691,4 +691,4 @@ equiv-fiberwise-equiv-fam-equiv B C = distributive-Π-Σ
 
 - The
   [2-out-of-6 property](https://ncatlab.org/nlab/show/two-out-of-six+property)
-  at nlab
+  at $n$Lab
diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md
@@ -697,6 +697,6 @@ module _
 ## External links
 
 - [Retracts in arrow categories](https://ncatlab.org/nlab/show/retract#in_arrow_categories)
-  at nlab
+  at $n$Lab
 
 A wikidata identifier was not available for this concept.
diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md
@@ -63,7 +63,7 @@ is-acyclic-Undirected-Graph l G =
 
 ## External links
 
-- [Trees](https://ncatlab.org/nlab/show/tree) at nlab
+- [Trees](https://ncatlab.org/nlab/show/tree) at $n$Lab
 - [Forests](<https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest>) at
   Wikipedia
 - [Acyclic graphs](https://mathworld.wolfram.com/AcyclicGraph.html) at Wolfram

diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -51,7 +51,7 @@ 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
+- [Bipartite graphs](https://ncatlab.org/nlab/show/bipartite+graph) at $n$Lab
 - [Complete bipartite graph](https://www.wikidata.org/entity/Q913598) at
   Wikidata
 - [Complete bipartite graph](https://en.wikipedia.org/wiki/Complete_bipartite_graph)

diff --git a/src/graph-theory/connected-undirected-graphs.lagda.md b/src/graph-theory/connected-undirected-graphs.lagda.md
@@ -49,7 +49,7 @@ module _
 
 ## External links
 
-- [Connected graph](https://ncatlab.org/nlab/show/connected+graph) at nlab
+- [Connected graph](https://ncatlab.org/nlab/show/connected+graph) at $n$Lab
 - [Connected graph](https://www.wikidata.org/entity/Q230655) on Wikidata
 - [Connectivity (graph theory)](<https://en.wikipedia.org/wiki/Connectivity_(graph_theory)>)
   on Wikipedia

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
@@ -26,8 +26,8 @@ Directed-Graph-Fin = Σ ℕ (λ V → Fin V → Fin V → ℕ)
 
 ## External links
 
-- [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
-- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
+- [Digraph](https://ncatlab.org/nlab/show/digraph) at $n$Lab
+- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at $n$Lab
 - [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

diff --git a/src/graph-theory/directed-graphs.lagda.md b/src/graph-theory/directed-graphs.lagda.md
@@ -135,8 +135,8 @@ module equiv {l1 l2 : Level} where
 
 ## External links
 
-- [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
-- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
+- [Digraph](https://ncatlab.org/nlab/show/digraph) at $n$Lab
+- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at $n$Lab
 - [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

diff --git a/src/graph-theory/enriched-undirected-graphs.lagda.md b/src/graph-theory/enriched-undirected-graphs.lagda.md
@@ -198,7 +198,7 @@ module _
 
 ## External links
 
-- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://ncatlab.org/nlab/show/graph) at $n$Lab
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia

diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md
@@ -547,4 +547,4 @@ module _
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
   Wolfram Mathworld
-- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
@@ -304,4 +304,4 @@ module _
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
   Wolfram Mathworld
-- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/equivalences-undirected-graphs.lagda.md b/src/graph-theory/equivalences-undirected-graphs.lagda.md
@@ -306,4 +306,4 @@ module _
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
   Wolfram Mathworld
-- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/finite-graphs.lagda.md b/src/graph-theory/finite-graphs.lagda.md
@@ -102,7 +102,7 @@ incident-edges-vertex-Undirected-Graph-𝔽 G x =
 
 ## External links
 
-- [Multigraph](https://ncatlab.org/nlab/show/multigraph) at nlab
+- [Multigraph](https://ncatlab.org/nlab/show/multigraph) at $n$Lab
 - [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

diff --git a/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md b/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md
@@ -51,4 +51,4 @@ is-geometric-realization-reflecting-map-Undirected-Graph l G f =
 ## External links
 
 - [Geometric realization](https://ncatlab.org/nlab/show/geometric+realization)
-  at nlab
+  at $n$Lab
diff --git a/src/graph-theory/hypergraphs.lagda.md b/src/graph-theory/hypergraphs.lagda.md
@@ -44,7 +44,7 @@ module _
 
 ## External links
 
-- [Hypergraph](https://ncatlab.org/nlab/show/hypergraph) at nlab
+- [Hypergraph](https://ncatlab.org/nlab/show/hypergraph) at $n$Lab
 - [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

diff --git a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
@@ -65,4 +65,4 @@ module _
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
   Wolfram Mathworld
-- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md b/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
@@ -81,4 +81,4 @@ pr2 (pr2 (terminal-reflecting-map-Undirected-Graph G) p e) x =
 ## External links
 
 - [Geometric realization](https://ncatlab.org/nlab/show/geometric+realization)
-  at nlab
+  at $n$Lab
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
@@ -41,7 +41,7 @@ module _
 
 ## External links
 
-- [Reflexive graph](https://ncatlab.org/nlab/show/reflexive+graph) at nlab
+- [Reflexive graph](https://ncatlab.org/nlab/show/reflexive+graph) at $n$Lab
 - [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

diff --git a/src/graph-theory/simple-undirected-graphs.lagda.md b/src/graph-theory/simple-undirected-graphs.lagda.md
@@ -67,7 +67,7 @@ Simple-Undirected-Graph l1 l2 =
 
 ## External links
 
-- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://ncatlab.org/nlab/show/graph) at $n$Lab
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
 - [Simple graph](https://www.wikidata.org/entity/Q15838309) on Wikidata

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
@@ -27,7 +27,7 @@ Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)
 
 ## External links
 
-- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://ncatlab.org/nlab/show/graph) at $n$Lab
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia