diff --git a/src/Cat/Diagram/Idempotent.lagda.md b/src/Cat/Diagram/Idempotent.lagda.md
index d2986cc27..e356ebaf5 100644
--- a/src/Cat/Diagram/Idempotent.lagda.md
+++ b/src/Cat/Diagram/Idempotent.lagda.md
@@ -58,11 +58,10 @@ is-split→is-idempotent {f = f} spl =
 
 It's not the case that idempotents are split in every category. Those
 where this is the case are called **idempotent-complete**. Every
-category can be embedded, by a [full and faithful] functor, into an
+category can be embedded, by a [[fully faithful]] functor, into an
 idempotent-complete category; This construction is called the [Karoubi
 envelope] of $\cC$.
 
-[full and faithful]: Cat.Functor.Properties.html#ff-functors
 [Karoubi envelope]: Cat.Instances.Karoubi.html
 
 ```agda
diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md
index e6543a9d4..f0834804b 100644
--- a/src/Cat/Displayed/Comprehension.lagda.md
+++ b/src/Cat/Displayed/Comprehension.lagda.md
@@ -27,6 +27,7 @@ module Cat.Displayed.Comprehension
 ```agda
 open Cat.Reasoning B
 open Cat.Displayed.Reasoning E
+open Displayed E
 open Functor
 open _=>_
 open Total-hom
diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md
index dfe15f515..f01fb1ffd 100644
--- a/src/Cat/Displayed/GenericObject.lagda.md
+++ b/src/Cat/Displayed/GenericObject.lagda.md
@@ -22,6 +22,7 @@ module Cat.Displayed.GenericObject
 open Precategory B
 open Cat.Displayed.Morphism E
 open Cat.Displayed.Reasoning E
+open Displayed E
 open Functor
 ```
 -->
diff --git a/src/Cat/Displayed/Univalence.lagda.md b/src/Cat/Displayed/Univalence.lagda.md
index 6934efb87..363c46cf3 100644
--- a/src/Cat/Displayed/Univalence.lagda.md
+++ b/src/Cat/Displayed/Univalence.lagda.md
@@ -27,6 +27,7 @@ private
   module ∫E = Cat.Reasoning (∫ E)
   module E = Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
+open Displayed E
 open Total-hom
 open E
 ```
diff --git a/src/Cat/Displayed/Univalence/Reasoning.lagda.md b/src/Cat/Displayed/Univalence/Reasoning.lagda.md
index 806707f57..8cdfe7df1 100644
--- a/src/Cat/Displayed/Univalence/Reasoning.lagda.md
+++ b/src/Cat/Displayed/Univalence/Reasoning.lagda.md
@@ -36,6 +36,7 @@ private module B = Cr B
 open Cat.Displayed.Univalence E
 open Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
+open Displayed E
 open _≅[_]_
 ```
 -->