chore: formatting

the1lab · Aug 10, 2023 · c7dd4cf · c7dd4cf
1 parent a3645cc
commit c7dd4cf
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git 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
@@ -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 =