diff --git a/src/Data/Int/Universal.lagda.md b/src/Data/Int/Universal.lagda.md
index c5526e175..6ac6c0465 100644
--- a/src/Data/Int/Universal.lagda.md
+++ b/src/Data/Int/Universal.lagda.md
@@ -55,11 +55,13 @@ unique among functions with these properties.
       → ∀ x → f x ≡ map-out p r x
 ```
 
-By a standard categorical argument, existence and uniqueness together give us an
+By a [standard categorical argument], existence and uniqueness together give us an
 *induction principle* for the integers: to construct a section of a type family
 $P : \bb{Z} \to \ty$, it is enough to give an element of $P(0)$ and a family of
 equivalences $P(n) \simeq P(n + 1)$.
 
+[standard categorical argument]: Data.Wellfounded.W.html#initial-algebras-are-inductive-types
+
 ```agda
   ℤ-η : ∀ z → map-out point rotate z ≡ z
   ℤ-η z = sym (map-out-unique id refl (λ _ → refl) z)