diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 36b26f95c..fb183b607 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -114,7 +114,8 @@ niv update nixpkgs -v 21.11.337905.902d91def1e
 
 ## Setup without nix-shell
 
-- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-1-install-agda>).
+- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/v2.7.0/getting-started/installation.html#step-1-install-agda>
+).
 - In a folder `LIB`, clone the dependencies
     + [agda-stdlib](https://github.com/agda/agda-stdlib)
     + [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes)
diff --git a/src/Ledger/EssentialAgda.lagda b/src/EssentialAgda.lagda
similarity index 89%
rename from src/Ledger/EssentialAgda.lagda
rename to src/EssentialAgda.lagda
index 9f58f67c8..fd2bf454b 100644
--- a/src/Ledger/EssentialAgda.lagda
+++ b/src/EssentialAgda.lagda
@@ -3,12 +3,12 @@
 Here we describe some of the essential concepts and syntax of the Agda programming language and proof assistant.
 The goal is to provide some background for readers who are not already familiar with Agda, to help them
 understand the other sections of the specification.  For more details, the reader is
-encouraged to consult the official Agda documentation~(\cite{agda2024}).
+encouraged to consult the official \hrefAgdaDocs{}~(\cite{agda2024}).
 
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
-module Ledger.EssentialAgda where
+module EssentialAgda where
 
 open import Prelude using (Type)
 open import Data.Nat
@@ -53,4 +53,4 @@ p24 = record p23 { snd = 4 }
 This results a new record, \AgdaFunction{p24}, which denotes the pair
 \AgdaInductiveConstructor{⦅}~\AgdaNumber{2}~\AgdaInductiveConstructor{,}~\AgdaNumber{4}~\AgdaInductiveConstructor{⦆}.
 \\[6pt]
-See also \url{https://agda.readthedocs.io/en/\AgdaVersion/language/record-types.html}.
+See also \hrefAgdaDocs[language/record-types.html][agda.readthedocs.io/record-types].
diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
index 49ca82d69..dd23ae482 100644
--- a/src/Ledger/Certs.lagda
+++ b/src/Ledger/Certs.lagda
@@ -189,10 +189,10 @@ private variable
 
 \subsection{Changes Introduced in Conway Era}
 
-% In the Conway era, support for pointer addresses, genesis delegations and MIR
-% certificates is removed (see~\cite{cip1694}).  In \DState, this means that the four
-% fields relating to those features are no longer present, and \DelegEnv contains none
-% of the fields it used to in the Shelley era~(\cite[Sec.~9.2]{shelley-ledger-spec}).
+In the Conway era, support for pointer addresses, genesis delegations and MIR
+certificates is removed (see~\cite{cip1694}).  In \DState, this means that the four
+fields relating to those features are no longer present, and \DelegEnv contains none
+of the fields it used to in the Shelley era~(\cite[Sec.~9.2]{shelley-ledger-spec}).
 
 \subsubsection{Delegation}
 
diff --git a/src/Ledger/PDF.lagda b/src/Ledger/PDF.lagda
index 8d1cc43b9..7d8fd98df 100644
--- a/src/Ledger/PDF.lagda
+++ b/src/Ledger/PDF.lagda
@@ -56,7 +56,7 @@ open import Ledger.Chain
 
 open import Ledger.Properties
 
-open import Ledger.EssentialAgda
+open import EssentialAgda
 open import Ledger.PDF.ConwayBootstrapEnact
 open import Ledger.PDF.ConwayBootstrap
 \end{code}
@@ -95,7 +95,7 @@ open import Ledger.PDF.ConwayBootstrap
 
 \appendix
 
-\input{Ledger/EssentialAgda}
+\input{EssentialAgda}
 \input{Ledger/PDF/ConwayBootstrapEnact}
 \input{Ledger/PDF/ConwayBootstrap}
 
diff --git a/src/latex/preamble.tex b/src/latex/preamble.tex
index 5b835f7ab..d08b2ce6e 100644
--- a/src/latex/preamble.tex
+++ b/src/latex/preamble.tex
@@ -79,3 +79,13 @@
 \msg_new:nnn {agda-latex-macros} {invalid-cip}
   {CIP-#1 is not a known CIP. The hyperlink will not be created.}
 \ExplSyntaxOff
+
+\NewDocumentCommand{\hrefAgdaDocs}{O{} O{Agda documentation}}{%
+  \href{https://agda.readthedocs.io/en/\AgdaVersion/#1}{#2}%
+}
+% For a link to the main Agda documentation website, just use \hrefAgdaDocs{}.
+% For a link to a specific section of the Agda docs, use
+% \hrefAgdaDocs[URLsuffix]{Link text}.
+% For example, \hrefAgdaDocs[language/record-types.html][agda.readthedocs.io/record-types],
+% produces a link to url https://agda.readthedocs.io/en/\AgdaVersion/language/record-types.html
+% with link text "agda.readthedocs.io/record-types".