diff --git a/src/plta/Naturals.lagda b/src/plta/Naturals.lagda index 019c7fee..01826709 100644 --- a/src/plta/Naturals.lagda +++ b/src/plta/Naturals.lagda @@ -269,7 +269,7 @@ specifies operators to support reasoning about equivalence, and adds all the names specified in the `using` clause into the current scope. In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We will see how these are used below. We take all these as givens for now, -but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/Equality.md %}). +but will see how they are defined in Chapter [Equality](Equality). Agda uses underbars to indicate where terms appear in infix or mixfix operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written