From c7dd4cf024f30ac333b0d69855bb59a37d957e77 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 10 Aug 2023 12:39:08 -0700
Subject: [PATCH] chore: formatting

---
 src/Cat/Functor/Subcategory.lagda.md | 1 +
 src/Order/DCPO/Free.lagda.md         | 2 ++
 2 files changed, 3 insertions(+)

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 =