diff --git a/src/Cat/Functor/Subcategory.lagda.md b/src/Cat/Functor/Subcategory.lagda.md
index 8dde72cef..7a022856f 100644
--- a/src/Cat/Functor/Subcategory.lagda.md
+++ b/src/Cat/Functor/Subcategory.lagda.md
@@ -1,3 +1,4 @@
+<!--
 ```agda
 open import Cat.Functor.Properties
 open import Cat.Univalent
diff --git a/src/Order/DCPO/Free.lagda.md b/src/Order/DCPO/Free.lagda.md
index 400a0675a..f2474cc81 100644
--- a/src/Order/DCPO/Free.lagda.md
+++ b/src/Order/DCPO/Free.lagda.md
@@ -40,6 +40,8 @@ The [discrete poset] on a set $A$ is a DCPO. To see this, note that
 every semi-directed family $f : I \to A$ in a discrete poset is constant.
 Furthermore, $f$ is directed, so it is merely inhabited.
 
+[discrete poset]: Order.Instances.Discrete.html
+
 ```agda
 Disc-is-dcpo : ∀ {ℓ} {A : Set ℓ} → is-dcpo (Disc A)
 Disc-is-dcpo {A = A} .is-dcpo.directed-lubs {Ix = Ix} f dir =